Boolsk tilfredsstillelse

Boolsk tilfredsstillelse , eller proposisjonell tilfredsstillelse eller SAT , er problemet med å avgjøre om en boolsk formel er tilfredsstillende eller utilfredsstillende. Formelen sies å være tilfredsstillende hvis variablene kan tilordnes slik at formelen antar den sanne sannhetsverdien . Motsatt sies det å være utilfredsstillende hvis denne oppgaven ikke eksisterer (derfor er funksjonen uttrykt av formelen identisk falsk).

Problemet med å bestemme boolsk tilfredsstillelse

I kompleksitetsteori er det boolske tilfredsstillelsesproblemet (SAT) et beslutningsproblem, hvis instans er et boolsk uttrykk dannet av operatorer AND, OR, NOT, "(", ")" brukt på variabler og sett med variabler.

Spørsmålet er dette: gitt et uttrykk, er det noen tilordning av SANNE og FALSE verdier som gjør hele uttrykket sant? En formel for proposisjonell logikk sies å være tilfredsstillende hvis en slik oppgave eksisterer. SAT-problemet er av sentral betydning i mange områder av informatikk, inkludert teoretisk informatikk , studiet av algoritmer , maskinvaredesign, etc.

Uten tap av generalitet kan problemet spores tilbake til det spesielle tilfellet der formelen er uttrykt i konjunktiv normalform (CNF), det vil si som en AND av klausuler som hver er dannet av en OR av bokstaver. Faktisk, ved å bruke De Morgans teoremer , kan formelen spores tilbake til tilfellet der NOT-operatorene bare brukes på variabler, og ikke på uttrykk; vi refererer til en variabel eller dens negasjon som en bokstavelig . For eksempel er både x 1 og ikke ( x 2 ) bokstavelig, den første positive og den andre negative . Hvis vi ELLER en gruppe bokstaver, lager vi en klausul som nevnt , for eksempel ( x 1 eller ikke ( x 2 )). Til slutt vurderer vi formlene som er konjunksjon (AND) av klausuler - faktisk opererer vi i CNF.

Cook -Levin-teoremet viser at problemet med å avgjøre om en proposisjonell formel er tilfredsstillende er NP-fullstendig . For eksempel er NP-fullstendig (og kalles "3SAT", "3CNFSAT" eller "3-tilfredshet") problemet med å bestemme tilfredsstillelsen til en formel der hver klausul har maksimalt tre bokstaver. Imidlertid, hvis vi begrenser hver klausul til å ha maksimalt to bokstaver, er det resulterende problemet, kalt 2SAT , NL-fullstendig . Å bestemme tilfredsstillelsen til en formel der hver klausul er en Horn-setning (det vil si at den inneholder høyst én positiv bokstav) er et P-komplett problem og kalles Horn-tilfredshet .

SAT var det første beslutningsproblemet hvis NP-fullstendighet ble vist. Til tross for dette har det blitt gjort enorme fremskritt det siste tiåret, og identifisert skalerbare algoritmer for å løse SAT-er med titusenvis av variabler og millioner av begrensninger. Eksempler på disse problemene er til stede i modellsjekking , elektronisk designautomatisering (EDA), FPGA , logikksyntese , etc.

Kompleksitet

NP-fullstendighet

Før 1971 og Cook-Levin-teoremet eksisterte ikke konseptet med et NP-komplett problem i det hele tatt. Som vi har sett, forblir dette problemet av denne kompleksiteten selv om man er i CNF ; riktignok med 3 variabler per klausul (3-CNF), i uttrykk som:

( x 11 ELLER x 12 ELLER x 13 ) OG ( x 21 OR x 22 OR x 23 ) OG ( x 31 OR x 32 OR x 33 ) OG ...

der hver x er en variabel eller negasjonen av en variabel, og hver variabel kan vises flere ganger i formeluttrykket.

En nyttig egenskap ved Cooks foreslåtte reduksjon er at settet med løsninger (oppdrag) ikke reduseres i antall. For eksempel, hvis en graf har 17 gyldige 3-farger, vil den produserte SAT-formelen fortsatt ha 17.

2-tilfredsstillelse

SAT-problemet er enklere hvis formlene er begrenset til DNF , den såkalte disjunktive normalformen, der leddsetningene er AND av bokstavelige (muligens negerte) og kombineres i OR med hverandre. Denne normale formen er dualen av CNF, og en formel i DNF er fortsatt tilfredsstillende hvis og bare hvis minst en av dens klausuler er; for at dette skal skje, må en klausul ikke inneholde både x og IKKE x for en eller annen variabel x . Verifikasjonen av dette problemet kan utføres i polynomisk tid.

