Problém splnitelnosti booleovských formulí (SAT) je dle Cookovy věty NP-úplný. Polynomiální převod dokazuje, že problém 3-CNF SAT je také NP-úplný (je zřejmé, že lze ANO-instanci 3-CNF SATu vyhodnotit v polynomiálním čase – čili tento problém je v NP).

SAT

Rozhodovací problém splnitelnosti booleovských formulí se ptá, zda-li existuje ohodnocení, ve kterém je daná formule, zapsaná v konjunktivním normálním tvaru, pravdivá.

3-CNF SAT

Rozhodovací problém 3-CNF SAT se ptá, zda-li existuje ohodnocení, ve kterém je daná formule, jenž je v konjunktivním normálním tvaru a obsahuje maximálně 3 literály, pravdivá.

Převod

Pokud zadaná formule obsahuje pouze klausule, které mají maximálně 3 literály, pak je převod triviálně hotov. V opačném případě je zapotřebí přepsat každou klausuli, která má více než 3 literály, na konjunkci několika klausulí o maximálně 3 literálech tak, aby byla tato vyjádření ekvivalentní. Toho lze dosáhnout zavedením nových logických proměnných x_{i}, které budou mezi jednotlivými klausulemi 3-CNF SAT problému přenášet informaci, zda-li již byla splnitelnost původní klausule zaručena (pokud je x_{i} nepravda, tak již ohodnocení předešlých proměnných zaručuje splnitelnost původní klausule).

Klausuli \\phi = l_{1} \\vee l_{2} \\vee \\cdots \\vee l_{i} přepíšeme jako:

(l_{1} \\vee l_{2} \\vee x_{1}) \\wedge (\\neg x_{1} \\vee l_{3} \\vee x_{2}) \\wedge (\\neg x_{2} \\vee l_{4} \\vee x_{3}) \\wedge \\cdots \\wedge (\\neg x_{i-3} \\vee l_{i-1} \\vee l_{i})

Výslednou formuli 3-CNF SAT problému získáme jako konjunkci nově vzniklých klausulí a klausulí, které nebyly transformovány (těch, které měly méně než 3 literály).

Složitost převodu

Pokud měla formule k klausulí, z nichž ta nejdelší obsahovala právě s literálů, pak při transformaci každé klausule bylo přidáno maximálně s-3 nových logických proměnných. Výsledná formule proto obsahuje navíc 2 \\cdot k \\cdot (s-3) literálů (každá proměnná je použita právě 2x). Převod je proto polynomiální.

Literatura

  • DEMLOVÁ, Marie. Teorie algoritmů : Text k přednášce.







Doporučujeme