Zhaohui Fu
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.
- 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.Google Scholar
- O. Coudert. Two-level logic minimization: An overview. Integration the VLSI journal, 17(2):97--140, 1994. Google ScholarDigital Library
- O. Coudert. On solving covering problems. In Proceedings of the 33rd Design Automation Conference (DAC'96), pages 197--202, 1996. Google ScholarDigital Library
- O. Coudert and J. C. Madre. New ideas for solving covering problems. In Proceedings of the 32nd Design Automation Conference (DAC'95), pages 641--646, 1995. Google ScholarDigital Library
- N. Eén and N. Sörensson. The MiniSat page, http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/, 2006.Google Scholar
- P. Flores, H. Neto, and J. Marques-Silva. An exact solution to the minimum size test pattern problem. IEEE Transactions on Design Automation of Electronic Systems, 6(4):629--644, 2001. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- R. Gomory. Outline of an algorithm for integer solution to linear programs. Bulletin of the American Mathematical Society, 64:275--278, 1958.Google ScholarCross Ref
- 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.Google Scholar
- ILOG. Cplex homepage, http://www.ilog.com/products/cplex/, 2006.Google Scholar
- D. S. Johnson. Approximation algorithms for combinatorial problems. Journal of Computer and System Sciences, 9:256--278, 1974.Google ScholarDigital Library
- S. Khanna, M. Sudan, L. Trevisan, and D. Williamson. The approximability of constraint satisfaction problems. SIAM Journal of Computing, 30(6): 1863--1920, 2000. Google ScholarDigital Library
- X. Y. Li. Optimization Algorithms for the Minimum-Cost Satisfiability Problem. PhD thesis, Department of Computer Science, North Carolina State University, Raleigh, North Carolina, 2004. 162 pages. Google ScholarDigital Library
- S. Liao and S. Devadas. Solving covering problems using LPR-based lower bounds. In Proceedings of the 34th Design Automation Conference (DAC'97), pages 117--120, 1997. Google ScholarDigital Library
- 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.Google Scholar
- 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. Google ScholarDigital Library
- V. Manquinho and O. Roussel. Pseudo-Boolean evaluation 2005 http://www.cril.univ-artois.fr/PB05/, August 2005.Google Scholar
- J. Marques-Silva and K. A. Sakallah. GRASP: A search algorithm for propositional satisfiability. IEEE Transactions on Computers, 48:506--521, 1999. Google ScholarDigital Library
- 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.Google Scholar
- M. W. Moskewicz, C. F. Madigan, Y. Zhao, L. Zhang, and S. Malik. Chaff: Engineering an efficient SAT solver. In Proceedings of the 38th Design Automation Conference (DAC'01), 2001. Google ScholarDigital Library
- S. Yang. Logic synthesis and optimization benchmarks user guide. Technical Report 1991-IWLS-UG-Saeyang, MCNC, Research Triangle Park, NC, 1991.Google Scholar
Index Terms
- Solving the minimum-cost satisfiability problem using SAT based branch-and-bound search
Recommendations
Efficient SAT solving for non-clausal formulas using DPLL, graphs, and watched cuts
DAC '09: Proceedings of the 46th Annual Design Automation ConferenceBoolean satisfiability (SAT) solvers are used heavily in hardware and software verification tools for checking satisfiability of Boolean formulas. Most state-of-the-art SAT solvers are based on the Davis-Putnam-Logemann-Loveland (DPLL) algorithm and ...
Iterative SAT Solving for Minimum Satisfiability
ICTAI '12: Proceedings of the 2012 IEEE 24th International Conference on Tools with Artificial Intelligence - Volume 01Minimum Satisfiability (MinSAT) denotes one of the optimization versions of the Boolean Satisfiability (SAT) problem. In some settings MinSAT is preferred to using Maximum Satis-fiability (MaxSAT). Several encodings and dedicated branch and bound ...
Accelerating Boolean Satisfiability (SAT) solving by common subclause elimination
Boolean Satisfiability (SAT) is an important problem in many domains. Modern SAT solvers have been widely used in important industrial applications including automated planning and verification. To solve more problems in real applications, new ...
Comments