SAT er åpenbart enklere hvis antall bokstaver per klausul er begrenset til maksimalt 2, og i dette tilfellet er problemet, som nevnt, 2SAT. Dette problemet kan også løses i polynomtid, og komplett for NL-klassen, og kan transformeres ytterligere ved å modifisere AND-forbindelsene med XOR , og lage et eller-eksklusivt 2-tilfredshetsfullt , komplett problem for SL = L -klassen .

En av de viktigste SAT-restriksjonene er HORNSAT, der formler er konjunksjoner av Horn-klausuler . Problemet kan løses i polynomisk tid ved hjelp av Horn-tilfredshetsalgoritmen og er derfor P-fullstendig . Det kan sees på som den P-komplekse versjonen av SAT-problemet.

Forutsatt at kompleksitetsklassene P og NP ikke er like, er ingen av disse SAT-reduksjonene som nettopp er beskrevet NP-fullstendige. Antakelsen om at P og NP er ulik er imidlertid ikke bevist til dags dato, og representerer et av de viktigste målene som forfølges av matematikere over hele verden.

3-tilfredsstillelse

Det er et spesielt tilfelle av k - tilfredsstillelse ( k -SAT), der hver setning inneholder høyst k = 3 bokstaver. Det var et av Karps 21 NP-komplette problemer .

Her er et eksempel, der ~ indikerer NOT-operatoren:

E = ( x 1 OR ~ x 2 OR ~ x 3 ) OG ( x 1 OR x 2 OR x 4 )

E har to setninger (inneholdt i parentes), fire bokstaver ( x 1 , x 2 , x 3 , x 4 ), og k = 3 (tre bokstaver per klausul).

Siden k-SAT (generelt tilfelle) koker ned til 3-SAT, og 3-SAT kan vise seg å være NP-komplett , kan det også brukes til å bevise at andre problemer er det. Prosedyren består i å vise at en løsning av et annet problem kan brukes til å løse 3-SAT. Et eksempel på et problem der denne metoden har blitt brukt er crack-problemet . Det er ofte lettere å bruke reduksjoner fra 3-SAT enn fra SAT selv for å bevise at visse problemer er NP-fullstendige.

Utvidelser til SAT

En utvidelse som har fått en viss popularitet siden 2003 har vært Satisfiability-modulteoriene som kan berike CNF-formler med lineære begrensninger, vektorer, alle-forskjellige begrensninger, utolkede funksjoner, etc. Disse utvidelsene forblir vanligvis NP-komplette; noen effektive løsere har imidlertid evnen til å håndtere dem som om de var enkle begrensninger.

Tilfredsstillelsesproblemet ser ut til å bli vanskeligere (PSPACE-komplett) hvis vi tillater bruk av kvantifiserere som "for hver" eller "det er noen" som opererer på boolske variabler. Et eksempel på slike uttrykk kan være:

Hvis vi utelukkende bruker kvantifisereren , står vi fortsatt overfor SAT-problemet. Hvis vi i stedet bare tillater bruken av kvantifisereren , blir det et Co-NP-komplett problem med å identifisere om formen viser seg å være en tautologi . Hvis vi tillater bruk av begge, kalles det et boolsk kvantifisert formelproblem (QBF), som har vist seg å være PSPACE-komplett . Det er en utbredt oppfatning at slike problemer er strengt tatt vanskeligere enn noen NP, selv om bevis for dette faktum ikke er vist.

Det finnes en rekke varianter av problemet som påvirker antall variabeltilordninger som gjør formelen sann. Den vanlige SAT ber bare om at minst én skal eksistere; MAJSAT, som krever flertallet av alle oppdrag for å gjøre det sant, er komplett for PP , sannsynlighetsklassen. Problemet med hvor mange oppgaver som tilfredsstiller en gitt formel er ikke et beslutningsproblem, og finnes i #P . UNIQUE-SAT eller USAT er i stedet problemet med å avgjøre når en formel, kjent for å ha enten en eller ingen oppgave som tilfredsstiller den, faktisk har en eller null. Selv om dette problemet kan virke enklere , har det vist seg at hvis det er en algoritme ( randomisert polynomtid ) som løser dette problemet, så kan alle problemer i NP løses med samme letthet.

Problemet med maksimal tilfredsstillelse , en FNP- generalisering av SAT, ber om maksimalt antall klausuler som kan tilfredsstilles av hver oppgave. Det er noen gode algoritmer som tilnærmer det effektivt, men det er NP-vanskelig å løse det nøyaktig. Enda mer nedslående, det er også et APX-komplett problem , dvs. det er ingen polynom-tidstilnærming for dette problemet med mindre det er bevist at P = NP!

SAT-oppløsningsalgoritmer

