Moderne Beweiser für quantifizierte boolesche Formeln (QBF) entscheiden nicht nur die Erfüllbarkeit einer Formel, sondern sie liefern auch Skolem-Funktionen, die die Lösungen wahrer Formeln darstellen. Leider geht die Fähigkeit, Skolem-Funktionen zu finden, verloren, wenn spezielle Vereinfachungstechniken angewendet werden. Diese Techniken sind allerdings oft notwendig, damit der verwendete Beweiser eine Lösung effizient finden kann. Wir zeigen in dieser Arbeit, wie Skolem-Funktionen auch unter Verwendung dieser Vereinfachungstechniken gefunden werden können.
Abstract
Modern solvers for quantified Boolean formulas (QBF) not only decide the satisfiability of a formula, but also return a set of Skolem functions representing a model for a true QBF. Unfortunately, in combination with a preprocessor this ability is lost for many preprocessing techniques. A preprocessor rewrites the input formula to an equi-satisfiable formula which is often easier to solve than the original formula. Then the Skolem functions returned by the solver represent a solution for the preprocessed formula, but not necessarily for the original encoding. Our solution to this problem is to combine Skolem functions obtained from a QRAT trace as produced by the widely-used preprocessor Bloqqer with Skolem functions for the preprocessed formula. This approach is agnostic of the concrete rewritings performed by the preprocessor and allows the combination of Bloqqer with any Skolem function producing solver, hence realizing a smooth integration into the solving tool chain.
