„Logikai kielégítési probléma” változatai közötti eltérés

A Wikipédiából, a szabad enciklopédiából
Újabb szerkesztés →
Tartalom törölve Tartalom hozzáadva
VizuálisWikiszöveges
K karesz (vitalap | szerkesztései)
7 szerkesztés
Készült a(z) „Boolean satisfiability problem” oldal lefordításával
(Nincs különbség)

A lap 2022. június 9., 18:56-kori változata

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, [1] ami sok gyakorlati SAT-problémára elegendő, pl. mesterséges intelligencia, áramkör tervezés ., [2] é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, [3] [4] az algoritmusokat, a kriptográfiát [5] [6] és a mesterséges intelligenciát . [7] 

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 x1 egy pozitív literál, ¬x2 egy negatív literál, x1 ∨ ¬x2 egy záradék. Az (x1 ∨ ¬x2) ∧ (¬x1 ∨ x2 ∨ x3) ∧ ¬x1 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 R(l1,...,ln) formájú néhány R logikai függvényre és (közönséges) literálokra li . 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.

(x1 ∨ x2 ∨ … ∨ xn) ∧
(y1 ∨ x2 ∨ … ∨ xn) ∧
(x1 ∨ y2 ∨ … ∨ xn) ∧
(y1 ∨ y2 ∨ … ∨ xn) ∧ ... ∧
(x1 ∨ x2 ∨ … ∨ yn) ∧
(y1 ∨ x2 ∨ … ∨ yn) ∧
(x1 ∨ y2 ∨ … ∨ yn) ∧
(y1 ∨ y2 ∨ … ∨ yn);

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 [8] é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 CNF [note 1] 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

A 3-SAT példány (x ∨ x ∨ y) ∧ (¬x ∨ ¬y ∨ ¬y) ∧ (¬x ∨ y ∨ y) 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 l1 ∨ ⋯ ∨ ln tagmondatokat n - 2 tagmondat konjunkciójára

(l1 ∨ l2 ∨ x2) ∧
(¬x2 ∨ l3 ∨ x3) ∧
(¬x3 ∨ l4 ∨ x4) ∧ ⋯ ∧
(¬xn − 3 ∨ ln − 2 ∨ xn − 2) ∧
(¬xn − 2 ∨ ln − 1 ∨ ln)

ahol x2, ⋯ , xn − 2 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. [9]

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 . [note 2] 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ó [note 3] 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. [10]

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) exp(o(n)) 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. [11]

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 l1 ∨ ⋯ ∨ lj tagmondat j < k literálokkal kiegészíthető fix dummy változókkal l1 ∨ ⋯ ∨ lj ∨ dj+1 ∨ ⋯ ∨ dk . Az összes tagmondat kitöltése után 2 k -1 extra tagmondatot kell hozzáfűzni , hogy csak d1 = ⋯ = dk=FALSE 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 ¬x ∨ ¬y ∨ ¬y .

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

Balra: egy x ∨ y ∨ z 3-SAT záradék Schaefer-féle redukciója. R eredménye TRUE (1), ha pontosan az egyik argumentuma IGAZ, ellenkező esetben FALSE (0) . 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 green 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. [12]

A Schaefer olyan konstrukciót kínál, amely lehetővé teszi a polinomiális idő egyszerű csökkentését 3-SAT-ról egy a háromhoz 3-SAT-ra. Legyen "( x vagy y vagy z )" egy záradék egy 3CNF képletben. Adjon hozzá hat új logikai változót a, b, c, d, e és f, hogy ezt a záradékot szimulálja, és ne mást. Ekkor az R ( x, a, d ) ∧ R ( y, b, d ) ∧ R ( a, b, e ) ∧ R ( c, d, f ) ∧ R ( z, c, FALSE) képlet teljesíthető a friss változók néhány beállítása akkor és csak akkor, ha x, y vagy z közül legalább az egyik TRUE, lásd a képet (balra). Így bármely 3-SAT-példány m klózzal és n változóval konvertálható egy a háromból egy-egy 3-SAT-példánygá, 5 m záradékkal és n +6 m változóval. [13] Egy másik redukció csak négy új változót és három tagmondatot tartalmaz: R (¬ x, a, b ) ∧ R ( b, y, c ) ∧ R( c, d ,¬ z ), lásd a képet (jobbra).

