| | This Article | |
| |
| |
| | Share | |
| |
| |
| | Bibliographic References | |
| |
| |
| | Add to: | |
| |
 Digg
 Furl
 Spurl
 Blink
 Simpy
 Google
 Del.icio.us
 Y!MyWeb
| |
| | Search | |
| |
| |
| | |
B-Cubing: New Possibilities for Efficient SAT-Solving
November 2006 (vol. 55 no. 11)
pp. 1315-1324
SAT (Boolean satisfiability) has become the primary Boolean reasoning engine for many EDA (electronic design automation) applications, so the efficiency of SAT-solving is of great practical importance. B-cubing is our extension and generalization of Goldberg et al.'s supercubing, an approach to pruning in SAT-solving completely different from the standard approach used in leading solvers. We have built a B-cubing-based solver that is competitive with, and often outperforms, leading conventional solvers (e.g., ZChaff II) on a wide range of EDA benchmarks. However, B-cubing is hard to understand and even the correctness of the algorithm is not obvious. This paper presents the theoretical basis for B-cubing, proves our approach correct, details our implementation and experimental results, and maps out other correct possibilities for further improving SAT-solving.
[1] A. Biere, A. Cimatti, M. Clarke, M. Fujita, and Y. Zhu, “Symbolic Model Checking Using SAT Procedures Instead of BDDs,” Proc. 36th ACM/IEEE Design Automation Conf., pp. 317-320, 1999.
[2] K.L. McMillan, “Interpolation and SAT-Based Model Checking,” Proc. Computer-Aided Verification (CAV '03), pp. 1-13, 2003.
[3] G. Nam, K. Sakallah, and R. Rutenbar, “A Boolean Satisfiability-Based Incremental Rerouting Approach with Application to FPGAs,” Proc. Conf. Design Automation and Test in Europe, pp.560-565, 2001.
[4] P. Stephan, R. Brayton, and A. Sangiovanni-Vincentelli, “Combinational Test Generation Using Satisfiability,” IEEE Trans. Computer-Aided Design of Integrated Circuits and Systems, vol. 15, no. 9, pp. 1167-1176, Sept. 1996.
[5] Z. Zeng, M.J. Ciesielski, and B. Rouzeyre, “Functional Test Generation Using Constraint Logic Programming,” Proc. 11th Int'l Conf. VLSI/SOC, IFIP TC10/WG10.5, pp. 375-387, 2001.
[6] M. Davis and H. Putnam, “A Computing Procedure for Quantification Theory,” J. ACM, vol. 7, no. 3, pp. 201-215, 1960.
[7] M. Davis, G. Logemann, and D. Loveland, “A Machine Program for Theorem-Proving,” Comm. ACM, vol. 5, no. 7, pp. 394-397, 1962.
[8] J.N. Hooker and V. Vinay, “Branching Rules for Satisfiability,” J.Automated Reasoning, vol. 15, no. 3, pp. 359-383, 1995.
[9] A. Bhalla, I. Lynce, J. de Sousa, and J. Marques-Silva, “Heuristic Backtracking Algorithms for SAT,” Proc. Fourth Int'l Workshop Microprocessor Test and Verification: Common Challenges and Solutions, pp. 69-74, 2003.
[10] C.M. Li and Anbulagan, “Heuristics Based on Unit Propagation for Satisfiability Problems,” Proc. First Intl Joint Conf. Artificial Intelligence (IJCAI), pp. 366-371, 1997.
[11] J.P. Marques-Silva and K.A. Sakallah, “GRASP: A Search Algorithm for Propositional Satisfiability,” IEEE Trans. Computers, vol. 48, no. 5, pp. 506-521, May 1999.
[12] L. Zhang, C.F. Madigan, M.H. Moskewicz, and S. Malik, “Efficient Conflict Driven Learning in a Boolean Satisfiability Solver,” Proc. Int'l Conf. Computer-Aided Design, pp. 279-285, 2001.
[13] F. Bacchus, “Enhancing Davis Putnam with Extended Binary Clause Reasoning,” Proc. Nat'l Conf. Artificial Intelligence (AAAI '02), pp. 613-619, 2002.
[14] H. Zhang and M.E. Stickel, “An Efficient Algorithm for Unit Propagation,” Proc. Fourth Int'l Symp. Artificial Intelligence and Math. (AI-MATH '96), 1996.
[15] M.W. Moskewicz, C.F. Madigan, Y. Zhao, L. Zhang, and S. Malik, “Chaff: Engineering an Efficient SAT Solver,” Proc. Design Automation Conf., pp. 530-535, 2001.
[16] F. Bacchus and J. Winter, “Effective Preprocessing with Hyper-Resolution and Equality Reduction,” SAT, pp. 341-355, 2003.
[17] J.P. Warners and H. van Maaren, “A Two Phase Algorithm for Solving a Class of Hard Satisfiability Problems,” Operations Research Letters, vol. 23, pp. 81-88, 1998.
[18] M. Heule, H. van Maaren, “Aligning CNF- and Equivalence-Reasoning,” Proc. Int'l Conf. Theory and Applications of Satisfiability Testing (SAT), pp. 174-181, 2004.
[19] C.M. Li, “Integrating Equivalency Reasoning Into Davis-Putnam Procedure,” Proc. AAAI 17th Nat'l Conf. Artificial Intelligence, pp.291-296, 2000.
[20] L. Zhang and S. Malik, “The Quest for Efficient Boolean Satisfiability Solvers,” Proc. 18th Int'l Conf. Automated Deduction, pp. 295-313, 2002.
[21] M.R. Prasad, “Propositional Satisfiability Algorithms in EDA Applications” PhD dissertation, Univ. of California at Berkeley, 2001.
[22] E. Goldberg, M.R. Prasad, and R.K. Brayton, “Using Problem Symmetry in Search Based Satisfiability Algorithms,” Proc. Conf. Design, Automation and Test in Europe, pp. 134-142, 2002.
[23] D. Babić and A.J. Hu, “Integration of Supercubing and Learning in a SAT Solver,” Proc. Asia South Pacific Design Automation Conf., pp.438-444, 2005.
[24] A. Nadel, “Backtrack Search Algorithms for Propositional Logic Satisfiability: Review and Innovations,” master's thesis, Tel-Aviv University, 2002.
[25] D. Babić, J. Bingham, and A.J. Hu, “Efficient SAT Solving: Beyond Supercubes,” Proc. 42nd Design Automation Conf., pp. 744-749, 2005.
[26] D. Babić, J. Bingham, and A.J. Hu, “B-Cubing Theory: New Possibilities for Efficient SAT-Solving,” Proc. Int'l Workshop High-Level Design Validation and Test, 2005.
[27] D.-Z. Du and K. Ko, Theory of Computational Complexity. John Wiley and Sons, 2000.
[28] J.P. Warners and H. van Maaren, “Recognition of Tractable Satisfiability Problems through Balanced Polynomial Representations,” Proc. Fifth Twente Workshop Graphs and Combinatorial Optimization, pp. 229-244, 2000.
Index Terms:
SAT, Boolean satisfiability, search space pruning.
Citation:
Domagoj Babic, Jesse Bingham, Alan J. Hu, "B-Cubing: New Possibilities for Efficient SAT-Solving," IEEE Transactions on Computers, vol. 55, no. 11, pp. 1315-1324, Nov. 2006, doi:10.1109/TC.2006.175
