Document Open Access Logo

Conditional Autarkies: Hard Formulas Made Easy

Authors Ilario Bonacina , Maria Luisa Bonet , Antonina Kolokolova , Massimo Lauria

PDF

File

Thumbnail PDF
PDF
LIPIcs.SAT.2026.8.pdf
  • Filesize: 0.9 MB
  • 18 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof complexity
  • Theory of computation → Automated reasoning
Keywords
  • conditional autarkies
  • perfect matching principle
  • pigeonhole principle
  • redundancy rules
  • proof complexity

Metrics

Abstract

State-of-the-art SAT solvers increasingly use techniques beyond resolution. For instance, adding redundant clauses allows the solver to reduce the solution space, e.g., to break symmetries. We investigate the strength of relatively weak redundancy reasoning: conditional autarkies and set-blocked clauses, with no new variables and no deletions. 
We show that adding conditional autarkies (as set-blocked clauses) on top of resolution allows efficient refutations of a number of natural combinatorial principles that may occur in SAT benchmarks. In particular, we give efficient proofs of the perfect matching on a grid, the mutilated chessboard, the counting principle modulo 3, and the relativized pigeonhole principle.

Cite As Get BibTex

Ilario Bonacina, Maria Luisa Bonet, Antonina Kolokolova, and Massimo Lauria. Conditional Autarkies: Hard Formulas Made Easy. In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 8:1-8:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.SAT.2026.8

Author Details

Ilario Bonacina
  • Universitat Politècnica de Catalunya, Barcelona, Spain
Maria Luisa Bonet
  • Universitat Politècnica de Catalunya, Barcelona, Spain
Antonina Kolokolova
  • Memorial University of Newfoundland, St. Johns', Canada
Massimo Lauria
  • Università di Roma La Sapienza, Italy

Funding

  • Bonacina, Ilario: Funded by the AEI with the grant number PID2022-138506NB-C22.
  • Bonet, Maria Luisa: Funded by the AEI with the grant number PID2022-138506NB-C21.
  • Kolokolova, Antonina: Supported by an NSERC Discovery grant.
  • Lauria, Massimo: Supported by project "Logical Methods in Combinatorics" N. 2022BXH4R5 of the Italian Ministry of University and Research (MIUR).

