Preskoči na glavni sadržaj

2SAT

Notacija

¬\lnot jest logička operacija NOT (NE).

\land jest logička operacija AND (I).

\lor jest logička operacija OR (ILI).

\equiv ili     \iff označava logičku ekvivalenciju.

\Longrightarrow predstavlja logičku implikaciju.

Uvod

SAT (Boolean satisfiability problem) jest problem pridruživanja istine ili laži varijablama tako da se zadovolji neka Booleova funkcija zapisana u kanonskom obliku produkta maksterma. To se preciznije naziva konjunktivna normalna forma.

2-SAT poseban je slučaj SAT-a kada se svaki maksterm sastoji od dvije varijable.

(x0x2)(x0¬x3)(x1¬x3)(x1¬x4)(x2¬x4)(x0¬x5)(x1¬x5)(x2¬x5)(x3x6)(x4x6)(x5x6)\begin{aligned} &(x_0\lor x_2)\land(x_0\lor\lnot x_3)\land(x_1\lor\lnot x_3)\land(x_1\lor\lnot x_4)\land{} \\ &(x_2\lor\lnot x_4)\land{}(x_0\lor \lnot x_5)\land (x_1\lor\lnot x_5)\land (x_2\lor\lnot x_5)\land{} \\ &(x_3\lor x_6)\land (x_4\lor x_6)\land (x_5\lor x_6) \end{aligned}

Iznad je napisan primjer funkcije koju je potrebno zadovoljiti. Cilj nam je dodijeliti varijablama xix_i vrijednosti istinu ili laž, tako da izraz naposljetku bude istinit. Primjetimo da to znači da u svakoj zagradi barem jedan operand operacije iliili mora biti istinit. Ako je taj operand oblika xix_i, tada mora vrijediti xi=1x_i = 1. Ako pak je taj operand oblika ¬xi\lnot x_i, onda mora biti xi=0x_i = 0.

Znamo:

(x0¬x3)    (¬x0¬x3)    (x3x0)(x_0\lor\lnot x_3) \;\equiv\; (\lnot x_0\Rightarrow\lnot x_3) \;\equiv\; (x_3\Rightarrow x_0)

Dakle možemo konstruirati usmjereni graf s po dva vrha za svaku varijablu: jedan za nju samu, i još jedan za njezin komplement. Povlačimo brid iz jednog vrha u drugi kada vrijednost prvog vrha implicira vrijednost drugog vrha u zadanoj formuli. Na donjoj je slici konstruiran takav graf za gore navedeni primjer.

Graf konstruiran pomoću zadane funkcije

Rješenje

2SAT problem ima rješenje ako i samo ako njegov zapis kao gore definirani graf s implikacijama nema xix_i i ¬xi\lnot x_i u istoj strogo povezanoj komponenti, za svaku varijablu xix_i.

U protivnom postoji barem jedno rješenje, koje je moguće dobiti sljedećim postupkom:

  • Konstruiramo usmjereni graf GG kao što je gore opisano
  • Odredimo strogo povezane komponente grafa
  • Kondenziramo graf, odnosno u GG svaku strogo povezanu komponentu stegnemo da dobijemo GG', u kojem svaki vrh predstavlja jednu strogo povezanu komponentu iz GG. U grafu GG' postoji brid iz uu' u vv' ako postoji brid uvuv u GG takav da je uuu \in u' i vvv \in v'.
  • Topološki sortiramo vrhove u GG' i rješenje zapišemo u neku listu LL
  • Obrnutim redoslijedom prolazimo kroz LL i obrađujemo komponentu po komponentu:
    • Svi vrhovi u komponenti moraju biti iste logične vrijednosti, znači ili su svi istiniti ili su svi lažni.
    • Ako barem jedan vrh nema pridruženu logičnu vrijednost, tada ćemo svim vrhovima u komponenti pridružiti istinu. Ako u nekom vrhu piše xix_i, postavljamo xi=1x_i = 1. Ako pak u nekom vrhu piše ¬xi\lnot x_i, tada postavljamo xi=0x_i = 0. Time postižemo da je svaki vrh u komponenti istinit, pa ne može doći do lažne implikacije 101 \Rightarrow 0.
    • Ovo smo radili obrnutim topološkim redoslijedom jer, ako postoji put od komponente XX do komponente YY, želimo prvo postaviti komponentu YY da bude istinita. Ovime sprječavamo da dođe do lažne implikacije 101 \Rightarrow 0.