Divider and Unique Inverse Benchmarks Submitted to the SAT Competition 2018

Armin Biere

Divider and Unique Inverse Benchmarks Submitted to the SAT Competition 2018

Armin Biere

Institut für Formale Modelle und Verifikation

Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

Abstract

Our benchmark submission for the SAT 2018 Competition consist of two sets of word-level properties originally formulated as SMT problems in the quantiﬁer-free theory of bitvectors in BTOR [1] or SMTLIB [2] format. We then use our SMT solver Boolector [3] to synthesize AIGs [4], which in turn were translated to DIMACS format.

Originalsprache	Englisch
Titel	Proceedings of SAT Competition 2018 - Solver and Benchmark Descriptions
Herausgeber*innen	Heule, Marijn J. H.; Järvisalo, Matti Juhani; Suda, Martin
Erscheinungsort	Helsinki
Verlag	Department of Computer Science Series of Publications B
Seiten	56
Seitenumfang	1
Band	B-2018-1
Publikationsstatus	Veröffentlicht - 2018

Wissenschaftszweige

102 Informatik
102001 Artificial Intelligence
102011 Formale Sprachen
102022 Softwareentwicklung
102031 Theoretische Informatik
603109 Logik
202006 Computer Hardware

JKU-Schwerpunkte

Computation in Informatics and Mathematics

Dieses zitieren

@inproceedings{7bad99d4b3574fd5a12df19d3493e3f3,

title = "Divider and Unique Inverse Benchmarks Submitted to the SAT Competition 2018",

abstract = "Our benchmark submission for the SAT 2018 Competition consist of two sets of word-level properties originally formulated as SMT problems in the quantiﬁer-free theory of bitvectors in BTOR [1] or SMTLIB [2] format. We then use our SMT solver Boolector [3] to synthesize AIGs [4], which in turn were translated to DIMACS format.",

author = "Armin Biere",

year = "2018",

language = "English",

volume = "B-2018-1",

pages = "56",

editor = "\{Heule, Marijn J. H.; J{\"a}rvisalo, Matti Juhani; Suda, Martin\}",

booktitle = "Proceedings of SAT Competition 2018 - Solver and Benchmark Descriptions",

publisher = "Department of Computer Science Series of Publications B",

}

Divider and Unique Inverse Benchmarks Submitted to the SAT Competition 2018. / Biere, Armin.
Proceedings of SAT Competition 2018 - Solver and Benchmark Descriptions. Hrsg. / Heule, Marijn J. H.; Järvisalo, Matti Juhani; Suda, Martin. Band B-2018-1 Helsinki: Department of Computer Science Series of Publications B, 2018. S. 56.

Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

TY - GEN

T1 - Divider and Unique Inverse Benchmarks Submitted to the SAT Competition 2018

AU - Biere, Armin

PY - 2018

Y1 - 2018

N2 - Our benchmark submission for the SAT 2018 Competition consist of two sets of word-level properties originally formulated as SMT problems in the quantiﬁer-free theory of bitvectors in BTOR [1] or SMTLIB [2] format. We then use our SMT solver Boolector [3] to synthesize AIGs [4], which in turn were translated to DIMACS format.

AB - Our benchmark submission for the SAT 2018 Competition consist of two sets of word-level properties originally formulated as SMT problems in the quantiﬁer-free theory of bitvectors in BTOR [1] or SMTLIB [2] format. We then use our SMT solver Boolector [3] to synthesize AIGs [4], which in turn were translated to DIMACS format.

M3 - Conference proceedings

VL - B-2018-1

SP - 56

BT - Proceedings of SAT Competition 2018 - Solver and Benchmark Descriptions

A2 - Heule, Marijn J. H.; Järvisalo, Matti Juhani; Suda, Martin, null

PB - Department of Computer Science Series of Publications B

CY - Helsinki

ER -