Matematické Fórum

Pro začátek:

It is also possible to solve 2-satisfiability instances in polynomial time using first-order resolution.[11] Each instance of the resolution rule amounts to finding two implications and , and inferring by transitivity a third implication . Thus, if one applies this rule until no more implications can be inferred, the resulting collection of implications is described by the transitive closure of the implication graph, which has polynomial size. The instance is satisfiable if and only if resolution cannot derive an empty clause in the conjunctive normal form of the instance. However, this procedure, while taking only polynomial time, is not as efficient as the linear-time strongly connected component analysis of Aspvall et al.

více na http://en.wikipedia.org/wiki/2-satisfiability

↑ hollowback:Rezolucí dvou klauzulí o nejvýše dvou literálech vznikne klauzule o nejvýše dvou literálech. My vytvoříme prostor všech klauzulí o nejvýše dvou literálech, které lze odvodit. Protože je rozoluční metoda korektní, formule je splnitelná, právě když neodvodíme prázdnou klauzuli.

Na začátku si všechny klauzule zařadíme do fronty  "ke zpracování". Pak vždy vezmeme klauzuli a pro všechny klauzule ve frontě zjistííme, jestli jsme pomocí ní schopni rezolucí vyrobit novou kluzuli. Pokud ano, přidáme ji do fronty. Pokud ne, jdeme dál. Toto provedeme pro všechny pvky ve frontě. Postup pro všechny prvky opakujeme do doby, dokud přibývají nové klauzule. V okamžiku, kdy odvodíme prázdnoou klauzuli algoritmus ukočíme s tím, že formule je nesplnitelná. Pokud k tomu nedojde, je splnitelná

↑ hollowback:Řekněme, že máme n proměnných. U dvousložkové klauzule mohu první složku volit 2n způsoby (proměnná nebo negace), druhou také 2n způsoby, celkem tedy 4n^2 možných zápisů klauzulí (většinu počítáme dvakrát, jednou a nebo b, podruhé b nebo a, ale to nevadí). Jednosložkových je 2n a prázdná jediná. Celkem můžeme pracovat s O(n^2) klauzulemi. Fronta nikdy neřesáhne délku O(n^2). Bude se nám hodit pomocné pole, kde si budeme značit, které klauzule už jsme získali, to bude také velké O(n^2). Protože fronta může mít délu a O(n^2) a můžeme přes ni procházet až O(n^2)-krát. Celkem spotřebujeme O(n^4) času. To bby se určitě dalo snížit ;)