Proof System for Practical QBF Reasoning

Description

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.

Period	14 Dec 2017
Event title	Research Seminar at the Faculty of Mathematics at the University of Ljubliana
Event type	Other
Location	AustriaShow on map