SAT problém

V teoretické informatiky se SAT problém nebo problém satisfiability Boolean je rozhodovací problém , který vzhledem k logiky výrokové formule , určuje, zda existuje přiřazení výrokových proměnných, které dělá formule pravdivá.

Tento problém je v teorii složitosti velmi důležitý . Vyneslo to na světlo Cookova věta , která je základem teorie NP-úplnosti a problému P = NP . Problém SAT má také mnoho aplikací, zejména v oblasti omezení spokojenosti , klasického plánování , kontroly modelů , diagnostiky a dokonce i konfigurátoru PC nebo jeho operačního systému: vracíme se k výrokovým vzorcům a používáme SAT solver .

Terminologie

Vzorce výrokové logiky

Vzorce výrokové logiky jsou sestaveny z výrokových proměnných a booleovských spojek „a“ ( ), „nebo“ ( ), „ne“ ( ). Vzorec je uspokojivý (říkáme také uspokojivý ), pokud existuje přiřazení výrokových proměnných, díky nimž je vzorec logicky pravdivý. Například : $\ přistát$ $\ lor$ $\ lnot$

Vzorec je uspokojivý, protože pokud má hodnotu false, vzorec se vyhodnotí jako true. ${\ Displaystyle (p \ land q) \ lor \ lnot p}$ $p$
Vzorec je neuspokojivý, protože žádná hodnota p nemůže vzorec učinit pravdivým. ${\ displaystyle (p \ land \ lnot p)}$

Spojovací věty a normální forma

Doslovný je výrokové proměnné (pozitivní doslovný) nebo negací výrokové proměnné (negativní doslovný). Klauzule je disjunkce formuláře , kde jsou literály. $\ Ell$ $v_ {j}$ ${\ displaystyle \ lnot v_ {j}}$ ${\ displaystyle {\ overset {n} {\ underset {i = 1} {\ bigvee}}} \ ell _ {i} = (\ ell _ {1} \ lor \ ell _ {2} \ lor \ ldots \ lor \ ell _ {n})}$ $\ ell _ {i}$

Výrokový vzorec kalkulu je v konjunktivní normální formě (nebo klauze nebo CNF pro anglickou konjunktivní normální formu ), pokud se jedná o spojení vět.

PříkladDovolit je množina proměnných a vzorec .

\ {v_ {1}, v_ {2}, v_ {3} \} \

f = (v_ {1} \ lor v_ {2}) \ land (\ neg v_ {1} \ lor v_ {3}) \ land (\ neg v_ {2} \ lor \ neg v_ {1})

{\ displaystyle (v_ {1} \ lor v_ {2})}

, a jsou klauze se dvěma literály na klauzuli.

{\ displaystyle (\ neg v_ {1} \ lor v_ {3})}

{\ displaystyle (\ neg v_ {2} \ lor \ neg v_ {1})}

Jejich konjunkce je normální konjunktivní forma.

F

Není-li výrokový vzorec v konjunktivní normální formě, můžeme jej transformovat do ekvivalentní konjunktivní normální formy maximálně exponenciální velikosti v počátečním vzorci. Můžeme ji také transformovat do ekvisatibovatelné konjunktivní normální formy lineární velikosti v počátečním vzorci.

Omezení problému SAT

Zvažujeme syntaktická omezení problému SAT.

Problém CNF-SAT je omezení SAT problému na normální spojovací formy.
Problém 2-SAT je omezení problému SAT na konjunktivní normální tvary s maximálně 2 literály na klauzuli.
Problém 3-SAT je omezení problému SAT na konjunktivní normální tvary s maximálně 3 literály na klauzuli.
- Příklad instance: . $(v_ {1} \ lor \ neg v_ {2} \ lor v_ {3}) \ land (\ neg v_ {1} \ lor v_ {3} \ lor v_ {4})$
Problém HORN-SAT je omezení SAT problému na konjunktivní normální tvary, kde věty jsou Hornovy věty .

Složitost a omezení

CNF-SAT

SAT problém je NP - úplný problém podle Cookovy věty . Zejména není známo, že by jej vyřešil žádný deterministický polynomiální algoritmus. Podobně, protože jakýkoli vzorec může být v počátečním vzorci transformován do ekvisatibovatelné konjunktivní normální formy lineární velikosti, je problém CNF-SAT také NP-úplný .

