Strong Extension-Free Proof Systems.

Area of Science:

• Automated reasoning
• Computational logic
• Boolean satisfiability (SAT)

Background:

• Modern SAT solvers utilize sophisticated techniques for efficient problem-solving.
• Developing proof systems that capture these techniques is crucial for understanding SAT solver capabilities.
• Short proofs for hard formulas remain a significant challenge in proof complexity.

Purpose of the Study:

• Introduce novel proof systems for propositional logic.
• Enable the generation of short proofs for computationally hard formulas.
• Succinctly represent techniques employed by contemporary SAT solvers.

Main Methods:

• Design proof systems allowing derivation of redundant clauses that preserve satisfiability.
• Characterize clause redundancy via semantic implication, then restrict for polynomial-time decidability.
• Base restricted implication on unit propagation, a core SAT solver technique.

Main Results:

• The new proof systems generate short proofs for hard formulas, including pigeonhole formulas, without new variables.
• Efficiently decidable redundancy criteria are established.
• Proof checking is efficient due to the unit propagation-based implication relation.

Conclusions:

• The introduced proof systems are surprisingly powerful, even without variable augmentation.
• These systems offer a succinct way to express SAT solver techniques.
• The findings advance the understanding of proof complexity and SAT solving.