Martina Seidl: Proof Systems for Practical QBF Reasoning
Source: Mathematics and theoretical computing seminar
Title: Proof Systems for Practical QBF Reasoning
Abstract: Recently, several new algorithms to solve quantified Boolean formulas (QBF) have been presented. Further, established algorithms were considerably revised and extended. For complete solvers, there are currently two dominant solving paradigms: search-based solvers with clause and cube learning (QCDCL) are founded on classical Q-resolution and extensions. Expansion-based solvers are founded on instantiation-based calculi. Both kinds of solvers strongly benefit from an additional preprocessing step during which the formula is rewritten in a satisfiability-preserving manner. For formally capturing all of these preprocessing techniques, we introduced the QRAT proof system that distinguishes itself in various aspects from the previously mentioned proof systems.
In this talk, we survey the different proof systems on which modern QBF solving technology is based. Special focus is set on the QRAT proof system.