3-SAT

Problém 3 - SAT je také NP - úplný. K prokázání NP-obtížnosti 3-SAT stačí prokázat, že problém CNF-SAT je polynomiálně redukovatelný na 3-SAT. Snížení transformuje každý klauzule se do . ${\ displaystyle \ ell _ {1} \ lor \ ell _ {2} \ lor \ ldots \ lor \ ell _ {n}}$ $n \ geq 3$ ${\ displaystyle (\ ell _ {1} \ lor \ ell _ {2} \ lor u_ {1}) \ land (\ ell _ {3} \ lor \ lnot u_ {1} \ lor u_ {2}) \ land \ ldots \ land (\ ell _ {n-2} \ lor \ lnot u_ {n-4} \ lor u_ {n-3}) \ land (\ ell _ {n-1} \ lor \ ell _ { n} \ lor \ lnot u_ {n-3})}$

2-SAT

Problém 2-SAT je omezení problému SAT na konjunktivní normální tvary s maximálně 2 literály na klauzuli. Tento problém je ve třídě P . Za předpokladu , že to není NP-úplné. Existuje několik deterministických polynomiálních algoritmů k řešení problému 2-SAT. $P \ neq NP$

Algoritmus Aspvalla, Plassa a Tarjana Algoritmus má konjunktivní vzorec normální formy s maximálně 2 literály na klauzuli.

\ varphi

Klauzule druhého řádu je ekvivalentní implikacím a .

v_ {1} \ lor v_ {2}

\ lnot v_ {1} \ rightarrow v_ {2}

\ lnot v_ {2} \ rightarrow v_ {1}

Abychom vyřešili 2-SAT, zkonstruujeme duální směrovaný graf (nazývaný 2-SAT graf) podle následujících dvou pravidel:

vrcholy jsou výrokové proměnné ve vzorci a negace výrokových proměnných ve vzorci; $v_ {i} \,$ $\ lnot v_ {i} \,$ $v_ {i} \,$
přidáme oblouky a pro každou klauzuli . $(\ lnot v_ {1}, v_ {2})$ $(\ lnot v_ {2}, v_ {1})$ $v_ {1} \ lor v_ {2}$

Vzorec je splnitelná právě tehdy, když pro každou výrokové proměnné z , a jsou rozděleny do dvou odlišných pevně spojených prvků v 2-SAT grafu. Poté použijeme Tarjanův algoritmus (nebo Kosarajuův algoritmus ) k výpočtu silně propojených komponent 2-SAT grafu.

\ varphi

v_ {i} ~

\ varphi

v_ {i} ~

\ lnot v_ {i}

Christos Papadimitriou v roce 1994 ukázal, že problém 2-SAT je úplný NL .

HORN-SAT

Problém satisfiability z množiny výrokových doložek Horn (to znamená, že se nanejvýš jeden pozitivní literál doložkou) je ve třídě P . Přesněji řečeno, existuje lineární algoritmus o velikosti vět, který řeší problém uspokojivosti. Je P-kompletní (pro zmenšení logaritmického prostoru ).

Schaeferova věta o dichotomii

Schaeferova věta dává nezbytné a dostatečné podmínky pro to, aby varianta SAT problému mohla být ve třídě P nebo NP - úplná . Zjistili jsme výsledky složitosti týkající se 3-SAT (NP-kompletní), 2-SAT (v P), HORN-SAT (v P) jako aplikací této věty.

Algoritmy pro SAT

Nejviditelnější metodou řešení problému SAT je procházení pravdivostní tabulky problému, ale složitost je pak exponenciální ve srovnání s počtem proměnných.

Systematická metoda

K prokázání uspokojivosti CNF stačí zvolit proměnnou a rekurzivně prokázat uspokojivost nebo . Postup je rekurzivně jednodušší, protože s nebo může být často zjednodušen. Rekurzivní volání, takže vytvoří binární strom ve vyhledávání . $\ phi \$ $v ~$ $v \ land \ phi$ $\ neg v \ land \ phi$ $\ land \ phi$ $a = v \$ $a = \ neg v$

Obecně jsou v každém uzlu jednotkové klauze (CNF je ve tvaru ), které umožňují výrazně omezit prostor pro vyhledávání. $\ phi = a \ land \ phi '$

