This Article 
 Bibliographic References 
 Add to: 
Solution and Optimization of Systems of Pseudo-Boolean Constraints
October 2007 (vol. 56 no. 10)
pp. 1415-1424
Optimized solvers for the Boolean Satisfiability (SAT) problem have many applications in areas such as hardware and software verification, FPGA routing, planning, etc. Further uses are complicated by the need to express "counting constraints" in conjunctive normal form (CNF). Expressing such constraints by pure CNF leads to more complex SAT instances. Alternatively, those constraints can be handled by Integer Linear Programming (ILP), but generic ILP solvers may ignore the Boolean nature of 0-1 variables. Therefore specialized 0-1 ILP solvers extend SAT solvers to handle these so-called "pseudo-Boolean" (PB) constraints.This work provides an update on the on-going competition between generic ILP techniques and specialized 0-1 ILP techniques. To make a fair comparison, we generalize recent ideas for fast SAT-solving to more general 0-1 ILP problems that may include counting constraints and optimization. This generalization is embodied in our PB constraint solver and optimizer PBS, which is compared with state-of-the-art CNF and generic ILP solvers. Another aspect of our comparison is evaluation on 0-1 ILP benchmarks that originate in Electronic Design Automation (EDA), but that cannot be directly solved by a SAT solver. Specifically, we solve instances of the Max-SAT and Max-ONEs optimization problems which seek to maximize the number of satisfied clauses and the "true" values over all satisfying assignments, respectively. Those problems have straightforward applications to SAT-based routing and are additionally important due to reductions from Max-Cut, Max-Clique, and Min Vertex Cover. Our experimental results show that specialized 0-1 techniques implemented in PBS tend to outperform generic ILP techniques on Boolean optimization problems as well as on general EDA SAT problems.

