Titelaufnahme

Titel
A solver for quantified boolean formulas in negation normal form / Martina Seidl
VerfasserSeidl, Martina
Begutachter / BegutachterinEgly, Uwe ; Creignou, Nadia
Erschienen2007
UmfangXII, 128 S. : graph. Darst.
HochschulschriftWien, Techn. Univ., Diss., 2007
Anmerkung
Zsfassung in dt. Sprache
SpracheEnglisch
Bibl. ReferenzOeBB
DokumenttypDissertation
Schlagwörter (DE)Quantifizierte Boolsche Formeln / Negationsnormalform / automatisches Beweisen
Schlagwörter (EN)quantified Boolean formulas / negation normalform / automatic deduction
Schlagwörter (GND)Boolesche Formel / Negation / Normalform / Automatisches Beweisverfahren
URNurn:nbn:at:at-ubtuw:1-21782 Persistent Identifier (URN)
Zugriffsbeschränkung
 Das Werk ist frei verfügbar
Dateien
A solver for quantified boolean formulas in negation normal form [0.73 mb]
Links
Nachweis
Klassifikation
Zusammenfassung (Deutsch)

In dieser Arbeit wurde ein Beweiser für quantifizierte Boolsche Formeln (QBF) entwickelt, der sich, im Gegensatz zu den meisten state-of-the-art Systemen, nicht nur auf Formeln in konjunktiver Pränexnormalform (PCNF) beschränkt.

Die Kodierung vieler Probleme nach QBF führt im allgemeinen nicht zu Formeln in PCNF. Ein zusätzlicher Transformationsschritt wird notwendig, wobei meistens neue Variable eingeführt werden müssen, und die Struktur der Formel zerstört wird.

Weiters ist die PCNF einer Formel im Allgemeinen nicht eindeutig.

Weiters ist es nicht einfach vorherzusagen, welche Normalformvariante für welchen Beweiser am Besten geeignet ist. Um diese Probleme zu umgehen, haben wir den Beweiser qpro entwickelt, der auch Formeln lösen kann, die nicht in PCNF transformiert wurden.

Zusammenfassung (Englisch)

We present a new solver for quantified Boolean formulas (QBFs) which, compared to current state-of-the-art systems, does not require the input formula to be in prenex conjunctive normal form (PCNF).

For many applications, encodings into QBFs usually do not result in PCNF formulas. This makes a further transformation step necessary which often introduces new variables and disrupts the structure of the formula.

In fact, different normal form variants of a formula exist and it is by far not predictable in advance which variant results in good runtimes.

To overcome those problems in normal form translations, our solver qpro can handle QBFs not necessarily given in PCNF.