Beweiser für quantifizierte Boolesche Ausdrücke - QUAFFLE

Arman Allahyari-Abhari

Universität Bremen

Fachbereich 3

2

Leitfaden

Grundlagen (SAT) Grundlagen (QBF) QUAFFLE-Algorithmik Performance Zusammenfassung

3

Formalismen (SAT)

Eine CNF hat die Form:

,

wobei als Klausel bezeichnet wird und eine Disjunktion von Literalen ist, also die Form hat.

Ein Literal ist eine Variable in positiver oder negativer Phase.

mm CCCC 121 ...

iC

jx

kjjj xxx ...21

4

SAT-Problem

Sei eine Boolesche Formel f in CNF gegeben. Das Erfüllbarkeitsproblem (kurz: SAT) stellt die Frage, ob es eine Belegung gibt, so dass f = 1 ist.

SAT ist NP-Vollständig (Cook, 1971)

Hohe Laufzeitkomplexität Erst: Davis-Putnam-Algorithmus (Mem. Blowup) Später: Davis-Logemann-Loveland (CPU)

5

Algorithmus von Davis, Logemann & Loveland (SAT) Gegenüber DP-Algorithmus wesentlich

geringerer Speicherbedarf Modularer Aufbau (gut erweiterbar) Neuer Flaschenhals: CPU Reiner DLL-Algorithmus für aktuelle

Probleme noch zu langsam

6

Fortschritte in SAT

Basis: DLL-Algorithmus (Dann: GRASP, Chaff, BerkMin)

Verbesserungen: Learning durch Konflikte (CBE) Verbessertes Backtracking (FDA, CDB) Optimierte Boolean Constraint Propagation Bessere Entscheidungsheuristiken (VSIDS) Database Management (Clause Aging/Deletion, …) Restarts …

7

Formalismen (QBF)

Eine quantifizierte Boolsche Formel (QBF) hat die Form: ,

wobei eine aussagenlogische Formel mit den Variablen ist. Im Folgenden wird in KNF vorliegen.

ist entweder ein Existenzquantor oder ein Allquantor . Die Quantifizierungsreihenfolge ist zwingend einzuhalten

.....11 nnxQxQ

