Abstract
Sophisticated compact SAT encodings exist for many types of constraints. Alternatively, for instances with many (or large) constraints, the SAT solver can also be extended with built-in propagators (the SAT Modulo Theories approach, SMT). For example, given a cardinality constraint x 1 + … + x n ≤ k, as soon as k variables become true, such a propagator can set the remaining variables to false, generating a so-called explanation clause of the form \(x_1 \wedge \ldots \wedge x_k \rightarrow{\bar{x_i}}\). But certain “bottle-neck” constraints end up generating an exponential number of explanations, equivalent to a naive SAT encoding, much worse than using a compact encoding with auxiliary variables from the beginning. Therefore, Abío and Stuckey proposed starting off with a full SMT approach and partially encoding, on the fly, only certain “active” parts of constraints. Here we build upon their work. Equipping our solvers with some additional bookkeeping to monitor constraint activity has allowed us to shed light on the effectiveness of SMT: many constraints generate very few, or few different, explanations. We also give strong experimental evidence showing that it is typically unnecessary to consider partial encodings: it is competitive to encode the few really active constraints entirely. This makes the approach amenable to any kind of constraint, not just the ones for which partial encodings are known.
This is a preview of subscription content, log in via an institution to check access.
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
Anbulagan, Grastien, A.: Importance of Variables Semantic in CNF Encoding of Cardinality Constraints. In: Bulitko, V., Beck, J.C. (eds.) Eighth Symposium on Abstraction, Reformulation, and Approximation, SARA 2009. AAAI (2009)
Abío, I., Nieuwenhuis, R., Oliveras, A., Rodríguez-Carbonell, E., Mayer-Eichberger, V.: A new look at bdds for pseudo-boolean constraints. J. Artif. Intell. Res (JAIR) 45, 443–480 (2012)
Asín, R., Nieuwenhuis, R., Oliveras, A., Rodríguez-Carbonell, E.: Cardinality networks and their applications. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 167–180. Springer, Heidelberg (2009)
Asín, R., Nieuwenhuis, R., Oliveras, A., Rodríguez-Carbonell, E.: Cardinality Networks: a theoretical and empirical study. Constraints 16(2), 195–221 (2011)
Abío, I., Stuckey, P.J.: Conflict directed lazy decomposition. In: Milano, M. (ed.) CP 2012. LNCS, vol. 7514, pp. 70–85. Springer, Heidelberg (2012)
Bailleux, O., Boufkhad, Y.: Efficient CNF Encoding of Boolean Cardinality Constraints. In: Rossi, F. (ed.) CP 2003. LNCS, vol. 2833, pp. 108–122. Springer, Heidelberg (2003)
Bailleux, O., Boufkhad, Y., Roussel, O.: A translation of pseudo boolean constraints to sat. JSAT 2(1-4), 191–200 (2006)
Bailleux, O., Boufkhad, Y., Roussel, O.: New Encodings of Pseudo-Boolean Constraints into CNF. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 181–194. Springer, Heidelberg (2009)
Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press (February 2009)
Codish, M., Zazon-Ivry, M.: Pairwise cardinality networks. In: Clarke, E.M., Voronkov, A. (eds.) LPAR-16 2010. LNCS, vol. 6355, pp. 154–172. Springer, Heidelberg (2010)
Eén, N., Sörensson, N.: Translating Pseudo-Boolean Constraints into SAT. Journal on Satisfiability, Boolean Modeling and Computation 2, 1–26 (2006)
Goldberg, E., Novikov, Y.: BerkMin: A Fast and Robust SAT-Solver. In: 2002 Conference on Design, Automation, and Test in Europe, DATE 2002, pp. 142–149. IEEE Computer Society (2002)
Manolios, P., Papavasileiou, V.: Pseudo-Boolean solving by incremental translation to SAT. In: Formal Methods in Computer-Aided Design, FMCAD 2011 (2011)
Marques-Silva, J., Planes, J.: Algorithms for Maximum Satisfiability using Unsatisfiable Cores. In: 2008 Conference on Design, Automation and Test in Europe Conference, DATE 2008, pp. 408–413. IEEE Computer Society (2008)
Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT Modulo Theories: From an abstract Davis–Putnam–Logemann–Loveland procedure to DPLL(T). Journal of the ACM, JACM 53(6), 937–977 (2006)
Ohrimenko, O., Stuckey, P.J., Codish, M.: Propagation = lazy clause generation. In: Bessière, C. (ed.) CP 2007. LNCS, vol. 4741, pp. 544–558. Springer, Heidelberg (2007)
Sinz, C.: Towards an optimal CNF encoding of boolean cardinality constraints. In: van Beek, P. (ed.) CP 2005. LNCS, vol. 3709, pp. 827–831. Springer, Heidelberg (2005)
Büttner, M., Rintanen, J.: uttner and J. Rintanen. Satisfiability planning with constraints on the number of actions. In: Biundo, S., Myers, K.L., Rajan, K. (eds.) 15th International Conference on Automated Planning and Scheduling, ICAPS 2005, pp. 292–299. AAAI (2005)
Vardi, M.Y.: Symbolic techniques in propositional satisfiability solving. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 2–3. Springer, Heidelberg (2009)
Warners, J.P.: A Linear-Time Transformation of Linear Inequalities into Conjunctive Normal Form. Information Processing Letters 68(2), 63–69 (1998)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Abío, I., Nieuwenhuis, R., Oliveras, A., Rodríguez-Carbonell, E., Stuckey, P.J. (2013). To Encode or to Propagate? The Best Choice for Each Constraint in SAT. In: Schulte, C. (eds) Principles and Practice of Constraint Programming. CP 2013. Lecture Notes in Computer Science, vol 8124. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-40627-0_10
Download citation
DOI: https://doi.org/10.1007/978-3-642-40627-0_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-40626-3
Online ISBN: 978-3-642-40627-0
eBook Packages: Computer ScienceComputer Science (R0)