Abstract
Constraint “at most one” is a basic cardinality constraint which requires that at most one of its \(n\) boolean inputs is set to \(1\). This constraint is widely used when translating a problem into a conjunctive normal form (CNF) and we investigate its CNF encodings suitable for this purpose. An encoding differs from a CNF representation of a function in that it can use auxiliary variables. We are especially interested in propagation complete encodings which have the property that unit propagation is strong enough to enforce consistency on input variables. We show a lower bound on the number of clauses in any propagation complete encoding of the “at most one” constraint. The lower bound almost matches the size of the best known encodings. We also study an important case of 2-CNF encodings where we show a slightly better lower bound. The lower bound holds also for a related “exactly one” constraint.
P. Kučera—Supported by the Czech Science Foundation (grant GA15-15511S).
P. Savický—Supported by CE-ITI and GAČR under the grant GBP202/12/G061 and by the institutional research plan RVO:67985807.
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
References
Asín, R., Nieuwenhuis, R., Oliveras, A., Rodríguez-Carbonell, E.: Cardinality networks: a theoretical and empirical study. Constraints 16(2), 195–221 (2011). doi:10.1007/s10601-010-9105-0
Aspvall, B., Plass, M.F., Tarjan, R.E.: A linear-time algorithm for testing the truth of certain quantified boolean formulas. Inf. Process. Lett. 8(3), 121–123 (1979)
Babka, M., Balyo, T., Čepek, O., Gurský, Š., Kučera, P., Vlček, V.: Complexity issues related to propagation completeness. Artif. Intell. 203, 19–34 (2013)
Bacchus, F.: GAC via unit propagation. In: Bessière, C. (ed.) CP 2007. LNCS, vol. 4741, pp. 133–147. Springer, Heidelberg (2007). doi:10.1007/978-3-540-74970-7_12
Bailleux, O., Boufkhad, Y.: Efficient CNF encoding of boolean cardinality constraints. In: Proceedings of 9th International Conference on Principles and Practice of Constraint Programming, CP 2003, Kinsale, Ireland, Berlin, Heidelberg, 29 September–3 October 2003, pp. 108–122 (2003). doi:10.1007/978-3-540-45193-8_8
Ben-Haim, Y., Ivrii, A., Margalit, O., Matsliah, A.: Perfect hashing and CNF encodings of cardinality constraints. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 397–409. Springer, Heidelberg (2012). doi:10.1007/978-3-642-31612-8_30
Biere, A., Heule, M., van Maaren, H., Walsh, T.: Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press, Amsterdam, The Netherlands (2009)
Bordeaux, L., Marques-Silva, J.: Knowledge compilation with empowerment. In: Bieliková, M., Friedrich, G., Gottlob, G., Katzenbeisser, S., Turán, G. (eds.) SOFSEM 2012. LNCS, vol. 7147, pp. 612–624. Springer, Heidelberg (2012). doi:10.1007/978-3-642-27660-6_50
Chen, J.: A new SAT encoding of the at-most-one constraint. In: ModRef 2010 (2010)
Crama, Y., Hammer, P.: Boolean Functions: Theory, Algorithms, and Applications. Encyclopedia of Mathematics and Its Applications. Cambridge University Press, Cambridge (2011)
Frisch, A.M., Giannaros, P.A.: SAT encodings of the at-most-k constraint. some old, some new, some fast, some slow. In: Proceeding of the Tenth International Workshop of Constraint Modelling and Reformulation (2010)
Frisch, A.M., Peugniez, T.J., Doggett, A.J., Nightingale, P.W.: Solving non-boolean satisfiability problems with stochastic local search: A comparison of encodings. J. Autom. Reason. 35(1), 143–179 (2005). doi:10.1007/s10817-005-9011-0
Hölldobler, S., Nguyen, V.H.: An efficient encoding of the at-most-one constraint. Technical Report MSU-CSE-00-2, Knowledge Representation and Reasoning Groupp. 2013–04, Technische Universitt Dresden, 01062 Dresden, Germany (2013). http://www.wv.inf.tu-dresden.de/Publications/2013/report-13-04.pdf
Klieber, W., Kwon, G.: Efficient CNF encoding for selecting 1 from n objects. In: Fourth Workshop on Constraints in Formal Verification (2007)
Kučera, P., Savický, P., Vorel, V.: A lower bound on CNF encodings of the at-most-one constraint (2017). https://arxiv.org/abs/1704.08934, arXiv:1704.08934 [cs.CC]
Marques-Silva, J., Lynce, I.: Towards robust CNF encodings of cardinality constraints. In: Bessière, C. (ed.) CP 2007. LNCS, vol. 4741, pp. 483–497. Springer, Heidelberg (2007). doi:10.1007/978-3-540-74970-7_35
Sinz, C.: Towards an optimal CNF encoding of boolean cardinality constraints. In: Proceedings of 11th International Conference on Principles and Practice of Constraint Programming, CP 2005, Sitges, Spain, 1–5 October 2005, pp. 827–831. Berlin, Heidelberg (2005). doi:10.1007/11564751_73
del Val, A.: Tractable databases: how to make propositional unit resolution complete through compilation. In: Knowledge Representation and Reasoning, pp. 551–561 (1994)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Kučera, P., Savický, P., Vorel, V. (2017). A Lower Bound on CNF Encodings of the At-Most-One Constraint. In: Gaspers, S., Walsh, T. (eds) Theory and Applications of Satisfiability Testing – SAT 2017. SAT 2017. Lecture Notes in Computer Science(), vol 10491. Springer, Cham. https://doi.org/10.1007/978-3-319-66263-3_26
Download citation
DOI: https://doi.org/10.1007/978-3-319-66263-3_26
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-66262-6
Online ISBN: 978-3-319-66263-3
eBook Packages: Computer ScienceComputer Science (R0)