Nem minden egyenlő 3-kielégíthetőség

Egy másik változat a nem minden egyenlő 3-as kielégíthetőségi probléma (más néven NAE3SAT ). Adott egy konjunktív normálalak, amelyben záradékonként három literál van, a probléma annak meghatározása, hogy létezik-e olyan hozzárendelés a változókhoz, hogy egyik tagmondatban sem mindhárom literálnak ugyanaz az igazságértéke. Ez a probléma is NP-teljes, még ha tagadószimbólumot sem fogadunk el, Schaefer dichotómia tétele szerint. [12]

Lineáris SAT

A 3-SAT képlet Lineáris SAT ( LSAT ), ha minden tagmondat (literálok halmazának tekintve) legfeljebb egy másik klózt metsz, sőt, ha két klóz metszi egymást, akkor pontosan egy literál közös bennük. Egy LSAT-képlet ábrázolható diszjunkt, félig zárt intervallumok halmazaként egy vonalon. Annak eldöntése, hogy egy LSAT-képlet kielégíthető-e, NP-teljes. [14]

2-kielégíthetőség

A SAT könnyebb, ha egy záradékban a literálok számát legfeljebb 2-re korlátozzák, ebben az esetben a problémát 2-SAT- nak nevezik. Ez a probléma polinomiális időben megoldható, és valójában az NL komplexitási osztályra teljes . Ha ezen felül az összes OR műveletet literálokban XOR műveletekre változtatjuk, akkor az eredményt kizárólagos vagy 2-es kielégíthetőségnek nevezzük, ami teljes probléma az SL = L összetettségi osztály esetében.

Horn-kielégíthetőség

A Horn-klózok adott kötőszójának kielégíthetőségének eldöntésének problémáját Horn-satisfiabilitynek vagy HORN-SAT -nak nevezzük. Polinomiális időben megoldható a Unit propagation algoritmus egyetlen lépésével, amely a Horn-klózok halmazának (wrt az IGAZ-hoz rendelt literálok halmazának) egyetlen minimális modelljét állítja elő. A kürttel való kielégíthetőség P-teljes . Ez a Boole-féle kielégítési probléma P változataként tekinthető. A számszerűsített Horn-képletek igazságtartalmának meghatározása polinomiális időben is elvégezhető. [15]

A Horn záradékok azért érdekesek, mert képesek kifejezni egy változó implikációját más változók halmazából. Valójában az egyik ilyen ¬ x 1 ∨ ... ∨ ¬ x n ∨ y kitétel átírható x 1 ∧ ... ∧ x n → y alakban, vagyis ha x 1 ,..., x n mind TRUE, akkor y -nak is TRUE kell lennie.

A Horn-formulák osztályának általánosítása az átnevezhető-Horn-képletek osztálya, amely azon formulák halmaza, amelyek Horn-formába helyezhetők úgy, hogy néhány változót a megfelelő tagadással helyettesítünk. Például ( x 1 ∨ ¬ x 2 ) ∧ (¬ x 1 ∨ x 2 ∨ x 3 ) ∧ ¬ x 1 nem Horn képlet, de átnevezhető Horn képletre ( x 1 ∨ ¬ x 2 ) ∧ (¬ x 1 ∨ x 2 ∨ ¬ y 3 ) ∧ ¬ x 1 úgy, hogy y 3 -at bevezetjük x 3 negációjaként. Ezzel szemben az ( x 1 ∨ ¬ x 2 ∨ ¬ x 3 ) ∧ (¬ x 1 ∨ x 2 ∨ x 3 ) ∧ ¬ x 1 átnevezése nem vezet Horn képlethez. Az ilyen csere meglétének ellenőrzése elvégezhető lineáris időben; ezért az ilyen képletek kielégíthetősége P-ben van, mivel ez úgy oldható meg, hogy először végrehajtjuk ezt a cserét, majd ellenőrizzük a kapott Horn-képlet kielégíthetőségét.