Příklad Zvažte CNF:

(v_ {1} \ lor \ neg v_ {2}) \ land \ neg v_ {3} \ land (v_ {3} \ lor \ neg v_ {1})

. Druhá klauzule ( ) je jednotná a umožňuje ji získat okamžitě . Můžeme nahradit hodnoty v tomto CNF. To dává:

\ neg v_ {3}

v_ {3} = {\ textit {false}}

v_ {3}

(v_ {1} \ lor \ neg v_ {2}) \ land \ neg {\ textit {false}} \ land ({\ textit {false}} \ lor \ neg v_ {1}) = (v_ {1} \ lor \ neg v_ {2}) \ land \ neg v_ {1}

. Opět máme unitární klauzuli a máme . Pak množením získáme .

v_ {1} = {\ textit {false}} ~

v_ {2} = {\ textit {false}} ~

V tomto příkladu jsme našli hodnoty tří proměnných, aniž bychom rozšířili vyhledávací strom. Obecně lze prostor pro vyhledávání značně zmenšit. Na druhou stranu, pokud se proměnná v CNF vždy objeví pozitivně , pak můžeme představovat, protože je uspokojivá, právě když je uspokojivá (a podobně, pokud se proměnná objeví záporně). V předchozím příkladu se tedy jeví pouze negativně a přiřazení lze provést. Všimněte si, že toto přiřazení umožňuje urychlit objevování řešení, ale tato řešení by mohla existovat provedením opačného přiřazení. Na těchto myšlenkách je založen algoritmus DPLL (Davis, Putnam, Davis, Logemann, Loveland). $v \$ $\ phi \$ $v = {\ textit {true}} \$ $\ phi \$ $\ phi \ land v$ $v_ {2} \$ $v_ {2} = false \$

Volba proměnné, která má být vyvinuta, je velmi důležitá pro výkon SAT algoritmů. Obecně volíme proměnné, které se nejčastěji objevují, pokud je to možné v klauzulích velikosti 2. $v \$

Učební klauze podle konfliktů

Princip řešitelů CDCL (Conflict-Driven Clause Learning) je použít mechanismus k učení nových klauzulí během hledání, poté maximálně využít informace získané v naději na zkrácení doby hledání. Z praktického hlediska je tato metodika při řešení konkrétních problémů velmi účinná. Učení klauzulí je následující: když se během vyhledávání objeví konflikt, tj. Když se ukáže, že částečné přiřazení není v souladu se sadou klauzulí, můžeme izolovat podmnožinu těchto přiřazení a podmnožinu těchto klauzulí, které jsou odpovědné pro konflikt (přiřazení neodpovídají doložkám). Klauzule učení dělá dvě věci. Nejprve se vyhne opakování stejných chyb několikrát ve stromu vyhledávání. Zadruhé, naučená klauzule bude v rozporu se stavem vyhledávacího stromu. Proto bude nutné provést backtracking, aby bylo zajištěno, že alespoň jeden z těchto literálů je pravdivý.

Existují různé metody pro generování nových klauzulí z místní nekonzistence.

Naivní metoda

Nechť instance, která má být vyřešena, má následující vzorec : $\ phi _ {1}$

{\ begin {array} {rcl} C_ {1} & = & x_ {1} \ lor x_ {2} \\ C_ {2} & = & \ neg x_ {1} \ lor x_ {3} \\\ konec {pole}}

a částečné interpretace definovány: . Tato interpretace vede ke konfliktu, protože to naznačuje , zatímco to naznačuje . Generovat klauzule představující tento konflikt, je možné vzít negaci interpretace : . Tato metoda má však jednu hlavní nevýhodu: velikost klauzule je zcela určena celou interpretací. Některé části výkladu však mohou být zcela nezávislé na konfliktu, který si přejeme představit. Ve skutečnosti přidáme do instance vzorce: a buď aktuální interpretaci . Konflikt vzniká z prvních dvou klauzulí, a tedy z hodnot a . Klauzule generovaná negací interpretace však zohlední všechny proměnné kromě . Výsledkem bude doložka zbytečně dlouhá. ${\ mathcal {I}}$ $x_ {2} = {\ textit {false}}, x_ {3} = {\ textit {false}}$ $x_ {2}$ $x_ {1} = pravda$ $x_ {3}$ $x_ {1} = false$ ${\ mathcal {I}}$ $\ neg {\ mathcal {I}} = \ neg (\ neg x_ {2} \ land \ neg x_ {3}) = x_ {2} \ lor x_ {3}$ $\ phi _ {1}$ $C _ {{i}} = x_ {i} \ lor x _ {{i + 1}}, 4 \ leq i \ leq N$ ${\ mathcal {I}} = \ {x_ {2} = false, x_ {3} = false, x _ {{4 \ leq i \ leq N}} = false \}$ $x_ {2}$ $x_ {3}$ $x_ {1}$

