@inproceedings{HeuleJB:CPAIOR2013,
 author = {Marijn Heule and Matti J\"arvisalo and Armin Biere},
 title = {Revisiting Hyper Binary Resolution},
 booktitle = {Proceedings of the 10th International Conference on 
Integration of Artificial Intelligence and Operations Research Techniques 
in Constraint Programming (CPAIOR 2013)},
 editor = {Carla Gomes and Meinolf Sellmann},
 series = {Lecture Notes in Computer Science},
 volume = {7874},
 pages = {77--93},
 year = {2013},
}

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 CNF-level SAT techniques on 
combinational equivalent checking instances.