{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,20]],"date-time":"2025-11-20T12:37:44Z","timestamp":1763642264443,"version":"3.40.3"},"publisher-location":"Cham","reference-count":18,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319662626"},{"type":"electronic","value":"9783319662633"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-66263-3_26","type":"book-chapter","created":{"date-parts":[[2017,8,8]],"date-time":"2017-08-08T04:05:11Z","timestamp":1502165111000},"page":"412-428","source":"Crossref","is-referenced-by-count":3,"title":["A Lower Bound on CNF Encodings of the At-Most-One Constraint"],"prefix":"10.1007","author":[{"given":"Petr","family":"Ku\u010dera","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Petr","family":"Savick\u00fd","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vojt\u011bch","family":"Vorel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,8,9]]},"reference":[{"issue":"2","key":"26_CR1","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/s10601-010-9105-0","volume":"16","author":"R As\u00edn","year":"2011","unstructured":"As\u00edn, R., Nieuwenhuis, R., Oliveras, A., Rodr\u00edguez-Carbonell, E.: Cardinality networks: a theoretical and empirical study. Constraints 16(2), 195\u2013221 (2011). doi:\n10.1007\/s10601-010-9105-0","journal-title":"Constraints"},{"issue":"3","key":"26_CR2","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1016\/0020-0190(79)90002-4","volume":"8","author":"B Aspvall","year":"1979","unstructured":"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\u2013123 (1979)","journal-title":"Inf. Process. Lett."},{"key":"26_CR3","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1016\/j.artint.2013.07.006","volume":"203","author":"M Babka","year":"2013","unstructured":"Babka, M., Balyo, T., \u010cepek, O., Gursk\u00fd, \u0160., Ku\u010dera, P., Vl\u010dek, V.: Complexity issues related to propagation completeness. Artif. Intell. 203, 19\u201334 (2013)","journal-title":"Artif. Intell."},{"key":"26_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/978-3-540-74970-7_12","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2007","author":"F Bacchus","year":"2007","unstructured":"Bacchus, F.: GAC via unit propagation. In: Bessi\u00e8re, C. (ed.) CP 2007. LNCS, vol. 4741, pp. 133\u2013147. Springer, Heidelberg (2007). doi:\n10.1007\/978-3-540-74970-7_12"},{"doi-asserted-by":"publisher","unstructured":"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\u20133 October 2003, pp. 108\u2013122 (2003). doi:\n10.1007\/978-3-540-45193-8_8","key":"26_CR5","DOI":"10.1007\/978-3-540-45193-8_8"},{"key":"26_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1007\/978-3-642-31612-8_30","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"Y Ben-Haim","year":"2012","unstructured":"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\u2013409. Springer, Heidelberg (2012). doi:\n10.1007\/978-3-642-31612-8_30"},{"key":"26_CR7","volume-title":"Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications","author":"A Biere","year":"2009","unstructured":"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)"},{"key":"26_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"612","DOI":"10.1007\/978-3-642-27660-6_50","volume-title":"SOFSEM 2012: Theory and Practice of Computer Science","author":"L Bordeaux","year":"2012","unstructured":"Bordeaux, L., Marques-Silva, J.: Knowledge compilation with empowerment. In: Bielikov\u00e1, M., Friedrich, G., Gottlob, G., Katzenbeisser, S., Tur\u00e1n, G. (eds.) SOFSEM 2012. LNCS, vol. 7147, pp. 612\u2013624. Springer, Heidelberg (2012). doi:\n10.1007\/978-3-642-27660-6_50"},{"unstructured":"Chen, J.: A new SAT encoding of the at-most-one constraint. In: ModRef 2010 (2010)","key":"26_CR9"},{"key":"26_CR10","series-title":"Encyclopedia of Mathematics and Its Applications","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511852008","volume-title":"Boolean Functions: Theory, Algorithms, and Applications","author":"Y Crama","year":"2011","unstructured":"Crama, Y., Hammer, P.: Boolean Functions: Theory, Algorithms, and Applications. Encyclopedia of Mathematics and Its Applications. Cambridge University Press, Cambridge (2011)"},{"unstructured":"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)","key":"26_CR11"},{"issue":"1","key":"26_CR12","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/s10817-005-9011-0","volume":"35","author":"AM Frisch","year":"2005","unstructured":"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\u2013179 (2005). doi:\n10.1007\/s10817-005-9011-0","journal-title":"J. Autom. Reason."},{"unstructured":"H\u00f6lldobler, 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\u201304, Technische Universitt Dresden, 01062 Dresden, Germany (2013). \nhttp:\/\/www.wv.inf.tu-dresden.de\/Publications\/2013\/report-13-04.pdf","key":"26_CR13"},{"unstructured":"Klieber, W., Kwon, G.: Efficient CNF encoding for selecting 1 from n objects. In: Fourth Workshop on Constraints in Formal Verification (2007)","key":"26_CR14"},{"unstructured":"Ku\u010dera, P., Savick\u00fd, P., Vorel, V.: A lower bound on CNF encodings of the at-most-one constraint (2017). \nhttps:\/\/arxiv.org\/abs\/1704.08934\n\n, \narXiv:1704.08934\n\n [cs.CC]","key":"26_CR15"},{"key":"26_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"483","DOI":"10.1007\/978-3-540-74970-7_35","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2007","author":"J Marques-Silva","year":"2007","unstructured":"Marques-Silva, J., Lynce, I.: Towards robust CNF encodings of cardinality constraints. In: Bessi\u00e8re, C. (ed.) CP 2007. LNCS, vol. 4741, pp. 483\u2013497. Springer, Heidelberg (2007). doi:\n10.1007\/978-3-540-74970-7_35"},{"doi-asserted-by":"publisher","unstructured":"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\u20135 October 2005, pp. 827\u2013831. Berlin, Heidelberg (2005). doi:\n10.1007\/11564751_73","key":"26_CR17","DOI":"10.1007\/11564751_73"},{"doi-asserted-by":"crossref","unstructured":"del Val, A.: Tractable databases: how to make propositional unit resolution complete through compilation. In: Knowledge Representation and Reasoning, pp. 551\u2013561 (1994)","key":"26_CR18","DOI":"10.1016\/B978-1-4832-1452-8.50146-9"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2017"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-66263-3_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,8,8]],"date-time":"2017-08-08T14:51:14Z","timestamp":1502203874000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-66263-3_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319662626","9783319662633"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66263-3_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}