{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:34:17Z","timestamp":1740123257250,"version":"3.37.3"},"reference-count":34,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2023,9,1]],"date-time":"2023-09-01T00:00:00Z","timestamp":1693526400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,9,14]],"date-time":"2023-09-14T00:00:00Z","timestamp":1694649600000},"content-version":"vor","delay-in-days":13,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/100014037","name":"National Defense Science and Engineering Graduate","doi-asserted-by":"publisher","award":["FA9550-21-F-0003"],"award-info":[{"award-number":["FA9550-21-F-0003"]}],"id":[{"id":"10.13039\/100014037","id-type":"DOI","asserted-by":"publisher"}]},{"name":"National Science Foundation, United States","award":["CCF-2108521"],"award-info":[{"award-number":["CCF-2108521"]}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2023,9]]},"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. Lastly, we tested the robustness of <jats:sc>PReLearn<\/jats:sc> by applying other forms of preprocessing as well as by randomly permuting variable names in the formula before running <jats:sc>PReLearn<\/jats:sc>, and we found <jats:sc>PReLearn<\/jats:sc> performed similarly with and without the changes to the formula.<\/jats:p>","DOI":"10.1007\/s10817-023-09681-3","type":"journal-article","created":{"date-parts":[[2023,9,14]],"date-time":"2023-09-14T13:51:47Z","timestamp":1694699507000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Preprocessing of Propagation Redundant Clauses"],"prefix":"10.1007","volume":"67","author":[{"given":"Joseph E.","family":"Reeves","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marijn J. H.","family":"Heule","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Randal E.","family":"Bryant","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,9,14]]},"reference":[{"issue":"1","key":"9681_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. Theoret. Comput. Sci. 310(1), 513\u2013525 (2004)","journal-title":"Theoret. Comput. Sci."},{"key":"9681_CR2","unstructured":"Anders, M.: SAT preprocessors and symmetry. In: Theory and Applications of Satisfiability Testing (SAT). Leibniz International Proceedings in Informatics (LIPIcs), vol. 236, pp. 1\u20131120. Schloss Dagstuhl-Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2022)"},{"key":"9681_CR3","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. J. Artif. Intell. Res. 66, 443\u2013472 (2019)","journal-title":"J. Artif. Intell. Res."},{"issue":"3","key":"9681_CR4","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2898435","volume":"17","author":"A Atserias","year":"2016","unstructured":"Atserias, A., Lauria, M., Nordstr\u00f6m, J.: Narrow proofs may be maximally long. ACM Trans. Comput. Logic 17(3), 1\u201330 (2016)","journal-title":"ACM Trans. Comput. Logic"},{"key":"9681_CR5","doi-asserted-by":"crossref","unstructured":"Audemard, G., Katsirelos, G., Simon, L.: A restriction of extended resolution for clause learning sat solvers. In: Proceedings of the AAAI Conference on Artificial Intelligence, pp. 15\u201320 (2010)","DOI":"10.1609\/aaai.v24i1.7553"},{"key":"9681_CR6","unstructured":"Biere, A., Fazekas, K., Fleury, M., Heisinger, M.: CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling Entering the SAT Competition 2020. unpublished (2020)"},{"key":"9681_CR7","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":"9681_CR8","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":"9681_CR9","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":"9681_CR10","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, Cham (2016)","DOI":"10.1007\/978-3-319-40970-2_8"},{"key":"9681_CR11","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, Berlin (2005)","DOI":"10.1007\/11499107_5"},{"key":"9681_CR12","unstructured":"Freeman, J.W.: Improvements to propositional satisfiability search algorithms. PhD thesis, University of Pennsylvania, United States of America (1995)"},{"key":"9681_CR13","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. Theoret. Comput. Sci. 39, 297\u2013308 (1985)","journal-title":"Theoret. Comput. Sci."},{"key":"9681_CR14","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, Cham (2015)","DOI":"10.1007\/978-3-319-21401-6_40"},{"key":"9681_CR15","doi-asserted-by":"crossref","unstructured":"Heule, M.J.H., 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":"9681_CR16","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. Cham (2019)","DOI":"10.1007\/978-3-030-20652-9_13"},{"key":"9681_CR17","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, Cham (2019)","DOI":"10.1007\/978-3-030-17462-0_3"},{"key":"9681_CR18","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, Cham (2017)","DOI":"10.1007\/978-3-319-63046-5_9"},{"key":"9681_CR19","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":"9681_CR20","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, Cham (2016)","DOI":"10.1007\/978-3-319-40970-2_15"},{"key":"9681_CR21","doi-asserted-by":"publisher","first-page":"533","DOI":"10.1007\/s10817-019-09516-0","volume":"64","author":"MJH Heule","year":"2020","unstructured":"Heule, M.J.H., Kiesl, B., Biere, A.: Strong extension free proof systems. J. Autom. Reason. 64, 533\u2013544 (2020)","journal-title":"J. Autom. Reason."},{"key":"9681_CR22","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, Berlin (2012)","DOI":"10.1007\/978-3-642-31365-3_28"},{"key":"9681_CR23","first-page":"113","volume-title":"Theory and Applications of Satisfiability Testing (SAT)","author":"H Katebi","year":"2010","unstructured":"Katebi, H., Sakallah, K.A., Markov, I.L.: Symmetry and satisfiability: an update. In: Strichman, O., Szeider, S. (eds.) Theory and Applications of Satisfiability Testing (SAT), pp. 113\u2013127. Springer, Berlin (2010)"},{"key":"9681_CR24","unstructured":"Lecoutre, C., Roussel, O.: Proceedings of the 2018 XCSP3 Competition, pp. 40\u201341 (2018)"},{"key":"9681_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":"9681_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":"9681_CR27","unstructured":"Marques-Silva, J.P., Lynce, I., Malik, S.: Conflict-driven clause learning SAT solvers. In: Handbook of Satisfiability, pp. 131\u2013153. IOS Press, Amsterdam (2009)"},{"key":"9681_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, pp. 530\u2013535. ACM, New York, NY, USA (2001)","DOI":"10.1145\/378239.379017"},{"key":"9681_CR29","first-page":"436","volume-title":"AAAI Conference on Artificial Intelligence","author":"JAN P\u00e9rez","year":"2005","unstructured":"P\u00e9rez, J.A.N., Voronkov, A.: Generation of hard non-clausal random satisfiability problems. In: Veloso, M.M., Kambhampati, S. (eds.) AAAI Conference on Artificial Intelligence, pp. 436\u2013442. AAAI Press, Palo Alto (2005)"},{"key":"9681_CR30","first-page":"106","volume-title":"Preprocessing of Propagation Redundant Clauses","author":"JE Reeves","year":"2022","unstructured":"Reeves, J.E., Heule, M.J.H., Bryant, R.E.: Preprocessing of Propagation Redundant Clauses, pp. 106\u2013124. Springer, Berlin (2022)"},{"key":"9681_CR31","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, Cham (2014)","DOI":"10.1007\/978-3-319-08587-6_28"},{"key":"9681_CR32","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":"9681_CR33","first-page":"466","volume-title":"On the Complexity of Derivation in Propositional Calculus","author":"GS Tseitin","year":"1983","unstructured":"Tseitin, G.S.: On the Complexity of Derivation in Propositional Calculus, pp. 466\u2013483. Springer, Berlin (1983)"},{"key":"9681_CR34","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. Springer, Cham (2014)","DOI":"10.1007\/978-3-319-09284-3_31"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-023-09681-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-023-09681-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-023-09681-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,21]],"date-time":"2023-09-21T04:04:59Z","timestamp":1695269099000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-023-09681-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,9]]},"references-count":34,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2023,9]]}},"alternative-id":["9681"],"URL":"https:\/\/doi.org\/10.1007\/s10817-023-09681-3","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2023,9]]},"assertion":[{"value":"1 February 2023","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"16 August 2023","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"14 September 2023","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare no competing interests.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}}],"article-number":"31"}}