SAT problem

Izvor: Wikipedia

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[uredi - уреди]

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 literalom. Na primer, i x1 i ~(x2) (gde je ~ simbol za negaciju) su literali - prvi je pozitivan literal, a drugi je negativan. Ako grupišemo literale operatorom ILI, dobijamo klauze, poput (x1 ili ~(x2)). 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[uredi - уреди]

NP-kompletnost[uredi - уреди]

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 konjuktivnoj normalnoj formi sa tri literala po klauzi (3-KNF), što daje 3-SAT problem. Ovakav izraz je oblika:

(x11 ILI x12 ILI x13) I
(x21 ILI x22 ILI x23) I
(x31 ILI x32 ILI x33) 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[uredi - уреди]

Glavni članak: 2-SAT problem

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[uredi - уреди]

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 = (x1 ili ~x2 ili ~x3) i (x1 ili x2 ili x4)

E ima dve klauze (odvojene zagradama), četiri literala (x1, x2, x3, x4), 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 (x1 do x4) tako da ceo izraz ima vrednost TAČNO. U gornjem primeru postoji takva dodela (x1 = TAČNO, x2 = TAČNO, x3=TAČNO, x4=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 x1 = 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[1] 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[uredi - уреди]