A 2 tagmondattal rendelkező képlet lehet nem kielégítő (piros), 3-as (zöld), xor-3-megelégedett (kék) és/vagy 1 a 3-ban elégedett (sárga), attól függően, hogy a VALÓDI betűk száma az 1. (hor) és 2. (vert) kitétel.

XOR-kielégíthetőség

Egy másik speciális eset a problémák osztálya, ahol minden tagmondat XOR (vagyis kizárólagos vagy ), nem pedig (sima) OR operátorokat tartalmaz. [note 4] Ez P -ben van, mivel egy XOR-SAT képlet egy mod 2 lineáris egyenletrendszernek is tekinthető, és köbidőben is megoldható Gauss-eliminációval ; [16] lásd a keretet egy példaért. Ez az átdolgozás a Boole- algebrák és a Boole-gyűrűk közötti rokonságon, valamint azon a tényen alapul, hogy a modulo two aritmetika egy véges mezőt alkot. Mivel egy XOR b XOR c akkor és csak akkor IGAZ, ha { a, b, c } pontosan 1 vagy 3 tagja IGAZ, az 1 a 3-ban SAT feladat minden megoldása egy adott CNF képletre is megoldás. az XOR-3-SAT probléma megoldása, és az XOR-3-SAT mindegyik megoldása a 3-SAT megoldása, vö. kép. Ennek következtében minden CNF képletnél megoldható a képlet által definiált XOR-3-SAT probléma, és az eredmény alapján arra következtethetünk, hogy a 3-SAT probléma megoldható, vagy az 1 a 3-ban. A SAT probléma megoldhatatlan.

Feltéve, hogy a P és NP komplexitási osztályok nem egyenlőek, sem a 2-, sem a Horn-, sem az XOR-kielégíthetőség nem NP-teljes, ellentétben a SAT-tal.

Schaefer dichotómia tétele

A fenti korlátozások (CNF, 2CNF, 3CNF, Horn, XOR-SAT) a szóban forgó képleteket részképletek kötőszavainak kötötték; minden megszorítás egy meghatározott formát ad minden részképlethez: például a 2CNF-ben csak a bináris tagmondatok lehetnek részképletek.

Schaefer dichotómia tétele kimondja, hogy a Boole-függvényekre vonatkozó bármilyen korlátozásra, amely felhasználható ezen részképletek kialakítására, a megfelelő kielégítési probléma P-ben vagy NP-ben van. A 2CNF, Horn és XOR-SAT formulák kielégíthetőségének P-beli tagsága ennek a tételnek speciális esetei. [12]

Az alábbi táblázat összefoglalja a SAT néhány gyakori változatát.

