{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,2]],"date-time":"2026-03-02T22:34:22Z","timestamp":1772490862103,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540749691","type":"print"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-74970-7_35","type":"book-chapter","created":{"date-parts":[[2007,10,9]],"date-time":"2007-10-09T23:49:08Z","timestamp":1191973748000},"page":"483-497","source":"Crossref","is-referenced-by-count":33,"title":["Towards Robust CNF Encodings of Cardinality Constraints"],"prefix":"10.1007","author":[{"given":"Joao","family":"Marques-Silva","sequence":"first","affiliation":[]},{"given":"In\u00eas","family":"Lynce","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"35_CR1","doi-asserted-by":"crossref","unstructured":"Ans\u00f3tegui, C., Many\u00e1, 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\u201315 (2004)","DOI":"10.1007\/11527695_1"},{"key":"35_CR2","doi-asserted-by":"crossref","unstructured":"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\u2013122 (2003)","DOI":"10.1007\/978-3-540-45193-8_8"},{"key":"35_CR3","unstructured":"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)"},{"key":"35_CR4","doi-asserted-by":"crossref","unstructured":"Bailleux, O., Boufkhad, Y., Roussel, O.: A translation of pseudo Boolean constraints to SAT. Journal on Satisfiability, Boolean Modeling and Computation\u00a0(2 March 2006)","DOI":"10.3233\/SAT190021"},{"key":"35_CR5","unstructured":"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\u2013208 (July 1997)"},{"key":"35_CR6","doi-asserted-by":"crossref","unstructured":"B\u00e9jar, R., H\u00e4hnle, R., Many\u00e0, F.: A modular reduction of regular logic to classical logic. In: Proceedings of the International Symposium on Multiple-Valued Logics, pp. 221\u2013226 (2001)","DOI":"10.1109\/ISMVL.2001.924576"},{"key":"35_CR7","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Communications of the Association for Computing Machinery\u00a05, 394\u2013397 (1962)","journal-title":"Communications of the Association for Computing Machinery"},{"key":"35_CR8","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. Journal of the Association for Computing Machinery\u00a07, 201\u2013215 (1960)","journal-title":"Journal of the Association for Computing Machinery"},{"key":"35_CR9","doi-asserted-by":"crossref","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT solver. In: Proceedings of the International Conference on Theory and Applications of Satisfiability Testing, pp. 502\u2013518 (May 2003)","DOI":"10.1007\/978-3-540-24605-3_37"},{"key":"35_CR10","doi-asserted-by":"crossref","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: Translating pseudo-Boolean constraints into SAT. Journal on Satisfiability, Boolean Modeling and Computation\u00a02 (March 2006)","DOI":"10.3233\/SAT190014"},{"key":"35_CR11","unstructured":"Gent, I.P.: Arc consistency in SAT. In: Proceedings of the European Conference on Artificial Intelligence, pp. 121\u2013125 (2002)"},{"key":"35_CR12","unstructured":"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\u2013110 (September 2004)"},{"key":"35_CR13","unstructured":"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\u2013145 (2002)"},{"key":"35_CR14","doi-asserted-by":"crossref","unstructured":"Goldberg, E., Novikov, Y.: BerkMin: a fast and robust SAT-solver. In: Proceedings of the Design Automation and Test in Europe Conference, pp. 142\u2013149 (March 2002)","DOI":"10.1109\/DATE.2002.998262"},{"key":"35_CR15","unstructured":"Gomes, C.P., Selman, B., Kautz, H.: Boosting combinatorial search through randomization. In: Proceedings of the National Conference on Artificial Intelligence, pp. 431\u2013437 (July 1998)"},{"issue":"3","key":"35_CR16","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1016\/0004-3702(90)90009-O","volume":"45","author":"S. Kasif","year":"1990","unstructured":"Kasif, S.: On the parallel complexity of discrete relaxation in constraint satisfaction networks. Artificial Intelligence\u00a045(3), 275\u2013286 (1990)","journal-title":"Artificial Intelligence"},{"key":"35_CR17","doi-asserted-by":"crossref","unstructured":"Marques-Silva, J., Sakallah, K.: GRASP: A new search algorithm for satisfiability. In: Proceedings of the International Conference on Computer-Aided Design, pp. 220\u2013227 (November 1996)","DOI":"10.1109\/ICCAD.1996.569607"},{"key":"35_CR18","doi-asserted-by":"crossref","unstructured":"Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Engineering an efficient SAT solver. In: Design Automation Conference, pp. 530\u2013535 (June 2001)","DOI":"10.1145\/378239.379017"},{"key":"35_CR19","unstructured":"Nadel, A.: Backtrack search algorithms for propositional logic satisfiability: Review and innovations. Master\u2019s thesis, Hebrew University of Jerusalem (November 2002)"},{"key":"35_CR20","unstructured":"Ryan, L.: Efficient algorithms for clause-learning SAT solvers. Master\u2019s thesis, Simon Fraser University (February 2004)"},{"key":"35_CR21","doi-asserted-by":"crossref","unstructured":"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\u2013831 (October 2005)","DOI":"10.1007\/11564751_73"},{"key":"35_CR22","doi-asserted-by":"crossref","unstructured":"Walsh, T.: SAT v CSP. In: Proceedings of the International Conference on Principles and Practice of Constraint Programming, pp. 441\u2013456 (September 2000)","DOI":"10.1007\/3-540-45349-0_32"},{"issue":"2","key":"35_CR23","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1016\/S0020-0190(98)00144-6","volume":"68","author":"J.P. Warners","year":"1998","unstructured":"Warners, J.P.: A linear-time transformation of linear inequalities into conjunctive normal form. Information Processing Letters\u00a068(2), 63\u201369 (1998)","journal-title":"Information Processing Letters"},{"key":"35_CR24","doi-asserted-by":"crossref","unstructured":"Zhang, H.: SATO: An efficient propositional prover. In: Proceedings of the International Conference on Automated Deduction, pp. 272\u2013275 (July 1997)","DOI":"10.1007\/3-540-63104-6_28"},{"key":"35_CR25","unstructured":"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\u2013285 (2001)"}],"container-title":["Lecture Notes in Computer Science","Principles and Practice of Constraint Programming \u2013 CP 2007"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-74970-7_35.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,21]],"date-time":"2025-01-21T14:28:42Z","timestamp":1737469722000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-74970-7_35"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540749691"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-74970-7_35","relation":{},"subject":[]}}