Presentation slides:

    Sam Buss
    DRAT Proofs and Extensions
    Orevkov'80, 5th St. Petersburg Days of Logic and Computability
    Zoom presentation, May 15, 2021.

    Download talk slides.

Related paper

Abstract: Modern propositional satisfiability solvers (SAT solvers) are remarkable successful, able to solve instances of satisfiability with 100 000's of variables, or even millions of variables. This is due largely to the success of conflict driven clause learning. This talk will discuss the logical foundations of CDCL solvers and their connections to resolution. The DRAT proof system has been introduced as a proof system for verifying the correctness of CDCL refutations. The DRAT proof system is surprisingly powerful in that it simulates extended resolution. We introduce a stronger form of DRAT proofs, called Substitution Propagation. We discuss upper and lower bounds on the length of Substitution Propagation and DRAT proofs when they are not allowed to introduce new variables. (New results are joint with Neil Thapen.)

Back to Sam Buss's publications page.