Kód Név Korlátozások Követelmények Osztály
3SAT 3-kielégíthetőség Minden tagmondat 3 literált tartalmaz. Legalább egy szó szerint igaznak kell lennie. NPC
2SAT 2-kielégíthetőség Minden tagmondat 2 literált tartalmaz. Legalább egy szó szerint igaznak kell lennie. P
1-in-3-SAT Pontosan-1 3-SAT Minden tagmondat 3 literált tartalmaz. Pontosan egy szó szerint kell igaznak lennie. NPC
1 a 3-ban SAT+ Pontosan-1 Pozitív 3-SAT Minden tagmondat 3 pozitív literált tartalmaz. Pontosan egy szó szerint kell igaznak lennie. NPC
NAE3SAT Nem minden egyenlő 3-kielégíthetőség Minden tagmondat 3 literált tartalmaz. Egy vagy két literálnak igaznak kell lennie. NPC
NAE3SAT+ Nem minden egyenlő pozitív 3-SAT Minden tagmondat 3 pozitív literált tartalmaz. Egy vagy két literálnak igaznak kell lennie. NPC
PL-SAT Planar SAT Az előfordulási gráf (tagmondat-változó gráf) síkbeli . Legalább egy szó szerint igaznak kell lennie. NPC
L3SAT Lineáris 3-SAT Mindegyik tagmondat legfeljebb egy másik tagmondatot metsz, és a metszéspont pontosan egy literál. Legalább egy szó szerint igaznak kell lennie. NPC
KÜRT-SZOM Kürt kielégíthetőség Kürtmondat (legfeljebb egy pozitív literál). Legalább egy szó szerint igaznak kell lennie. P
XOR-SZOM Xor kielégíthetőség Minden záradék XOR műveleteket tartalmaz OR helyett. Minden literál XOR-jának igaznak kell lennie. P

A SAT kiterjesztései

A 2003 óta jelentős népszerűségre szert tett kiterjesztés a kielégíthetőségi modulo elméletek ( SMT ), amelyek a CNF-képleteket lineáris megszorításokkal, tömbökkel, mindenféle megszorítással, értelmezetlen függvényekkel [17] stb. Az ilyen kiterjesztések általában NP-teljesek maradnak, de ma már nagyon hatékony megoldók állnak rendelkezésre, amelyek sok ilyen jellegű megszorítást képesek kezelni.

A kielégíthetőségi probléma nehezebbé válik, ha mind a "mindenkire" ( ∀ ), mind a "vannak léteznek" ( ∃ ) kvantorok megengedik a logikai változók összekapcsolását. Példa egy ilyen kifejezésre: ∀x ∀y ∃z (x ∨ y ∨ z) ∧ (¬x ∨ ¬y ∨ ¬z) ; érvényes, mivel x és y összes értékére megtalálható z megfelelő értéke, ti. z =TRUE, ha x és y is FALSE, és z =FALSE egyébként. Maga a SAT (tacitly) csak ∃ kvantorokat használ. Ha csak ∀ kvantorok megengedettek helyette, akkor az úgynevezett tautológia problémát kapjuk, amely koNP-teljes . Ha mindkét kvantor engedélyezett, a problémát kvantifikált logikai képletproblémának ( QBF ) nevezik, amelyről kimutatható, hogy PSPACE-teljes . Széles körben elterjedt az a vélemény, hogy a PSPACE-teljes problémák szigorúan nehezebbek, mint bármely probléma az NP-ben, bár ez még nem bizonyított. Erősen párhuzamos P-rendszerek használatával a QBF-SAT problémák lineáris időben megoldhatók. [18]

