Marijn Heule, Matti Järvisalo, Armin Biere,
"Revisiting Hyper Binary Resolution"
: Proc. 10th Intl. Conf. on Integration of Artificial Intelligence and Operations Research Techniques in Constraint Programming (CPAIOR'13), LNCS, Serie Lecture Notes in Computer Science (LNCS), Vol. 7874, Springer, Seite(n) 77-93, 2013
Revisiting Hyper Binary Resolution
Sprache des Titels:
Proc. 10th Intl. Conf. on Integration of Artificial Intelligence and Operations Research Techniques in Constraint Programming (CPAIOR'13), LNCS
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.