We present QRAT, a novel proof system for quantified Boolean formulas. With QRAT it is now possible to produce certificates for all reasoning techniques implemented in state-of-the-art QBF preprocessors. Such certificates are not only useful to efficiently validate the correctness of a result, but they also allow the extraction of Skolem functions, i.e., winning strategies for satisfiable formula instances.
In this talk, we first introduce the rules of QRAT, then we show how they can be used to express some powerful reasoning techniques implemented in modern preprocessors, and finally we outline how to extract a Skolem function from a QRAT proof.
Forschungs-