[1] F Aloul, A Ramani, I Markov, and K Sakallah, “Solving Difficult SAT Instances in the Presence of Symmetry,” Proc. Design Automation Conf. (DAC '02), pp. 731-736, 2002.
[2] L. Baptista and J.P. Marques-Silva, “Using Randomization and Learning to Solve Hard Real-World Instances of Satisfiability,” Proc. Sixth Int'l Conf. Principles and Practice of Constraint Programming (CP '00), 2000.
[3] P. Barth, “A Davis-Putnam Based Enumeration Algorithm for Linear Pseudo-Boolean Optimization,” Technical Report MPI-I-95-2-003, Max-Planck-Institut Für Informatik, 1995.
[4] P. Barth, “OPBDP: A Davis-Putnam Based Enumeration Algorithm for Linear Pseudo-Boolean Optimization,” opbdp, 2007.
[5] R. Bayardo, Jr. and R. Schrag, “Using CSP Look-Back Techniques to Solve Real World SAT Instances,” Proc. Nat'l Conf. Artificial Intelligence, pp. 203-208, 1997.
[6] F.M. Brown, Boolean Reasoning. Kluwer Academic, 1990.
[7] D. Chai and A. Kuehlmann, “A Fast Pseudo-Boolean Constraint Solver,” Proc. Design Automation Conf. (DAC '03), pp. 830-835, 2003.
[8] N. Creignou, S. Kanna, and M. Sudan, Complexity Classifications of Boolean Constraint Satisfaction Problems. SIAM, 2001.
[9] M. Davis, G. Logemann, and D. Loveland, “A Machine Program for Theorem Proving,” Comm. ACM, vol. 5, no. 7, pp. 394-397, 1962.
[10] DIMACS Challenge Benchmarks, ftp://Dimacs.rutgers.EDU/pub/challenge/sat/ benchmarkscnf, 2007.
[11] H. Dixon and M. Ginsberg, “Inference Methods for a Pseudo-Boolean Satisfiability Solver,” Proc. Nat'l Conf. Artificial Intelligence, pp. 635-640, 2002.
[12] M. Garey and D. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness. W.H. Freeman, 1979.
[13] E. Goldberg and Y. Novikov, “BerkMin: A Fast and Robust SAT-Solver,” Proc. Design, Automation, and Test in Europe Conf. (DATE '02), pp. 142-149, 2002.
[14] H. Hoos and T. Stützle, http:/, 2007.
[15] ILOG CPLEX,, 2007.
[16] Z. Kohavi, , Switching and Finite Automata Theory, second ed. McGraw-Hill, 1978.
[17] R. Ladner and R. Fischer, “Parallel Prefix Computation,” J. ACM, vol. 27, no. 4, pp. 831-838, 1980.
[18] T. Larrabee, “Test Pattern Generation Using Boolean Satisfiability,” IEEE Trans. Computer-Aided Design, vol. 11, no. 1, pp. 4-15, 1992.
[19] I. Lynce, L. Baptista, and J. Marques-Silva, “Stochastic Systematic Search Algorithms for Satisfiability,” Proc. LICS Workshop Theory and Applications of Satisfiability Testing, 2001.
[20] V. Manquinho and J. Marques-Silva, “On Using Satisfiability-Based Pruning Techniques in Covering Algorithms,” Proc. Design Automation and Test Conf. in Europe, pp. 356-363, 2000.
[21] J. Marques-Silva and K. Sakallah, “GRASP: A Search Algorithm for Propositional Satisfiability,” IEEE Trans. Computers, vol. 48, no. 5, pp. 506-521, May 1999.
[22] N. Een and N. Sorensson, “An Extensible SAT-Solver,” Theory and Applications of Satisfiability Testing, pp. 502-518, 2003.
[23] M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, and S. Malik, “Chaff: Engineering an Efficient SAT Solver,” Proc. Design Automation Conf. (DAC), pp. 503-535, 2001.
[24] G. Nam, F. Aloul, K. Sakallah, and R. Rutenbar, “A Comparative Study of Two Boolean Formulations of FPGA Detailed Routing Constraints,” Proc. Int'l Symp. Physical Design (ISPD '01), pp. 222-227, 2001.
[25] B. Selman, H. Kautz, and B. Cohen, “Noise Strategies for Local Search,” Proc. Nat'l Conf. Artificial Intelligence, pp. 337-343, 1994.
[26] M. Velev and R. Bryant, “Effective Use of Boolean Satisfiability Procedure in the Formal Verification of Superscalar and VLIW Mircroprocessors,” Proc. Design Automation Conf. (DAC '01), pp.226-231, 2001.
[27] J. Walsor, “Solving Linear Pseudo-Boolean Constraint Problems with Local Search,” Proc. Nat'l Conf. Artificial Intelligence, pp. 269-274, 1997.
[28] J. Whittemore, J. Kim, and K. Sakallah, “SATIRE: A New Incremental Satisfiability Engine,” Proc. Design Automation Conf. (DAC '01), pp. 542-545, 2001.
[29] H. Xu, R. Rutenbar, and K. Sakallah, “Sub-SAT: A Formulation for Relaxed Boolean Satisfiability with Applications in Routing,” Proc. Int'l Symp. Physical Design (ISPD '02), 2002.
[30] J. Warners, “A Linear-Time Transformation of Linear Inequalities into Conjunctive Normal Form,” Information Processing Letters, vol. 68, no. 2, pp. 63-69, 1998.
[31] H. Zhang, “SATO: An Efficient Propositional Prover,” Proc. Int'l Conf. Automated Deduction, pp. 272-275, 1997.
[32] L. Zhang, C. Madigan, M. Moskewicz, and S. Malik, “Efficient Conflict Driven Learning in a Boolean Satisfiability Solver,” Proc. Int'l Conf. Computer-Aided Design (ICCAD '01), pp. 279-285, 2001.
[33] H. Zhang and M. Stickel, “An Efficient Algorithm for Unit-Propagation,” Proc. Int'l Symp. Artificial Intelligence and Math., pp.166-169, 1996.

Index Terms:
Boolean Satisfiability (SAT), Integer Linear Programming (ILP), Backtrack Search, Conjunctive Normal Form (CNF), Pseudo Boolean (PB), Max-SAT, Max-ONE, Global Routing
Fadi A. Aloul, Arathi Ramani, Karem A. Sakallah, Igor L. Markov, "Solution and Optimization of Systems of Pseudo-Boolean Constraints," IEEE Transactions on Computers, vol. 56, no. 10, pp. 1415-1424, Oct. 2007, doi:10.1109/TC.2007.1075
Usage of this product signifies your acceptance of the Terms of Use.