Abstract
Motivated by the performance improvements made to SAT solvers in recent years, a number of different encodings of constraints into SAT have been proposed. Concrete examples are the different SAT encodings for ≤ 1 (x 1,...,x n ) constraints. The most widely used encoding is known as the pairwise encoding, which is quadratic in the number of variables in the constraint. Alternative encodings are in general linear, and require using additional auxiliary variables. In most settings, the pairwise encoding performs acceptably well, but can require unacceptably large Boolean formulas. In contrast, linear encodings yield much smaller Boolean formulas, but in practice SAT solvers often perform unpredictably. This lack of predictability is mostly due to the large number of auxiliary variables that need to be added to the resulting Boolean formula. This paper studies one specific encoding for ≤ 1 (x 1,...,x n ) constraints, and shows how a state-of-the-art SAT solver can be adapted to overcome the problem of adding additional auxiliary variables. Moreover, the paper shows that a SAT solver may essentially ignore the existence of auxiliary variables. Experimental results indicate that the modified SAT solver becomes significantly more robust on SAT encodings involving ≤ 1 (x 1,...,x n ) constraints.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Ansótegui, C., Manyá, F.: Mapping problems with finite-domain variables to problems with boolean variables. In: Proceedings of the International Conference on Theory and Applications of Satisfiability Testing, pp. 1–15 (2004)
Bailleux, O., Boufkhad, Y.: Efficient CNF encoding of boolean cardinality constraints. In: Proceedings of the International Conference on Principles and Practice of Constraint Programming, pp. 108–122 (2003)
Bailleux, O., Boufkhad, Y.: Full CNF encoding: The counting constraints case. In: Proceedings of the International Conference on Theory and Applications of Satisfiability Testing (2004)
Bailleux, O., Boufkhad, Y., Roussel, O.: A translation of pseudo Boolean constraints to SAT. Journal on Satisfiability, Boolean Modeling and Computation (2 March 2006)
Bayardo Jr., R., Schrag, R.: Using CSP look-back techniques to solve real-world SAT instances. In: Proceedings of the National Conference on Artificial Intelligence, pp. 203–208 (July 1997)
Béjar, R., Hähnle, R., Manyà, F.: A modular reduction of regular logic to classical logic. In: Proceedings of the International Symposium on Multiple-Valued Logics, pp. 221–226 (2001)
Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Communications of the Association for Computing Machinery 5, 394–397 (1962)
Davis, M., Putnam, H.: A computing procedure for quantification theory. Journal of the Association for Computing Machinery 7, 201–215 (1960)
Eén, N., Sörensson, N.: An extensible SAT solver. In: Proceedings of the International Conference on Theory and Applications of Satisfiability Testing, pp. 502–518 (May 2003)
Eén, N., Sörensson, N.: Translating pseudo-Boolean constraints into SAT. Journal on Satisfiability, Boolean Modeling and Computation 2 (March 2006)
Gent, I.P.: Arc consistency in SAT. In: Proceedings of the European Conference on Artificial Intelligence, pp. 121–125 (2002)
Gent, I.P., Nightingale, P.: A new encoding of AllDifferent into SAT. In: Proceedings 3rd International Workshop on Modelling and Reformulating Constraint Satisfaction Problems, pp. 95–110 (September 2004)
Gent, I.P., Prosser, P.: An empirical study of the stable marriage problem with ties and incomplete lists. In: Proceedings of the European Conference on Artificial Intelligence, pp. 141–145 (2002)
Goldberg, E., Novikov, Y.: BerkMin: a fast and robust SAT-solver. In: Proceedings of the Design Automation and Test in Europe Conference, pp. 142–149 (March 2002)
Gomes, C.P., Selman, B., Kautz, H.: Boosting combinatorial search through randomization. In: Proceedings of the National Conference on Artificial Intelligence, pp. 431–437 (July 1998)
Kasif, S.: On the parallel complexity of discrete relaxation in constraint satisfaction networks. Artificial Intelligence 45(3), 275–286 (1990)
Marques-Silva, J., Sakallah, K.: GRASP: A new search algorithm for satisfiability. In: Proceedings of the International Conference on Computer-Aided Design, pp. 220–227 (November 1996)
Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Engineering an efficient SAT solver. In: Design Automation Conference, pp. 530–535 (June 2001)
Nadel, A.: Backtrack search algorithms for propositional logic satisfiability: Review and innovations. Master’s thesis, Hebrew University of Jerusalem (November 2002)
Ryan, L.: Efficient algorithms for clause-learning SAT solvers. Master’s thesis, Simon Fraser University (February 2004)
Sinz, C.: Towards an optimal CNF encoding of boolean cardinality constraints. In: Proceedings of the International Conference on Principles and Practice of Constraint Programming, pp. 827–831 (October 2005)
Walsh, T.: SAT v CSP. In: Proceedings of the International Conference on Principles and Practice of Constraint Programming, pp. 441–456 (September 2000)
Warners, J.P.: A linear-time transformation of linear inequalities into conjunctive normal form. Information Processing Letters 68(2), 63–69 (1998)
Zhang, H.: SATO: An efficient propositional prover. In: Proceedings of the International Conference on Automated Deduction, pp. 272–275 (July 1997)
Zhang, L., Madigan, C.F., Moskewicz, M.W., Malik, S.: Efficient conflict driven learning in boolean satisfiability solver. In: Proceedings of the International Conference on Computer-Aided Design, pp. 279–285 (2001)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Marques-Silva, J., Lynce, I. (2007). Towards Robust CNF Encodings of Cardinality Constraints. In: Bessière, C. (eds) Principles and Practice of Constraint Programming – CP 2007. CP 2007. Lecture Notes in Computer Science, vol 4741. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-74970-7_35
Download citation
DOI: https://doi.org/10.1007/978-3-540-74970-7_35
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-74969-1
Online ISBN: 978-3-540-74970-7
eBook Packages: Computer ScienceComputer Science (R0)