Abstract
Back in 1999, Kullmann [1] initiated the study of those systems by defining the notion of "blocked clauses." In recent years certain generalizations of blocked clauses have been used for proof logging in practical SAT solvers. Restricted versions of those systems were shown by Buss and Thapen [2] to be surprisingly strong in that, despite working only with clauses and using no extension variables, some of those systems have polynomial-size proofs of many "hard" formulas like the pigeonhole principle, bit pigeonhole principle, parity principle, clique-coloring principle, and Tseitin tautologies. Recently, we [3] gave a generic recipe for easily proving separations between those proof systems by using the notion of effective simulations (of Pitassi and Santhanam) and existing separations from extended resolution. There is now an entire zoo of those systems and there are interesting open questions about their proof complexity. I will define a few of those systems, give examples, and mention open problems.
[1]: Oliver Kullmann. On a generalization of extended resolution. Discrete Applied Mathematics, 96–97:149–176, 1999.
[2]: Sam Buss and Neil Thapen. DRAT and propagation redundancy proofs without new variables. Logical Methods in Computer Science, 17(2:12), 2021. (Earlier version in SAT 2019.)
[3]: Emre Yolcu and Marijn J.H. Heule. Exponential separations using guarded extension variables. ITCS 2023.