{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,23]],"date-time":"2026-10-23T11:59:44Z","timestamp":1792756784390,"version":"4.5.0"},"publisher-location":"Cham","reference-count":34,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319092836","type":"print"},{"value":"9783319092843","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-09284-3_22","type":"book-chapter","created":{"date-parts":[[2014,7,2]],"date-time":"2014-07-02T09:43:21Z","timestamp":1404294201000},"page":"285-301","source":"Crossref","is-referenced-by-count":22,"title":["Detecting Cardinality Constraints in CNF"],"prefix":"10.1007","author":[{"given":"Armin","family":"Biere","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Daniel","family":"Le Berre","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Emmanuel","family":"Lonca","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Norbert","family":"Manthey","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"22_CR1","doi-asserted-by":"crossref","unstructured":"Aloul, F.A., Ramani, A., Markov, I.L., Sakallah, K.A.: Generic ilp versus specialized 0-1 ilp: An update. In: Pileggi, L.T., Kuehlmann, A. (eds.) ICCAD, pp. 450\u2013457. ACM (2002)","DOI":"10.1145\/774572.774638"},{"issue":"1-4","key":"22_CR2","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/s10472-007-9062-5","volume":"49","author":"C. Ans\u00f3tegui","year":"2007","unstructured":"Ans\u00f3tegui, C., Larrubia, J., Li, C.M., Many\u00e0, F.: Exploiting multivalued knowledge in variable selection heuristics for sat solvers. Ann. Math. Artif. Intell.\u00a049(1-4), 191\u2013205 (2007)","journal-title":"Ann. Math. Artif. Intell."},{"key":"22_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/11527695_1","volume-title":"Theory and Applications of Satisfiability Testing","author":"C. Ans\u00f3tegui","year":"2005","unstructured":"Ans\u00f3tegui, C., Many\u00e0, F.: Mapping problems with finite-domain variables to problems with boolean variables. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol.\u00a03542, pp. 1\u201315. Springer, Heidelberg (2005)"},{"key":"22_CR4","unstructured":"Ans\u00f3tegui Gil, C.J.: Complete SAT solvers for Many-Valued CNF Formulas. Ph.D. thesis. University of Lleida (2004)"},{"key":"22_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-642-02777-2_18","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2009","author":"R. As\u00edn","year":"2009","unstructured":"As\u00edn, R., Nieuwenhuis, R., Oliveras, A., Rodr\u00edguez-Carbonell, E.: Cardinality networks and their applications. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol.\u00a05584, pp. 167\u2013180. Springer, Heidelberg (2009)"},{"key":"22_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/978-3-540-45193-8_8","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2003","author":"O. Bailleux","year":"2003","unstructured":"Bailleux, O., Boufkhad, Y.: Efficient cnf encoding of boolean cardinality constraints. In: Rossi, F. (ed.) CP 2003. LNCS, vol.\u00a02833, pp. 108\u2013122. Springer, Heidelberg (2003)"},{"key":"22_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/978-3-319-07046-9_18","volume-title":"Integration of AI and OR Techniques in Constraint Programming","author":"P. Barahona","year":"2014","unstructured":"Barahona, P., H\u00f6lldobler, S., Nguyen, V.-H.: Representative Encodings to Translate Finite CSPs into SAT. In: Simonis, H. (ed.) CPAIOR 2014. LNCS, vol.\u00a08451, pp. 251\u2013267. Springer, Heidelberg (2014)"},{"key":"22_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1007\/3-540-56944-8_40","volume-title":"Logic Programming and Automated Reasoning","author":"P. Barth","year":"1993","unstructured":"Barth, P.: Linear 0-1 inequalities and extended clauses. In: Voronkov, A. (ed.) LPAR 1993. LNCS, vol.\u00a0698, pp. 40\u201351. Springer, Heidelberg (1993)"},{"key":"22_CR9","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.\u00a07317, pp. 397\u2013409. Springer, Heidelberg (2012)"},{"key":"22_CR10","unstructured":"Biere, A.: Lingeling, plingeling and treengeling entering the sat competition 2013. In: Balint, A., Belov, A., Heule, M., J\u00e4rvisalo, M. (eds.) Proceedings of SAT Competition 2013. Solver and Benchmark Descriptions, vol.\u00a0B-2013-1, pp. 51\u201352. University of Helsinki, Department of Computer Science Series of Publications B (2013)"},{"key":"22_CR11","unstructured":"Chen, J.C.: A new sat encoding of the at-most-one constraint. In: Proc. of the Tenth Int. Workshop of Constraint Modelling and Reformulation (2010)"},{"issue":"1","key":"22_CR12","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1016\/0166-218X(87)90039-4","volume":"18","author":"W. Cook","year":"1987","unstructured":"Cook, W., Coullard, C., Tur\u00e1n, G.: On the complexity of cutting-plane proofs. Discrete Applied Mathematics\u00a018(1), 25\u201338 (1987)","journal-title":"Discrete Applied Mathematics"},{"issue":"1-4","key":"22_CR13","first-page":"1","volume":"2","author":"N. E\u00e9n","year":"2006","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: Translating pseudo-boolean constraints into sat. JSAT\u00a02(1-4), 1\u201326 (2006)","journal-title":"JSAT"},{"key":"22_CR14","unstructured":"Frisch, A., Giannaros, P.: Sat encodings of the at-most-k constraint: Some old, some new, some fast, some slow. In: Proceedings of the 9th International Workshop on Constraint Modelling and Reformulation, ModRef 2010 (2010)"},{"key":"22_CR15","doi-asserted-by":"crossref","unstructured":"Fu, Z., Malik, S.: Extracting logic circuit structure from conjunctive normal form descriptions. In: VLSI Design, pp. 37\u201342. IEEE Computer Society (2007)","DOI":"10.1109\/VLSID.2007.81"},{"key":"22_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"388","DOI":"10.1007\/978-3-642-14186-7_37","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2010","author":"A. Gelder Van","year":"2010","unstructured":"Van Gelder, A., Spence, I.: Zero-one designs produce small hard sat instances. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol.\u00a06175, pp. 388\u2013397. Springer, Heidelberg (2010)"},{"key":"22_CR17","unstructured":"Gent, I.P., Nightingale, P.: A new encoding of alldifferent into sat. In: Proc. 3rd International Workshop on Modelling and Reformulating Constraint Satisfaction Problems, pp. 95\u2013110 (2004)"},{"key":"22_CR18","unstructured":"Gent, I., Prosser, P., Smith, B.: A 0\/1 encoding of the gaclex constraint for pairs of vectors. In: ECAI 2002 workshop W9: Modelling and Solving Problems with Constraints. University of Glasgow (2002)"},{"issue":"0","key":"22_CR19","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1016\/0304-3975(85)90144-6","volume":"39","author":"A. Haken","year":"1985","unstructured":"Haken, A.: The intractability of resolution. Theoretical Computer Science\u00a039(0), 297\u2013308 (1985)","journal-title":"Theoretical Computer Science"},{"key":"22_CR20","unstructured":"H\u00f6lldobler, S., Nguyen, V.H.: On SAT-Encodings of the At-Most-One Constraint. In: Katsirelos, G., Quimper, C.G. (eds.) Proc. The Twelfth International Workshop on Constraint Modelling and Reformulation, Uppsala, Sweden, September 16-20, pp. 1\u201317 (2013)"},{"issue":"1-4","key":"22_CR21","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/BF02186368","volume":"12","author":"J.N. Hooker","year":"1988","unstructured":"Hooker, J.N.: Generalized resolution and cutting planes. Ann. Oper. Res.\u00a012(1-4), 217\u2013239 (1988)","journal-title":"Ann. Oper. Res."},{"key":"22_CR22","series-title":"The IBM Research Symposia Series","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/978-1-4684-2001-2_9","volume-title":"Complexity of Computer Computations","author":"R. Karp","year":"1972","unstructured":"Karp, R.: Reducibility among combinatorial problems. In: Miller, R., Thatcher, J., Bohlinger, J. (eds.) Complexity of Computer Computations. The IBM Research Symposia Series, pp. 85\u2013103. Springer, US (1972)"},{"key":"22_CR23","unstructured":"Klieber, W., Kwon, G.: Efficient cnf encoding for selecting 1 from n objects. In: International Workshop on Constraints in Formal Verification (2007)"},{"key":"22_CR24","unstructured":"van Lambalgen, M.: 3MCard 3MCard A Lookahead Cardinality Solver. Master\u2019s thesis. Delft University of Technology (2006)"},{"key":"22_CR25","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1016\/S1571-0653(04)00314-2","volume":"9","author":"D. Berre Le","year":"2001","unstructured":"Le Berre, D.: Exploiting the real power of unit propagation lookahead. Electronic Notes in Discrete Mathematics\u00a09, 59\u201380 (2001)","journal-title":"Electronic Notes in Discrete Mathematics"},{"key":"22_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/978-3-642-39611-3_14","volume-title":"Hardware and Software: Verification and Testing","author":"N. Manthey","year":"2013","unstructured":"Manthey, N., Heule, M.J.H., Biere, A.: Automated reencoding of boolean formulas. In: Biere, A., Nahir, A., Vos, T. (eds.) HVC. LNCS, vol.\u00a07857, pp. 102\u2013117. Springer, Heidelberg (2013)"},{"key":"22_CR27","unstructured":"Manthey, N., Steinke, P.: Quadratic direct encoding vs. linear order encoding, a one-out-of-n transformation on cnf. In: Proceedings of the First International Workshop on the Cross-Fertilization Between CSP and SAT, CSPSAT11 (2011)"},{"issue":"2","key":"22_CR28","doi-asserted-by":"crossref","first-page":"75","DOI":"10.3233\/AIC-2012-0517","volume":"25","author":"R. Martins","year":"2012","unstructured":"Martins, R., Manquinho, V.M., Lynce, I.: Parallel search for maximum satisfiability. AI Commun.\u00a025(2), 75\u201395 (2012)","journal-title":"AI Commun."},{"key":"22_CR29","series-title":"LNCS","first-page":"122","volume-title":"SAT 2014","author":"M. Mik\u0161a","year":"2014","unstructured":"Mik\u0161a, M., Nordstr\u00f6m, J.: Long proofs of (Seemingly) simple formulas. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol.\u00a08561, pp. 122\u2013138. Springer, Heidelberg (2014)"},{"key":"22_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1007\/3-540-46135-3_13","volume-title":"Principles and Practice of Constraint Programming - CP 2002","author":"R. Ostrowski","year":"2002","unstructured":"Ostrowski, R., Gr\u00e9goire, \u00c9., Mazure, B., Sais, L.: Recovering and exploiting structural knowledge from cnf formulas. In: Van Hentenryck, P. (ed.) CP 2002. LNCS, vol.\u00a02470, pp. 185\u2013199. Springer, Heidelberg (2002)"},{"key":"22_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"827","DOI":"10.1007\/11564751_73","volume-title":"Principles and Practice of Constraint Programming - CP 2005","author":"C. Sinz","year":"2005","unstructured":"Sinz, C.: Towards an optimal cnf encoding of boolean cardinality constraints. In: van Beek, P. (ed.) CP 2005. LNCS, vol.\u00a03709, pp. 827\u2013831. Springer, Heidelberg (2005)"},{"key":"22_CR32","doi-asserted-by":"crossref","unstructured":"Spence, I.: sgen1: A generator of small but difficult satisfiability benchmarks. ACM Journal of Experimental Algorithmics\u00a015 (2010)","DOI":"10.1145\/1671970.1671972"},{"key":"22_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1007\/3-540-45349-0_32","volume-title":"Principles and Practice of Constraint Programming - CP 2000","author":"T. Walsh","year":"2000","unstructured":"Walsh, T.: Sat v csp. In: Dechter, R. (ed.) CP 2000. LNCS, vol.\u00a01894, pp. 441\u2013456. Springer, Heidelberg (2000)"},{"key":"22_CR34","unstructured":"Weaver, S.: Satisfiability Advancements Enabled by State Machines. Ph.D. thesis. University of Cincinnati (2012)"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2014"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-09284-3_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,8,21]],"date-time":"2020-08-21T22:01:43Z","timestamp":1598047303000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-09284-3_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319092836","9783319092843"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-09284-3_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]}}}