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
Original Titel:
Revisiting Hyper Binary Resolution
Sprache des Titels:
Englisch
Original Buchtitel:
Proc. 10th Intl. Conf. on Integration of Artificial Intelligence and Operations Research Techniques in Constraint Programming (CPAIOR'13), LNCS
Original Kurzfassung:
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.