Satisfacție booleană

De la Wikipedia, enciclopedia liberă.
Salt la navigare Salt la căutare

Satisfacția booleană , sau satisfacția propozițională sau SAT , este problema de a determina dacă o formulă booleană este satisfăcătoare sau nesatisfăcătoare. Se spune că formula este satisfăcătoare dacă variabilele pot fi atribuite astfel încât formula să-și asume adevărata valoare de adevăr. În schimb, se spune că este nesatisfăcător dacă această atribuire nu există (prin urmare, funcția exprimată prin formulă este identică falsă).

Problema determinării satisfacției booleene

În teoria complexității , problema de satisfacție booleană (SAT) este o problemă de decizie, a cărei instanță este o expresie booleană formată din operatori ȘI, SAU, NU, "(", ")" aplicată variabilelor și seturilor de variabile.

Întrebarea este următoarea: dată o expresie, există vreo atribuire a valorilor ADEVĂRATE și FALSE care să facă întreaga expresie adevărată? Se spune că o formulă a logicii propoziționale este satisfăcătoare dacă există o astfel de atribuire. Problema SAT are o importanță centrală în multe domenii ale informaticii, inclusiv informatica teoretică , studiul algoritmilor , proiectarea hardware etc.

Fără pierderea generalității, problema poate fi trasată înapoi în cazul particular în care formula este exprimată în formă normală conjunctivă (CNF), adică ca ȘI a unor clauze formate fiecare dintr-un OR al literelor. De fapt, prin aplicarea teoremelor lui De Morgan , formula poate fi urmărită înapoi în cazul în care operatorii NU sunt aplicați doar variabilelor și nu expresiilor; ne referim la o variabilă sau la negarea acesteia ca la un literal . De exemplu, atât x 1 cât și nu ( x 2 ) sunt literali, primul pozitiv și al doilea negativ . Dacă SAU un grup de literali, creăm o clauză așa cum am menționat, cum ar fi ( x 1 sau nu ( x 2 )). În cele din urmă, luăm în considerare formulele care sunt conjuncție (ȘI) ale clauzelor - de fapt, operăm în CNF.

Teorema Cook-Levin arată că problema determinării dacă orice formulă propozițională este satisfăcătoare este NP-completă . De exemplu, NP-complet (și se numește "3SAT", "3CNFSAT" sau "3-satisfiabilitate") este problema determinării satisfacției unei formule în care fiecare clauză are maximum trei literali. Cu toate acestea, dacă restrângem fiecare clauză să aibă maximum doi literali, atunci problema rezultată, numită 2SAT , este NL-completă . Determinarea satisfacției unei formule în care fiecare clauză este o clauză Horn (adică conține cel mult un literal pozitiv) este o problemă P-completă și se numește satisfacție Horn .

SAT a fost prima problemă de decizie a cărei completitudine NP a fost arătată. În ciuda acestui fapt, s-au făcut progrese enorme în ultimul deceniu, identificând algoritmi scalabili pentru a rezolva SAT-urile cu zeci de mii de variabile și milioane de constrângeri. Exemple de astfel de probleme sunt prezente în verificarea modelelor , Electronic Design Automation (EDA), FPGA , sinteza logică etc.

Complexitate

NP-completitudine

Înainte de 1971 și teorema lui Cook-Levin , conceptul unei probleme NP complete nu exista deloc. După cum am văzut, această problemă rămâne de această complexitate chiar dacă cineva se află în CNF ; deși cu 3 variabile pe clauză (3-CNF), în expresii precum:

( x 11 SAU x 12 SAU x 13 ) ȘI
( x 21 SAU x 22 SAU x 23 ) ȘI
( x 31 SAU x 32 SAU x 33 ) ȘI ...

unde fiecare x este o variabilă sau negarea unei variabile și fiecare variabilă poate apărea de mai multe ori în expresia formulă.

O proprietate utilă a reducerii propuse de Cook este că setul de soluții (atribuții) nu este redus ca număr. De exemplu, dacă un grafic are 17 3 culori valide, formula SAT produsă va avea în continuare 17.

2-satisfacție

Pictogramă lupă mgx2.svg Același subiect în detaliu: 2-satisfacție .

Problema SAT este mai simplă dacă formulele sunt limitate la DNF , așa-numita formă normală disjunctivă, în care clauzele sunt ȘI ale literelor (posibil negate) și sunt combinate în OR între ele. Această formă normală este dualitatea CNF și o formulă în DNF este încă satisfăcătoare dacă și numai dacă cel puțin una dintre clauzele sale este satisfăcătoare; pentru ca acest lucru să se întâmple, o clauză nu trebuie să conțină atât x, cât și NU x pentru o variabilă x . Verificarea acestei probleme poate fi efectuată în timp polinomial.

