Efficient SAT solving: beyond supercubes

ABSTRACT

SAT (Boolean satisfiability) has become the primary Boolean reasoning engine for many EDA applications, so the efficiency of SAT solving is of great practical importance. Recently, Goldberg et al introduced supercubing, a different approach to search-space pruning, based on a theory that unifies many existing methods. Their implementation reduced the number of decisions, but no speedup was obtained. In this paper, we generalize beyond supercubes, creating a theory we call B-cubing, and show how to implement Bcubing in a practical solver. On extensive benchmark runs, using both real problems and synthetic benchmarks, the new technique is competitive on average with the newest version of ZChaff, is much faster in some cases, and is more robust.

REFERENCES

• 1: Domagoj Babić , Alan J. Hu, Integration of supercubing and learning in a SAT solver, Proceedings of the 2005 conference on Asia South Pacific design automation, January 18-21, 2005, Shanghai, China [doi>10.1145/1120725.1120908]
• 2: F. Bacchus and J. Winter. Effective Preprocessing with Hyper-Resolution and Equality Reduction. In SAT, pages 341--355, 2003.
• 3: A. Bhalla, I. Lynce, J. de Sousa, and J. Marques-Silva. Heuristic backtracking algorithms for SAT. In 4th International Workshop on Microprocessor Test and Verification, pages 69--74, 2003.
• 4: A. Biere. The Evolution from LIMMAT to NANOSAT. Technical Report 444, Dept. of Computer Science, ETH Zörich, 2004.
• 5: A. Biere , A. Cimatti , E. M. Clarke , M. Fujita , Y. Zhu, Symbolic model checking using SAT procedures instead of BDDs, Proceedings of the 36th ACM/IEEE conference on Design automation, p.317-320, June 21-25, 1999, New Orleans, Louisiana, United States [doi>10.1145/309847.309942]
• 6: Randal E. Bryant, Graph-based algorithms for Boolean function manipulation, IEEE Transactions on Computers, v.35 n.8, p.677-691, Aug. 1986 [doi>10.1109/TC.1986.1676819]
• 7: Martin Davis , Hilary Putnam, A Computing Procedure for Quantification Theory, Journal of the ACM (JACM), v.7 n.3, p.201-215, July 1960 [doi>10.1145/321033.321034]
• 8: D.-Z. Du and K. Ko. Theory of Computational Complexity. John Wiley and Sons, 2000.
• 9: E. Goldberg , M. Prasad , R. Brayton, Using Problem Symmetry in Search Based Satisfiability Algorithms, Proceedings of the conference on Design, automation and test in Europe, p.134, March 04-08, 2002
• 10: J. N. Hooker and V. Vinay. Branching rules for satisfiability. Journal of Automated Reasoning, 15(3):359--383, 1995.
• 11: Shin-ichi Minato, Zero-suppressed BDDs for set manipulation in combinatorial problems, Proceedings of the 30th international conference on Design automation, p.272-277, June 14-18, 1993, Dallas, Texas, United States [doi>10.1145/157485.164890]
• 12: João P. Marques-Silva , Karem A. Sakallah, GRASP: A Search Algorithm for Propositional Satisfiability, IEEE Transactions on Computers, v.48 n.5, p.506-521, May 1999 [doi>10.1109/12.769433]
• 13: K. L. McMillan. Interpolation and SAT-based model checking. In CAV 03: Computer-Aided Verification, LNCS 2725, pages 1--13. Springer, 2003.
• 14: Matthew W. Moskewicz , Conor F. Madigan , Ying Zhao , Lintao Zhang , Sharad Malik, Chaff: engineering an efficient SAT solver, Proceedings of the 38th conference on Design automation, p.530-535, June 2001, Las Vegas, Nevada, United States [doi>10.1145/378239.379017]
• 15: A. Nadel. Backtrack Search Algorithms for Propositional Logic Satisfiability: Review and Innovations. Master's thesis, Tel-Aviv University, 2002.
• 16: G. Nam , K. Sakallah , R. Rutenbar, A boolean satisfiability-based incremental rerouting approach with application to FPGAs, Proceedings of the conference on Design, automation and test in Europe, p.560-565, March 2001, Munich, Germany
• 17: Mukul Ranjan Prasad , Robert K. Brayton, Propositional satisfiability algorithms in eda applications, 2001
• 18: L. Ryan. Efficient algortihtms for clause-learning SAT solvers. Master's thesis, Simon Fraser University, 2004.
• 19: P. Stephan, R. Brayton, and A. Sangiovanni-Vincentelli. Combinational test generation using satisfiability. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 15(9):1167--1176, Sept 1996.
• 20: J. P. Warners and H. van Maaren. A two phase algorithm for solving a class of hard satisfiability problems. Operations Research letters, 23:81--88, 1998.
• 21: Joost P. Warners , Hans van Maaren, Recognition of tractable satisfiability problems through balanced polynomial representations, Proceedings of the 5th Twente workshop on on Graphs and combinatorial optimization, p.229-244, February 2000, Enschede, The Netherlands
• 22: H. Zhang and M. E. Stickel. An efficient Algorithm for Unit Propagation. In Proceedings of the Fourth International Symposium on Artificial Intelligence and Mathematics (AI-MATH'96), Fort Lauderdale (Florida USA), 1996.
• 23: Lintao Zhang , Conor F. Madigan , Matthew H. Moskewicz , Sharad Malik, Efficient conflict driven learning in a boolean satisfiability solver, Proceedings of the 2001 IEEE/ACM international conference on Computer-aided design, November 04-08, 2001, San Jose, California
• 24: Lintao Zhang , Sharad Malik, The Quest for Efficient Boolean Satisfiability Solvers, Proceedings of the 18th International Conference on Automated Deduction, p.295-313, July 27-30, 2002

INDEX TERMS

Primary Classification:
  J. Computer Applications
  J.6 COMPUTER-AIDED ENGINEERING
      Subjects: Computer-aided design (CAD)

Additional Classification:
  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.8 Problem Solving, Control Methods, and Search
          Subjects: Graph and tree search strategies

General Terms:
Algorithms, Verification

Keywords:
SAT, formal verification, learning, search space pruning