SMT-Problem und -Algorithmus (DPLL(T))

SMT-Problem
und -Algorithmus
(DPLL(T))
Sebastian Krings
Einleitung
SMT-Problem und -Algorithmus (DPLL(T))
SMT-Problem
Lazy SMT
DPLL(T)
Theorien
Kombination von
Theorien
Sebastian Krings
19.05.2015
Überblick
SMT-Problem
und -Algorithmus
(DPLL(T))
Sebastian Krings
Einleitung
SMT-Problem
Lazy SMT
DPLL(T)
Theorien
I
Einleitung und Algorithmus
I
Auswahl von Theorien
I
Kombinieren von Theorien
Kombination von
Theorien
SMT Problem
SMT-Problem
und -Algorithmus
(DPLL(T))
Sebastian Krings
Einleitung
SMT-Problem
Lazy SMT
DPLL(T)
Theorien
Entscheidungsproblem: Gegeben eine (quantorfreie?) FOL
Formel und eine (entscheidbare?) Kombination von Theorien
τ1 ∪ .. ∪ τn . Gibt es eine Belegung der freien Variablen
x1 , .., xm , so dass die Formel wahr ist?
Kombination von
Theorien
SMT Problem - Beispiel
SMT-Problem
und -Algorithmus
(DPLL(T))
Sebastian Krings
Einleitung
SMT-Problem
Lazy SMT
DPLL(T)
Theorien
φ = (x1 > 0) ∧ (x1 < 15) ∧ f (0) = f (x1 ) ⇒
(rd(wr (P, x2 , x3 ), x2 + x1 ) = x3 + 1
Kombination von
Theorien
SMT Theorie - LIA (Linear Integer Arithmetic)
SMT-Problem
und -Algorithmus
(DPLL(T))
Sebastian Krings
Einleitung
SMT-Problem
Lazy SMT
DPLL(T)
Theorien
φ = (x1 > 0) ∧ (x1 < 15) ∧ f (0) = f (x1 ) ⇒
(rd(wr (P, x2 , x3 ), x2 + x1 ) = x3 + 1
Kombination von
Theorien
SMT Theorie - EUF (Equality over Uninterpreted
Functions)
SMT-Problem
und -Algorithmus
(DPLL(T))
Sebastian Krings
Einleitung
SMT-Problem
Lazy SMT
DPLL(T)
Theorien
Kombination von
Theorien
φ = (x1 > 0) ∧ (x1 < 15) ∧ f (0) = f (x1 ) ⇒
(rd(wr (P, x2 , x3 ), x2 + x1 ) = x3 + 1
SMT Theorie - Arrays
SMT-Problem
und -Algorithmus
(DPLL(T))
Sebastian Krings
Einleitung
SMT-Problem
Lazy SMT
DPLL(T)
Theorien
φ = (x1 > 0) ∧ (x1 < 15) ∧ f (0) = f (x1 ) ⇒
(rd(wr (P, x2 , x3 ), x2 + x1 ) = x3 + 1
Kombination von
Theorien
SMT Problem - Lösung?
SMT-Problem
und -Algorithmus
(DPLL(T))
Sebastian Krings
Einleitung
SMT-Problem
Lazy SMT
DPLL(T)
Theorien
φ = (x1 > 0) ∧ (x1 < 15) ∧ f (0) = f (x1 ) ⇒
(rd(wr (P, x2 , x3 ), x2 + x1 ) = x3 + 1
Kombination von
Theorien
Lazy SMT
SMT-Problem
und -Algorithmus
(DPLL(T))
Sebastian Krings
Einleitung
SMT-Problem
Lazy SMT
DPLL(T)
I
Naiver Ansatz: Formel zu Normalform konvertieren,
Schrittweise prüfen
I
I
I
Teuer?
Immer möglich?
Lazy Ansatz: SAT Solver zur Enumeration verwenden
ohne Normalform explizit zu berechnen
Theorien
Kombination von
Theorien
Outline Algorithmus
SMT-Problem
und -Algorithmus
(DPLL(T))
Sebastian Krings
F = CNF_bool ( φ )
while true :
r e s , M = check_SAT ( F )
i f r e s == t r u e :
M’ = to_T (M)
r e s = check_T (M’ )
i f r e s == t r u e :
r e t u r n SAT
else :
F += !M
else :
r e t u r n UNSAT
SAT-level reasoning vs. Theorie?
Einleitung
SMT-Problem
Lazy SMT
DPLL(T)
Theorien
Kombination von
Theorien
SMT-Problem
und -Algorithmus
(DPLL(T))
Lazy SMT
Sebastian Krings
Einleitung
SMT-Problem
Lazy SMT
DPLL(T)
Theorien
Kombination von
Theorien
Beispiel
Online Algorithmus
SMT-Problem
und -Algorithmus
(DPLL(T))
Sebastian Krings
Einleitung
SMT-Problem
Lazy SMT
DPLL(T)
Theorien
I
Bisher: Keine enge Integration SAT / SMT
I
Theorie-Solver kann nur verwerfen oder zustimmen,
nicht steuern
I
Engere Integration im DPLL(T) Algorithmus
Kombination von
Theorien
Wishlist
SMT-Problem
und -Algorithmus
(DPLL(T))
Sebastian Krings
Einleitung
SMT-Problem
Lazy SMT
DPLL(T)
I
Backjumping und lernen innerhalb der Theorie
I
Inkrementelles Lösen
I
Propagation Theorie nach SAT
I
Frühzeitiges Verwerfen von Lösungen (in SAT Knoten
statt Blättern!)
Theorien
Kombination von
Theorien
Outline Algorithmus
d e f DPLL−T ( ) :
w h i l e True :
c o n f l i c t = False
i f unit_propagation ( ) :
r e s = T. check ( ! a l l _ a s s i g n e d ( ) )
i f r e s == F a l s e : c o n f l i c t = True
e l i f r e s == True :
c o n f l i c t = theory_propagation ()
e l i f learn_T_lemmas ( ) : c o n t i n u e
e l i f ! all_assigned ( ) : decide ()
else :
build_model ( )
r e t u r n SAT
e l s e : c o n f l i c t = True
if conflict :
lvl , cl s = conflict_analysis ()
i f l v l < 0 : r e t u r n UNSAT
else :
backtrack ( l v l )
learn ( cls )
SMT-Problem
und -Algorithmus
(DPLL(T))
Sebastian Krings
Einleitung
SMT-Problem
Lazy SMT
DPLL(T)
Theorien
Kombination von
Theorien
Equality over Uninterpreted Functions
SMT-Problem
und -Algorithmus
(DPLL(T))
Sebastian Krings
Einleitung
SMT-Problem
Lazy SMT
DPLL(T)
Theorien
I
Congruence Closure Algorithmus
I
Polynomielle Laufzeit
I
Vollständig für Gleichheit / Nicht vollständig für
Ungleichheit
Kombination von
Theorien
SMT-Problem
und -Algorithmus
(DPLL(T))
Congruence Closure
Sebastian Krings
Einleitung
SMT-Problem
Lazy SMT
DPLL(T)
Theorien
Kombination von
Theorien
Beispiel
Lineare Integer Arithmetik
SMT-Problem
und -Algorithmus
(DPLL(T))
Sebastian Krings
Einleitung
I
Beispiel: Σxi = 15
I
NP vollständiges Problem
Häufig numerische Verfahren + Branch and Bound
I
I
I
I
Numerische / approximative Lösung
Branch and Bound: φ := φ ∧ (x ≤ c ∨ c ≤ x)
Entscheidbare Unterprobleme durch eigene Algorithmen
I
I
Gleichheit
Difference Logic
SMT-Problem
Lazy SMT
DPLL(T)
Theorien
Kombination von
Theorien
Lineare Arithmetik auf Rationals
SMT-Problem
und -Algorithmus
(DPLL(T))
Sebastian Krings
Einleitung
SMT-Problem
Lazy SMT
DPLL(T)
Theorien
I
Beispiel: Σai ∗ xi = 15
I
Numerische Lösungsverfahren (Simplex Algorithmus)
I
Exponentielle Worst-Case-Laufzeit, meist aber schnell
Kombination von
Theorien
Bitvektoren
SMT-Problem
und -Algorithmus
(DPLL(T))
Sebastian Krings
Einleitung
SMT-Problem
Lazy SMT
DPLL(T)
Theorien
I
Beispiele: xor / and, ....
I
Rewriting (z.B. zu Integer)
Bit-Blasting
I
I
Constraints auf einzelnen Bits, dann SAT Solver
Kombination von
Theorien
Eager Bit-Blasing
SMT-Problem
und -Algorithmus
(DPLL(T))
Sebastian Krings
Einleitung
SMT-Problem
Lazy SMT
DPLL(T)
Theorien
I
Komplette Formel wird aufgeblasen
I
Verlässt DPLL
I
Schwierig mit anderen Theorien zu Kombinieren
Kombination von
Theorien
Lazy Bit-Blasing
SMT-Problem
und -Algorithmus
(DPLL(T))
Sebastian Krings
Einleitung
SMT-Problem
Lazy SMT
DPLL(T)
Theorien
I
Nur Bitvektoren werden aufgeblasen
I
Nur wenn von DPLL verlangt
I
Leichter zu Kombinieren
I
In Praxis derzeit langsamer
Kombination von
Theorien
SMT Problem - Beispiel
SMT-Problem
und -Algorithmus
(DPLL(T))
Sebastian Krings
Einleitung
SMT-Problem
Lazy SMT
DPLL(T)
Theorien
φ = (x1 > 0) ∧ (x1 < 15) ∧ f (0) = f (x1 ) ⇒
(rd(wr (P, x2 , x3 ), x2 + x1 ) = x3 + 1
Mehr als eine Theorie!
Kombination von
Theorien
Kombination von Theorien
SMT-Problem
und -Algorithmus
(DPLL(T))
Sebastian Krings
Einleitung
SMT-Problem
Lazy SMT
DPLL(T)
I
I
Wir haben DPLL(T)
Offene Fragen:
I
I
I
Wie kommen wir zu DPLL(T1 , ..., Tn )?
Können bestehende Solver weiter verwendet werden?
Wenn ja wann?
Performance?
Theorien
Kombination von
Theorien
Nelson-Oppen-Kombination
SMT-Problem
und -Algorithmus
(DPLL(T))
Sebastian Krings
Einleitung
SMT-Problem
Lazy SMT
DPLL(T)
I
I
Kombinationstechnik für Solver
Voraussetzungen:
I
I
I
Signaturen sind disjunkt
Erfüllbaren Formeln sind erfüllbar in einem unendlichen
Model
Formeln enthalten keine Quantoren
Theorien
Kombination von
Theorien
Nelson-Oppen-Kombination
SMT-Problem
und -Algorithmus
(DPLL(T))
Sebastian Krings
Einleitung
SMT-Problem
Lazy SMT
DPLL(T)
Theorien
I
I
Kombinationstechnik für Solver
Idee:
I
I
Umformen so dass Logiken getrennt
Kommunikation über geteilte Variablen
Kombination von
Theorien
Nelson-Oppen-Kombination
SMT-Problem
und -Algorithmus
(DPLL(T))
Sebastian Krings
Einleitung
SMT-Problem
Lazy SMT
DPLL(T)
Theorien
Kombination von
Theorien
Beispiel

Download Report