Kielégíthetőségi probléma Boole-képleteknél

Az oldal jelenlegi verzióját még nem ellenőrizték tapasztalt közreműködők, és jelentősen eltérhet a 2021. június 15-én felülvizsgált verziótól ; az ellenőrzések 3 szerkesztést igényelnek .

A Boole-képletek ( SAT , vyp ) kielégíthetőségének problémája a számítási komplexitás elmélete szempontjából fontos algoritmikus probléma .

A feladatpéldány egy logikai képlet , amely csak változónevekből, zárójelekből és műveletekből ( ÉS ), ( OR ) és ( HE ) áll. A probléma a következő: lehetséges-e hamis és igaz értékeket rendelni a képletben előforduló összes változóhoz úgy, hogy a képlet igaz legyen? $\ék$ $\vee$ $\neg$

A Stephen Cook által 1971-ben bebizonyított Cook-tétel szerint a konjunktív normál formában írt Boole-képletek SAT-problémája NP-teljes . A konjunktív formában való írás követelménye elengedhetetlen, hiszen például a diszjunktív normál formában bemutatott képletek SAT-problémája a képletrekord méretétől függően lineáris időben triviálisan megoldódik (a képlet kielégítéséhez csak a jelenléte legalább egy olyan kötőszóra van szükség , amely nem tartalmaz egyszerre és nem tagadást valamelyik változóhoz ). $x$ $\neg x$ $x$

Pontos megfogalmazás

A felismerési probléma pontos megfogalmazása érdekében egy véges ábécét rögzítünk, amelynek segítségével nyelvi példányokat adunk meg. Hopcroft , Motwani és Ullman Bevezetés az automataelméletbe , a nyelvekbe és a számításba című könyvükben a következő ábécé használatát javasolja : . ${\displaystyle \{\wedge ,\vee ,\neg ,(,),x,0,1\))$

Az ábécé használatakor a zárójelek és az operátorok természetesen íródnak, és a változók a következő neveket kapják: , számuk alapján bináris jelöléssel . ${\megjelenítési stílus x1,x10,x11,x100,\pontok }$

Legyen néhány logikai képlet , amely a szokásos matematikai jelöléssel van írva, karakterhosszúságú. Ebben az egyes változók minden előfordulását legalább egy szimbólum írta le, ezért ebben a képletben legfeljebb változó szerepel. Ez azt jelenti, hogy a fent javasolt jelölésben minden változó szimbólumokkal lesz írva . Ebben az esetben az új jelölésben a teljes képlet karakterhosszú lesz, vagyis a karakterlánc hossza polinomszámmal fog növekedni . $N$ $N$ $O\left(\log{N}\right)$ $O\bal(N\log{N}\jobb)$

Például a képlet a következő lesz : . $a\wedge\neg(b\vee c)$ $x1\wedge\neg(x10\vee x11)$

Számítási összetettség

Stephen Cook 1970-es cikkében vezették be először az " NP-teljes probléma " kifejezést , és a SAT probléma volt az első olyan probléma, amelyre ezt a tulajdonságot bebizonyították.

A Cook-tétel bizonyítása során az NP osztály minden egyes problémája kifejezetten SAT-ra redukálódik. A Cook-féle eredmények megjelenése után az NP-teljesség számos egyéb problémára is bebizonyosodott. Ilyenkor leggyakrabban egy-egy feladat NP-teljességének bizonyítására adjuk meg a SAT-probléma adott feladatra való polinomiális redukcióját , esetleg több lépésben, azaz több köztes feladat felhasználásával.

A SAT probléma speciális esetei

A SAT probléma érdekes, fontos speciális esetei a következők:

a konjunktív normál formában (SATCNF vagy VKNF) lévő Boole-képletek kielégíthetőségének problémája hasonló probléma, egy feltétellel a képlethez: konjunktív normál formában kell írni ; szintén NP-teljes ;
kielégíthetőségi probléma Boole-képletekhez k-konjunktív normál formában (k-SAT vagy k-SAT) - kielégítési probléma, feltéve, hogy a képlet k-konjunktív normál formában van írva ; ez a probléma NP-teljes a . A probléma megoldásához használhatja a valószínűségi Schoening algoritmust ; $k\geq 3$
a 2-konjunktív normál formában lévő Boole-képletek kielégíthetőségi problémája polinomiális megoldással rendelkezik, azaz a P osztályba tartozik .

CDCL megoldók

A SAT-feladatok párhuzamosításának egyik leghatékonyabb módszere a CDCL-megoldók (CDCL, angol konfliktusvezérelt záradéktanulás ), amelyek a DPLL algoritmus nem kronologikus változataira épülnek [1] [2] .

Lásd még

Jegyzetek

↑ Marques-Silva JP GRASP: A propozíciós kielégíthetőség keresési algoritmusa / JP Marques-Silva, KA Sakallah // IEEE Transactions on Computers. - 1999. - 1. évf. 48, 5. sz. - P. 506-521.
↑ Semenov A. A., Zaikin O. S. Algorithms for constructing dekompozíciós halmazok SAT-problémák nagyblokkos párhuzamosítására. „Matematika” sorozat 2012. V. 5, 4. sz. S. 79-94

Linkek

A nemzetközi SAT versenyek weboldala
A Sat Live egy általános oldal a SAT-ról.

NP-teljes problémák
A halmozás (csomagolás) maximalizálási problémája	Csomagolás konténerekbe kétdimenziós csomagolás lineáris csomagolás súly szerinti csomagolás érték szerinti csomagolás A hátizsák probléma
gráfelmélet halmazelmélet	Csúcsborítási probléma Kattintson a probléma Egy független halmaz (halmaz) problémája Állítsa be a fedési problémát Steiner probléma Az utazó eladó probléma Általános utazó eladó probléma
Algoritmikus problémák	Kielégíthetőségi probléma Boole-képleteknél (konjunktív normál formában)
Logikai játékok és rejtvények	Általános címkék (játék N 2 -1-ben) legrövidebb megoldási probléma Problémák, amelyek megoldásait a Tetrisben alkalmazzák Általános Sudoku probléma Latin négyzet kitöltési probléma Kakuro feladata
Nehézségi osztályok Operációkutatás Optimalizálás Kombinatorikus optimalizálás Alkalmazott matematika Algoritmusok elmélete Dinamikus programozás 21 NP-teljes Karp probléma