10 ROZHODOVACÍ PROCEDURY A VERIFIKACE PAVEL SURYNEK, KTIML HTTP://KTIML.MFF.CUNI.CZ/~SURYNEK/NAIL094
Matematicko-fyzikální fakulta Univerzita Karlova v Praze
1
ROZHODOVÁNÍ TEORIÍ POMOCÍ SAT ŘEŠIČE (SMT) 2 | Rozhodovací procedury a verifikace, 10. přednáška
Pavel Surynek, 2015
SAT řešič a obecné teorie (1)
Budeme chtít využít efektivity SAT řešiče při rozhodování obecných teorií.
Obě technologie budou kooperovat
Nechť T je nějaká teorie (například logika s rovností a neinterpretovanými funkcemi). Budeme předpokládat existenci rozhodovací procedury pro konjunktivní fragment teorie T (rozhodované formule mají tvar konjunkce literálů) – rozhodovací procedura bude značena DECIDET. Cílem je zkonstruovat rozhodovací proceduru pro T, která bude vytvořena integrací rozhodovací procedury DECIDET a SAT řešiče.
SAT řešič vybírá literály, které je nutno splnit, aby byla splněna booleovská struktura formule. Rozhodovací procedura DECIDET kontroluje, zda je výběr provedený SAT řešičem konzistentní s teorií T.
Výhodou je efektivita, obecnost a modularita
3 | Rozhodovací procedury a verifikace, 10. přednáška
Pavel Surynek, 2015
SAT řešič a obecné teorie (2)
Teorie T bude bezkvantifikátorová teorie se signaturou Σ. Výrokové kódování literálů:
Výrokové kódování formulí v NNF tvaru:
Každému Σ-literálu l bude přiřazena výroková proměnná e(l), kterou budeme nazývat výrokovým kódem literálu l (propositional encoder). Kódování lze rozšířit na celou formuli, nechť φ je Σ-formule v NNF tvaru, potom e(φ) bude označovat výrokovou formuli, která vznikla nahrazením každého literálu ve φ jeho výrokovým kódem. Formule e(φ) se nazývá výroková kostra formule φ (propositional skeleton). Př.: Σ-literál x=y bude kódován výrokovou proměnnou e(x=y). φ := (x = y) (x = z) nechť je Σ-formule. Výroková kostra formule φ tedy je e(φ) := e(x = y) e(x = z).
SAT řešič bude pracovat nad (postupně modifikovanou) výrokovou kostrou rozhodované formule.
4 | Rozhodovací procedury a verifikace, 10. přednáška
Pavel Surynek, 2015
Integrace SAT řešiče a DECIDET (1)
Nechť T je teorie rovnosti. Uvažme formuli φ v negačně normálním tvaru (NNF), kde:
Nejprve je určena výroková kostra formule φ:
e(φ) := e(x = y) (e(y = z) e(x ≠ z)) e(x = z)).
Jelikož jsou kódovány literály a nikoli atomy, e(φ) neobsahuje žádné negace a je tedy triviálně splnitelná. Budeme používat výrokovou formuli B, která se bude postupně vyvíjet.
φ := (x = y) ((y = z x ≠ z) (x = z)).
Na začátku položíme B = e(φ).
Formule B je předložena SAT řešiči k vyřešení.
5 | Rozhodovací procedury a verifikace, 10. přednáška
Pavel Surynek, 2015
Integrace SAT řešiče a DECIDET (2)
Přepokládejme, že SAT řešič vrátil splňující ohodnocení α formule B (tedy výrokové kostry), kde:
α := { e(x = y) True, e(y = z) True, e(x ≠ z) True, e(x = z) False }
Rozhodovací procedura DECIDET bude nyní rozhodovat, zda je konjunkce literálů, která odpovídá ohodnocení výrokových kódů, splnitelná.
Množinu literálů, jež odpovídá ohodnocení α bude označována jako Th(α): Literál l je zařazen do Th(α), jestliže α(e(l)) = True. Literál l je zařazen do Th(α), jestliže α(e(l)) = False.
Th^(α) bude značit konjunkci literálů v Th(α); tedy Th^(α) = lTh(α)l. Konkrétně: Th^(α) = (x = y) (y = z) (x ≠ z) (x = z)
6 | Rozhodovací procedury a verifikace, 10. přednáška
Pavel Surynek, 2015
Integrace SAT řešiče a DECIDET (3)
Rozhodovací procedura DECIDET detekuje, že Th^(α) = (x = y) (y = z) (x ≠ z) (x = z) není splnitelná. Th^(α) je tím pádem validní. K formuli B je přidána (konjunkcí) výroková kostra e(Th^(α)), kde:
Tato formule (blokující klauzule či lemma) zakazuje ohodnocení α, to znamená, že případné nové splňující ohodnocení B musí být různé od α. Obecně lemma označujeme jako t.
e(Th^(α)) := (e(x = y) e(y = z) e(x ≠ z) e(x = z)).
Uvedená volba blokující formule není nutně nejlepší vzhledem k urychlení prohledávání.
SAT řešiči předložíme k vyřešení formuli B po modifikaci:
α’ := { e(x = y) True, e(y = z) True, e(x ≠ z) False, e(x = z) True } Tedy Th^(α’) = (x = y) (y = z) (x ≠ z) (x = z).
7 | Rozhodovací procedury a verifikace, 10. přednáška
Pavel Surynek, 2015
Integrace SAT řešiče a DECIDET (4)
Nyní je vidět, jak vypadá integrace SAT řešiče a rozhodovací procedury pro teorii T DECIDET. α
Th^(α)
SAT řešič
DECIDET e(t)
Procedura DECIDET detekuje, že formule: Th^(α’) = (x = y) (y = z) (x ≠ z) (x = z) je splnitelná.
t
Ohodnocení, které splňuje Th^(α’) rovněž splňuje původní formuli s NNF výrokovou strukturou: φ = (x = y) ((y = z x ≠ z) (x = z)).
Uvedený proces lze několika směry vylepšit:
Není třeba čekat na úplné ohodnocení formule B. Když předložíme proceduře DECIDET formuli Th^(β), kde β je částečné ohodnocení, a DECIDET odpoví, že Th^(β) je nesplnitelná. Potom je lemma t silnější, neboť blokuje všechna ohodnocení, která rozšiřují β.
8 | Rozhodovací procedury a verifikace, 10. přednáška
Pavel Surynek, 2015
Integrace SAT řešiče a DECIDET (5)
Pokračování vylepšení:
Význam může mít i situace, když DECIDET odpoví, že Th^(β) je splnitelná pro částečné ohodnocení β. V takovém případě může DECIDET odvodit nové implikace.
Situaci ilustrujeme na příkladu:
β = { e(x = y) True, e(y = z) True }
Rozhodovací procedura DECIDET obdrží formuli:
Th^(β) = (x = y) (y = z)
A může (pokud je k tomu uzpůsobená) odvodit, že Th^(β) implikuje formuli (x = z), tuto informaci je možno vrátit zpět do SAT řešiče. Předpokládejme, že DECIDET bude toto umět.
Tedy ohodnocení β (díky zpětně propagované informaci) implikuje e(x=z)True a e(x≠z)False.
Toto tzv. propagování teorií (theory propagation) lze přidat ke standardní BCP.
9 | Rozhodovací procedury a verifikace, 10. přednáška
Pavel Surynek, 2015
Líné kódování (1)
Nechť φ je Σ-formule ve tvaru NNF:
Množina všech literálů formule φ se bude značit jako lit(φ).
Zformalizujeme rozhodovací proces demonstrovaný na předchozím příkladě. Následující algoritmus odpoví, zda je vstupní formule φ splnitelná.
function LAZY-BASIC(φ): boolean B ← e(φ) while True do (result,α) ← SOLVE-SAT(B) if not result then return False else (result,t) ← DECIDET(Th^(α)) if result then return True B ← B e(t) 10 | Rozhodovací procedury a verifikace, 10. přednáška
function SOLVE-SAT(B): (boolean,assignment) Rozhodne výrokovou formuli, vrátí indikátor splnitelnosti, případně splňující ohodnocení.
φ je nesplnitelná
φ je splnitelná
function DECIDET(ψ): (boolean,formula) Rozhodne konjunktivní Σformuli ψ v teorii T, vrátí indikátor splnitelnosti, případně lemma. Pavel Surynek, 2015
Líné kódování (2)
Na formuli t, kterou vrací DECIDET, jsou kladeny jisté podmínky:
(i) Formule
t musí být validní v teorii T (tedy T-validní).
Př.: Nechť T je teorie rovnosti, pak formule ((x = y) (y = z)) (x = z) je validní v T.
může obsahovat pouze atomy, které se vyskytují v původní vstupní formuli φ. (iii) Výrokový kód formule t musí zakazovat ohodnocení α; tedy e(t) není splněna ohodnocením α.
(ii) Formule t
Podmínka (i) je postačující pro korektnost algoritmu (odpoví-li, odpoví správně), (ii) a (iii) pak garantují, že algoritmus vždy skončí (podmínka (iii) zaručuje, že se žádné ohodnocení nebude opakovat).
11 | Rozhodovací procedury a verifikace, 10. přednáška
Pavel Surynek, 2015
Integrace líného kódování a DPLL (1)
Inkrementální splnitelnost (incremental satisfiability): Nechť Bi označuje formuli B v i-té iteraci funkce LAZY-BASIC. Platí, že podmínka reprezentovaná formulí Bi+1 je silnější než Bi pro každé i=1,2,... Každou naučenou klauzuli, kterou SAT řešič odvodil při řešení Bi pro i{1,2,...}, lze použít při řešení Bj pro j > i. Jedná se o speciální případ inkrementální splnitelnosti klauzule jsou pouze přidávany (obecně se mohou klauzule i odebírat, pak je otázka, které naučené klauzule mohou být znovu použity). Volání SOLVE-SAT ve funkci LAZY-BASIC lze nahradit voláním inkrementálního SAT řešiče → zvýšení efektivity.
Lepší variantou je integrovat rozhodovací proceduru pro teorii T (tedy funkci DECIDET) přímo do procedury DPLL (na vstupu je opět Σ-formule φ ve tvaru NNF).
12 | Rozhodovací procedury a verifikace, 10. přednáška
Pavel Surynek, 2015
Integrace líného kódování a DPLL (2) function LAZY-DPLL(φ): boolean B ← CNF(e(φ)) if BCP(B,α)=NULL then return False φ je while True do nesplnitelná (x,v) ← SELECT(φ,α) if (x,v)=NULL then (result,t) ← DECIDET(Th^(α)) if result then return True φ je splnitelná B ← B e(t) while not result where (result,α) ← BCP(B,α) do (level,φ) ← ANALYZE-CONFLICT(B,α) if level < 0 then return False φ je else BACK-TRACK(B,level) nesplnitelná else α ← α ∪ {α(x)=v} while not result where (result,α) ← BCP(B,α) do (level,φ) ← ANALYZE-CONFLICT(B,α) if level < 0 then return False φ je else BACK-TRACK(B,level) nesplnitelná 13 | Rozhodovací procedury a verifikace, 10. přednáška
function CNF(B): formula Převede zadanou formuli na tvar CNF. procedure BACK-TRACK (B, level) Vrátí se na zadanou úroveň rozhodování, zruší pozdější rozhodnutí. function SELECT (B,α): (variable, boolean) Vybere neohodnocenou proměnnou vzhledem k α a její ohodnocení; vrací NULL, když všechny proměnné ohodnoceny
Pavel Surynek, 2015
Integrace líného kódování a DPLL (3)
Algoritmus je možné dále vylepšit, uvažujme formuli φ, která obsahuje celočíselnou proměnnou x1 a literály x1≥10 a x1<0 (mimo jiné).
Předpokládejme, že bylo vybráno ohodnocení e(x1≥10) True a e(x1<0) True. Rozhodovací procedura DECIDET pro T by ihned detekovala nesplnitelnost pro konjunkci těchto dvou literálů. Ovšem DECIDET je zavolána až v okamžiku, kdy ohodnocení výrokových proměnných je úplné.
Tedy ohodnocování následující po ohodnocení e(x1≥10) True a e(x1<0) True představuje zbytečnou práci.
Rozhodovací proceduru DECIDET by bylo vhodné volat už pro částečná ohodnocení výrokových kódů:
Částečná ohodnocení, která nelze rozšířit na úplná splňující, mohou být včas zakázána. Implikovaná ohodnocení mohou být vrácena zpět SAT řešiči.
Př.: Jakmile e(x1≥10) True, může DECIDET odvodit, že e(x1<0) musí být False.
14 | Rozhodovací procedury a verifikace, 10. přednáška
Pavel Surynek, 2015
Pokročilejší integrace s DPLL (1)
Na vstupu je opět Σ-formule φ ve tvaru NNF, algoritmus odpoví, zda je φ splnitelná Na formuli t se kladou další function DPLLT(φ): boolean podmínky, aby byla zaručena B ← CNF(e(φ)) konečnost algoritmu. if BCP(B,α)=NULL then return False φ je while True do nesplnitelná (x,v) ← SELECT(φ,α) φ je splnitelná, α je if (x,v)=NULL then return True úplné ohodnocení. α ← α ∪ {α(x)=v} do while not result where (result,α) ← BCP(B,α) do (level,φ) ← ANALYZE-CONFLICT(B,α) if level < 0 then return False φ je else BACK-TRACK(B,level) nesplnitelná (ignoredResult,t) ← DECIDET(Th^(α)) B ← B e(t) Zde dojde k propagaci while t ≠ True teorie T do SAT řešiče.
15 | Rozhodovací procedury a verifikace, 10. přednáška
Pavel Surynek, 2015
Pokročilejší integrace s DPLL (2)
Podmínky, které musí splňovat odvozená formule t: Formule t musí být implikována φ a musí se omezovat na atomy vyskytující se v φ. Jestliže Th^(α) je nesplnitelná, potom e(t) musí zakazovat ohodnocení α. Jestliže Th^(α) je splnitelná, potom je potřeba splnit jednu ze dvou následujících podmínek, aby byla zajištěna konečnost algoritmu:
(i) e(t) je vynucující klauzule (konfliktní klauzule taková, že obsahuje právě jeden literál z aktuální rozhodovací úrovně), po přidání e(t) k B je v rámci volání BCP ohodnocen kód nějakého literálu. (ii) Když DECIDET nedokáže najít formuli t, že e(t) je vynucující klauzule, pak t i e(t) jsou ekvivalentní hodnotě True.
Pokud jsou všechny výrokové proměnné ohodnocené a Th^(α) je splnitelná, potom nastane případ (ii).
16 | Rozhodovací procedury a verifikace, 10. přednáška
Pavel Surynek, 2015
Pokročilejší integrace s DPLL (3)
Uvažujme příklad, kdy vstupní formule φ obsahuje dva literály: x1 ≥ 10 a x1 < 0 pro celočíselnou proměnnou x1.
Máme tedy dva výrokové kódy e(x1 ≥ 10) a e(x1 < 0). Po ohodnocení α = {e(x1 < 0) True}, procedura DECIDET detekuje, že (x1 ≥ 10) je implikovaná, tedy:
Odpovídající vynucující klauzule vzhledem k ohodnocení α tedy je:
t = (x1 ≥ 10) (x1 < 0) je T-validní formule. e(t) = e(x1 ≥ 10) e(x1 < 0).
Po přidání e(t) k formuli B dojde k okamžitému odvození e(x1 < 0) (a možná k dalším odvozením).
Poznámka:
Používají se dvě varianty procedury DECIDET, jedna varianta v rámci algoritmů LAZY-BASIC a LAZY-DPLL generuje blokující klauzuli, druhá varianta v rámci DPLLT, která generuje blokující klauzule, které jsou zároveň vynucující.
17 | Rozhodovací procedury a verifikace, 10. přednáška
Pavel Surynek, 2015
