Sam Buss (Theory Seminar)

"CDCL Sat Solvers, and DRAT proofs with and without new extension variables"

Image removed.

Sam Buss (UCSD)
Monday April 6th 2-3pm
Zoom Meeting https://ucsd.zoom.us/my/csetheoryseminar

Abstract: Conflict driven clause learning (CDCL) can be remarkably successful in practice for solving instances of satisfiability (SAT). It is known that CDCL solvers with restarts can be equivalent to resolution, a rather weak. The DRAT proof systems have been introduced as static proof systems for verifying the correctness of (augmented) CDCL refutations. When it is permitted to introduce new variables, DRAT proofs are as powerful as extended Frege systems. Our work studies the proof complexity of RAT proofs and several related systems including BC, SPR and PR which use blocked clauses and (subset) propagation redundancy and new system SR for substitution redundancy. These systems allow inferences which preserve satisfiability but not logical implication. When new variables are permitted these systems have the same proof theoretic strength as extended resolution. We thus focus on the systems that do not allow new variables to be introduced.  

 
We show that many of the systems are equivalent unifying and extended prior results. Our next main result is that many of the well-known ``hard'' principles have polynomial size $PR${}^-$ refutations. These include the pigeonhole principle, bit pigeonhole principle, parity principle, Tseitin tautologies and clique-coloring tautologies. SPR${}^-$ can also handle or-fication and xor-ification, and lifting with an index gadget. Our final result is an exponential size lower

bound the bit pigeonhole principle for RAT${}^-$ and several other systems.