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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Bacchus, F., Winter, J.: Effective preprocessing with hyper-resolution and equality reduction. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 341–355. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  2. 2.
    Gershman, R., Strichman, O.: Cost-effective hyper-resolution for preprocessing CNF formulas. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 423–429. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  3. 3.
    Heule, M., Dufour, M., van Zwieten, J., van Maaren, H.: March_eq: Implementing additional reasoning into an efficient look-ahead SAT solver. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, pp. 345–359. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  4. 4.
    Heule, M.J.H., van Maaren, H.: Chapter 5: Look-Ahead Based SAT Solvers. In: Handbook of Satisfiability, pp. 155–184. IOS Press (2009)Google Scholar
  5. 5.
    Van Gelder, A.: Toward leaner binary-clause reasoning in a satisfiability solver. Annals of Mathematics and Artificial Intelligence 43, 239–253 (2005)MathSciNetzbMATHCrossRefGoogle Scholar
  6. 6.
    Aho, A., Garey, M., Ullman, J.: The transitive reduction of a directed graph. SIAM Journal on Computing 1(2), 131–137 (1972)MathSciNetzbMATHCrossRefGoogle Scholar
  7. 7.
    Bacchus, F.: Enhancing Davis Putnam with extended binary clause reasoning. In: Proc. AAAI, pp. 613–619. AAAI Press (2002)Google Scholar
  8. 8.
    Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Trans. Computers 35(8), 677–691 (1986)zbMATHCrossRefGoogle Scholar
  9. 9.
    Kuehlmann, A., Krohm, F.: Equivalence checking using cuts and heaps. In: Proc. DAC, pp. 263–268. ACM (1997)Google Scholar
  10. 10.
    Williams, P.F., Andersen, H.R., Hulgaard, H.: Satisfiability checking using boolean expression diagrams. STTT 5(1), 4–14 (2003)CrossRefGoogle Scholar
  11. 11.
    Abdulla, P.A., Bjesse, P., Eén, N.: Symbolic reachability analysis based on SAT-solvers. In: Graf, S., Schwartzbach, M. (eds.) TACAS/ETAPS 2000. LNCS, vol. 1785, pp. 411–425. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  12. 12.
    Sheeran, M., Stålmarck, G.: A tutorial on Stålmarck’s proof procedure for propositional logic. Formal Methods in System Design 16(1), 23–58 (2000)CrossRefGoogle Scholar
  13. 13.
    Billionnet, A., Sutter, A.: An efficient algorithm for the 3-satisfiability problem. Operations Research Letters 12(1), 29–36 (1992)MathSciNetzbMATHCrossRefGoogle Scholar
  14. 14.
    Li, C.M., Anbulagan: Look-ahead versus look-back for satisfiability problems. In: Smolka, G. (ed.) CP 1997. LNCS, vol. 1330, pp. 341–355. Springer, Heidelberg (1997)CrossRefGoogle Scholar
  15. 15.
    Anbulagan, Pham, D.N., Slaney, J.K., Sattar, A.: Old resolution meets modern SLS. In: Proc. AAAI, pp. 354–359 (2005)Google Scholar
  16. 16.
    Heule, M.J.H.: March: Towards a lookahead SAT solver for general purposes, MSc thesis (2004)Google Scholar
  17. 17.
    Biere, A.: P{re,i}coSAT@SC’09. In: SAT 2009 Competitive Event Booklet (2009)Google Scholar
  18. 18.
    Boufkhad, Y.: Aspects probabilistes et algorithmiques du problème de satisfaisabilité, PhD thesis, Univertsité de Paris 6 (1996)Google Scholar
  19. 19.
    Simons, P.: Towards constraint satisfaction through logic programs and the stable model semantics, Report A47, Digital System Laboratory, Helsinki University of Technology (1997)Google Scholar
  20. 20.
    Mijnders, S., de Wilde, B., Heule, M.J.H.: Symbiosis of search and heuristics for random 3-SAT. In: Proc. LaSh (2010)Google Scholar
  21. 21.
    Biere, A.: (Q)CompSAT and (Q)PicoSAT at the SAT’06 Race (2006)Google Scholar
  22. 22.
    Han, H., Jin, H., Somenzi, F.: Clause simplification through dominator analysis. In: Proc. DATE, pp. 143–148. IEEE (2011)Google Scholar
  23. 23.
    Biere, A.: Lingeling, Plingeling, PicoSAT and PrecoSAT at SAT Race 2010. FMV Report Series TR 10/1, JKU, Linz, Austria (2010)Google Scholar
  24. 24.
    Soos, M.: CryptoMiniSat 2.5.0, SAT Race’10 solver description (2010)Google Scholar
  25. 25.
    Han, H., Somenzi, F.: On-the-fly clause improvement. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 209–222. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  26. 26.
    Järvisalo, M., Heule, M.J.H., Biere, A.: Inprocessing rules. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol. 7364, pp. 355–370. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  27. 27.
    Kunz, W., Pradhan, D.K.: Recursive learning: a new implication technique for efficient solutions to CAD problems-test, verification, and optimization. IEEE T-CAD 13(9) (1994)Google Scholar
  28. 28.
    Barrett, C.W., Sebastiani, R., Seshia, S.A., Tinelli, C.: Chpt. 26: SMT Modulo Theories. In: Handbook of Satisfiability. IOS Press (2009)Google Scholar
  29. 29.
    Marques-Silva, J., Glass, T.: Combinational equivalence checking using satisfiability and recursive learning. In: Proc. DATE (1999)Google Scholar
  30. 30.
    Groote, J.F., Warners, J.P.: The propositional formula checker HeerHugo. J. Autom. Reasoning 24(1/2), 101–125 (2000)MathSciNetzbMATHCrossRefGoogle Scholar
  31. 31.
    Heule, M.J.H., Kullmann, O., Wieringa, S., Biere, A.: Cube and conquer: Guiding CDCL SAT solvers by lookaheads. In: Eder, K., Lourenço, J., Shehory, O. (eds.) HVC 2011. LNCS, vol. 7261, pp. 50–65. Springer, Heidelberg (2012)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2013

Authors and Affiliations

  • Marijn J. H. Heule
    • 1
    • 3
  • Matti Järvisalo
    • 2
  • Armin Biere
    • 3
  1. 1.Department of Computer ScienceThe University of Texas at AustinUnited States
  2. 2.HIIT & Department of Computer ScienceUniversity of HelsinkiFinland
  3. 3.Institute for Formal Models and VerificationJohannes Kepler University LinzAustria

Personalised recommendations