A közönséges SAT megkérdezi, hogy van-e legalább egy olyan változó-hozzárendelés, amely igazzá teszi a képletet. Számos változat foglalkozik az ilyen feladatok számával:

  • A MAJ-SAT megkérdezi, hogy az összes hozzárendelés többsége TRUE-e a képletben. Ismeretes, hogy teljes a PP valószínűségi osztályra.
  • A #SAT, annak megszámlálásának problémája, hogy hány változó-hozzárendelés elégít ki egy képletet, számolási probléma, nem döntési probléma, és #P-teljes .
  • Az EGYEDI SAT [19] annak meghatározásának problémája, hogy egy képletnek pontosan egy hozzárendelése van-e. Teljes az US [20] komplexitási osztálya, amely egy nem-determinisztikus polinomiális idő Turing-géppel megoldható problémákat ír le, amely elfogadja, ha pontosan egy nemdeterminisztikus elfogadási út van, és elutasítja az ellenkezőjét.
  • UNAMBIGUOUS-SAT a kielégítési probléma elnevezése, amikor a bevitel legfeljebb egy kielégítő hozzárendeléssel rendelkező képletekre korlátozódik . A problémát USAT -nek is hívják. [21] Az UNAMBIGUOUS-SAT megoldási algoritmusa bármilyen viselkedést mutathat, beleértve a végtelen hurkolást is, egy több kielégítő hozzárendeléssel rendelkező képletnél. Bár ez a probléma egyszerűbbnek tűnik, Valiant és Vazirani megmutatta [22], hogy ha létezik egy gyakorlatias (azaz randomizált polinomiális idejű ) algoritmus a megoldására, akkor az NP minden problémája ugyanolyan könnyen megoldható.
  • A MAX-SAT, a maximális kielégítési probléma a SAT FNP általánosítása. Kéri a kitételek maximális számát, amelyet bármely hozzárendelés teljesíthet. Hatékony közelítő algoritmusokkal rendelkezik, de NP-nehéz pontosan megoldani. Még rosszabb, hogy APX -teljes, ami azt jelenti, hogy ehhez a problémához nincs polinomiális idő közelítési séma (PTAS), hacsak nem P=NP.
  • A WMSAT egy olyan minimális súlyú hozzárendelés megtalálásának problémája, amely kielégít egy monoton Boole-képletet (vagyis egy tagadás nélküli képletet). A propozíciós változók súlyát a feladat bemenetében adjuk meg. Egy hozzárendelés súlya a valódi változók súlyának összege. Ez a probléma NP-teljes (lásd [23] Th. 1).

Az egyéb általánosítások közé tartozik az első- és másodrendű logika kielégíthetősége, a kényszer-elégedettségi problémák, a 0-1 egész számok programozása .

Kielégítő feladat megtalálása

Míg a SAT döntési probléma, addig a kielégítő feladat megtalálásának keresési problémája SAT-ra csökken. Ez azt jelenti, hogy minden olyan algoritmus, amely helyesen válaszol, ha a SAT egy példánya megoldható, felhasználható a kielégítő hozzárendelés megtalálására. Először a kérdést a megadott Φ formulán tesszük fel. Ha a válasz "nem", a képlet nem kielégítő. Ellenkező esetben a kérdést a részben példányosított Φ { <i id="mwBJ8">x</i> <sub id="mwBKA">1</sub> =TRUE}, azaz Φ képletre tesszük fel úgy, hogy az első x 1 változót TRUE-ra cseréljük, és ennek megfelelően egyszerűsítjük. Ha a válasz "yes", akkor x 1 =TRUE, ellenkező esetben x 1 =FALSE. Más változók értékei utólag ugyanígy megtalálhatók. Az algoritmusnak összesen n +1 futtatására van szükség, ahol n a különböző változók száma Φ-ben.

Ezt a tulajdonságot a komplexitáselmélet számos tételében használják:

NP ⊆ P/poli ⇒ PH = Σ <sub id="mwBLA">2</sub> ( Karp–Lipton tétel )
NP ⊆ BPP ⇒ NP = RP
P = NP ⇒ FP = FNP

Algoritmusok a SAT megoldásához

Mivel a SAT probléma NP-teljes, csak exponenciális legrosszabb eset bonyolultságú algoritmusok ismertek rá. Ennek ellenére a 2000-es években fejlesztettek ki hatékony és méretezhető SAT algoritmusokat, amelyek drámai előrelépést tettek lehetővé a több tízezer változót és milliónyi megszorítást (vagyis záradékot) tartalmazó problémapéldányok automatikus megoldásában. Az elektronikus tervezési automatizálás (EDA) ilyen problémái közé tartozik például a formális ekvivalencia-ellenőrzés, a modellellenőrzés, a csővezetékes mikroprocesszorok formális ellenőrzése, [17] az automatikus tesztminta generálás, az FPGA -k útválasztása, [24] a tervezés és az ütemezési problémák stb. A SAT-megoldó motor az elektronikus tervezőautomatizálási eszköztár lényeges elemének is számít.