References

  1. Miklos Ajtai. The independence of the modulo p counting principles. In Proceedings of the twenty-sixth annual ACM symposium on Theory of computing, pages 402-411. ACM, 1994. Google Scholar
  2. Albert Atserias, Johannes Klaus Fichte, and Marc Thurley. Clause-learning algorithms with many restarts and bounded-width resolution. J. Artif. Intell. Res. (JAIR), 40:353-373, 2011. URL: https://doi.org/10.1613/jair.3152.
  3. Albert Atserias, Massimo Lauria, and Jakob Nordström. Narrow proofs may be maximally long. ACM Trans. Comput. Logic, 17(3), 2016. URL: https://doi.org/10.1145/2898435.
  4. Paul Beame, Russell Impagliazzo, Jan Krajíček, Toniann Pitassi, and Pavel Pudlák. Lower bounds on Hilbert’s nullstellensatz and propositional proofs. Proceedings of the London Mathematical Society, 73:1-26, 1996. Google Scholar
  5. Sam Buss and Jakob Nordström. Proof complexity and SAT solving. In Armin Biere, Marijn J. H. Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability 2nd Edition, pages 233-350. IOS Press, 2021. URL: https://doi.org/10.3233/FAIA200990.
  6. Sam Buss and Neil Thapen. DRAT and propagation redundancy proofs without new variables. Log. Methods Comput. Sci., 17(2), 2021. URL: https://lmcs.episciences.org/7400.
  7. Samuel R. Buss. Polynomial size proofs of the propositional pigeonhole principle. Journal of Symbolic Logic, 52(4):916-927, December 1987. URL: https://doi.org/10.2307/2273826.
  8. Niklas Eén and Armin Biere. Effective preprocessing in SAT through variable and clause elimination. Lecture Notes in Computer Science, pages 61-75, 2005. URL: https://doi.org/10.1007/11499107_5.
  9. Armin Haken. The intractability of resolution. Theoretical Computer Science, 39:297-308, 1985. URL: https://doi.org/10.1016/0304-3975(85)90144-6.
  10. Marijn J. H. Heule, Benjamin Kiesl, and Armin Biere. Clausal proofs of mutilated chessboards. In NASA Formal Methods - 11th International Symposium, NFM 2019, Houston, TX, USA, May 7-9, 2019, Proceedings, pages 204-210, 2019. URL: https://doi.org/10.1007/978-3-030-20652-9_13.
  11. Marijn J. H. Heule, Benjamin Kiesl, and Armin Biere. Strong extension-free proof systems. Journal of Automated Reasoning, 64:533-554, 2020. Conference version at CADE '17. URL: https://doi.org/10.1007/s10817-019-09516-0.
  12. Marijn JH Heule, Benjamin Kiesl, Martina Seidl, and Armin Biere. Pruning through satisfaction. In Haifa Verification Conference, pages 179-194. Springer, 2017. Google Scholar
  13. Johan Håstad. On small-depth Frege proofs for PHP. TheoretiCS, Phase 2, December 2025. URL: https://doi.org/10.46298/theoretics.25.27.
  14. Matti Järvisalo, Marijn JH Heule, and Armin Biere. Inprocessing rules. In International Joint Conference on Automated Reasoning, pages 355-370. Springer, 2012. Google Scholar
  15. Benjamin Kiesl, Marijn J. H. Heule, and Armin Biere. Truth assignments as conditional autarkies. In Automated Technology for Verification and Analysis - 17th International Symposium, ATVA 2019, Taipei, Taiwan, October 28-31, 2019, Proceedings, pages 48-64, 2019. URL: https://doi.org/10.1007/978-3-030-31784-3_3.
  16. Benjamin Kiesl, Adrián Rebola-Pardo, and Marijn J. H. Heule. Extended resolution simulates DRAT. In Didier Galmiche, Stephan Schulz, and Roberto Sebastiani, editors, IJCAR 2018, pages 516-531, Cham, 2018. Springer International Publishing. URL: https://doi.org/10.1007/978-3-319-94205-6_34.
  17. Benjamin Kiesl, Martina Seidl, Hans Tompits, and Armin Biere. Local redundancy in SAT: Generalizations of blocked clauses. Logical Methods in Computer Science, 14, 2018. URL: https://doi.org/10.23638/LMCS-14(4:3)2018.
  18. Hans Kleine Büning and Oliver Kullmann. Minimal unsatisfiability and autarkies. In Handbook of Satisfiability, pages 339-401. IOS Press, 2009. URL: https://doi.org/10.3233/978-1-58603-929-5-339.
  19. Jan Krajícek. Combinatorics of first order structures and propositional proof systems. Arch. Math. Log., 43:427-441, May 2004. URL: https://doi.org/10.1007/s00153-003-0186-y.
  20. Oliver Kullmann. On a generalization of extended resolution. Discrete Applied Mathematics, 96-97:149-176, 1999. URL: https://doi.org/10.1016/S0166-218X(99)00037-2.
  21. João P Marques-Silva and Karem A Sakallah. Grasp: A search algorithm for propositional satisfiability. Computers, IEEE Transactions on, 48(5):506-521, 1999. URL: https://doi.org/10.1109/12.769433.
  22. Knot Pipatsrisawat and Adnan Darwiche. On the power of clause-learning SAT solvers as resolution engines. Artificial Intelligence, 175(2):512-525, 2011. URL: https://doi.org/10.1016/j.artint.2010.10.002.
  23. Adrián Rebola-Pardo and Martin Suda. A theory of satisfiability-preserving proofs in SAT solving. In LPAR, pages 583-603, 2018. URL: https://doi.org/10.29007/TC7Q.
  24. Joseph E. Reeves, Marijn J. H. Heule, and Randal E. Bryant. Preprocessing of propagation redundant clauses. In Automated Reasoning - 11th International Joint Conference, IJCAR 2022, Haifa, Israel, August 8-10, 2022, Proceedings, pages 106-124, 2022. URL: https://doi.org/10.1007/978-3-031-10769-6_8.
  25. Amar Shah, Twain Byrnes, Joseph E. Reeves, and Marijn J. H. Heule. Learning short clauses via conditional autarkies. In Proceedings of the 25th Conference on Formal Methods in Computer-Aided Design, FMCAD 2025, Menlo Park, CA, USA, October 6-10, 2025, 2025. URL: https://doi.org/10.34727/2025/ISBN.978-3-85448-084-6_17.
  26. Allen Van Gelder. Complexity analysis of propositional resolution with autarky pruning. Discrete Appl. Math., 96–97(1):195-221, October 1999. URL: https://doi.org/10.1016/S0166-218X(99)00040-2.
  27. Emre Yolcu. Lower bounds for set-blocked clauses proofs. In STACS 2024, volume 289, pages 59:1-59:17, 2024. URL: https://doi.org/10.4230/LIPIcs.STACS.2024.59.
  28. Emre Yolcu and Marijn J. H. Heule. Exponential separations using guarded extension variables. In 14th Innovations in Theoretical Computer Science Conference, ITCS 2023, January 10-13, 2023, MIT, Cambridge, Massachusetts, USA, pages 101:1-101:22, 2023. URL: https://doi.org/10.4230/LIPIcs.ITCS.2023.101.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact