Revisiting Hyper Binary Resolution

Marijn Heule; Matti Järvisalo; Armin Biere

doi:10.1007/978-3-642-38171-3_6

Revisiting Hyper Binary Resolution

Marijn Heule
, Matti Järvisalo
, Armin Biere

Institute of Formal Models and Verification

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

Abstract

This paper focuses on developing efficient inference techniques for improving conjunctive normal form (CNF) Boolean satisfiability (SAT) solvers. We analyze a variant of hyper binary resolution from various perspectives: We show that it can simulate the circuit-level technique of structural hashing and how it can be realized efficiently using so called tree-based lookahead. Experiments show that our implementation improves the performance of state-of-the-art CNFlevel SAT techniques on combinational equivalent checking instances.

Original language	English
Title of host publication	Proc. 10th Intl. Conf. on Integration of Artificial Intelligence and Operations Research Techniques in Constraint Programming (CPAIOR'13), LNCS
Publisher	Springer
Pages	77-93
Number of pages	17
Volume	7874
ISBN (Print)	9783642381706
DOIs	https://doi.org/10.1007/978-3-642-38171-3_6
Publication status	Published - 2013

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	7874 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Fields of science

102011 Formal languages
102 Computer Sciences
101 Mathematics

JKU Focus areas

Computation in Informatics and Mathematics

Access to Document

10.1007/978-3-642-38171-3_6

Cite this

Heule, M., Järvisalo, M., & Biere, A. (2013). Revisiting Hyper Binary Resolution. In Proc. 10th Intl. Conf. on Integration of Artificial Intelligence and Operations Research Techniques in Constraint Programming (CPAIOR'13), LNCS (Vol. 7874, pp. 77-93). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7874 LNCS). Springer. https://doi.org/10.1007/978-3-642-38171-3_6

Heule, Marijn ; Järvisalo, Matti ; Biere, Armin. / Revisiting Hyper Binary Resolution. Proc. 10th Intl. Conf. on Integration of Artificial Intelligence and Operations Research Techniques in Constraint Programming (CPAIOR'13), LNCS. Vol. 7874 Springer, 2013. pp. 77-93 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{3f3fe56f32cb4b56946cb2f92877a026,

title = "Revisiting Hyper Binary Resolution",

abstract = "This paper focuses on developing efficient inference techniques for improving conjunctive normal form (CNF) Boolean satisfiability (SAT) solvers. We analyze a variant of hyper binary resolution from various perspectives: We show that it can simulate the circuit-level technique of structural hashing and how it can be realized efficiently using so called tree-based lookahead. Experiments show that our implementation improves the performance of state-of-the-art CNFlevel SAT techniques on combinational equivalent checking instances.",

author = "Marijn Heule and Matti J{\"a}rvisalo and Armin Biere",

year = "2013",

doi = "10.1007/978-3-642-38171-3\_6",

language = "English",

isbn = "9783642381706",

volume = "7874",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "77--93",

booktitle = "Proc. 10th Intl. Conf. on Integration of Artificial Intelligence and Operations Research Techniques in Constraint Programming (CPAIOR'13), LNCS",

}

Heule, M, Järvisalo, M & Biere, A 2013, Revisiting Hyper Binary Resolution. in Proc. 10th Intl. Conf. on Integration of Artificial Intelligence and Operations Research Techniques in Constraint Programming (CPAIOR'13), LNCS. vol. 7874, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 7874 LNCS, Springer, pp. 77-93. https://doi.org/10.1007/978-3-642-38171-3_6

Revisiting Hyper Binary Resolution. / Heule, Marijn; Järvisalo, Matti; Biere, Armin.
Proc. 10th Intl. Conf. on Integration of Artificial Intelligence and Operations Research Techniques in Constraint Programming (CPAIOR'13), LNCS. Vol. 7874 Springer, 2013. p. 77-93 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7874 LNCS).

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

TY - GEN

T1 - Revisiting Hyper Binary Resolution

AU - Heule, Marijn

AU - Järvisalo, Matti

AU - Biere, Armin

PY - 2013

Y1 - 2013

N2 - This paper focuses on developing efficient inference techniques for improving conjunctive normal form (CNF) Boolean satisfiability (SAT) solvers. We analyze a variant of hyper binary resolution from various perspectives: We show that it can simulate the circuit-level technique of structural hashing and how it can be realized efficiently using so called tree-based lookahead. Experiments show that our implementation improves the performance of state-of-the-art CNFlevel SAT techniques on combinational equivalent checking instances.

AB - This paper focuses on developing efficient inference techniques for improving conjunctive normal form (CNF) Boolean satisfiability (SAT) solvers. We analyze a variant of hyper binary resolution from various perspectives: We show that it can simulate the circuit-level technique of structural hashing and how it can be realized efficiently using so called tree-based lookahead. Experiments show that our implementation improves the performance of state-of-the-art CNFlevel SAT techniques on combinational equivalent checking instances.

UR - https://www.scopus.com/pages/publications/84892936575

U2 - 10.1007/978-3-642-38171-3_6

DO - 10.1007/978-3-642-38171-3_6

M3 - Conference proceedings

SN - 9783642381706

VL - 7874

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 77

EP - 93

BT - Proc. 10th Intl. Conf. on Integration of Artificial Intelligence and Operations Research Techniques in Constraint Programming (CPAIOR'13), LNCS

PB - Springer

ER -

Heule M, Järvisalo M, Biere A. Revisiting Hyper Binary Resolution. In Proc. 10th Intl. Conf. on Integration of Artificial Intelligence and Operations Research Techniques in Constraint Programming (CPAIOR'13), LNCS. Vol. 7874. Springer. 2013. p. 77-93. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-642-38171-3_6

Revisiting Hyper Binary Resolution

Abstract

Publication series

Fields of science

JKU Focus areas

Access to Document

Other files and links

Cite this