{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T05:10:46Z","timestamp":1743052246356,"version":"3.40.3"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783031107689"},{"type":"electronic","value":"9783031107696"}],"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,8,1]],"date-time":"2022-08-01T00:00:00Z","timestamp":1659312000000},"content-version":"vor","delay-in-days":212,"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>The<jats:italic>propagation redundant<\/jats:italic>(PR) proof system generalizes the<jats:italic>resolution<\/jats:italic>and<jats:italic>resolution asymmetric tautology<\/jats:italic>proof systems used by<jats:italic>conflict-driven clause learning<\/jats:italic>(CDCL) solvers. PR allows short proofs of unsatisfiability for some problems that are difficult for CDCL solvers. Previous attempts to automate PR clause learning used hand-crafted heuristics that work well on some highly-structured problems. For example, the solver<jats:sc>SaDiCaL<\/jats:sc>incorporates PR clause learning into the CDCL loop, but it cannot compete with modern CDCL solvers due to its fragile heuristics. We present<jats:sc>PReLearn<\/jats:sc>, a preprocessing technique that learns short PR clauses. Adding these clauses to a formula reduces the search space that the solver must explore. By performing PR clause learning as a preprocessing stage, PR clauses can be found efficiently without sacrificing the robustness of modern CDCL solvers. On a large portion of SAT competition benchmarks we found that preprocessing with<jats:sc>PReLearn<\/jats:sc>improves solver performance. In addition, there were several satisfiable and unsatisfiable formulas that could only be solved after preprocessing with<jats:sc>PReLearn<\/jats:sc>.<jats:sc>PReLearn<\/jats:sc>supports proof logging, giving a high level of confidence in the results.<\/jats:p>","DOI":"10.1007\/978-3-031-10769-6_8","type":"book-chapter","created":{"date-parts":[[2022,8,1]],"date-time":"2022-08-01T01:02:56Z","timestamp":1659315776000},"page":"106-124","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Preprocessing of Propagation Redundant Clauses"],"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":[[2022,8,1]]},"reference":[{"issue":"1","key":"8_CR1","doi-asserted-by":"publisher","first-page":"513","DOI":"10.1016\/S0304-3975(03)00395-5","volume":"310","author":"M Alekhnovich","year":"2004","unstructured":"Alekhnovich, M.: Mutilated chessboard problem is exponentially hard for resolution. Theoretical Computer Science 310(1), 513\u2013525 (2004)","journal-title":"Theoretical Computer Science"},{"key":"8_CR2","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1613\/jair.1.11741","volume":"66","author":"C Ans\u00f3tegui","year":"2019","unstructured":"Ans\u00f3tegui, C., Bonet, M.L., Gir\u00e1ldez-Cru, J., Levy, J., Simon, L.: Community structure in industrial SAT instances. Journal of Artificial Intelligence Research (JAR) 66, 443\u2013472 (2019)","journal-title":"Journal of Artificial Intelligence Research (JAR)"},{"key":"8_CR3","doi-asserted-by":"crossref","unstructured":"Atserias, A., Lauria, M., Nordstr\u00f6m, J.: Narrow proofs may be maximally long. ACM Transactions on Computational Logic 17(3) (2016)","DOI":"10.1145\/2898435"},{"key":"8_CR4","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. AAAI Press (2010)","DOI":"10.1609\/aaai.v24i1.7553"},{"key":"8_CR5","unstructured":"Biere, A., Fazekas, K., Fleury, M., Heisinger, M.: CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling entering the SAT competition 2020 (2020), unpublished"},{"key":"8_CR6","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. 9340, pp. 405\u2013422 (2015)","DOI":"10.1007\/978-3-319-24318-4_29"},{"key":"8_CR7","unstructured":"Codel, C.R., Reeves, J.E., Heule, M.J.H., Bryant, R.E.: Bipartite perfect matching benchmarks. In: Pragmatics of SAT (2021)"},{"issue":"4","key":"8_CR8","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1145\/1008335.1008338","volume":"8","author":"SA Cook","year":"1976","unstructured":"Cook, S.A.: A short proof of the pigeon hole principle using extended resolution. SIGACT News 8(4), 28\u201332 (1976)","journal-title":"SIGACT News"},{"key":"8_CR9","doi-asserted-by":"crossref","unstructured":"Devriendt, J., Bogaerts, B., Bruynooghe, M., Denecker, M.: Improved static symmetry breaking for SAT. In: Theory and Applications of Satisfiability Testing (SAT). LNCS, vol. 9710, pp. 104\u2013122. Springer (2016)","DOI":"10.1007\/978-3-319-40970-2_8"},{"key":"8_CR10","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. 3569, pp. 61\u201375. Springer (2005)","DOI":"10.1007\/11499107_5"},{"key":"8_CR11","unstructured":"Freeman, J.W.: Improvements to Propositional Satisfiability Search Algorithms. Ph.D. thesis, USA (1995)"},{"key":"8_CR12","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 39, 297\u2013308 (1985)","journal-title":"Theoretical Computer Science"},{"key":"8_CR13","doi-asserted-by":"crossref","unstructured":"Heule, M.J.H., Hunt, W.A., Wetzler, N.: Expressing symmetry breaking in DRAT proofs. In: Conference on Automated Deduction (CADE). LNCS, vol. 9195, pp. 591\u2013606. Springer (2015)","DOI":"10.1007\/978-3-319-21401-6_40"},{"key":"8_CR14","doi-asserted-by":"crossref","unstructured":"Heule, M.J.H., Kiesl, B., Biere, A.: Short proofs without new variables. In: Conference on Automated Deduction (CADE). LNCS, vol. 10395, pp. 130\u2013147. Springer (2017)","DOI":"10.1007\/978-3-319-63046-5_9"},{"key":"8_CR15","doi-asserted-by":"crossref","unstructured":"Heule, M.J.H., Kiesl, B., Biere, A.: Clausal proofs of mutilated chessboards. In: NASA Formal Methods. LNCS, vol. 11460, pp. 204\u2013210 (2019)","DOI":"10.1007\/978-3-030-20652-9_13"},{"key":"8_CR16","doi-asserted-by":"crossref","unstructured":"Heule, M.J.H., Kiesl, B., Biere, A.: Encoding redundancy for satisfaction-driven clause learning. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 11427, pp. 41\u201358. Springer (2019)","DOI":"10.1007\/978-3-030-17462-0_3"},{"key":"8_CR17","doi-asserted-by":"crossref","unstructured":"Heule, M.J.H., Kiesl, B., Biere, A.: Strong extension free proof systems. In: Journal of Automated Reasoning. vol. 64, pp. 533\u2013544 (2020)","DOI":"10.1007\/s10817-019-09516-0"},{"key":"8_CR18","doi-asserted-by":"crossref","unstructured":"Heule, M.J.H., Kiesl, B., Seidl, M., Biere, A.: PRuning through satisfaction. In: Haifa Verification Conference (HVC). LNCS, vol. 10629, pp. 179\u2013194 (2017)","DOI":"10.1007\/978-3-319-70389-3_12"},{"key":"8_CR19","doi-asserted-by":"crossref","unstructured":"Heule, M.J.H., Kullmann, O., Marek, V.W.: Solving and verifying the boolean pythagorean triples problem via cube-and-conquer. In: Theory and Applications of Satisfiability Testing (SAT). LNCS, vol. 9710, pp. 228\u2013245. Springer (2016)","DOI":"10.1007\/978-3-319-40970-2_15"},{"key":"8_CR20","doi-asserted-by":"crossref","unstructured":"Heule, M.J., Hunt, W.A., Wetzler, N.: Trimming while checking clausal proofs. In: Formal Methods in Computer-Aided Design (FMCAD). pp. 181\u2013188 (2013)","DOI":"10.1109\/FMCAD.2013.6679408"},{"key":"8_CR21","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. 7364, pp. 355\u2013370. Springer (2012)","DOI":"10.1007\/978-3-642-31365-3_28"},{"issue":"14","key":"8_CR22","doi-asserted-by":"publisher","first-page":"1553","DOI":"10.1016\/j.disc.2013.03.024","volume":"313","author":"N Johnston","year":"2013","unstructured":"Johnston, N.: Non-uniqueness of minimal superpermutations. Discrete Mathematics 313(14), 1553\u20131557 (2013)","journal-title":"Discrete Mathematics"},{"key":"8_CR23","doi-asserted-by":"crossref","unstructured":"Kiesl, B., Seidl, M., Tompits, H., Biere, A.: Super-blocked clauses. In: International Joint Conference on Automated Reasoning (IJCAR). LNCS, vol. 9706, pp. 45\u201361 (2016)","DOI":"10.1007\/978-3-319-40229-1_5"},{"key":"8_CR24","unstructured":"Lecoutre, C., Roussel, O.: XCSP3 competition 2018 proceedings. pp. 40\u201341 (2018)"},{"key":"8_CR25","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. 9710, pp. 123\u2013140 (2016)","DOI":"10.1007\/978-3-319-40970-2_9"},{"key":"8_CR26","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. 7857, pp. 102\u2013117 (2013)","DOI":"10.1007\/978-3-642-39611-3_14"},{"key":"8_CR27","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":"8_CR28","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":"8_CR29","unstructured":"Navarro, J.A., Voronkov, A.: Generation of hard non-clausal random satisfiability problems. In: AAAI Conference on Artificial Intelligence. pp. 436\u2013442. The MIT Press (2005)"},{"key":"8_CR30","doi-asserted-by":"crossref","unstructured":"Stump, A., Sutcliffe, G., Tinelli, C.: StarExec: A cross-community infrastructure for logic solving. In: International Joint Conference on Automated Reasoning (IJCAR). LNCS, vol. 8562, pp. 367\u2013373. Springer (2014)","DOI":"10.1007\/978-3-319-08587-6_28"},{"key":"8_CR31","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":"8_CR32","doi-asserted-by":"crossref","unstructured":"Tseitin, G.S.: On the Complexity of Derivation in Propositional Calculus, pp. 466\u2013483. Springer (1983)","DOI":"10.1007\/978-3-642-81955-1_28"},{"key":"8_CR33","doi-asserted-by":"crossref","unstructured":"Wetzler, N., Heule, M.J.H., Hunt, W.A.: DRAT-trim: Efficient checking and trimming using expressive clausal proofs. In: Theory and Applications of Satisfiability Testing (SAT). LNCS, vol. 8561, pp. 422\u2013429 (2014)","DOI":"10.1007\/978-3-319-09284-3_31"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-10769-6_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,13]],"date-time":"2023-02-13T04:15:37Z","timestamp":1676261737000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-10769-6_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031107689","9783031107696"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-10769-6_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"1 August 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"IJCAR","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Joint Conference on Automated Reasoning","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Haifa","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Israel","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":"8 August 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 August 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ijcar2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/easychair.org\/smart-program\/FLoC2022\/IJCAR-index.html","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":"85","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":"32","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":"9","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":"38% - 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.2","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":"5.2","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)"}}]}}