zbMATH — the first resource for mathematics

Revisiting hyper binary resolution. (English) Zbl 1382.68223
Gomes, Carla (ed.) et al., Integration of AI and OR techniques in constraint programming for combinatorial optimization problems. 10th international conference, CPAIOR 2013, Yorktown Heights, NY, USA, May 18–22, 2013. Proceedings. Berlin: Springer (ISBN 978-3-642-38170-6/pbk). Lecture Notes in Computer Science 7874, 77-93 (2013).
Summary: 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 CNF-level SAT techniques on combinational equivalent checking instances.
For the entire collection see [Zbl 1263.68017].
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
Full Text: DOI