SAT problem

U matematici i informatici, **SAT problem** ili **problem zadovoljivosti** se sastoji u utvrđivanju da li se promenljivima nekog bulovskog izraza mogu dodeliti vrednosti tako da cela formula ima vrednost TAČNO, ili formula ima vrednost NETAČNO za sve moguće kombinacije vrednosti promenljivih. U drugom slučaju se kaže da je funkcija nezadovoljiva; a u suprotnom je zadovoljiva. Promenljive su bulovske (imaju vrednosti 0 ili 1), što znači da je problem binarne prirode.

## Osnovne definicije, terminologija i primene
U teoriji kompleksnosti, **SAT problem** je problem odlučivanja, koji se sastoji iz bulovskih izraza zapisanih samo pomoću operatora I, ILI, NE, promenljivih, i zagrada.

Pitanje je: ako je dat izraz, da li postoji neka dodela vrednosti *TAČNO* i *NETAČNO* promenljivima, takva da ceo izraz ima vrednost *TAČNO*? Ako je tako, kaže se da je formula zadovoljiva. SAT problem pripada klasi NP-kompletnih problema. Ovaj problem je od kučne važnosti za razne oblasti računarstva, uključujući teorijsko računarstvo, algoritmiku, veštačku inteligenciju i dizajn hardvera.

Problem se može značajno *pojednostaviti*, a da ostane NP-kompletan. Uz primenu De Morganovih zakona, možemo da pretpostavimo da se operatori negacije primenjuju isključivo direktno na promenljive, ne na izraze; promenljivu ili njenu negaciju nazivamo *[[literal]]om*. Na primer, i *x*1 i ~(*x*2) (gde je ~ simbol za negaciju) su literali - prvi je *pozitivan* literal, a drugi je *negativan*. Ako grupišemo literale operatorom ILI, dobijamo *klauze*, poput (*x*1 *ili* ~(*x*2)). Konačno, neka se izraz sastoji od konjunkcija (I) klauza - ovo je konjuktivna normalna forma (KNF). Određivanje da li je izraz ovog oblika NP-kompletan, čak i ako svaka klauza ima najviše tri literala. Ovakav poslednji problem se naziva 3-SAT.

Sa druge strane, ako svaku klauzu ograničimo na najviše dva literala, rezultujući problem, 2-SAT, je '''NL'''-kompletan. Takođe, ako svaka klauza mora da bude Hornova klauza, sa najviše jednim pozitivnim literalom, rezultujući problem, Hornova zadovoljivost, je '''P'''-kompletan.

Kukova teorema dokazuje da je SAT problem NP-kompletan. Štaviše, ovo je bio prvi problem za koji je dokazano da je NP-kompletan. Međutim, osim ovog teorijskog značaja, tokom protekle decenije su razvijeni efikasni algoritmi za SAT problem, koji su doprineli velikom napretku u našoj sposobnosti da automatski rešavamo probleme koji imaju desetine hiljada promenljivih i milione uslova.

## Kompleksnost i verzije
### NP-kompletnost
SAT je bio prvi problem za koji je otkriveno da je NP-kompletan, što je 1971. dokazao Stiven Kuk (vidi Kukovu teoremu za dokaz). Do tada čak nije ni postojao koncept NP-kompletnog problema. Problem ostaje NP-kompletan čak i kad su svi izrazi zapisani u *[[konjuktivna normalna forma|konjuktivnoj normalnoj formi]]* sa tri literala po klauzi (3-KNF), što daje **3-SAT** problem. Ovakav izraz je oblika:
:(*x*11 ILI *x*12 ILI *x*13) I
:(*x*21 ILI *x*22 ILI *x*23) I
:(*x*31 ILI *x*32 ILI *x*33) I ...
gde je svako *x* promenljiva ili negacija promenljive, i svaka promenljiva može da se pojavljuje više puta u izrazu.

Korisno svojstvo Kukovog svođenja jeste da održava broj prihvatajućih odgovora. Na primer, ako graf ima 17 validnih 3-bojenja, SAT formula dobijena svođenjem će imati 17 zadovoljavajućih dodela.

### 2-zadovoljivost

SAT problem je lakši ako se ograničimo na formule u disjunktivnoj normalnoj formi, to jest, formule koje se sastoje od disjunkcije (ILI) terma, gde je svaki term konjunkcija (ILI) literala. Takva formula je zadovoljiva ako i samo ako je bar jedan njen term zadovoljiv, a term je zadovoljiv ako i samo ako ne sadrži i *x* i NE *x* za neku promenljivu *x*. Ovo se može proveriti u polinomijalnom vremenu.

SAT je takođe lakši ako je broj literala po klauzi ograničen na 2, u kom slučaju se zove 2-SAT. I ovaj problem se može rešiti u polinomijalnom vremenu, i kompletan je za klasu NL. Slično, ako ograničimo broj literala po klauzi na 2, i zamenimo operatore I operacijama ekskluzivne disjunkcije, dobijamo *ekskluzivno ili 2-SAT problem*, koji je kompletan za SL = L.

Jedna od najvažnijih verzija SAT problema je HORNSAT, gde je izraz konjunkcija Hornovih klauza. Ovaj problem je rešiv u polinomijalnom vremenu pomoću algoritma *[[Hornova zadovoljivost]]*. HORNSAT je P-kompletan problem. Može se posmatrati kao P verzija SAT problema.

Ako klase kompleksnosti P i NP nisu jednake, nijedna od ovih verzija nije NP-kompletna, za razliku od SAT problema. Pretpostavka da P i NP nisu jednake još uvek nije dokazana.

### 3-zadovoljivost
3-zadovoljivost je specijalni slučaj *k*-zadovoljivosti (*k*-SAT) ili prosto SAT, gde svaka klauza sadrži tačno *k* = 3 literala. Ovo je jedan od Karpovih 21 NP-kompletnih problema.

Sledi jedan primer, simbol ~ označava negaciju:
: E = (*x*1 ili ~*x*2 ili ~*x*3) i (*x*1 ili *x*2 ili *x*4)
E ima dve klauze (odvojene zagradama), četiri literala (*x*1, *x*2, *x*3, *x*4), i *k*=3 (tri literala po klauzi).

Da bismo rešili ovakav 3-SAT problem, moramo da utvridmo da li postoji istinitosna vrednost (TAČNO ili NETAČNO) koju možemo da dodelimo svakom od literala (*x*1 do *x*4) tako da ceo izraz ima vrednost TAČNO. U gornjem primeru postoji takva dodela (*x*1 = TAČNO, *x*2 = TAČNO, *x*3=TAČNO, *x*4=TAČNO), pa je ova formula zadovoljiva. Ovo je samo jedna od mnogo mogućih dodela, jer u ovom slučaju bi svaka kombinacija gde je *x*1 = TAČNO ispravna. U slučaju da ne postoji odgovarajuća dodela, formula je nezadovoljiva.

Kako se k-SAT (opšti slučaj) može svesti na 3-SAT, a za 3-SAT se može dokazati da je NP-kompletan, on se može koristiti da se za druge probleme dokaže da su NP-kompletni. Ovo se radi tako što se pokaže na koji način se rešenje nekog problema može iskoristiti da se reši 3-SAT. Primer problema gde se koristi ovaj metod je problem klike. Često je lakše vršiti svođenja sa 3-SAT problema nego sa SAT problema na probleme za koje se ispituje NP-kompletnost.

Postoji verzija 3-SAT problema gde se zahteva da je *tačno* jedna promenljiva u svakoj klauzi tačna, umesto *barem jedna*. I ova verzija problema je NP-kompletna.

## Reference