Zur Seitenansicht
 

Titelaufnahme

Titel
Skolem Function Continuation for Quantified Boolean Formulas
VerfasserFazekas, Katalin ; Heule, Marijn J. H. ; Seidl, Martina ; Biere, Armin
Erschienen in
Tests and Proofs / Gabmeyer, Sebastian; Johnsen, Einar Broch
ErschienenLinz : Universität, 2017
Ausgabe
Elektronische Ressource
Umfang1 Online-Ressource
Anmerkung
Open Access Publikation
SpracheEnglisch
SerieLecture Notes in Computer Science ; 10375
DokumenttypAufsatz in einem Sammelwerk
Schlagwörter (DE)Quantifizierte Boolesche Formeln / Skolem-Funktionen / Formel Vorverarbeitung
Schlagwörter (EN)Quantified Boolean Formulas / Skolem functions / Formal preprocessing
Projekt-/ReportnummerW1255-N23
Projekt-/ReportnummerS11408-N23
Projekt-/ReportnummerCCF-1618574
ISBN978-3-319-61466-3
URNurn:nbn:at:at-ubl:3-84 Persistent Identifier (URN)
Zugriffsbeschränkung
 Das Werk ist gemäß den "Hinweisen für BenützerInnen" verfügbar
Dateien
Skolem Function Continuation for Quantified Boolean Formulas [0.32 mb]
Links
Nachweis
Klassifikation
Zusammenfassung (Deutsch)

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.

Zusammenfassung (Englisch)

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.