Martina Seidl: Proof Systems for Practical QBF Reasoning

Datum objave: 12. 12. 2017
Seminar za temelje matematike in teoretično računalništvo
Četrtek, 14. 12. 2017, od 12h do 14h, Plemljev seminar, Jadranska 19
Speaker: Martina Seidl, Institute for Formal Models and Verification, Johannes Kepler Universität Linz.

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.