A logikában és a számítástechnikában a logikai kielégítési probléma (néha propozíciós kielégítési problémának nevezik, és rövidítve SATISFIABILITY, SAT vagy B-SAT) annak meghatározásának problémája, hogy létezik-e olyan értelmezés, amely kielégít egy adott logikai formula. Más szóval azt kérdezi, hogy egy adott logikai képlet változóit konzisztensen le lehet-e cserélni TRUE vagy FALSE értékekkel oly módon, hogy a képlet TRUE értékre ad kiértékelést. Ha ez a helyzet, akkor a képletet kielégítőnek nevezzük. Másrészt, ha nincs ilyen hozzárendelés, akkor a képlettel kifejezett függvény HAMIS az összes lehetséges változó-hozzárendelésre, és a képlet nem teljesíthető. Például az „a AND NOT b” képlet teljesíthető, mert megtalálhatjuk az a értékeket = TRUE és b = FALSE, amelyek (a AND NOT b) = TRUE. Ezzel szemben az " a AND NOT a " nem kielégítő.
A SAT az első olyan probléma, amelyről bebizonyosodott, hogy NP-teljes; lásd Cook–Levin-tétel. Ez azt jelenti, hogy az NP bonyolultsági osztályba tartozó összes probléma, amely természetes döntési és optimalizálási problémák széles skáláját tartalmazza, legfeljebb olyan nehezen megoldható, mint a SAT. Nincs ismert algoritmus, amely hatékonyan oldja meg az egyes SAT-problémákat, és általában úgy gondolják, hogy nem létezik ilyen algoritmus; ez a hiedelem azonban matematikailag nem bizonyított, és annak a kérdésnek a megoldása, hogy a SAT-nak van-e polinomiális idejű algoritmusa, egyenértékű a P versus NP problémával, amely a számítástechnika elméletének híres nyitott problémája.
Mindazonáltal 2007-től a heurisztikus SAT-algoritmusok több tízezer változót és több millió szimbólumból álló képletet tartalmazó problémapéldányokat is képesek megoldani,. ami sok gyakorlati SAT-problémára elegendő, pl. mesterséges intelligencia, áramkör tervezés, és automatikus tételbizonyítás.
Definíciók Egy propozíciós logikai képlet, amelyet Boole-kifejezésnek is neveznek, változókból, AND operátorokból (konjunkció, ∧-vel is jelölve), VAGY (disjunkció, ∨), NOT (negáció, ¬) és zárójelekből épül fel. Egy képlet akkor tekinthető kielégítőnek, ha megfelelő logikai értékek hozzárendelésével TRUE lehet (pl. TRUE, FALSE) a változóira. A Boole-féle kielégítési probléma (SAT) egy képlet segítségével ellenőrizhető, hogy kielégíthető-e. Ez a döntési probléma központi jelentőségű a számítástechnika számos területén, beleértve az elméleti számítástechnikát, a komplexitáselméletet, Here: p.86 Here: p.403 az algoritmusokat, a kriptográfiát és a mesterséges intelligenciát.
Konjunktív normál forma A literál vagy változó (ebben az esetben pozitív literálnak nevezzük), vagy egy változó negációja (negatív literál). A záradék a literálok (vagy egyetlen literál) diszjunkciója. Egy záradékot Horn-mondatnak nevezünk, ha legfeljebb egy pozitív literált tartalmaz. Egy képlet konjunktív normál formában (CNF) van, ha tagmondatok kötőszava (vagy egyetlen tagmondat). Például egy pozitív literál, egy negatív literál, egy záradék. Az képlet konjunktív normál formában van; első és harmadik tagmondata Horn-mondat, de a második tagmondata nem. A képlet x 1 kiválasztásával teljesíthető = FALSE, x 2 = FALSE, és x 3 tetszőlegesen, mivel (FALSE ∨ ¬FALSE) ∧ (¬FALSE ∨ FALSE ∨ x 3) ∧ ¬FALSE értéke (FALSE ∨ TRUE) ∧, ∨ TRUE ∨ FALSE ∨-ben TRUE. TRUE ∧ TRUE ∧ TRUE (azaz TRUE). Ezzel szemben a CNF képlet a ∧ ¬ a, amely egy literál két tagmondatából áll, nem teljesíthető , mivel =TRUE vagy =FALSE esetén TRUE ∧ ¬TRUE (azaz FALSE) vagy FALSE ∧ ¬FALSE (pl., ismét HAMIS), ill.
A SAT-probléma egyes változatainál hasznos definiálni egy általánosított konjunktív normálforma képlet fogalmát, ti. tetszőleges sok általánosított tagmondat kötőszójaként, amelyek közül az utóbbi formájú néhány R logikai függvényre és (közönséges) literálokra . Az engedélyezett logikai függvények különböző készletei különböző problémaverziókhoz vezetnek. Például R (¬ x, a, b) egy általánosított tagmondat, és R (¬ x, a, b) ∧ R (b, y, c) ∧ R (c, d, ¬ z) általánosított. konjunktív normál forma. Ezt a képletet az alábbiakban használjuk, ahol R a háromtagú operátor, amely éppen akkor TRUE, amikor az egyik argumentuma az.
A Boole-algebra törvényeit használva minden propozíciós logikai képlet átalakítható egy ekvivalens konjunktív normál formává, amely azonban exponenciálisan hosszabb is lehet. Például az (x 1 ∧ y 1) ∨ (x 2 ∧ y 2) ∨ ... ∨ (x n ∧ y n) képlet konjunktív normál formává alakítása eredményezi.
míg az előbbi 2 változó n konjunkciójának diszjunkciója, az utóbbi 2 n n változós tagmondatból áll.
A Tseytin-transzformáció használatával azonban találhatunk egy kiegyenlíthető konjunktív normál alakú formulát, amelynek hossza lineáris az eredeti propozíciós logikai képlet méretében.
Bonyolultság A SAT volt az első ismert NP-teljes probléma, amint azt Stephen Cook a Torontói Egyetemen 1971-ben és egymástól függetlenül Leonid Levin a Nemzeti Tudományos Akadémián 1973-ban bizonyította. Addig az NP-teljes probléma fogalma nem is létezett. A bizonyíték megmutatja, hogy az NP komplexitási osztály minden döntési problémája hogyan redukálható a CNFThe SAT problem for arbitrary formulas is NP-complete, too, since it is easily shown to be in NP, and it cannot be easier than SAT for CNF formulas. képletek SAT-problémájára, amelyeket néha CNFSAT-nak is neveznek. A Cook-féle redukció hasznos tulajdonsága, hogy megőrzi az elfogadó válaszok számát. Például annak eldöntése, hogy egy adott gráf 3-as színezésű- e, egy másik probléma az NP-ben; ha egy gráfnak 17 érvényes 3 színezése van, akkor a Cook–Levin redukcióval előállított SAT képlet 17 kielégítő hozzárendelést tartalmaz.
Az NP-teljesség csak a legrosszabb esetek futási idejére vonatkozik. A gyakorlati alkalmazásokban előforduló esetek közül sok sokkal gyorsabban megoldható. Lásd alább a SAT megoldásának algoritmusait.
3-kielégíthetőség bélyegkép|300px| A 3-SAT példány redukálva. A zöld csúcsok 3-kliket alkotnak, és megfelelnek a kielégítő x =FALSE, y =TRUE hozzárendelésnek A tetszőleges formulák kielégíthetőségi problémájához hasonlóan a formula kielégíthetőségének meghatározása konjunktív normál formában, ahol minden tagmondat legfeljebb három literálra korlátozódik, szintén NP-teljes; ezt a problémát 3-SAT, 3CNFSAT vagy 3- satisfiability-nek nevezik. A korlátlan SAT probléma 3-SAT-ra csökkentéséhez alakítsa át az tagmondatokat tagmondat konjunkciójára
ahol olyan friss változók, amelyek máshol nem fordulnak elő. Bár a két képlet logikailag nem egyenértékű, kiegyenlíthetőek. Az összes tagmondat transzformációjából adódó képlet legfeljebb háromszor olyan hosszú, mint az eredeti, azaz a hossznövekedés polinomiális.; here: Thm.10.4
A 3-SAT Karp 21 NP-teljes problémájának egyike, és kiindulópontként szolgál annak bizonyítására, hogy más problémák is NP-nehézek.i.e. at least as hard as every other problem in NP. A decision problem is NP-complete if and only if it is in NP and is NP-hard. Ez a polinomiális idő redukciójával történik 3-SAT-ról a másik problémára. Egy példa arra a problémára, ahol ezt a módszert alkalmazták, a klikk probléma : adott egy c tagmondatokból álló CNF-képlet, a megfelelő gráf minden literálhoz egy csúcsból, valamint a két nem ellentmondói.e. such that one literal is not the negation of the other literál közötti élből áll. különböző tagmondatokból, vö. kép. A gráfnak akkor és csak akkor van c-klikkje, ha a képlet kielégítő.
Létezik egy egyszerű véletlenszerű algoritmus Schöning (1999) alapján, amely n (4/3) n időben fut, ahol n a változók száma a 3-SAT állításban, és nagy valószínűséggel sikerül helyesen eldönteni a 3-SAT-ot.
Az exponenciális idő hipotézis azt állítja, hogy egyetlen algoritmus sem tudja megoldani a 3-SAT-t (vagy a k-SAT-ot bármely k > 2) időben (azaz alapvetően gyorsabb, mint n-ben exponenciális).
Selman, Mitchell és Levesque (1996) empirikus adatokat ad a véletlenszerűen generált 3-SAT képletek nehézségeiről, méretparamétereiktől függően. A nehézséget a DPLL algoritmus által indított rekurzív hívások számában mérik.
A 3-kielégíthetőség általánosítható k-kielégíthetőségre (k-SAT, k-CNF-SAT is), ha a CNF-ben lévő formulákat úgy tekintjük, hogy minden tagmondat legfeljebb k literált tartalmaz. Mivel azonban bármely k ≥ 3 esetén ez a probléma nem lehet sem könnyebb, mint 3-SAT, sem nehezebb, mint SAT, és az utóbbi kettő NP-teljes, ezért k-SAT-nak kell lennie.
Egyes szerzők a k-SAT-ot a pontosan k literált tartalmazó CNF-képletekre korlátozzák. Ez sem vezet eltérő komplexitási osztályhoz, mivel minden tagmondat j < k literálokkal kiegészíthető fix dummy változókkal . Az összes tagmondat kitöltése után 2 k -1 extra tagmondatot kell hozzáfűzni, hogy csak vezessen kielégítő hozzárendeléshez. Mivel k nem függ a képlet hosszától, az extra tagmondatok a hossz állandó növekedéséhez vezetnek. Ugyanebből az okból kifolyólag nem számít, hogy megengedettek-e duplikált literálok a tagmondatokban, mint például .
A SAT speciális esetei
Konjunktív normál forma A konjunktív normálformát (különösen záradékonként 3 literált) gyakran tekintik a SAT-képletek kanonikus reprezentációjának. Amint fentebb látható, az általános SAT-probléma 3-SAT-ra redukálódik, az ilyen formában lévő képletek kielégíthetőségének meghatározásának problémája.
Diszjunktív normál forma A SAT triviális, ha a formulák a diszjunktív normál formában lévőkre korlátozódnak, vagyis a literálok kötőszóinak diszjunkciói. Egy ilyen formula valóban akkor és csak akkor teljesíthető, ha legalább az egyik kötőszava kielégíthető, egy kötőszó pedig akkor és csak akkor teljesíthető, ha valamelyik x változóra nem tartalmazza az x-et és NEM x-et is. Ez lineáris időben ellenőrizhető. Továbbá, ha korlátozzuk, hogy teljesen diszjunktív normál formában legyenek, amelyben minden változó pontosan egyszer szerepel minden kötőszóban, akkor konstans időben ellenőrizhetők (minden kötőszó egy kielégítő hozzárendelést jelent). De exponenciális időbe és helybe telhet egy általános SAT-probléma diszjunktív normál formává alakítása; egy példa esetében cserélje ki a „∧” és „∨” értéket a fenti exponenciális felfújási példában konjunktív normálformákra.
Pontosan-1 3-kielégíthetőség bélyegkép|416px| Balra: egy x ∨ y ∨ z 3-SAT záradék Schaefer-féle redukciója. R eredménye , ha pontosan az egyik argumentuma IGAZ, ellenkező esetben . Az x, y, z értékeinek mind a 8 kombinációját megvizsgáljuk, soronként egyet. Az új a, ..., f változók kiválaszthatók úgy, hogy minden klózt kielégítsenek (pontosan egy argumentum minden R) minden sorban, kivéve az elsőt, ahol x ∨ y ∨ z HAMIS. Jobbra: Egyszerűbb redukció ugyanazokkal a tulajdonságokkal A 3-as kielégíthetőségi probléma egy változata az egy a háromból 3-SAT (más néven 1-in-3-SAT és pontosan-1 3-SAT). Adott egy konjunktív normálalak, amelyben záradékonként három literál található, a probléma annak meghatározása, hogy létezik-e igazság-hozzárendelés a változókhoz, így minden tagmondatnak pontosan egy IGAZ literálja van (és így pontosan két HAMIS literál). Ezzel szemben a közönséges 3-SAT megköveteli, hogy minden záradéknak legyen legalább egy TRUE literálja. Formálisan egy a háromhoz 3-SAT-probléma általánosított konjunktív normálformaként van megadva, minden általánosított tagmondattal egy háromtagú R operátort használva, amely TRUE, ha pontosan az egyik argumentuma az. Ha a 3-SAT képlet egy a háromhoz literálja pozitív, a kielégítési problémát egy a háromhoz pozitív 3-SAT- nak nevezzük.
A háromból egy 3-SAT, pozitív esetével együtt, NP-teljes "LO4" problémaként szerepel a szabványos hivatkozásban, a Computers and Intractability: A Guide to the Theory of NP-Completeness, Michael R. Garey és David S. Johnson. Thomas Jerome Schaefer NP-teljesnek bizonyult a háromhoz 3-SAT-ról a Schaefer-féle dichotómiatétel speciális eseteként, amely azt állítja, hogy minden probléma, amely bizonyos módon általánosítja a Boole-féle kielégíthetőséget, vagy a P osztályba tartozik, vagy NP-teljes.