{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,13]],"date-time":"2026-01-13T05:05:49Z","timestamp":1768280749481,"version":"3.49.0"},"publisher-location":"Cham","reference-count":52,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030995232","type":"print"},{"value":"9783030995249","type":"electronic"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,3,30]],"date-time":"2022-03-30T00:00:00Z","timestamp":1648598400000},"content-version":"vor","delay-in-days":88,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>When augmented with a Pseudo-Boolean (PB) solver, a Boolean satisfiability (SAT) solver can apply apply powerful reasoning methods to determine when a set of parity or cardinality constraints, extracted from the clauses of the input formula, has no solution. By converting the intermediate constraints generated by the PB solver into ordered binary decision diagrams (BDDs), a proof-generating, BDD-based SAT solver can then produce a clausal proof that the input formula is unsatisfiable. Working together, the two solvers can generate proofs of unsatisfiability for problems that are intractable for other proof-generating SAT solvers. The PB solver can, at times, detect that the proof can exploit modular arithmetic to give smaller BDD representations and therefore shorter proofs.<\/jats:p>","DOI":"10.1007\/978-3-030-99524-9_25","type":"book-chapter","created":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T06:14:55Z","timestamp":1648534495000},"page":"443-461","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Clausal Proofs for Pseudo-Boolean Reasoning"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5024-6613","authenticated-orcid":false,"given":"Randal E.","family":"Bryant","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7170-9242","authenticated-orcid":false,"given":"Armin","family":"Biere","sequence":"additional","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"}]}],"member":"297","published-online":{"date-parts":[[2022,3,30]]},"reference":[{"key":"25_CR1","doi-asserted-by":"crossref","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)","DOI":"10.1613\/jair.3653"},{"key":"25_CR2","doi-asserted-by":"crossref","unstructured":"Alekhnovich, M.: Mutilated chessboard problem is exponentially hard for resolution. Theoretical Computer Science 310(1-3), 513\u2013525 (Jan 2004)","DOI":"10.1016\/S0304-3975(03)00395-5"},{"key":"25_CR3","doi-asserted-by":"crossref","unstructured":"Audemard, G., Katsirelos, G., Simon, L.: A restriction of extended resolution for clause learning SAT solvers. In: AAAI Conference on Artificial Intelligence. pp. 15\u201320 (2010)","DOI":"10.1609\/aaai.v24i1.7553"},{"key":"25_CR4","doi-asserted-by":"crossref","unstructured":"Bareiss, E.H.: Sylvester\u2019s identity and multistep integer-preserving Gaussian elimination. Mathematics of Computation 22, 565\u2013578 (1968)","DOI":"10.1090\/S0025-5718-1968-0226829-0"},{"key":"25_CR5","doi-asserted-by":"crossref","unstructured":"Barnett, L.A., Biere, A.: Non-clausal redundancy properties. In: Conference on Automated Deduction (CADE). LNAI, vol. 12699, pp. 252\u2013272 (2021)","DOI":"10.1007\/978-3-030-79876-5_15"},{"key":"25_CR6","unstructured":"Biere, A.: Splatz, Lingeling, Plingeling, Treengeling, YalSAT Entering the SAT Competition 2016. In: Proc. of SAT Competition 2016 \u2013 Solver and Benchmark Descriptions. Dep. of Computer Science Series of Publications B, vol. B-2016-1, pp. 44\u201345. University of Helsinki (2016)"},{"key":"25_CR7","unstructured":"Biere, A., Fazekas, K., Fleury, M., Heisinger, M.: CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling entering the SAT Competition 2020. In: Proc.\u00a0of SAT Competition 2020 \u2013 Solver and Benchmark Descriptions. Department of Computer Science Report Series B, vol. B-2020-1, pp. 51\u201353. University of Helsinki (2020)"},{"key":"25_CR8","doi-asserted-by":"crossref","unstructured":"Biere, A., J\u00e4rvisalo, M., Kiesl, B.: Preprocessing SAT solving. In: Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol.\u00a0336, pp. 391\u2013435. IOS Press, second edn. (2021)","DOI":"10.3233\/FAIA200992"},{"key":"25_CR9","doi-asserted-by":"crossref","unstructured":"Biere, A., Le Berre, D., Lonca, E., Manthey, N.: Detecting cardinality constraints in CNF. In: Theory and Applications of Satisfiability Testing (SAT). LNCS, vol.\u00a08561, pp. 285\u2013301 (2014)","DOI":"10.1007\/978-3-319-09284-3_22"},{"key":"25_CR10","doi-asserted-by":"crossref","unstructured":"Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Trans. Computers 35(8), 677\u2013691 (1986)","DOI":"10.1109\/TC.1986.1676819"},{"key":"25_CR11","doi-asserted-by":"crossref","unstructured":"Bryant, R.E., Heule, M.J.H.: Generating extended resolution proofs with a BDD-based SAT solver. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Part I. LNCS, vol. 12651, pp. 76\u201393 (2021)","DOI":"10.1007\/978-3-030-72016-2_5"},{"key":"25_CR12","doi-asserted-by":"crossref","unstructured":"Bryant, R.E., Heule, M.J.H.: Generating extended resolution proofs with a BDD-based SAT solver. CoRR abs\/2105.00885 (2021)","DOI":"10.26226\/morressier.604907f41a80aac83ca25ceb"},{"key":"25_CR13","unstructured":"Burch, J.R., Clarke, E.M., Long, D.E.: Symbolic model checking with partitioned transition relations. In: VLSI91 (1991)"},{"key":"25_CR14","doi-asserted-by":"crossref","unstructured":"Chai, D., Kuehlmann, A.: A fast pseudo-Boolean constraint solver. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 24(3), 305\u2013317 (2005)","DOI":"10.1109\/TCAD.2004.842808"},{"key":"25_CR15","doi-asserted-by":"crossref","unstructured":"Chatalic, P., Simon, L.: ZRes: The old Davis-Putnam procedure meets ZBDD. In: Conference on Automated Deduction (CADE). LNCS, vol.\u00a01831, pp. 449\u2013454 (2000)","DOI":"10.1007\/10721959_35"},{"key":"25_CR16","unstructured":"Chen, J.: A new SAT encoding of at-most-one constraint. In: Workshop on Constraint Modeling and Reformulation (2010)"},{"key":"25_CR17","doi-asserted-by":"crossref","unstructured":"Chew, L., Heule, M.J.H.: Sorting parity encodings by reusing variables. In: Theory and Applications of Satisfiability Testing (SAT). LNCS, vol. 12178, pp. 1\u201310 (2020)","DOI":"10.1007\/978-3-030-51825-7_1"},{"key":"25_CR18","unstructured":"Codel, C., Reeves, J., Heule, M.J.H., Bryant, R.E.: Bipartite perfect matching benchmarks. In: Pragmatics of SAT (2021)"},{"key":"25_CR19","doi-asserted-by":"crossref","unstructured":"Cook, S.A.: A short proof of the pigeon hole principle using extended resolution. SIGACT News 8(4), 28\u201332 (Oct 1976)","DOI":"10.1145\/1008335.1008338"},{"key":"25_CR20","doi-asserted-by":"crossref","unstructured":"Cruz-Filipe, L., Heule, M.J.H., Hunt, W.A., Kaufmann, M., Schneider-Kamp, P.: Efficient certified RAT verification. In: Conference on Automated Deduction (CADE). LNCS, vol. 10395, pp. 220\u2013236 (2017)","DOI":"10.1007\/978-3-319-63046-5_14"},{"key":"25_CR21","doi-asserted-by":"crossref","unstructured":"Dantzig, G.B., Eaves, B.C.: Fourier-Motzkin elimination and its dual with application to integer programming. In: Combinatorial Programming: Methods and Applications. pp. 93\u2013102. Springer (1974)","DOI":"10.1007\/978-94-011-7557-9_4"},{"key":"25_CR22","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":"25_CR23","doi-asserted-by":"crossref","unstructured":"Duff, I.S., Reid, J.K.: A comparison of sparsity orderings for obtaining a pivotal sequence in Gaussian elimination. IMA Journal of Applied Mathematics 14(3), 281\u2013291 (1974)","DOI":"10.1093\/imamat\/14.3.281"},{"key":"25_CR24","doi-asserted-by":"crossref","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: Translating pseudo-Boolean constraints into SAT. Journal of Satisfiability, Boolean Modeling and Computation 2, 1\u201326 (2006)","DOI":"10.3233\/SAT190014"},{"key":"25_CR25","unstructured":"Ellfers, J., Nordstr\u00f6m, J.: Documentation of some combinatorial benchmarks. In: Proceedings of the SAT Competition 2016 (2016)"},{"key":"25_CR26","doi-asserted-by":"crossref","unstructured":"Gabber, O., Galil, Z.: Explicit construction of linear-sized superconcentrators. Journal of Computer and System Sciences 22, 407\u2013420 (1981)","DOI":"10.1016\/0022-0000(81)90040-4"},{"key":"25_CR27","doi-asserted-by":"crossref","unstructured":"Gocht, S., Nordstr\u00f6m, J.: Certifying parity reasoning efficiently using pseudo-Boolean proofs. In: AAAI Conference on Artificial Intelligence. pp. 3768\u20133777 (2021)","DOI":"10.1609\/aaai.v35i5.16494"},{"key":"25_CR28","doi-asserted-by":"crossref","unstructured":"Gomory, R.: Outline of an algorithm for integer solutions to linear programs. Bulletin of the American Mathematical Society 64, 275\u2013278 (1958)","DOI":"10.1090\/S0002-9904-1958-10224-4"},{"key":"25_CR29","doi-asserted-by":"crossref","unstructured":"Haken, A.: The intractability of resolution. Theoretical Computer Science 39, 297\u2013308 (1985)","DOI":"10.1016\/0304-3975(85)90144-6"},{"key":"25_CR30","doi-asserted-by":"crossref","unstructured":"Han, C.S., Jiang, J.H.R.: When Boolean satisfiability meets Gaussian elimination in a simplex way. In: Computer-Aided Verification (CAV). LNCS, vol.\u00a07358, pp. 410\u2013426 (2012)","DOI":"10.1007\/978-3-642-31424-7_31"},{"key":"25_CR31","doi-asserted-by":"crossref","unstructured":"Heule, M.J.H., Hunt, Jr., W.A., Wetzler, N.D.: Verifying refutations with extended resolution. In: Conference on Automated Deduction (CADE). LNCS, vol.\u00a07898, pp. 345\u2013359 (2013)","DOI":"10.1007\/978-3-642-38574-2_24"},{"key":"25_CR32","doi-asserted-by":"crossref","unstructured":"Hooker, J.N.: Generalized resolution and cutting planes. Annals of Operations Research 12, 217\u2013238 (1988)","DOI":"10.1007\/BF02186368"},{"key":"25_CR33","doi-asserted-by":"crossref","unstructured":"Hosaka, K., Takenaga, Y., Yajima, S.: Size of ordered binary decision diagrams representing threshold functions. Theoretical Computer Science 180, 47\u201360 (1996)","DOI":"10.1016\/S0304-3975(97)83807-8"},{"key":"25_CR34","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 (2012)","DOI":"10.1007\/978-3-642-31365-3_28"},{"key":"25_CR35","doi-asserted-by":"crossref","unstructured":"Jussila, T., Sinz, C., Biere, A.: Extended resolution proofs for symbolic SAT solving with quantification. In: Theory and Applications of Satisfiability Testing (SAT). LNCS, vol.\u00a04121, pp. 54\u201360 (2006)","DOI":"10.1007\/11814948_8"},{"key":"25_CR36","unstructured":"Klieber, W., Kwon, G.: Efficient CNF encoding for selecting 1 from N objects. In: Constraints in Formal Verification (CFV) (2007)"},{"key":"25_CR37","doi-asserted-by":"crossref","unstructured":"Laitinen, T., Junttila, T., Niemel\u00e4, I.: Extending clause learning SAT solvers with complete parity reasoning. In: International Conference on Tools with Artificial Intelligence. pp. 65\u201372. IEEE (2012)","DOI":"10.1109\/ICTAI.2012.18"},{"key":"25_CR38","doi-asserted-by":"crossref","unstructured":"Li, C.M.: Equivalent literal propagation in the DLL procedure. Discrete Applied Mathematics 130(2), 251\u2013276 (2003)","DOI":"10.1016\/S0166-218X(02)00407-9"},{"key":"25_CR39","doi-asserted-by":"crossref","unstructured":"Manthey, N., Heule, M.J.H., Biere, A.: Automated reencoding of Boolean formulas. In: Haifa Verification Conference. LNCS, vol.\u00a07857 (2013)","DOI":"10.1007\/978-3-642-39611-3_14"},{"key":"25_CR40","unstructured":"Margulis, G.A.: Explicit construction of concentrators. Probl.\u00a0Perdachi Info (Problems in Information Transmission) 9(4), 71\u201380 (1973)"},{"key":"25_CR41","doi-asserted-by":"crossref","unstructured":"Markowitz, H.M.: The elimination form of the inverse and its application to linear programming. Management Science 3(3), 213\u2013284 (1957)","DOI":"10.1287\/mnsc.3.3.255"},{"key":"25_CR42","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":"25_CR43","doi-asserted-by":"crossref","unstructured":"Robinson, J.A.: A machine-oriented logic based on the resolution principle. J.ACM 12(1), 23\u201341 (January 1965)","DOI":"10.1145\/321250.321253"},{"key":"25_CR44","doi-asserted-by":"crossref","unstructured":"Rosser, J.B.: A method of computing exact inverses of matrices with integer coefficients. Journal of Research of the National Bureau of Standards 49(5), 349\u2013358 (1952)","DOI":"10.6028\/jres.049.036"},{"key":"25_CR45","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":"25_CR46","doi-asserted-by":"crossref","unstructured":"Sinz, C., Biere, A.: Extended resolution proofs for conjoining BDDs. In: Computer Science Symposium in Russia (CSR). LNCS, vol.\u00a03967, pp. 600\u2013611 (2006)","DOI":"10.1007\/11753728_60"},{"key":"25_CR47","doi-asserted-by":"crossref","unstructured":"Soos, M., Nohl, K., Castelluccia, C.: Extending SAT solvers to cryptographic problems. In: Proc. of the 12th Int. Conference on Theory and Applications of Satisfiability Testing (SAT 2009). LNCS, vol.\u00a05584, pp. 244\u2013257 (2009)","DOI":"10.1007\/978-3-642-02777-2_24"},{"key":"25_CR48","doi-asserted-by":"crossref","unstructured":"Tseitin, G.S.: On the complexity of derivation in propositional calculus. In: Automation of Reasoning: 2: Classical Papers on Computational Logic 1967\u20131970. pp. 466\u2013483. Springer (1983)","DOI":"10.1007\/978-3-642-81955-1_28"},{"key":"25_CR49","doi-asserted-by":"crossref","unstructured":"Urquhart, A.: The complexity of propositional proofs. The Bulletin of Symbolic Logic 1(4), 425\u2013467 (1995)","DOI":"10.2307\/421131"},{"key":"25_CR50","doi-asserted-by":"crossref","unstructured":"Wetzler, N.D., Heule, M.J.H., Hunt\u00a0Jr., W.A.: DRAT-trim: Efficient checking and trimming using expressive clausal proofs. In: Theory and Applications of Satisfiability Testing (SAT). LNCS, vol.\u00a08561, pp. 422\u2013429 (2014)","DOI":"10.1007\/978-3-319-09284-3_31"},{"key":"25_CR51","doi-asserted-by":"crossref","unstructured":"Williams, H.P.: Fourier-Motzkin elimination extension to integer programming problems. Journal of Combinatorial Theory (A) 21, 118\u2013123 (1976)","DOI":"10.1016\/0097-3165(76)90055-8"},{"key":"25_CR52","unstructured":"Zhang, L., Malik, S.: Validating SAT solvers using an independent resolution-based checker: Practical implementations and other applications. In: Design, Automation and Test in Europe (DATE). pp. 880\u2013885 (2003)"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-99524-9_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,30]],"date-time":"2023-01-30T17:04:37Z","timestamp":1675098277000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-99524-9_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783030995232","9783030995249"],"references-count":52,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-99524-9_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"30 March 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Munich","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2 April 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 April 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2022\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"159","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"46","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"29% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"10","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"16 tool papers of the affiliated competition SV-Comp and 1 paper consisting of the competition report are also included in the proceedings","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}