SAT este evident mai simplu dacă numărul literelor pe clauză este limitat la maximum 2 și, în acest caz, problema este, așa cum am menționat, 2SAT. De asemenea, rezolvabilă în timp polinomial și completă pentru clasa NL, această problemă poate fi transformată în continuare prin modificarea conectivelor ȘI cu XOR , creând o problemă completă sau exclusivă de 2 satisfacții pentru clasa SL = L.

Una dintre cele mai importante restricții SAT este HORNSAT, unde formulele sunt conjuncții ale clauzelor Horn . Problema poate fi rezolvată în timp polinomial prin algoritmul de satisfacție Horn și, prin urmare, este P-completă . Poate fi văzută ca versiunea complexă P a problemei SAT.

Presupunând că clasele de complexitate P și NP nu sunt egale, niciuna dintre aceste reduceri SAT descrise doar nu sunt NP-complete. Presupunerea, cu toate acestea, că P și NP sunt inegale nu este dovedită până în prezent și reprezintă unul dintre obiectivele majore urmărite de matematicieni din întreaga lume.

3-satisfacție

Este un caz special de k- satisfiabilitate ( k -SAT), în care fiecare clauză conține cel mult k = 3 literali. A fost una dintre cele 21 de probleme complete ale lui Karp .

Iată un exemplu, în care ~ indică operatorul NOT:

E = ( x 1 SAU ~ x 2 SAU ~ x 3 ) ȘI ( x 1 SAU x 2 SAU x 4 )

E are două clauze (cuprinse între paranteze), patru litere ( x 1 , x 2 , x 3 , x 4 ) și k = 3 (trei litere per clauză).

Deoarece k-SAT (caz general) se reduce la 3-SAT, iar 3-SAT se poate dovedi a fi NP-complet , poate fi folosit și pentru a demonstra că sunt alte probleme. Procedura constă în a arăta că o soluție a unei alte probleme poate fi utilizată pentru a rezolva 3-SAT. Un exemplu de problemă în care a fost utilizată această metodă este problema crack . Este adesea mai ușor să folosiți reduceri de la 3-SAT decât de la SAT în sine pentru a demonstra că anumite probleme sunt NP-complete.

Extensii ale SAT

O extensie care a câștigat o oarecare popularitate din 2003 a fost teoriile modulului de satisfacție care pot îmbogăți formulele CNF cu constrângeri liniare, vectori, constrângeri diferite , funcții neinterpretate etc. Aceste extensii rămân de obicei NP-complete; unii rezolvători eficienți, cu toate acestea, au capacitatea de a le gestiona ca și cum ar fi constrângeri simple.

Problema satisfacției pare să devină mai dificilă (PSPACE-completă) dacă permitem utilizarea unor cuantificatoare precum „pentru fiecare” sau „există unele” care funcționează pe variabile booleene. Un exemplu de astfel de expresii ar putea fi:

Dacă folosim doar cuantificatorul , ne confruntăm încă cu problema SAT. Dacă în schimb permitem doar utilizarea cuantificatorului , devine o problemă completă a Co-NP a identificării dacă forma se dovedește a fi o tautologie . Dacă permitem utilizarea ambelor, se numește o problemă de formulă cuantificată booleană (QBF), care se dovedește a fi completă cu PSPACE . Se crede pe larg că astfel de probleme sunt strict mai dificile decât orice NP, deși nu a fost demonstrată dovada acestui fapt.

Există o serie de variante ale problemei care afectează numărul de atribuiri variabile care fac formula adevărată. SAT-ul obișnuit cere doar să existe cel puțin unul; MAJSAT, care necesită majoritatea tuturor sarcinilor pentru ao face adevărat, este complet pentru PP , clasa probabilistică. Problema numărului de misiuni care satisfac o anumită formulă nu este o problemă de decizie și se găsește în #P . UNIQUE-SAT sau USAT este, în schimb, problema de a determina când o formulă, cunoscută ca având una sau nicio atribuire care o satisface, are una sau zero, de fapt. Deși această problemă poate părea mai simplă, s- a demonstrat că, dacă există un algoritm ( timp polinom randomizat ) care rezolvă această problemă, atunci toate problemele din NP pot fi rezolvate cu aceeași ușurință.

Problema maximă de satisfacție , o generalizare FNP a SAT, solicită numărul maxim de clauze care pot fi satisfăcute de fiecare sarcină. Există câțiva algoritmi buni care îl aproximează eficient, dar este NP-greu să-l rezolvi exact. Chiar mai descurajant, este, de asemenea, o problemă APX-completă , adică nu există o aproximare polinomială-timp pentru această problemă, cu excepția cazului în care se dovedește că P = NP!

Algoritmi de rezoluție SAT

Există două clase de algoritmi de înaltă performanță care rezolvă instanțele problemei SAT: variante moderne ale algoritmului DPLL , cum ar fi algoritmul Chaff sau GRASP și algoritmi de căutare locale stocastici, cum ar fi WalkSAT .