Det er to klasser av høyytelsesalgoritmer som løser forekomster av SAT-problemet: moderne varianter av DPLL- algoritmen , slik som Chaff-algoritmen eller GRASP , og stokastiske lokale søkealgoritmer som WalkSAT .

En SAT DPLL-løser bruker systematisk tilbakesporingsprosedyren med det formål å utforske rommet av tilordninger av variabler (muligens av eksponentiell størrelse), på jakt etter tilordninger som tilfredsstiller formelen. Grunnlaget for søkeprosedyren ble foreslått på begynnelsen av 1960-tallet i to artikler som nå er kjent som en del av Davis-Putnam-Logemann-Loveland ( DPLL ) algoritmen. Moderne SAT-løsere, utviklet i løpet av det siste tiåret, beriker disse konseptene med konfliktanalyseprosedyrer, klausullæring, ikke-kronologisk tilbakesporing (også kjent som backjumping ), lineær forplantning, adaptiv forgrening og tilfeldige omstarter. Det har vist seg at disse tilleggene til grunnleggende funksjon var nødvendige for å kunne håndtere de større tilfellene av SAT, som har oppstått i teoretiske studier innen felt som kunstig intelligens, operasjonell forskning og andre. Noen kraftige løsere er i det offentlige domene; Spesielt MiniSAT , vinneren av SAT-konkurransen i 2005, består av bare 600 linjer med kode.

Genetiske algoritmer og andre generelle anvendelsesprosedyrer har blitt brukt for å løse SAT-problemer, spesielt i nærvær av begrenset (eller til og med ingen) kunnskap om den spesifikke strukturen til problemforekomsten som skal løses. Noen typer store (tilfredsstillende) tilfeldige forekomster av SAT kan løses med Survey Propagation (SP).

Merknader

  1. D. Babić, J. Bingham og AJ Hu, "B-Cubing: New Possibilities for Efficient SAT-Solving", IEEE Transactions on Computers 55 (11): 1315–1324, 2006.
  2. RE Bryant, SM German og MN Velev, "Mikroprosessorverifisering ved bruk av effektive beslutningsprosedyrer for en logikk om likhet med utolkede funksjoner," i Analytic Tableaux and Related Methods, s. 1-13, 1999.
  3. E. Clarke, A. Biere, R. Raimi og Y. Zhu, "Bounded Model Checking Using Satisfiability Solving," Formal Methods in System Design, vol. 19, nei. 1, 2001.
  4. SA Cook, "The Complexity of Theorem Proving Procedures," i Proc. 3rd Ann. ACM Symp. på Theory of Computing, s. 151–158, Association for Computing Machinery, 1971.
  5. M. Davis og H. Putnam, "A Computing Procedure for Quantification Theory," Journal of the Association for Computing Machinery, vol. 7, s. 201-215, 1960.
  6. M. Davis, G. Logemann og D. Loveland, "A Machine Program for Theorem-Proving," Communications of the ACM, vol. 5, nei. 7, s. 394–397, 1962.
  7. N. Een og N. Sorensson, "An Extensible SAT-solver," i Satisfiability Workshop, 2003.
  8. Michael R. Garey og David S. Johnson. Datamaskiner og intractability: En guide til teorien om NP-fullstendighet. WH Freeman, 1979. ISBN 0-7167-1045-5 A9.1: LO1 - LO7, s. 259-260.
  9. G.-J. Nam, KA Sakallah og R. Rutenbar, "A New FPGA Detailed Routing Approach via Search-Based Boolean Satisfiability," IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 21, nei. 6, s. 674–684, 2002.
  10. JP Marques-Silva og KA Sakallah, "GRASP: A Search Algorithm for Propositional Satisfiability," IEEE Transactions on Computers, vol. 48, nei. 5, s. 506-521, 1999.
  11. J.-P. Marques-Silva og T. Glass, "Combinational Equivalence Checking Using Satisfiability and Recursive Learning," i Proc. Design, Automation and Test in Europe Conference, s. 145-149, 1999.
  12. MW Moskewicz, CF Madigan, Y. Zhao, L. Zhang og S. Malik, "Chaff: engineering an efficient SAT solver," i Proc. 38th ACM / IEEE Design Automation Conference, s. 530-535, Las Vegas, Nevada, 2001.
  13. M. Perkowski og A. Mishchenko, "Logic Synthesis for Regular Layout using Satisfiability," i Proc. Intl Workshop on Boolean Problems, 2002.

Eksterne lenker

SAT-løsere:

Publikasjoner / konferanser:

Referansemål:

SAT-løsere generelt:

Denne artikkelen inneholder utdrag fra: SIGDA e-nyhetsbrev av Prof. Karem Sakallah
Originalteksten er tilgjengelig på denne adressen.