Presentation slides:
Sam Buss
DRAT Proofs and Extensions:
Satisfiability Solving with Conflict Driven Clause Learning
and Non-implicational Inferences
University of Birmingham, June 15, 2023.
Download
talk slides.
Abstract: This talk discusses (a) DPLL and CDCL SAT solvers and (b) DRAT and related inference systems.