Un rezolvator SAT DPLL folosește în mod sistematic procedura de urmărire înapoi în scopul explorării spațiului atribuirilor variabile (posibil de magnitudine exponențială), căutând atribuții care să satisfacă formula. Bazele procedurii de căutare au fost propuse la începutul anilor 1960 în două lucrări care sunt acum cunoscute ca parte a algoritmului Davis-Putnam-Logemann-Loveland ( DPLL ). Solvenții moderni SAT, dezvoltați în ultimul deceniu, îmbogățesc aceste concepte cu analiza conflictelor, învățarea clauzelor, retracționarea necronologică (cunoscută și sub denumirea de backjumping ), propagarea liniară, ramificarea adaptivă și repornirea aleatorie. Aceste adăugiri la funcționarea de bază s-au dovedit a fi necesare pentru a face față cazurilor mai mari de SAT, care au apărut în studiul teoretic în domenii precum inteligența artificială, cercetarea operațională și altele. Unii solutori puternici sunt în domeniul public; în special MiniSAT , câștigătorul concursului SAT din 2005, este alcătuit din doar 600 de linii de cod.

Algoritmii genetici și alte proceduri generale de aplicare au fost folosite pentru a rezolva problemele SAT, în special în prezența unor cunoștințe limitate (sau chiar absente) despre structura specifică a instanței problemei care trebuie rezolvată. Unele tipuri de instanțe aleatorii mari (satisfăcătoare) ale SAT pot fi rezolvate cu Propagarea sondajului (SP).

Notă

  1. D. Babić, J. Bingham și AJ Hu, „B-Cubing: Noi posibilități pentru rezolvarea eficientă a SAT”, IEEE Transactions on Computers 55 (11): 1315–1324, 2006.
  2. RE Bryant, SM German și MN Velev, „Verificarea microprocesorului utilizând proceduri decizionale eficiente pentru o logică a egalității cu funcții neinterpretate”, în Tablouri analitice și metode conexe, pp. 1-13, 1999.
  3. E. Clarke, A. Biere, R. Raimi și Y. Zhu, „Bounded Model Checking Using Satisfiability Solving”, Metode formale în proiectarea sistemului, vol. 19, nr. 1, 2001.
  4. SA Cook, „Complexitatea procedurilor de demonstrare a teoremei”, în Proc. 3 Ann. ACM Symp. pe Teoria calculelor, pp. 151–158, Asociația pentru mașini de calcul, 1971.
  5. M. Davis și H. Putnam, „A Computing Procedure for Quantification Theory”, Journal of the Association for Computing Machinery, vol. 7, pp. 201-215, 1960.
  6. M. Davis, G. Logemann și D. Loveland, „A Machine Program for Theorem-Demosting”, Communications of the ACM, vol. 5, nr. 7, pp. 394–397, 1962.
  7. N. Een și N. Sorensson, „Un Extensible SAT-solver”, în Satisfiability Workshop, 2003.
  8. Michael R. Garey și David S. Johnson. Calculatoare și Intractability: Un ghid pentru teoria completitudinii NP. WH Freeman, 1979. ISBN 0-7167-1045-5 A9.1: LO1 - LO7, pp. 259-260.
  9. G.-J. Nam, KA Sakallah și R. Rutenbar, „O nouă abordare detaliată a rutării FPGA prin satisfacție booleană bazată pe căutare”, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 21, nr. 6, pp. 674-684, 2002.
  10. JP Marques-Silva și KA Sakallah, „GRASP: Un algoritm de căutare pentru satisfacția propunerii”, IEEE Transactions on Computers, vol. 48, nr. 5, pp. 506-521, 1999.
  11. J.-P. Marques-Silva și T. Glass, "Combinational Equivalence Checking Using Satisfiability and Recursive Learning", în Proc. Design, Automation and Test in Europe Conference, pp. 145-149, 1999.
  12. MW Moskewicz, CF Madigan, Y. Zhao, L. Zhang și S. Malik, „Chaff: ingineria unui rezolvator SAT eficient”, în Proc. 38th ACM / IEEE Design Automation Conference, pp. 530-535, Las Vegas, Nevada, 2001.
  13. M. Perkowski și A. Mishchenko, „Sinteza logică pentru aspectul regulat utilizând satisfacția”, în Proc. Intl Workshop on Boolean Problems, 2002.

linkuri externe

Solutii SAT:

Publicații / Conferințe:

Repere:

Solutii SAT în general:

Acest articol conține fragmente din: buletinul electronic SIGDA al prof. Karem Sakallah
Textul original este disponibil la această adresă.

Adus de la „ https://it.wikipedia.org/w/index.php?title=Satisfactability_boolean&oldid=119163819 ”