{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,24]],"date-time":"2025-08-24T01:17:49Z","timestamp":1755998269828,"version":"3.40.3"},"publisher-location":"Cham","reference-count":48,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031656262"},{"type":"electronic","value":"9783031656279"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,7,26]],"date-time":"2024-07-26T00:00:00Z","timestamp":1721952000000},"content-version":"vor","delay-in-days":207,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Satisfiability (SAT) solvers have been using the same input format for decades: a formula in conjunctive normal form. Cardinality constraints appear frequently in problem descriptions: over <jats:inline-formula><jats:alternatives><jats:tex-math>$$64\\%$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mrow>\n                    <mml:mn>64<\/mml:mn>\n                    <mml:mo>%<\/mml:mo>\n                  <\/mml:mrow>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula> of the SAT Competition formulas contain at least one cardinality constraint, while over <jats:inline-formula><jats:alternatives><jats:tex-math>$$17\\%$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mrow>\n                    <mml:mn>17<\/mml:mn>\n                    <mml:mo>%<\/mml:mo>\n                  <\/mml:mrow>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula> contain many large cardinality constraints. Allowing general cardinality constraints as input would simplify encodings and enable the solver to handle constraints natively or to encode them using different (and possibly dynamically changing) clausal forms. We modify the modern SAT solver <jats:sc>CaDiCaL<\/jats:sc> to handle cardinality constraints natively. Unlike the stronger cardinality reasoning in pseudo-Boolean (PB) or other systems, our incremental approach with cardinality-based propagation requires only moderate changes to a SAT solver, preserves the ability to run important inprocessing techniques, and is easily combined with existing proof-producing and validation tools. Our experimental evaluation on SAT Competition formulas shows our solver configurations with cardinality support consistently outperform other SAT and PB solvers.<\/jats:p>","DOI":"10.1007\/978-3-031-65627-9_6","type":"book-chapter","created":{"date-parts":[[2024,7,25]],"date-time":"2024-07-25T19:01:31Z","timestamp":1721934091000},"page":"110-132","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["From Clauses to Klauses"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4585-0565","authenticated-orcid":false,"given":"Joseph E.","family":"Reeves","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5587-8801","authenticated-orcid":false,"given":"Marijn J. H.","family":"Heule","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5024-6613","authenticated-orcid":false,"given":"Randal E.","family":"Bryant","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,7,26]]},"reference":[{"key":"6_CR1","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1613\/jair.3653","volume":"45","author":"I Ab\u00edo","year":"2012","unstructured":"Ab\u00edo, I., Nieuwenhuis, R., Oliveras, A., Rodr\u00edguez-Carbonell, E.: A new look at BDDs for pseudo-Boolean constraints. Journal of Artificial Intelligence Research 45, 443\u2013480 (2012)","journal-title":"Journal of Artificial Intelligence Research"},{"key":"6_CR2","doi-asserted-by":"crossref","unstructured":"Ab\u00edo, I., Stuckey, P.J.: Conflict directed lazy decomposition. In: Principles and Practice of Constraint Programming (CP) (2012)","DOI":"10.1007\/978-3-642-33558-7_8"},{"key":"6_CR3","doi-asserted-by":"crossref","unstructured":"Bailleux, O., Boufkhad, Y.: Efficient CNF encoding of boolean cardinality constraints. In: Principles and Practice of Constraint Programming (CP). pp. 108\u2013122. Springer (2003)","DOI":"10.1007\/978-3-540-45193-8_8"},{"key":"6_CR4","doi-asserted-by":"crossref","unstructured":"Becker, B., Drechsler, R., Eggersgl\u00fc\u00df, S., Sauer, M.: Recent advances in SAT-based ATPG: Non-standard fault models, multi constraints and optimization. In: Design and Technology of Integrated Systems in Nanoscale Era (DTIS). pp. 1\u201310 (2014)","DOI":"10.1109\/DTIS.2014.6850674"},{"key":"6_CR5","doi-asserted-by":"crossref","unstructured":"Berre, D.L., Parrain, A.: The sat4j library, release 2.2. Journal on Satisfiability, Boolean Modeling and Computation 7, 59\u20136 (2010)","DOI":"10.3233\/SAT190075"},{"key":"6_CR6","unstructured":"Biere, A.: CaDiCaL, Lingeling, Plingeling, Treengeling, and YalSAT entering the SAT competition 2017 (2017)"},{"key":"6_CR7","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without bdds. In: Tools and Algorithms for Construction and Analysis of Systems (TACAS) (1999)","DOI":"10.21236\/ADA360973"},{"key":"6_CR8","unstructured":"Biere, A., Fazekas, K., Fleury, M., Heisinger, M.: CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling entering the SAT competition 2020 (2020)"},{"key":"6_CR9","doi-asserted-by":"crossref","unstructured":"Biere, A., Fr\u00f6hlich, A.: Evaluating CDCL variable scoring schemes. In: Theory and Applications of Satisfiability Testing (SAT). LNCS, vol.\u00a09340, pp. 405\u2013422 (2015)","DOI":"10.1007\/978-3-319-24318-4_29"},{"key":"6_CR10","doi-asserted-by":"crossref","unstructured":"Biere, A., Le\u00a0Berre, D., Lonca, E., Manthey, N.: Detecting cardinality constraints in CNF. In: Theory and Applications of Satisfiability Testing (SAT). LNCS, vol.\u00a08561, pp. 285\u2013301. Springer (2014)","DOI":"10.1007\/978-3-319-09284-3_22"},{"key":"6_CR11","doi-asserted-by":"crossref","unstructured":"Brown, S.T., Buitrago, P., Hanna, E., Sanielevici, S., Scibek, R., Nystrom, N.A.: Bridges-2: A Platform for Rapidly-Evolving and Data Intensive Research, pp.\u00a01\u20134. Association for Computing Machinery, New York, NY, USA (2021)","DOI":"10.1145\/3437359.3465593"},{"issue":"8","key":"6_CR12","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"RE Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Trans. Computers 35(8), 677\u2013691 (1986)","journal-title":"IEEE Trans. Computers"},{"key":"6_CR13","doi-asserted-by":"crossref","unstructured":"Bryant, R.E., Biere, A., Heule, M.J.H.: Clausal proofs for pseudo-Boolean reasoning. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 12651, pp. 76\u201393 (2022)","DOI":"10.1007\/978-3-030-99524-9_25"},{"key":"6_CR14","doi-asserted-by":"crossref","unstructured":"Bryant, R.E., Biere, A., Heule, M.J.H.: Clausal proofs for pseudo-boolean reasoning. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS). p. 443\u2013461. Springer (2022)","DOI":"10.1007\/978-3-030-99524-9_25"},{"key":"6_CR15","unstructured":"Codel, C.: Verifying SAT Encodings in Lean. Master\u2019s thesis, Carnegie Mellon University Pittsburgh, PA (2022)"},{"key":"6_CR16","doi-asserted-by":"crossref","unstructured":"Cook, W., Coullard, C.R., Tur\u00e1n, G.: On the complexity of cutting-plane proofs. Discrete Applied Mathematics 18(1), 25\u201338 (1987)","DOI":"10.1016\/0166-218X(87)90039-4"},{"key":"6_CR17","doi-asserted-by":"crossref","unstructured":"Dechter, R.: Bucket elimination: A unifying framework for reasoning. Artificial Intelligence 113(1\u20132), 41\u201385 (1999)","DOI":"10.1016\/S0004-3702(99)00059-4"},{"key":"6_CR18","doi-asserted-by":"crossref","unstructured":"E\u00e9n, N., Biere, A.: Effective preprocessing in SAT through variable and clause elimination. In: Theory and Applications of Satisfiability Testing (SAT). LNCS, vol.\u00a03569, pp. 61\u201375. Springer (2005)","DOI":"10.1007\/11499107_5"},{"issue":"4","key":"6_CR19","doi-asserted-by":"publisher","first-page":"543","DOI":"10.1016\/S1571-0661(05)82542-3","volume":"89","author":"N E\u00e9n","year":"2003","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: Temporal induction by incremental SAT solving. Electron. Notes Theor. Comput. Sci. 89(4), 543\u2013560 (2003)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"6_CR20","doi-asserted-by":"crossref","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: Translating pseudo-Boolean constraints into SAT. Journal on Satisfiability, Boolean Modeling and Computation, 2(1-4), 1\u201326 (2006)","DOI":"10.3233\/SAT190014"},{"key":"6_CR21","doi-asserted-by":"crossref","unstructured":"Elffers, J., Nordstr\u00f6m, J.: Divide and conquer: Towards faster pseudo-Boolean solving. In: Lang, J. (ed.) International Joint Conference on Artificial Intelligence (IJCAI). pp. 1291\u20131299. ijcai.org (2018)","DOI":"10.24963\/ijcai.2018\/180"},{"key":"6_CR22","doi-asserted-by":"crossref","unstructured":"Elffers, J., Nordstr\u00f6m, J.: A cardinal improvement to pseudo-Boolean solving. In: Conference on Artificial Intelligence (AAAI). pp. 1495\u20131503. AAAI Press (2020)","DOI":"10.1609\/aaai.v34i02.5508"},{"key":"6_CR23","unstructured":"Freeman, J.W.: Improvements to Propositional Satisfiability Search Algorithms. Ph.D. thesis, University of Pennsylvania, USA (1995)"},{"key":"6_CR24","unstructured":"Gent, I.P.: Arc consistency in sat. In: European Conference on Artificial Intelligence (2002)"},{"key":"6_CR25","unstructured":"Gocht, S., Martins, R., Nordstr\u00f6m, J., Oertel, A.: Certified CNF translations for pseudo-Boolean solving. In: Meel, K.S., Strichman, O. (eds.) Theory and Applications of Satisfiability Testing (SAT). LIPIcs, vol.\u00a0236, pp. 16:1\u201316:25. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2022)"},{"key":"6_CR26","doi-asserted-by":"crossref","unstructured":"Hooker, J.: Generalized resolution and cutting planes. Annals of Operations Research 12, 217\u2013239 (1988)","DOI":"10.1007\/BF02186368"},{"key":"6_CR27","doi-asserted-by":"crossref","unstructured":"Ignatiev, A., Morgado, A., Marques-Silva, J.: PySAT: A Python toolkit for prototyping with SAT oracles. In: Theory and Applications of Satisfiability Testing (SAT). pp. 428\u2013437 (2018)","DOI":"10.1007\/978-3-319-94144-8_26"},{"key":"6_CR28","unstructured":"Jabbour, S., Sais, L., Salhi, Y.: A pigeon-hole based encoding of cardinality constraints. Theory and Practice of Logic Programming 13 (2013)"},{"key":"6_CR29","doi-asserted-by":"crossref","unstructured":"J\u00e4rvisalo, M., Heule, M.J.H., Biere, A.: Inprocessing rules. In: International Joint Conference on Automated Reasoning (IJCAR). LNCS, vol.\u00a07364, pp. 355\u2013370. Springer (2012)","DOI":"10.1007\/978-3-642-31365-3_28"},{"key":"6_CR30","unstructured":"Klieber, W., Kwon, G.: Efficient CNF encoding for selecting 1 from $$n$$ objects. In: Constraints in Formal Verification (CFV). p.\u00a039 (2007)"},{"key":"6_CR31","doi-asserted-by":"crossref","unstructured":"Li, C.M., Xiao, F., Luo, M., Many\u00e0, F., L\u00fc, Z., Li, Y.: Clause vivification by unit propagation in CDCL SAT solvers. Artificial Intelligence 279(C) (2020)","DOI":"10.1016\/j.artint.2019.103197"},{"key":"6_CR32","doi-asserted-by":"crossref","unstructured":"Liang, J., Ganesh, V., Poupart, P., Czarnecki, K.: Learning rate based branching heuristic for SAT solvers. In: Theory and Applications of Satisfiability Testing (SAT). LNCS, vol.\u00a09710, pp. 123\u2013140 (2016)","DOI":"10.1007\/978-3-319-40970-2_9"},{"key":"6_CR33","doi-asserted-by":"crossref","unstructured":"Lotz, K., Goel, A., Dutertre, B., Kiesl-Reiter, B., Kong, S., Majumdar, R., Nowotka, D.: Solving string constraints using sat. In: Enea, C., Lal, A. (eds.) Computer Aided Verification (CAV). pp. 187\u2013208. Springer, Cham (2023)","DOI":"10.1007\/978-3-031-37703-7_9"},{"key":"6_CR34","unstructured":"Maglalang, J.C.: Native cardinality constraints: More expressive, more efficient constraints (2019)"},{"key":"6_CR35","doi-asserted-by":"crossref","unstructured":"Manthey, N., Heule, M.J.H., Biere, A.: Automated reencoding of Boolean formulas. In: Haifa Verification Conference (HVC). LNCS, vol.\u00a07857, pp. 102\u2013117 (2013)","DOI":"10.1007\/978-3-642-39611-3_14"},{"key":"6_CR36","unstructured":"Marques-Silva, J., Lynce, I., Malik, S.: Conflict-driven clause learning SAT solvers. In: Handbook of Satisfiability, pp. 131\u2013153. IOS Press (2009)"},{"key":"6_CR37","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Proceedings of the 38th Annual Design Automation Conference, p. 530\u2013535. ACM (2001)","DOI":"10.1145\/378239.379017"},{"key":"6_CR38","doi-asserted-by":"crossref","unstructured":"Nguyen, V.H., Nguyen, V.Q., Kim, K., Barahona, P.: Empirical study on SAT-encodings of the at-most-one constraint. In: Conference on Smart Media and Applications. p. 470\u2013475. Smart Media and Applications (SMA), ACM, New York, NY, USA (2021)","DOI":"10.1145\/3426020.3426170"},{"key":"6_CR39","doi-asserted-by":"crossref","unstructured":"Niemetz, A., Preiner, M.: Bitwuzla. In: Computer Aided Verification (CAV). p. 3\u201317. Springer (2023)","DOI":"10.1007\/978-3-031-37703-7_1"},{"key":"6_CR40","doi-asserted-by":"crossref","unstructured":"Oh, C.: Between SAT and UNSAT: The fundamental difference in CDCL SAT. In: Theory and Applications of Satisfiability Testing (SAT). pp. 307\u2013323. Springer International Publishing (2015)","DOI":"10.1007\/978-3-319-24318-4_23"},{"key":"6_CR41","doi-asserted-by":"crossref","unstructured":"Pan, G., Vardi, M.Y.: Search vs.\u00a0symbolic techniques in satisfiability solving. In: Theory and Applications of Satisfiability Testing (SAT). LNCS, vol.\u00a03542, pp. 235\u2013250 (2005)","DOI":"10.1007\/11527695_19"},{"key":"6_CR42","doi-asserted-by":"crossref","unstructured":"Sinz, C.: Towards an optimal CNF encoding of Boolean cardinality constraints. In: Principles and Practice of Constraint Programming (CP). LNCS, vol.\u00a03709, pp. 827\u2013831 (2005)","DOI":"10.1007\/11564751_73"},{"key":"6_CR43","doi-asserted-by":"crossref","unstructured":"Soh, T., Le\u00a0Berre, D., Roussel, S., Banbara, M., Tamura, N.: Incremental SAT-based method with native boolean cardinality handling for the hamiltonian cycle problem. In: European Conference on Logics in Artificial Intelligence. vol.\u00a08761, p. 684-693. Springer (2014)","DOI":"10.1007\/978-3-319-11558-0_52"},{"key":"6_CR44","unstructured":"Soos, M., Bryant, R.E.: Combining CDCL, Gauss-Jordan elimination, and proof generation. In: Pragmatics of SAT (2022)"},{"key":"6_CR45","unstructured":"Stephan\u00a0Gocht, Ciaran\u00a0McCreesh, J.N.: Veripb: The easy way to make your combinatorial search algorithm trustworthy. In: From Constraint Programming to Trustworthy AI (2020)"},{"key":"6_CR46","doi-asserted-by":"crossref","unstructured":"Tan, Y.K., Heule, M.J.H., Myreen, M.O.: cake_lpr: Verified propagation redundancy checking in CakeML. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Part II. LNCS, vol. 12652, pp. 223\u2013241 (2021)","DOI":"10.1007\/978-3-030-72013-1_12"},{"key":"6_CR47","doi-asserted-by":"crossref","unstructured":"Whittemore, J., Kim, J., Sakallah, K.: Satire: A new incremental satisfiability engine. In: Design Automation Conference (DAC). p. 542\u2013545. DAC \u201901, ACM, New York, NY, USA (2001)","DOI":"10.1145\/378239.379019"},{"key":"6_CR48","unstructured":"Wynn, E.: A comparison of encodings for cardinality constraints in a SAT solver. ArXiv abs\/1810.12975 (2018)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-65627-9_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,25]],"date-time":"2024-07-25T19:02:08Z","timestamp":1721934128000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-65627-9_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031656262","9783031656279"],"references-count":48,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-65627-9_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"26 July 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Montreal, QC","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 July 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 July 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"36","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2024\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}