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 literalom. Na primer, i x₁ i ~(x₂) (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₁ ili ~(x₂)). 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 konjuktivnoj normalnoj formi sa tri literala po klauzi (3-KNF), što daje 3-SAT problem. Ovakav izraz je oblika:

(x₁₁ ILI x₁₂ ILI x₁₃) I

(x₂₁ ILI x₂₂ ILI x₂₃) I

(x₃₁ ILI x₃₂ ILI x₃₃) 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₁ ili ~x₂ ili ~x₃) i (x₁ ili x₂ ili x₄)

E ima dve klauze (odvojene zagradama), četiri literala (x₁, x₂, x₃, x₄), 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₁ do x₄) tako da ceo izraz ima vrednost TAČNO. U gornjem primeru postoji takva dodela (x₁ = TAČNO, x₂ = TAČNO, x₃=TAČNO, x₄=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₁ = 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.