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

Institute of Formal Models and Verification

Research output: Chapter in Book/Report/Conference proceeding › Conference proceedings › peer-review

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.

Original language	English
Title of host publication	Proceedings of SAT Competition 2018 - Solver and Benchmark Descriptions
Editors	Heule, Marijn J. H.; Järvisalo, Matti Juhani; Suda, Martin
Place of Publication	Helsinki
Publisher	Department of Computer Science Series of Publications B
Pages	56
Number of pages	1
Volume	B-2018-1
Publication status	Published - 2018

Fields of science

102 Computer Sciences
102001 Artificial intelligence
102011 Formal languages
102022 Software development
102031 Theoretical computer science
603109 Logic
202006 Computer hardware

JKU Focus areas

Computation in Informatics and Mathematics

Cite this

@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. ed. / Heule, Marijn J. H.; Järvisalo, Matti Juhani; Suda, Martin. Vol. B-2018-1 Helsinki: Department of Computer Science Series of Publications B, 2018. p. 56.

Research output: Chapter in Book/Report/Conference proceeding › Conference proceedings › peer-review

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 -