Analýza konfliktů

Když se použije tato metoda, vytvoří se graf, který představuje počátek šíření, tzv. Implikační graf. Uzly představují skutečné literály. Existují dva typy uzlů: čtvercové uzly, jejichž doslovná hodnota pochází z libovolné volby a kulaté uzly, jejichž hodnota pochází z šíření. S každým uzlem jsou spojeny také informace: úroveň daného uzlu. Tato úroveň je definována počtem literálů vybraných před provedením šíření, pokud došlo k šíření. Jinak je úroveň definována počtem vybraných literálů, včetně aktuálního literálu. Oblouky propojují literály, které jsou součástí klauzule šíření. Cíl oblouku je šířený literál, přičemž zdrojem (zdroji) jsou ostatní literály v klauzuli. Nechť instance, která má být vyřešena, má následující vzorec : $\ phi _ {2}$

{\ displaystyle {\ begin {array} {rcl} C_ {1} & = & \ neg d \ lor f \\ C_ {2} & = & \ neg d \ lor \ neg e \ lor g \\ C_ {3 } & = & \ neg h \ lor j \\ C_ {4} & = & \ neg h \ lor i \\ C_ {5} & = & \ neg i \ lor a \\ C_ {6} & = & \ neg g \ lor \ neg i \ lor b \\ C_ {7} & = & \ neg a \ lor c \\ C_ {8} & = & \ neg b \ lor \ neg c \ end {pole}}}

doprovázen výkladem, které jsou specifikovány úrovně různých literálů stejně jako doslovný vedoucí k nesouladu: . Poté je možné z něj nakreslit následující graf. ${\ mathcal {I}} = \ {d | _ {1}, f | _ {1}, e | _ {2}, g | _ {2}, h | _ {3}, i | _ {3 }, j | _ {3}, a | _ {3}, b | _ {3}, c | _ {3} \}$ $\ neg c$

Díky tomuto grafu je možné vytvořit klauzuli představující příčinu konfliktu. Použitá metoda je následující: začneme vytvořením překladače klauzulí vedoucích ke konfliktu. Pak, pokud existuje více než jeden literál aktuální úrovně, vytvoří se nové resolvent mezi aktuálním resolventem a příčinou jednoho z literálů aktuální úrovně. V našem příkladu to dá (kde představuje rozlišení mezi klauzí a klauzí ) ${\ mathcal {R}} _ {1}$ ${\ mathcal {R}} _ {{i + 1}}$ ${\ mathcal {R}} _ {i}$ $C_ {i} \ vdash _ {{\ mathcal {R}}} C_ {j}$ $Tento}$ $C_ {j}$

{\ begin {array} {rcccl} {\ mathcal {R}} _ {1} & = & C_ {7} \ vdash _ {{\ mathcal {R}}} C_ {8} & = & \ neg a \ lor \ neg b \\ {\ mathcal {R}} _ {2} & = & {\ mathcal {R}} _ {1} \ vdash _ {{\ mathcal {R}}} C_ {6} & = & \ neg g \ lor \ neg i \ lor \ neg a \\ {\ mathcal {R}} _ {3} & = & {\ mathcal {R}} _ {2} \ vdash _ {{\ mathcal {R} }} C_ {5} & = & \ neg g \ lor \ neg i \\ {\ mathcal {R}} _ {4} & = & {\ mathcal {R}} _ {3} \ vdash _ {{\ mathcal {R}}} C_ {4} & = & \ neg h \ lor \ neg g. \ End {pole}}

Nechronologické zpětné sledování

Jakmile se klauzule naučí, bude použita pro vrácení zpět. Myšlenkou nechronologického vrácení zpět je, že vrácení bude provedeno tak, že stav přiřazení je takový, že zůstane pouze jeden nepřiřazený literál. Díky naučené klauzi bude tedy možné pokračovat v různých propagacích, když to bez ní již nebude možné.

Vezmeme-li příklad uvedený v části analýzy konfliktů, naučená klauzule nám dá dva literály. Úrovně odpovídajících proměnných jsou: proměnná = 3, proměnná = 2. Chcete-li vědět, na které úrovni je nutné se vrátit, musíte se podívat na nejhlubší úroveň (úroveň je hlubší než úroveň ) proměnných jedné úroveň vyšší než aktuální úroveň. Protože naučená klauzule obsahuje pouze dva literály, existuje pouze jedna úroveň odlišná od aktuální úrovně: úroveň 2. Vrátení zpět se proto provádí až po tuto úroveň, a proto se ponechává jako interpretace . S takovou interpretací však naučená klauzule obsahuje pouze jednu nepřiřazenou proměnnou: zatímco druhá je ovlivněna takovým způsobem, že literál je nepravdivý. To znamená, že je nutné šířit proměnnou na hodnotu false. $\ phi _ {2}$ ${\ mathcal {R}} _ {4} = \ neg h \ lor \ neg g$ $h$ $G$ $i + 1$ $i$ ${\ mathcal {I}} = \ {d | _ {1}, f | _ {1}, e | _ {2}, g | _ {2} \}$ $h$ $\ neg g$ $h$

Ačkoli v tomto příkladu je vrácení zpět provedeno pouze na jedné úrovni, je možné, že jde nahoru několik úrovní najednou. Představte si, že můžeme přidat N úrovní mezi úrovní 2 a úrovní 3, kde všechny proměnné, které se tam objevují, jsou nové proměnné. Vzhledem k tomu, že tyto úrovně by neměly žádný dopad na starou úroveň 3, vrácení zpět by tyto úrovně N + 1 náhle zvýšilo.

Perspektivní přístupy

Prospektivní přístup spočívá v prozkoumání výzkumného stromu za účelem zjištění určitých úkolů. Proto, vzhledem k CNF , dána uninstantiated proměnné , na CNFs a hledali . Pokud dva CNF vedou k vytvoření instance stejné proměnné se stejnou hodnotou, pak lze vytvořit instanci z CNF . $\ phi \$ $v \$ $\ phi \ land v$ $\ phi \ land \ neg v$ $v '$ $\ phi \$

Příklad Zvažte CNF . Zajímáme se zde o proměnnou a proměnnou prospektujeme .

\ phi = (v_ {1} \ lor v_ {2}) \ land (v_ {1} \ lor \ neg v_ {2} \ lor v_ {3}) \ land (\ neg v_ {1} \ lor v_ { 2} \ lor v_ {4}) \ land (\ neg v_ {3} \ lor \ neg v_ {4})

v_ {2} \

v_ {1} \

Zvažte zadání . Získáváme a tedy přiřazení (protože se tato proměnná zobrazuje pouze pozitivně).

v_ {1} = {\ textit {true}} \

(v_ {2} \ lor v_ {4}) \ land (\ neg v_ {3} \ lor \ neg v_ {4})

v_ {2} = {\ textit {true}} \

Zvažte zadání . Získáváme, a proto je přiřazení jednotkovou klauzí.

v_ {1} = {\ textit {false}} \

v_ {2} \ land (\ neg v_ {2} \ lor v_ {3}) \ land (\ neg v_ {3} \ lor \ neg v_ {4})

v_ {2} = {\ textit {true}} \

Ve všech případech je toto přiřazení získáno a je proto možné z CNF .

v_ {2} = {\ textit {true}} \

\ phi \

Připomeňme, že složitost problému SAT pochází z exponenciální velikosti vyhledávacího stromu ve srovnání s počtem proměnných. Prospektování umožňuje výrazně snížit tento počet proměnných z kořenového adresáře (nebo kteréhokoli uzlu stromu) s relativně nízkou dodatečnou složitostí s ohledem na zmenšení vyhledávacího stromu.

Dynamický program

Samer a Szeider navrhli dynamický programový algoritmus FTP, kde byla šířka stromu grafu spojená s testovaným vzorcem. Výhodou tohoto algoritmu je, že umí také počítat ocenění a proto vyřešte problém #SAT. Může být také paralelizován . Je implementován v nástroji gpuSAT (paralelizace je implementována pomocí GPU).

Místní vyhledávání

Počínaje přiřazením všech proměnných se pokusíme upravit určitá ocenění, abychom snížili počet nesplněných klauzulí. Tento algoritmus trpí několika nedostatky: může spadat do lokálních minim a není schopen prokázat neuspokojivost, ale je velmi účinný při nestrukturovaných problémech (tj. Často problémech generovaných náhodně). V případě selhání po delší době je možné zvolit nové náhodné přiřazení, aby se zabránilo místním minimům.

Aplikace

Je možné omezit (přeložit) některé problémy umělé inteligence na problém SAT, aby bylo možné tyto problémy efektivně vyřešit.

Diagnostický

Diagnóza statických systémů spočívá ve stanovení, zda se systém chová zavinění vzhledem k pozorování vstupů a výstupů systému. Model systému lze přeložit do sady omezení (disjunkce): pro každou komponentu systému se vytvoří proměnná, která se vyhodnotí jako pravdivá, pokud má komponenta neobvyklé chování ( Ab normal ). Pozorování lze také přeložit řadou disjunkce. Přiřazení nalezené algoritmem uspokojivosti je diagnostické. $vs.$ $ABC)$

Klasické plánování

Klasickým problémem plánování je najít sled akcí vedoucích z jednoho stavu systému do sady stavů. Vzhledem k maximální délce roviny a množině booleovských stavových proměnných použitých k popisu stavu systému vytváříme pro každou proměnnou výrokové proměnné . Proměnná je true, pokud je stavová proměnná true po čísle akce . Vytváříme také proměnné pro všechno a jakoukoli akci . Proměnná je pravdivá, pokud je číslo akce . Potom je možné transformovat model systému na sadu klauzulí. Například pokud akce způsobí, že proměnná projde na true, když je nepravdivá , pak CNF bude obsahovat klauzuli (která je přeložena klauzulí ). Přiřazení nalezené algoritmem uspokojivosti lze okamžitě přeložit do plánu. $ne$ $PROTI$ $v ^ {i}$ $i \ in \ {0, \ dots, n \}$ $v \ ve V$ $v_ {i}$ $i$ $a ^ {i}$ $i \ in \ {1, \ dots, n \}$ $na$ $a ^ {i}$ $i$ $na$ $na$ $v_ {1}$ $(\ neg v ^ {0}) \ Rightarrow a ^ {1} \ Rightarrow v ^ {1}$ ${\ displaystyle v ^ {0} \ lor \ neg a ^ {1} \ lor v ^ {1}}$

Klasické plánování pomocí SAT je velmi efektivní, pokud známe délku n roviny . Pokud tato hodnota není známa, lze hledat plány pro přírůstkovou hodnotu, která je někdy drahá (zejména proto, že CNF není uspokojivá až do n - 1).

Kontrola modelu

Podobný přístup byl použit pro kontrolu modelu . Hlavní rozdíl spočívá v tom, že kontrola modelu se na rozdíl od plánování vztahuje na trajektorie nekonečné délky. Pokud je však stavový prostor systému konečný, v určitém bodě se smyčky nekonečné trajektorie smyčí a my můžeme omezit velikost trajektorií, kterou je nutné ověřit. Checking ohraničené modelem využívá této vlastnosti transformovat problém model checking v celé řadě problémů splnitelnosti.

Kryptografie

Složitost problému SAT je podstatnou součástí zabezpečení jakéhokoli krypto systému.

Například funkce bezpečného hash představuje černou skříňku, kterou lze v konečném čase a prostoru formulovat jako spojení normálních klauzulí, jejichž logické proměnné přímo odpovídají možným hodnotám vstupních dat funkce. Hash, a každá z výsledných bitů bude reagovat na booleovský test rovnosti s datovými bity libovolného vstupního datového bloku. Funkce bezpečného hašování se používají zejména v autentizačních systémech (znalost tajných vstupních dat použitých k vytvoření hodnoty hash) a podpisu (proti jakékoli „snadné“ změně nebo padělání vstupních dat, které jsou známé spolu s funkcí hash samotnou a jeho výsledek).

Zabezpečení hashovací funkce závisí na možnosti načtení libovolného vstupního datového bloku (možná odlišného od tajného datového bloku, pro který byla získána daná hash hodnota), což umožňuje vyrovnat binární hodnotu vrácenou hashovací funkcí. Metoda systematického zkoumání všech možných hodnot vstupních dat, pro které je hashovací funkce použita jako věštec, účinně umožňuje uspokojit otázku hashové hodnoty, která je stejná jako hledaná, ale její algoritmická složitost bude být exponenciální (v závislosti na maximální bitové velikosti vstupních dat hash funkce).

Pokus o vyrovnání hodnoty hash se vstupními proměnnými neznámé hodnoty je problém SAT (a protože v praxi se vstupní data funkce hash skládají z mnoha bitů, bude to problém n -SAT s n poměrně vysokou hodnotou (a v každém případě větší nebo rovný 3) Víme tedy, že tento problém je v polynomiálním čase redukovatelný na problém 3 - SAT, který je NP-úplný.

Zabezpečení hashovací funkce bude silně spojeno se skutečností, že je nemožné ji jednodušeji omezit (než pomocí NP-úplného algoritmu dostatečné složitosti) snížením spojovací formy vět, které ji jednoduše definují, aby bylo možné izolovat podmnožiny vstupních proměnných menší velikosti, ale dostatečné k určení části výsledku hashovací funkce, jejíž pořadí n pak bude mnohem nižší, a k tomu, aby již nebylo nutné zkoumat pouze možné hodnoty těchto pouze podmnožin proměnných pro splnění podmínky rovnosti výsledku, aniž by bylo nutné testovat všechny ostatní proměnné, jejichž hodnota může být libovolně nastavena na určité hodnoty určené jednodušším algoritmem (osvojení klauzí, perspektivní přístupy výše).

Modální logika

Problém SAT lze použít jako podprogram k vyřešení problému uspokojivosti modální logiky.

Rozšíření

Problém SAT je rozšířen.

Kvantovaný booleovský vzorec
Teorie modulové uspokojivosti (SMT)
UNIQUE-SAT: připouští výrokový vzorec jedinečné přiřazení výrokových proměnných?
MAX-SAT: vzhledem k sadě klauzulí najděte maximální počet klauzulí, které lze splnit.
Problém spokojenosti s omezením
Satisfiability v modální logiky , prvního řádu logiku , druhého řádu logiku ...

Historický

Martin Davis a Hilary Putnam nabízejí jejich algoritmus pro problém SAT v roce 1960, pak se zlepšil George Logemann a Donald Loveland (ne) ( algoritmus Davis-Putnam-Logemann-Loveland ). Hybnost byla dána, když ji Stephen Cook použil jako paradigma NP-úplných problémů . Další impuls byl dán v roce 2002, kdy začala konkurence SAT mezi softwarem pro řešení problémů SAT.

Poznámky a odkazy

Inês Lynce a Joël Ouaknine , „ Sudoku jako SAT problém “, Proc. devátého mezinárodního sympozia o umělé inteligenci a matematice , Springer,1 st 01. 2006( číst online , konzultováno 10. května 2016 )
Stephen A. Cook , „ Složitost postupů dokazujících věty “, Computing Surveys (CSUR) , ACM, sTOC '71,1 st 01. 1971, str. 151–158 ( DOI 10.1145 / 800157.805047 , číst online , přístup k 30. prosinci 2015 )
Boris A. Trakhtenbrot , „ Přehled ruských přístupů k algoritmům Perebor (vyhledávání hrubou silou) “, Annals of the History of Computing , sv. 6,1 st říjen 1984,, str. 384-400 ( ISSN 0164-1239 , DOI 10.1109 / MAHC.1984.10036 , číst online , přístup k 30. prosinci 2015 )
(in) A. Biere , A. Beer , Mr. Heule a H. van Maaren , Handbook of Satisfiability: Volume 185 Frontiers in Artificial Intelligence and Applications , Amsterdam, IOS Press,15. února 2009, 966 s. ( ISBN 978-1-58603-929-5 a 1-58603-929-6 , číst online )
„ Uspokojivé “ , na CNRTL .
„ Splnitelné “ , na Larousse .
(in) Bengt Aspvall, Michael F. Plass a Robert E. Tarjan, „ Algoritmus lineárního času pro testování pravdivosti některých kvantifikovaných booleovských vzorců “, Information Processing Letters , 8, s. 1. 121-123 (1979), [ číst online ] .
William F. Dowling a Jean H. Gallier , „ Algoritmy lineárního času pro testování uspokojivosti výrokových vzorců klaksonu “, The Journal of Logic Programming , sv. 1,1 st říjen 1984,, str. 267-284 ( DOI 10.1016 / 0743-1066 (84) 90014-1 , číst online , přístup k 31. prosinci 2015 )
Neil D. Jones a William T. Laaser , „ Kompletní problémy pro deterministický polynomiální čas “, Theoretical Computer Science , sv. 3, n o 1,Říjen 1976, str. 105–117 ( ISSN 0304-3975 , DOI 10.1016 / 0304-3975 (76) 90068-2 , číst online , přístup k 6. září 2018 )
Thomas J. Schaefer (1978). „Problémy se složitostí uspokojivosti“ STOC 1978 : 216–226 s. ( DOI : 10,1145 / 800133,804350 ).
(en) Martin Davis a Hillary Putnam, „Výpočetní postup pro teorii kvantifikace“, Sdělení ACM , 7, s. 201-215 (1960) [ číst online ]
(en) Martin Davis, George Logemann a Donald Loveland, „Strojový program pro prokázání věty“, Komunikace ACM , 5, s. 2 394-397 (1962), [ číst online ]
během SAT Challenge 2012, kategorie aplikace | So výzva 2012
(in) Stefan Szeider , Theory and Applications of Satisfiability Testing , Springer Berlin Heidelberg,2004( ISBN 978-3-540-20851-8 a 9783540246053 , DOI 10.1007 / 978-3-540-24605-3_15 , číst online ) , s. 188–202
Jean-Marie Lagniez , Daniel Le Berre , Tiago de Lima a Valentin Montmirail , „ Rekurzivní zkratka pro CEGAR: Aplikace na modální logiku K Problém uspokojivosti “, Sborník z dvacáté šesté mezinárodní společné konference o umělé inteligenci , mezinárodní společné konference o organizaci umělé inteligence,srpna 2017, str. 674-680 ( ISBN 9780999241103 , DOI 10,24963 / ijcai.2017 / 94 , číst on-line , přístupný 1 st září 2018 )
(in) Thomas Caridroit, Jean-Marie Lagniez Daniel Le Berre, Tiago Lima Valentin Montmirail „ Přístup založený na SAT k řešení problému uspokojivosti modální logiky S5 “ , Sborník z třicáté první {AAAI} konference o umělé inteligenci, San Francisco, Kalifornie, {USA.} , 4. – 9. Února 2017, s. 3864--3870 ( číst online )
(en-US) R. Sebastiani a M. Vescovi , „ Automated Reasoning in Modal and Description Logics via SAT Encoding: the Case Study of K (m) / ALC-Satisfiability “ , Journal of Artificial Intelligence Research , sv. 35,25. června 2009, str. 343-389 ( ISSN 1076 - 9757 , DOI 10,1613 / jair.2675 , číst on-line , přístupný 1 st září 2018 )
Soutěžní web SAT .

Podívejte se také

Bibliografie

René Cori a Daniel Lascar , Matematická logika I. Výrokový počet, Booleovy algebry, predikátový počet [ detail vydání ]
J.-M. Alliot, T. Schiex, P. Brisset a F. Garcia, Umělá inteligence a teoretické výpočty , Cépaduès, 2002 ( ISBN 2-85428-578-6 )
L. Sais, SAT Problém: Pokrok a výzvy , 2008 ( ISBN 2746218860 )
Sharad Malik a Lintao Zhang Boolean Satisfiability: From Theoretical Hardness to Practical Success , Communications of the ACM, (2009) Vol. 52 č. 8, strany 76–82.
John Franco a John Martin, Handbook of satisfiability , IOS Press ( číst online ) , „Kapitola 1: Historie uspokojivosti“

Související články

Externí odkaz

„ Oficiální stránka soutěže SAT “

„ SAT hra, hra, kde musíte najít ocenění, které splňuje booleovský vzorec “