КТИ-2016: On the interplay between proof complexity and sat solving

Jakob Nordström - KTH Royal Institute of Technology Although determining satisfiability of Boolean formulas is an NP-complete problem, and is hence believed to require exponential time in the worst case, algorithmic developments over the last 15-20 years have led to so-called SAT solvers that successfully handle real-world formulas with millions of variables. It is still quite poorly understood when and how such solvers work, however. Proof complexity studies formal methods for reasoning about Boolean form