A modern SAT-megoldók által használt főbb technikák közé tartozik a Davis–Putnam–Logemann–Loveland algoritmus (vagy DPLL), a konfliktusvezérelt záradéktanulás (CDCL) és a sztochasztikus helyi keresési algoritmusok, például a WalkSAT . Szinte minden SAT megoldó tartalmaz időtúllépést, így ésszerű időn belül leállnak, még akkor is, ha nem találnak megoldást. A különböző SAT-megoldók a különböző példányokat könnyűnek vagy nehéznek találják, és egyesek a kielégíthetetlenség bizonyításában, mások pedig a megoldások megtalálásában jeleskednek.

A SAT-megoldókat SAT-megoldó versenyeken fejlesztik és hasonlítják össze. [25] A modern SAT-megoldók jelentős hatást gyakorolnak többek között a szoftverellenőrzés, a mesterséges intelligencia kényszermegoldása és az operációkutatás területére is.

Lásd még

  • Kielégíthetetlen mag
  • Kielégíthetőségi modulo elméletek
  • Számolás SAT
  • Planar SAT
  • Karloff–Zwick algoritmus
  • Az áramkör kielégíthetősége

Megjegyzések

  1. ↑ The 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.
  2. ↑ 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.
  3. ↑ i.e. such that one literal is not the negation of the other
  4. ↑ Formally, generalized conjunctive normal forms with a ternary boolean function R are employed, which is TRUE just if 1 or 3 of its arguments is. An input clause with more than 3 literals can be transformed into an equisatisfiable conjunction of clauses á 3 literals similar to above; i.e. XOR-SAT can be reduced to XOR-3-SAT.

Külső linkek

Hivatkozások

További hivatkozások a megjelenés dátuma szerint:  

Ez a cikk az ACM SIGDA e-hírlevél rovatának anyagát tartalmazza, Prof. Karem Sakallah



