Solving the minimum-cost satisfiability problem using SAT based branch-and-bound search

ABSTRACT

Boolean Satisfiability (SAT) has seen many successful applications in various fields, such as Electronic Design Automation (EDA) and Artificial Intelligence (AI). However, in some cases it may be required/preferable to use variations of the general SAT problem. In this paper we consider one important variation, the Minimum-Cost Satisfiability Problem (MinCostSAT). MinCostSAT is a SAT problem which minimizes the cost of the satisfying assignment. MinCostSAT has various applications, e.g. Automatic Test Pattern Generation (ATPG), FPGA Routing, AI Planning, etc. This problem has been tackled before - first by covering algorithms, e.g. scherzo [3], and more recently by SAT based algorithms, e.g. bsolo [16]. However the SAT algorithms they are based on are not the current generation of highly efficient solvers. The solvers in this generation, e.g. Chaff [20], MiniSat [5] etc., incorporate several new advances, e.g. two literal watching based Boolean Constraint Propagation, that have delivered order of magnitude speedups. We first point out the challenges in using this class of solvers for the MinCostSAT problem and then present techniques to overcome these challenges. The resulting solver MinCostChaff shows order of magnitude improvement over several current best known branch-and-bound solvers for a large class of problems, ranging from Minimum Test Pattern Generation, Bounded Model Checking in EDA to Graph Coloring and Planning in AI.

REFERENCES

• 1: P. Barth. A Davis-Putnam enumeration algorithm for linear pseudo-Boolean optimization. Technical Report MPI-I-95-2-003, Max Plank Institute Computer Science, 1995.
• 2: Olivier Coudert, Two-level logic minimization: an overview, Integration, the VLSI Journal, v.17 n.2, p.97-140, Oct. 1994 [doi>10.1016/0167-9260(94)00007-7]
• 3: Olivier Coudert, On solving covering problems, Proceedings of the 33rd annual conference on Design automation, p.197-202, June 03-07, 1996, Las Vegas, Nevada, United States [doi>10.1145/240518.240555]
• 4: Olivier Coudert , Jean Chritophe Madre, New ideas for solving covering problems, Proceedings of the 32nd ACM/IEEE conference on Design automation, p.641-646, June 12-16, 1995, San Francisco, California, United States [doi>10.1145/217474.217603]
• 5: N. Eén and N. Sörensson. The MiniSat page, http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/, 2006.
• 6: Paulo F. Flores , Horácio C. Neto , João P. Marques-Silva, An exact solution to the minimum size test pattern problem, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.6 n.4, p.629-644, October 2001 [doi>10.1145/502175.502186]
• 7: Z. Fu and S. Malik. On solving the Partial MAX-SAT problem. In International Conference on Theory and Applications of Satisfiability Testing (SAT'06), LNCS 4121, pages 252--265, 2006.
• 8: R. Gomory. Outline of an algorithm for integer solution to linear programs. Bulletin of the American Mathematical Society, 64:275--278, 1958.
• 9: H. H. Hoos and T. Stützle. SATLIB: An online resource for research on SAT, http://www.satlib.org.SAT 2000, pages 283--292, 2000.
• 10: ILOG. Cplex homepage, http://www.ilog.com/products/cplex/, 2006.
• 11: D. S. Johnson. Approximation algorithms for combinatorial problems. Journal of Computer and System Sciences, 9:256--278, 1974.
• 12: Sanjeev Khanna , Madhu Sudan , Luca Trevisan , David P. Williamson, The Approximability of Constraint Satisfaction Problems, SIAM Journal on Computing, v.30 n.6, p.1863-1920, 2001 [doi>10.1137/S0097539799349948]
• 13: Xiao Yu Li , Matthias F. Stallmann , Franc Brglez, Optimization algorithms for the minimum-cost satisfiability problem, North Carolina State University, 2004
• 14: Stan Liao , Srinivas Devadas, Solving covering problems using LPR-based lower bounds, Proceedings of the 34th annual conference on Design automation, p.117-120, June 09-13, 1997, Anaheim, California, United States [doi>10.1145/266021.266046]
• 15: V. Manquinho, P. Flores, J. Marques-Silva, and A. Oliverira. Prime implicant computation using satisfiability algorithms. In Proceedings of the IEEE International Conference on Tools with Artificial Intelligence (ICTAI'99), pages 117--120, 1999.
• 16: V. Manquinho and J. Marques-Silva. Search pruning techniques in SAT-based branch-and-bound algorithms for the binate covering problem. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 21:505--516, 2002.
• 17: V. Manquinho and O. Roussel. Pseudo-Boolean evaluation 2005 http://www.cril.univ-artois.fr/PB05/, August 2005.
• 18: 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]
• 19: S. Miyazaki, K. Iwama, and Y. Kambayashi. Database queries as combinatorial optimization problems. In Proceedings of the International Symposium on Cooperative Database Systems for Advanced Applications, pages 448--454, 1996.
• 20: 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]
• 21: S. Yang. Logic synthesis and optimization benchmarks user guide. Technical Report 1991-IWLS-UG-Saeyang, MCNC, Research Triangle Park, NC, 1991.

INDEX TERMS

Primary Classification:
  B. Hardware
  B.6 LOGIC DESIGN
      B.6.3 Design Aids

General Terms:
Algorithms, Verification

Keywords:
Boolean satisfiability, MinCostSAT, branch-and-bound, optimization