2026-07-20T05:58:30Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:26314 2026-07-16T10:50:11Z ddc:004 open_access

Conditional Autarkies: Hard Formulas Made Easy Bonacina, Ilario Bonet, Maria Luisa Kolokolova, Antonina Lauria, Massimo conditional autarkies perfect matching principle pigeonhole principle redundancy rules proof complexity 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Ilario Bonacina and Maria Luisa Bonet and Antonina Kolokolova and Massimo Lauria 2026 Is Part Of LIPIcs, Volume 377, 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.SAT.2026.8 urn:nbn:de:0030-drops-263145 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.8 eng https://creativecommons.org/licenses/by/4.0/legalcode