Az eredeti szöveg itt érhető elSablon:Logic

  1. ↑ Ohrimenko, Olga; Stuckey, Peter J. & Codish, Michael, Principles and Practice of Constraint Programming – CP 2007, pp. 544–558, DOI 10.1007/978-3-540-74970-7_39.
  2. ↑ Hong (2010. november 1.). „QED: Quick Error Detection tests for effective post-silicon validation”. 2010 IEEE International Test Conference, 1–10. o. DOI:10.1109/TEST.2010.5699215.  
  3. ↑ Karp, Richard M..szerk.: Raymond E. Miller: Reducibility Among Combinatorial Problems, Complexity of Computer Computations. New York: Plenum, 85–103. o. (1972). ISBN 0-306-30707-3. Hozzáférés ideje: 2020. május 7.  Here: p.86
  4. ↑ Alfred V. Aho and John E. Hopcroft and Jeffrey D. Ullman. The Design and Analysis of Computer Algorithms. Reading/MA: Addison-Wesley (1974). ISBN 0-201-00029-6  Here: p.403
  5. ↑ Massacci (2000. február 1.). „Logical Cryptanalysis as a SAT Problem” (angol nyelven). Journal of Automated Reasoning 24 (1), 165–203. o. DOI:10.1023/A:1006326723002. ISSN 1573-0670.  
  6. ↑ Mironov (2006. május 10.). „Applications of SAT Solvers to Cryptanalysis of Hash Functions” (angol nyelven). Theory and Applications of Satisfiability Testing - SAT 2006, Berlin, Heidelberg 4121, 102–115. o, Kiadó: Springer. DOI:10.1007/11814948_13.  
  7. ↑ Vizel (2015). „Boolean Satisfiability Solvers and Their Applications in Model Checking”. Proceedings of the IEEE 103 (11), 2021–2035. o. DOI:10.1109/JPROC.2015.2455034.  
  8. ↑ Cook (1971). „The Complexity of Theorem-Proving Procedures”. Proceedings of the 3rd Annual ACM Symposium on Theory of Computing, 151–158. o. DOI:10.1145/800157.805047.  
  9. ↑ Alfred V. Aho. The Design and Analysis of Computer Algorithms. Addison-Wesley (1974). ISBN 9780201000290 ; here: Thm.10.4
  10. ↑ Schöning, Uwe. A Probabilistic Algorithm for k-SAT and Constraint Satisfaction Problems, Proc. 40th Ann. Symp. Foundations of Computer Science, 410–414. o.. DOI: 10.1109/SFFCS.1999.814612 (1999. október 1.). ISBN 0-7695-0409-4 
  11. ↑ Bart Selman (1996). „Generating Hard Satisfiability Problems”. Artificial Intelligence 81 (1–2), 17–29. o. DOI:10.1016/0004-3702(95)00045-3.  
  12. ↑ a b c (1978) „The complexity of satisfiability problems”.: 216–226.  Forráshivatkozás-hiba: Érvénytelen <ref> címke, „schaefer” nevű forráshivatkozás többször van definiálva eltérő tartalommal
  13. ↑ (Schaefer, 1978), p.222, Lemma 3.5
  14. ↑ Arkin (2018. december 11.). „Selecting and covering colored points” (angol nyelven). Discrete Applied Mathematics 250, 75–86. o. DOI:10.1016/j.dam.2018.05.011. ISSN 0166-218X.  
  15. ↑ Buning (1995). „Resolution for Quantified Boolean Formulas”. Information and Computation 117 (1), 12–18. o, Kiadó: Elsevier. DOI:10.1006/inco.1995.1025.  
  16. ↑ Moore, Cristopher (2011), The Nature of Computation, <https://books.google.com/books?id=z4zMiZyAE1kC&pg=PA366>.
  17. ↑ a b R. E. Bryant, S. M. German, and M. N. Velev, Microprocessor Verification Using Efficient Decision Procedures for a Logic of Equality with Uninterpreted Functions, in Analytic Tableaux and Related Methods, pp. 1–13, 1999.
  18. ↑ Alhazov (2003). „Solving a PSPACE-Complete Problem by Recognizing P Systems with Restricted Active Membranes”. Fundamenta Informaticae 58, 67–77. o.   Here: Sect.3, Thm.3.1
  19. ↑ Blass (1982. október 1.). „On the unique satisfiability problem”. Information and Control 55 (1), 80–88. o. DOI:10.1016/S0019-9958(82)90439-9. ISSN 0019-9958.  
  20. ↑ Complexity Zoo:U - Complexity Zoo. complexityzoo.uwaterloo.ca. [2019. július 9-i dátummal az eredetiből archiválva]. (Hozzáférés: 2019. december 5.)
  21. ↑ Kozen, Dexter C.. Supplementary Lecture F: Unique Satisfiability, Theory of Computation, Texts in Computer Science (angol nyelven). London: Springer-Verlag, 180. o. (2006. május 10.). ISBN 9781846282973 
  22. ↑ Valiant (1986). „NP is as easy as detecting unique solutions”. Theoretical Computer Science 47, 85–93. o. DOI:10.1016/0304-3975(86)90135-0.  
  23. ↑ Buldas (2017. május 10.). „Simple Infeasibility Certificates for Attack Trees” (angol nyelven). Advances in Information and Computer Security 10418, 39–55. o, Kiadó: Springer International Publishing. DOI:10.1007/978-3-319-64200-0_3.  
  24. ↑ Gi-Joon Nam (2002). „A new FPGA detailed routing approach via search-based Boolean satisfiability”. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 21 (6), 674. o. DOI:10.1109/TCAD.2002.1004311.  
  25. ↑ The international SAT Competitions web page. (Hozzáférés: 2007. november 15.)
A lap eredeti címe: „https://hu.wikipedia.org/w/index.php?title=Logikai_kielégítési_probléma&oldid=25002686”