1....n)(i ix

iQ

mnn CCxQxQ .... ..... 111

8

Formalismen (QBF) #2

Da und , können gleichquantifizierte Variablen mit der selben Priorität in disjunkten Mengen zusammen-gefasst werden:

Für den Quantor haben alle in enthaltenen Variablen das Quantifizierungs-Level j.

nk ,.... ..... 111 mkk CCXQXQ

xyyx

jQ jX

iX

xyyx

mnn CCxQxQ .... ..... 111

9

Augmented CNF

Ein cube ist eine Konjunktion von Literalen:

Eine ACNF ist eine mit (redundanten) cubes erweiterte Darstellung der CNF für QBF:

Wenn ein erfüllt ist, dann ist auch die CNF erfüllt

)... (.... ..... '1111 mmnn SSCCxQxQ

iS

klll ...21

iS

10

Besondere Klauseln/Cubes

Eine tautology clause ist eine Klausel, die beide Phasen einer Variablen enthält (Klausel erfüllt)

Ein empty cube ist ein Cube, der beide Phasen einer Variablen enthält (Cube unerfüllbar)

11

Weitere Definitionen/Konventionen

E(C) und E(S) stellen die Menge der existenziellen Literale und U(C) und U(S) die der universellen Literale in der Klausel C bzw. dem Cube S dar.

Existenzielle Literale werden durch a,b,c, usw. und Universelle duch x,y,z, usw. dargestellt

12

Zusammenhang von SAT & QBF

SAT ist spezieller Fall von QBF, da SAT-Probleme implizit nur Existenz-Quantoren enthalten

Entwicklung im Bereich SAT ist in den letzten Jahren weit fortgeschritten (DP, DLL, GRASP, Chaff, BerkMin)

Ziel: SAT-Techniken erweitern, so dass diese auch auf QBF anwendbar sind

13

QUAFFLE – Ein QBF-Solver

Release: Sept. 2002 Authoren: L. Zhang, S. Malik (Chaff) Webseite:

http://www.princeton.edu/~chaff/quaffle.html Benchmarks: http://www.qbflib.org

Schwerpunkt: effizientes Learning

14

Davis-Logemann-Loveland für QBF

Die Branch-Prozedur muss die Reihenfolge der Quantifizierungen einhalten

Die deduce-Prozedur muss eine erweiterte Implikationsregel nutzen

Wurde nun eine erfüllende Belegung gefunden, so ist die Suche nicht beendet:Beide Branches von universellen Variablen müssen erfüllt sein

Backtrack, Flip und weiter

15

Davis-Logemann-Loveland für QBF

//Variable entscheiden

//Implikation

//Konfliktbehandlung

//Behandlung von //SAT–Fällen

//Ende desImplikationsdurchlaufs

//Terminierung

16

Konflikt-/SAT-Behandlung

analyse_conflict() sucht die am Konflikt beteiligte existenzielle Variable mit dem höchsten decision level, flippt diese und gibt das decision level zurück

analyse_SAT() sucht die universelle Variable mit dem höchsten decision level, flippt diese und gibt das decision level zurück

17

Wichtig

Regeln auf Klauseln lassen ausschließlich Folgerungen auf existenzielle Literale zu

Regeln auf Cubes lassen ausschließlich Folgerungen auf universelle Literale zu

18

Konfliktregel für non-tautology clauses

Gilt für eine non-tautology clause C

(1)

(alle existenziellen Literale haben den Wert 0)

(2)

(kein universelles Literal hat den Wert 1)

dann ist C eine conflicting clause (aktueller Zweig

unerfüllbar).

0)( ),( aVCEa

1)( ),( xVCUx

19

Implikationsregel für non-tautology clauses

Gilt für eine non-tautology clause C mit Literal a

(1)

alle existenziellen Literale außer a haben den Wert 0, a ist unzugewiesen.

(2)

kein universelles Literal hat den Wert 1. Wenn ein solches Literal unzugewiesen ist, ist sein Quantifizierungs-Level größer als das von a.

dann muss a den Wert 1 haben.

.)( ),( XaVCEa 0V(b) ; ),( alle abCEbFür

.1)( ),( xVCUx )()( ,)( aLxLdannXxVWenn

20

Satisfying rule für non-empty cubes

Gilt für einen non-empty cube S

(1)alle universellen Literale haben den Wert 1

(2) kein existenzielles Literal hat den Wert 0.

dann muss der Klausel-Term erfüllt sein.

1)( ),( xVSUx

0)( ),( aVSEa

21

Implikationsregel für non-empty cubesGilt für einen non-empty cube S mit Literal x

(1)alle universellen Literale außer x haben den Wert 1, x ist unzugewiesen.

(2) kein existenzielles Literal hat den Wert 0. Wenn ein solches Literal unzugewiesen ist, ist sein Quantifizierungs-Level größer als das von x.

dann muss x den Wert 0 zugewiesen bekommen (Immer universelle Variablen), damit der Zweig abgeschnitten wird (SAT-Learning).

.)( ),( XxVSUx 1V(y) ; ),( alle xySUyFür

.0)( ),( aVSEa )()( ,)( xLaLdannXaVWenn

22

Conflict Driven Learning

Ziel: Gemachte Fehler (falsche Branches) in Form von neuen Klauseln festhalten, um so den Suchraum zu verringern

Verbesserung der analyse_conflict()-Routine Lernen durch Resolution der beteiligten

Klauseln

23

Resolution

Gegeben seien zwei Klauseln und . enthält die Literale und die Literale . Die Literale und gehören der selben Variablen an, haben aber verschiedene Phasen.

Durch Anwendung von Resolution erhält man eine neue Klausel .

1C 2C1C 2C all m ,..., ,1

',..., ,, 21 alll nmm a'a

nmm llll ..., ,,..., , 11

24

Conflict Driven Learning//Learning

//Konflikt-

diagnose

25

SAT-basiertes Lernen

Wenn erfüllende Belegung für Klausel-Term gefunden, nicht unbedingt Lösung der QBF (Allquantoren)

Problem: SAT-Ansätze fokussieren auf Konflikte.Keine Technik für erfüllende Belegungen, die Allquantoren nicht erfüllen, zu lernen.

Neuer Ansatz: Satisfiability-Directed Learning

26

Cube-Generierung

Wenn erfüllende Belegung für Klausel-Term gefunden, diese als cube an die ACNF anfügen:

Beispiel:

ist erfüllende Belegung.

Zugehörigen cube in die ACNF einfügen:

Heuristiken entscheiden, welche hinzugef. werden

', ya

27

Cube-Generierung//Cube-Generator

//SAT-Analyse

28

Perfomance (1) - Quaffle im Vergleich mit anderen QBF-Solvern

29

Performance (2)

30

Zusammenfassung

Tritt ein Konflikt auf, wird eine Klausel gelernt, die unerfüllbare Zweige abschneidet

Tritt ein SAT-Fall ein, wird ein Cube gelernt, der erfüllbare Zweige abschneidet

Satisfiability-Directed-Learning nur für Instanzen sinnvoll, die viele erfüllbare Zweige mit vielen universellen Quantoren haben.

31

Vielen Dank!