Boolsk tilfredsstillelsesproblem - Boolean satisfiability problem

I logikk og informatikk er problemet med booleske tilfredsstillelse (noen ganger kalt proposisjonelt tilfredsstillelsesproblem og forkortet SATISFIABILITY , SAT eller B-SAT ) problemet med å avgjøre om det finnes en tolkning som tilfredsstiller en gitt boolsk formel . Med andre ord spør den om variablene i en gitt boolsk formel konsekvent kan erstattes av verdiene TRUE eller FALSE på en slik måte at formelen evalueres til TRUE . Hvis dette er tilfellet, kalles formelen tilfredsstillende . På den annen side, hvis ingen slik tildeling eksisterer, er funksjonen uttrykt med formelen FALSK for alle mulige variable tildelinger, og formelen er utilfredsstillende . For eksempel er formelen " a OG IKKE b " tilfredsstillende fordi man kan finne verdiene a  = TRUE og b  = FALSE, som gjør ( a AND NOT b ) = TRUE. I kontrast er " en OG IKKE en " utilfredsstillende.

SAT er det første problemet som ble påvist å være NP-komplett ; se teoremet Cook - Levin . Dette betyr at alle problemer i kompleksitetsklassen NP , som inkluderer et bredt spekter av naturlige beslutnings- og optimaliseringsproblemer, på det meste er like vanskelig å løse som SAT. Det er ingen kjent algoritme som effektivt løser hvert SAT -problem, og det antas generelt at ingen slik algoritme eksisterer; men denne troen er ikke bevist matematisk, og å løse spørsmålet om SAT har en polynom- tidsalgoritme er ekvivalent med P versus NP-problemet , som er et kjent åpent problem i teorien om databehandling.

Imidlertid er heuristiske SAT-algoritmer i 2007 i stand til å løse problemforekomster som involverer titusenvis av variabler og formler som består av millioner av symboler, noe som er tilstrekkelig for mange praktiske SAT-problemer fra f.eks. Kunstig intelligens , kretsdesign og automatisk teorem som beviser .

Grunnleggende definisjoner og terminologi

En -basert utsagnslogikk formel , også kalt boolske uttrykk , er bygget opp av variabler , operatører og ( sammen , også betegnet med ∧), OR ( motsetninger , ∨), NOT ( negasjon , ¬) og parenteser. En formel sies å være tilfredsstillende hvis den kan gjøres SANN ved å tilordne passende logiske verdier (dvs. SANN, FALSK) til variablene. Det boolske tilfredsstillelsesproblemet (SAT) får en formel for å kontrollere om det er tilfredsstillende. Dette beslutningsproblemet er sentralt på mange områder innen informatikk , inkludert teoretisk informatikk , kompleksitetsteori , algoritme , kryptografi og kunstig intelligens .

Det er flere spesielle tilfeller av det boolske tilfredsstillelsesproblemet der formlene må ha en bestemt struktur. En bokstav er enten en variabel, kalt positiv bokstavelig , eller negasjonen av en variabel, kalt negativ bokstavelig . En klausul er en disjunksjon av bokstavene (eller en enkelt bokstav). En klausul kalles en Hornklausul hvis den inneholder høyst en positiv bokstav. En formel er i konjunktiv normal form (CNF) hvis den er en sammenheng av klausuler (eller en enkelt klausul). For eksempel er x ₁ en positiv bokstav, ¬ x ₂ er en negativ bokstav, x ₁ ∨ ¬ x ₂ er en klausul. Formelen ( x ₁ ∨ ¬ x ₂ ) ∧ (¬ x ₁ ∨ x ₂ ∨ x ₃ ) ∧ ¬ x ₁ er i konjunktiv normal form; dens første og tredje ledd er Hornklausuler, men den andre klausulen er ikke. Formelen er tilfredsstillende ved å velge x ₁  = FALSK, x ₂  = FALSK og x ₃ vilkårlig, siden (FALSK ∨ ¬FALSK) ∧ (¬FALSK ∨ FALSK ∨ x ₃ ) ∧ ¬FALSK vurderer til (FALSK ∨ SANN) ∧ (TRUE ∨ FALSE ∨ x ₃ ) ∧ TRUE, og på sin side til TRUE ∧ TRUE ∧ TRUE (dvs. til TRUE). I kontrast er CNF -formelen a ∧ ¬ a , bestående av to ledd i en bokstav, utilfredsstillende, siden den for a = TRUE eller a = FALSE evalueres til TRUE ∧ ¬TRUE (dvs. FALSE) eller FALSE ∧ ¬FALSE (dvs. , igjen FALSK).

For noen versjoner av SAT -problemet er det nyttig å definere forestillingen om en generalisert form for konjunktiv normal form , dvs. som en kombinasjon av vilkårlig mange generaliserte klausuler , sistnevnte har formen R ( l ₁ , ..., l _n ) for noen boolsk funksjon R og (vanlige) bokstaver l _i . Ulike sett med tillatte boolske funksjoner fører til forskjellige problemversjoner. Som et eksempel er R (¬ x , a , b ) en generalisert klausul, og R (¬ x , a , b ) ∧ R ( b , y , c ) ∧ R ( c , d , ¬ z ) er en generalisert konjunktiv normal form. Denne formelen brukes nedenfor , med R som den ternære operatoren som er SANN akkurat når nøyaktig ett av argumentene er.

Ved å bruke lovene i boolsk algebra kan hver proposisjonell logikkformel transformeres til en tilsvarende konjunktiv normalform, som imidlertid kan være eksponensielt lengre. For eksempel omdanner formelen ( x ₁ ∧ y ₁ ) ∨ ( x ₂ ∧ y ₂ ) ∨ ... ∨ ( x _n ∧ y _n ) til konjunktive normalformutbytter

( x ₁  ∨  x ₂  ∨… ∨  x _n ) ∧

( y ₁  ∨  x ₂  ∨… ∨  x _n ) ∧

( x ₁  ∨  y ₂  ∨… ∨  x _n ) ∧

( y ₁  ∨  y ₂  ∨… ∨  x _n ) ∧ ... ∧

( x ₁  ∨  x ₂  ∨… ∨  y _n ) ∧

( y ₁  ∨  x ₂  ∨… ∨  y _n ) ∧

( x ₁  ∨  y ₂  ∨… ∨  y _n ) ∧

( y ₁  ∨  y ₂  ∨… ∨  y _n ) ;

mens førstnevnte er en disjunksjon av n konjunksjoner av 2 variabler, består sistnevnte av 2 ⁿ ledd av n variabler.

Kompleksitet og begrensede versjoner

Ubegrenset tilfredshet (SAT)

SAT var det første kjente NP-komplette problemet, som bevist av Stephen Cook ved University of Toronto i 1971 og uavhengig av Leonid Levin ved National Academy of Sciences i 1973. Fram til den tid var ikke begrepet et NP-komplett problem eksisterer til og med. Beviset viser hvordan alle beslutningsproblemer i kompleksitetsklassen NP kan reduseres til SAT -problemet for CNF -formler, noen ganger kalt CNFSAT . En nyttig egenskap ved Cooks reduksjon er at den beholder antall svar som godtas. For eksempel, å avgjøre hvorvidt en gitt kurve som har en tre-fargestoffer er et annet problem i NP; hvis en graf har 17 gyldige trefarger, vil SAT-formelen produsert av Cook-Levin-reduksjonen ha 17 tilfredsstillende oppgaver.

NP-fullstendighet refererer bare til kjøretiden til de verste tilfellene. Mange av tilfellene som forekommer i praktiske applikasjoner kan løses mye raskere. Se algoritmer for å løse SAT nedenfor.

SAT er trivielt hvis formlene er begrenset til de i disjunktiv normal form , det vil si at de er en disjunksjon av konjunksjoner av bokstavene. En slik formel er virkelig tilfredsstillende hvis og bare hvis minst en av dens konjunksjoner er tilfredsstillende, og en konjunksjon er tilfredsstillende hvis og bare hvis den ikke inneholder både x og IKKE x for noen variabel x . Dette kan kontrolleres i lineær tid. Hvis de er begrenset til å være i fullstendig disjunktiv normal form , der hver variabel vises nøyaktig én gang i hver konjunksjon, kan de kontrolleres i konstant tid (hver konjunksjon representerer en tilfredsstillende oppgave). Men det kan ta eksponentiell tid og plass å konvertere et generelt SAT -problem til en disjunktiv normalform; for et eksempel bytte "∧" og "∨" i det eksponentielle oppblåsingseksemplet ovenfor for konjunktive normalformer.

3-tilfredshet

3-SAT-forekomsten ( x ∨ x ∨ y ) ∧ (¬ x ∨ ¬ y ∨ ¬ y ) ∧ (¬ x ∨ y ∨ y ) redusert til et klikkproblem . De grønne hjørnene danner en 3-klikk og tilsvarer tilfredsstillende oppgave x = FALSK, y = SANN.

Som tilfredsstillelsesproblemet for vilkårlige formler, er det også NP-komplett å bestemme tilfredsheten til en formel i konjunktiv normalform der hver klausul er begrenset til høyst tre bokstaver; dette problemet kalles 3-SAT , 3CNFSAT eller 3-satisfiability . For å redusere det ubegrensede SAT -problemet til 3 -SAT, forvandle hver ledd l ₁ ∨ ⋯ ∨ l _n til en sammenheng av n - 2 ledd

( l ₁ ∨ l ₂ ∨ x ₂ ) ∧

(¬ x ₂ ∨ l ₃ ∨ x ₃ ) ∧

(¬ x ₃ ∨ l ₄ ∨ x ₄ ) ∧ ⋯ ∧

(¬ x _{n - 3} ∨ l _{n - 2} ∨ x _{n - 2} ) ∧

(¬ x _{n - 2} ∨ l _{n - 1} ∨ l _n )

hvor x ₂ , ⋯,  x _{n - 2} er friske variabler som ikke forekommer andre steder. Selv om de to formlene ikke er logisk likeverdige , er de equisatisfiable . Formelen som oppstår ved transformering av alle ledd er maksimalt 3 ganger så lang som originalen, dvs. lengdeveksten er polynom.

3-SAT er en av Karps 21 NP-komplette problemer , og den brukes som utgangspunkt for å bevise at andre problemer også er NP-harde . Dette gjøres ved polynom-tidsreduksjon fra 3-SAT til det andre problemet. Et eksempel på et problem der denne metoden har blitt brukt er klikkproblemet : gitt en CNF-formel bestående av c- ledd, består den tilsvarende grafen av et toppunkt for hver bokstav, og en kant mellom hver to ikke-motstridende bokstav fra forskjellige ledd, jfr. bilde. Grafen har en c -klikk hvis og bare hvis formelen er tilfredsstillende.

Det er en enkel randomisert algoritme på grunn av Schöning (1999) som kjører i tid (4/3) ⁿ hvor n er antall variabler i 3-SAT-proposisjonen, og lykkes med stor sannsynlighet for å korrekt bestemme 3-SAT.

Den eksponentielle tidshypotesen hevder at ingen algoritme kan løse 3 -SAT (eller faktisk k -SAT for noen ) i eksp ( o ( n )) tid (dvs. fundamentalt raskere enn eksponentiell i n ). ${\ displaystyle k> 2}$

Selman, Mitchell og Levesque (1996) gir empiriske data om vanskeligheten ved tilfeldig genererte 3-SAT-formler, avhengig av størrelsesparametrene. Vanskeligheten måles i antall rekursive anrop foretatt av en DPLL -algoritme .

3-tilfredshet kan generaliseres til k-tilfredshet ( k-SAT , også k-CNF-SAT ), når formler i CNF vurderes med hver klausul som inneholder opptil k bokstaver. Siden imidlertid for ethvert k ≥ 3, kan dette problemet verken være enklere enn 3-SAT eller vanskeligere enn SAT, og de to sistnevnte er NP-komplette, så det må være k-SAT.

Noen forfattere begrenser k-SAT til CNF-formler med nøyaktig k bokstaver . Dette fører heller ikke til en annen kompleksitetsklasse, ettersom hver ledd l ₁ ∨ ⋯ ∨ l _j med j < k bokstaver kan polstres med faste dummyvariabler til l ₁ ∨ ⋯ ∨ l _j ∨ d _{j +1} ∨ ⋯ ∨ d _k . Etter å ha polstret alle ledd, må 2 ^k -1 ekstra klausuler legges til for å sikre at bare d ₁ = ⋯ = d _k = FALSK kan føre til et tilfredsstillende oppdrag. Siden k ikke er avhengig av formellengden, fører ekstraklausulene til en konstant lengdeøkning. Av samme grunn spiller det ingen rolle om dupliserte bokstaver er tillatt i ledd, som i ¬ x ∨ ¬ y ∨ ¬ y .

Akkurat-1 3-tilfredshet

Venstre: Schäfer reduksjon av en 3-SAT klausul x ∨ y ∨ z . Resultatet av R er TRUE (1) hvis nøyaktig ett av argumentene er TRUE, og FALSE (0) ellers. Alle de 8 kombinasjonene av verdier for x , y , z blir undersøkt, en per linje. De ferske variablene a , ..., f kan velges for å tilfredsstille alle ledd (nøyaktig ett grønt argument for hver R ) i alle linjene unntatt den første, der x ∨ y ∨ z er FALSK. Høyre: En enklere reduksjon med de samme egenskapene.

En variant av 3-tilfredsstillelsesproblemet er en-i-tre 3-SAT (også kjent som 1-i-3-SAT og nøyaktig-1 3-SAT ). Gitt en konjunktiv normalform med tre bokstaver per ledd, er problemet å avgjøre om det finnes en sannhetsoppgave til variablene, slik at hver klausul har nøyaktig en SANN bokstav (og dermed nøyaktig to FALSE bokstaver). I kontrast krever vanlig 3-SAT at hver klausul har minst en SANN bokstavelig. Formelt gis et en-i-tre 3-SAT-problem som en generalisert konjunktiv normalform med alle generaliserte klausuler ved bruk av en ternær operator R som er SANN bare om akkurat ett av argumentene er det. Når alle bokstavene i en av tre 3-SAT-formler er positive, kalles tilfredsstillelsesproblemet én-i-tre positive 3-SAT .

En av tre 3-SAT, sammen med den positive saken, er oppført som NP-komplett problem "LO4" i standardreferansen, Computers and Intractability: A Guide to theory of NP-Completeness av Michael R. Garey og David S. Johnson . En av tre 3-SAT ble vist å være NP-komplett av Thomas Jerome Schaefer som et spesielt tilfelle av Schäfer's dikotomisetning , som hevder at ethvert problem med å generalisere boolsk tilfredsstillelse på en bestemt måte enten er i klasse P eller er NP- fullstendig.

Schaefer gir en konstruksjon som muliggjør en enkel polynom-tidsreduksjon fra 3-SAT til en-av-3 3-SAT. La "( x eller y eller z )" være en ledd i en 3CNF -formel. Legg til seks friske boolske variabler a , b , c , d , e og f , for å simulere denne klausulen og ingen andre. Da er formelen R ( x , a , d ) ∧ R ( y , b , d ) ∧ R ( a , b , e ) ∧ R ( c , d , f ) ∧ R ( z , c , FALSE) tilfredsstillende ved noen innstillinger for de friske variablene hvis og bare hvis minst en av x , y eller z er SANN, se bildet (til venstre). Enhver 3-SAT-forekomst med m- klausuler og n- variabler kan således konverteres til en tre-SAT-forekomst med tre meter S - setning på 5 m og n +6 m- variabler. En annen reduksjon innebærer bare fire friske variabler og tre ledd: R (¬ x , a , b ) ∧ R ( b , y , c ) ∧ R ( c , d , ¬ z ), se bilde (høyre).

Ikke-like-3-tilfredshet

En annen variant er det ikke-likeverdige 3-tilfredsstillelsesproblemet (også kalt NAE3SAT ). Gitt en konjunktiv normal form med tre bokstaver per ledd, er problemet å avgjøre om det er en tildeling til variablene slik at i ingen ledd har alle tre bokstavene samme sannhetsverdi. Dette problemet er også NP-komplett, selv om ingen negasjonssymboler er innrømmet, av Schäfer's dikotomisetning.

Lineær SAT

En 3-SAT-formel er lineær SAT ( LSAT ) hvis hver klausul (sett på som et sett med bokstaver) krysser høyst en annen klausul, og dessuten, hvis to klausuler krysser hverandre, så har de nøyaktig en bokstav til felles. En LSAT-formel kan avbildes som et sett med usammenhengende halvt lukkede intervaller på en linje. Å avgjøre om en LSAT-formel er tilfredsstillende eller ikke, er NP-komplett.

2-tilfredshet

SAT er lettere hvis antall bokstaver i en klausul er begrenset til høyst 2, i så fall kalles problemet 2-SAT . Dette problemet kan løses på polynomtid, og er faktisk komplett for kompleksitetsklassen NL . Hvis i tillegg hele eller virksomhet i liter endres til XOR operasjoner, er resultatet kalles eksklusiv-eller to-Satisfiability , som er et problem komplett for kompleksiteten klasse SL = L .

Horn-tilfredshet

Problemet med å bestemme tilfredsheten til en gitt konjunksjon av Horn-klausuler kalles Horn-tilfredsstillelse , eller HORN-SAT . Det kan løses på polynomtid med et enkelt trinn i enhetspropageringsalgoritmen , som produserer den minimale modellen av settet med Horn -klausuler (sett settet med bokstaver tildelt TRUE). Horn-tilfredsstillelse er P-komplett . Det kan sees på som Ps versjon av det boolske tilfredsstillelsesproblemet. Også å bestemme sannheten i kvantifiserte Horn -formler kan gjøres på polynomtid.

Hornklausuler er av interesse fordi de er i stand til å uttrykke implikasjon av en variabel fra et sett med andre variabler. En slik klausul ¬ x ₁ ∨ ... ∨ ¬ x _n ∨ y kan faktisk skrives om til x ₁ ∧ ... ∧ x _n → y , det vil si at x ₁ , ..., x _n alle er SANN , da må y også være SANN.

En generalisering av klassen med Horn-formler er den av formler som kan omdannes til Horn, som er settet med formler som kan plasseres i Horn-form ved å erstatte noen variabler med deres respektive negasjon. For eksempel er ( x ₁ ∨ ¬ x ₂ ) ∧ (¬ x ₁ ∨ x ₂ ∨ x ₃ ) ∧ ¬ x ₁ ikke en Horn -formel, men kan omdøpes til Horn -formelen ( x ₁ ∨ ¬ x ₂ ) ∧ (¬ x ₁ ∨ x ₂ ∨ ¬ y ₃ ) ∧ ¬ x ₁ ved å introdusere y ₃ som negasjon av x ₃ . I kontrast fører ingen omdøping av ( x ₁ ∨ ¬ x ₂ ∨ ¬ x ₃ ) ∧ (¬ x ₁ ∨ x ₂ ∨ x ₃ ) ∧ ¬ x ₁ til en Horn -formel. Kontroll av eksistensen av en slik erstatning kan gjøres på lineær tid; derfor er tilfredsheten til slike formler i P, da den kan løses ved først å utføre denne erstatningen og deretter kontrollere om den resulterende Horn -formelen er tilfredsstillende.

En formel med 2 ledd kan være utilfreds (rød), 3-fornøyd (grønn), xor-3-fornøyd (blå) eller/og 1-i-3-fornøyd (gul), avhengig av det SANN-bokstavelige antallet i 1. (hor) og 2. (vert) ledd.

XOR-tilfredshet

Et annet spesialtilfelle er klassen av problemer der hver klausul inneholder XOR (dvs. eksklusiv eller ) i stedet for (vanlig) ELLER -operatører. Dette er i P , siden en XOR-SAT-formel også kan sees på som et system av lineære ligninger mod 2, og kan løses på kubikk tid ved Gauss-eliminering ; se boksen for et eksempel. Denne omformingen er basert på slektskapet mellom boolske algebraer og boolske ringer , og det faktum at aritmetisk modulo to danner et begrenset felt . Siden en XOR b XOR c vurderer til SANN hvis og bare hvis nøyaktig 1 eller 3 medlemmer av { a , b , c } er SANN, er hver løsning av 1-i-3-SAT-problemet for en gitt CNF-formel også en løsning av XOR-3-SAT-problemet, og hver løsning av XOR-3-SAT er igjen en løsning av 3-SAT, jfr. bilde. Som en konsekvens er det for hver CNF-formel mulig å løse XOR-3-SAT-problemet som er definert av formelen, og basert på resultatet utlede enten at 3-SAT-problemet er løselig eller at 1-i-3- SAT -problemet er uløselig.

Forutsatt at kompleksitetsklassene P og NP ikke er like , er verken 2- eller Horn- eller XOR-tilfredsstillelse NP-komplett, i motsetning til SAT.

Schäfers dikotomisetning

Restriksjonene ovenfor (CNF, 2CNF, 3CNF, Horn, XOR-SAT) bundet de betraktede formlene til å være konjunksjoner av subformler; hver begrensning angir en spesifikk form for alle underformler: for eksempel kan bare binære ledd være subformler i 2CNF.

Schäfers dikotomi-setning sier at for enhver begrensning til boolske funksjoner som kan brukes til å danne disse underformlene, er det tilsvarende tilfredsstillelsesproblemet i P eller NP-komplett. Medlemskapet i P av tilfredsheten til 2CNF, Horn og XOR-SAT formler er spesielle tilfeller av denne teoremet.

Tabellen nedenfor oppsummerer noen vanlige varianter av SAT.

Utvidelser av SAT

En utvidelse som har fått betydelig popularitet siden 2003 er tilfredshetsmodulteorier ( SMT ) som kan berike CNF-formler med lineære begrensninger, matriser, alle forskjellige begrensninger, ufortolkede funksjoner , etc. Slike utvidelser forblir vanligvis NP-komplette, men svært effektive løsere er nå tilgjengelig som kan håndtere mange slike begrensninger.

Tilfredsstillelsesproblemet blir vanskeligere hvis både "for alle" ( ∀ ) og "det eksisterer" ( ∃ ) kvantifiserer får lov til å binde de boolske variablene. Et eksempel på et slikt uttrykk ville være ∀ x ∀ y ∃ z ( x ∨ y ∨ z ) ∧ (¬ x ∨ ¬ y ∨ ¬ z ) ; den er gyldig, siden for alle verdier av x og y kan en passende verdi på z bli funnet, dvs. z = TRUE hvis både x og y er FALSE, og z = FALSE annet. SAT selv (stilltiende) bruker bare ∃ kvantifiserere. Hvis bare ∀ quantifiers er tillatt i stedet, den såkalte tautologi Problemet er oppnådd, som er co-NP-komplett . Hvis begge kvantifiseringer er tillatt, kalles problemet det kvantifiserte boolske formelproblemet ( QBF ), som kan vises for å være PSPACE-komplett . Det er utbredt oppfatning at PSPACE-komplette problemer er strengt vanskeligere enn noe problem i NP, selv om dette ennå ikke er bevist. Ved å bruke svært parallelle P-systemer kan QBF-SAT-problemer løses i lineær tid.

Vanlig SAT spør om det er minst én variabel tildeling som gjør formelen sann. En rekke varianter omhandler antallet slike oppgaver:

• MAJ-SAT spør om de fleste oppgavene gjør formelen SANN. Det er kjent å være komplett for PP , en sannsynlighetsklasse.
• #SAT , problemet med å telle hvor mange variable oppgaver som tilfredsstiller en formel, er et telleproblem, ikke et beslutningsproblem, og er #P-komplett .
• UNIK SAT er problemet med å avgjøre om en formel har nøyaktig én oppgave. Det er komplett for USA , kompleksitetsklassen som beskriver problemer som kan løses av en ikke-deterministisk polynomisk Turing-maskin som godtar når det er nøyaktig en ikke-deterministisk aksepterende bane og avviser noe annet.
• UNAMBIGUOUS-SAT er navnet på tilfredsstillelsesproblemet når input er begrenset til formler som har høyst en tilfredsstillende oppgave. Problemet kalles også USAT . En løsningsalgoritme for UNAMBIGUOUS-SAT har lov til å vise all atferd, inkludert endeløs looping, på en formel som har flere tilfredsstillende oppgaver. Selv om dette problemet virker lettere, har Valiant og Vazirani vist at hvis det er en praktisk (dvs. randomisert polynomtid ) algoritme for å løse det, kan alle problemer i NP løses like enkelt.
• MAX-SAT , det maksimale tilfredsstillelsesproblemet , er en FNP- generalisering av SAT. Den ber om maksimalt antall klausuler som kan oppfylles av enhver oppgave. Den har effektive tilnærmingsalgoritmer , men er NP-vanskelig å løse nøyaktig. Enda verre, det er APX -komplett, noe som betyr at det ikke er noen tilnærmingsplan for polynom -tid (PTAS) for dette problemet med mindre P = NP.
• WMSAT er problemet med å finne en oppgave med minimumsvekt som tilfredsstiller en monoton boolsk formel (dvs. en formel uten negasjon). Vekter av proposisjonsvariabler er gitt i input av problemet. Vekten av en oppgave er summen av vekter av sanne variabler. Det problemet er NP-komplett (se Th. 1 av).

Andre generaliseringer inkluderer tilfredshet for første -og andreordens logikk , begrensningstilfredshetsproblemer , 0-1 heltalls programmering .

Selvreduserbarhet

SAT-problemet er selvreduserbart , det vil si at hver algoritme som svarer riktig hvis en forekomst av SAT kan løses, kan brukes til å finne en tilfredsstillende oppgave. Først blir spørsmålet stilt med den gitte formelen Φ. Hvis svaret er "nei", er formelen utilfredsstillende. Ellers blir spørsmålet stilt på den delvis instantiserte formelen Φ { x ₁ = TRUE} , dvs. Φ med den første variabelen x ₁ erstattet av TRUE, og forenklet deretter. Hvis svaret er "ja", så x ₁ = SANN, ellers x ₁ = FALSK. Verdier av andre variabler kan senere bli funnet på samme måte. Totalt kreves n +1 kjøringer av algoritmen, hvor n er antall forskjellige variabler i Φ.

Denne egenskapen til selvreduserbarhet brukes i flere teoremer i kompleksitetsteorien:

NP ⊆ P/poly ⇒ PH = Σ ₂   ( Karp – Lipton setning )

NP ⊆ BPP ⇒ NP = RP

P = NP ⇒ FP = FNP

Algoritmer for å løse SAT

Siden SAT-problemet er NP-komplett, er bare algoritmer med eksponentiell worst case-kompleksitet kjent for det. Til tross for dette ble effektive og skalerbare algoritmer for SAT utviklet i løpet av 2000 -tallet og har bidratt til dramatiske fremskritt i vår evne til å automatisk løse problemforekomster som involverer titusenvis av variabler og millioner av begrensninger (dvs. klausuler). Eksempler på slike problemer i elektronisk designautomatisering (EDA) inkluderer formell ekvivalenskontroll , modellkontroll , formell verifikasjon av rørprosesserte mikroprosessorer , automatisk testmønstergenerering , ruting av FPGA , planlegging og planleggingsproblemer og så videre. En SAT-løsningsmotor anses nå å være en viktig komponent i EDA- verktøykassen.

En DPLL SAT -løsning bruker en systematisk tilbakemeldingssøkprosedyre for å utforske (eksponensielt størrelse) plass til variable oppgaver på jakt etter tilfredsstillende oppgaver. Den grunnleggende søkeprosedyren ble foreslått i to hovedartikler på begynnelsen av 1960 -tallet (se referanser nedenfor) og blir nå ofte referert til som Davis - Putnam - Logemann - Loveland -algoritmen ("DPLL" eller "DLL"). Mange moderne tilnærminger til praktisk SAT -løsning er avledet fra DPLL -algoritmen og har samme struktur. Ofte forbedrer de bare effektiviteten til visse klasser av SAT -problemer, for eksempel forekomster som vises i industrielle applikasjoner eller tilfeldig genererte forekomster. Teoretisk har eksponentielle lavere grenser blitt bevist for DPLL -familien av algoritmer.

Algoritmer som ikke er en del av DPLL -familien inkluderer stokastiske lokale søkealgoritmer. Ett eksempel er WalkSAT . Stokastiske metoder prøver å finne en tilfredsstillende tolkning, men kan ikke utlede at en SAT -forekomst er utilfredsstillende, i motsetning til komplette algoritmer, for eksempel DPLL.

I kontrast setter randomiserte algoritmer som PPSZ-algoritmen av Paturi, Pudlak, Saks og Zane variabler i en tilfeldig rekkefølge i henhold til noen heuristikker, for eksempel oppløsning med begrenset bredde . Hvis heuristen ikke finner den riktige innstillingen, tildeles variabelen tilfeldig. PPSZ-algoritmen har en kjøretid på 3-SAT. Dette var den mest kjente kjøretiden for dette problemet inntil en nylig forbedring av Hansen, Kaplan, Zamir og Zwick som har en kjøretid på 3-SAT og for tiden den mest kjente kjøretiden for k-SAT, for alle verdier av k. I settingen med mange tilfredsstillende oppgaver har den randomiserte algoritmen av Schöning en bedre grense. ${\ displaystyle O (1.308^{n})}$${\ displaystyle O (1.307^{n})}$

Moderne SAT-løsere (utviklet på 2000-tallet) kommer i to varianter: "konfliktdrevet" og "blikk-fremover". Begge tilnærmingene stammer fra DPLL. Konfliktdrevne løsere, for eksempel konfliktdrevet klausulering (CDCL), forsterker den grunnleggende DPLL-søkealgoritmen med effektiv konfliktanalyse, klausulærlæring , ikke- kronologisk backtracking (aka backjumping ), samt "to- watch-literals " -enhet forplantning , adaptiv forgrening og tilfeldig omstart. Disse "tilleggene" til det grunnleggende systematiske søket har empirisk vist seg å være avgjørende for å håndtere de store SAT -forekomstene som oppstår i elektronisk designautomatisering (EDA). Velkjente implementeringer inkluderer Chaff og GRASP . Løsere med blikket fremover har spesielt styrket reduksjonene (som går utover forplantning av enhetsklausuler) og heuristikken, og de er generelt sterkere enn konfliktdrevne løsningsmenn i harde tilfeller (mens konfliktdrevne løsere kan være mye bedre i store tilfeller som faktisk har en lett forekomst inni).

Moderne SAT -løsere har også betydelig innvirkning på blant annet programvareverifisering, begrensningsløsning innen kunstig intelligens og operasjonsforskning. Kraftige løsningsmenn er lett tilgjengelige som gratis og åpen kildekode -programvare . Spesielt har den konfliktdrevne MiniSAT , som var relativt vellykket i SAT-konkurransen i 2005 , bare om lag 600 linjer med kode. En moderne Parallel SAT -løsning er ManySAT. Det kan oppnå super lineære speed-ups på viktige klasser av problemer. Et eksempel på blikk-frem- løvere er march_dl , som vant en premie i SAT-konkurransen i 2007 .

Enkelte typer store tilfeldige tilfredsstillende forekomster av SAT kan løses ved undersøkelsesformidling (SP). Spesielt i maskinvaredesign og verifikasjonsapplikasjoner avgjøres noen ganger tilfredshet og andre logiske egenskaper ved en gitt proposisjonsformel basert på en representasjon av formelen som et binært beslutningsdiagram (BDD).

Nesten alle SAT-løsere inkluderer time-out, så de avsluttes i rimelig tid, selv om de ikke finner en løsning. Ulike SAT -løsere vil finne forskjellige tilfeller enkle eller harde, og noen utmerker seg med å bevise utilfredsheten, og andre på å finne løsninger. All denne oppførselen kan sees i SAT -løsningskonkurransene.

Parallell SAT-løsning

Parallelle SAT-løsere kommer i tre kategorier: portefølje, dele-og-erobre og parallelle lokale søkealgoritmer. Med parallelle porteføljer, kjører flere forskjellige SAT -løsninger samtidig. Hver av dem løser en kopi av SAT-forekomsten, mens del-og-erobre-algoritmer deler problemet mellom prosessorene. Det finnes forskjellige tilnærminger for å parallellisere lokale søkealgoritmer.

Den internasjonale SAT -løsningskonkurransen har et parallellspor som gjenspeiler de siste fremskrittene innen parallell SAT -løsning. I 2016, 2017 og 2018 ble referanseindeksene kjørt på et system med delt minne med 24 prosessorkjerner , derfor kan løsere beregnet på distribuert minne eller mangecore-prosessorer ha gått til kort.

Porteføljer

Generelt er det ingen SAT -løsning som fungerer bedre enn alle andre løsere på alle SAT -problemer. En algoritme kan fungere godt for problemforekomster andre sliter med, men vil gjøre det verre med andre forekomster. I tillegg til en SAT -forekomst, er det ingen pålitelig måte å forutsi hvilken algoritme som vil løse denne forekomsten spesielt raskt. Disse begrensningene motiverer den parallelle porteføljemetoden. En portefølje er et sett med forskjellige algoritmer eller forskjellige konfigurasjoner av den samme algoritmen. Alle løsere i en parallell portefølje kjøres på forskjellige prosessorer for å løse det samme problemet. Hvis en løsning avsluttes, rapporterer porteføljeløseren at problemet er tilfredsstillende eller utilfredsstillende i henhold til denne løsningen. Alle andre løsere avsluttes. Å diversifisere porteføljer ved å inkludere en rekke løsere, som hver fungerer godt på et annet sett med problemer, øker robustheten til løseren.

Mange løsere bruker internt en tilfeldig tallgenerator . Å diversifisere sine frø er en enkel måte å diversifisere en portefølje på. Andre diversifiseringsstrategier innebærer å aktivere, deaktivere eller diversifisere visse heuristikker i den sekvensielle løseren.

En ulempe med parallelle porteføljer er mengden duplikatarbeid. Hvis klausulæring brukes i de sekvensielle løsningerne, kan deling av innlærte klausuler mellom parallelle løpende løsere redusere duplikatarbeid og øke ytelsen. Likevel gjør det bare å kjøre en portefølje av de beste løsningerne parallelt en konkurransedyktig parallellløser. Et eksempel på en slik løsning er PPfolio. Den ble designet for å finne en nedre grense for ytelsen en parallell SAT -løsning skulle kunne levere. Til tross for den store mengden duplikatarbeid på grunn av mangel på optimaliseringer, fungerte det bra på en delt minnemaskin. HordeSat er en parallell porteføljeløser for store klynger med databehandlingsnoder. Den bruker forskjellige konfigurerte forekomster av den samme sekvensielle løsningen i kjernen. Spesielt for harde SAT -tilfeller kan HordeSat produsere lineære speedups og dermed redusere kjøretiden betydelig.

I de siste årene har parallelle portefølje SAT -løsningsmenn dominert parallellsporet til de internasjonale SAT -løsningskonkurransene . Viktige eksempler på slike løsningsmidler inkluderer Plingeling og smertefrie mcomsps.

Splitt og hersk

I motsetning til parallelle porteføljer, prøver parallell divider-og-erobre å dele søkeområdet mellom behandlingselementene. Del-og-erobre-algoritmer, for eksempel den sekvensielle DPLL, bruker allerede teknikken for å dele søkeområdet, og derfor er forlengelsen mot en parallell algoritme rett frem. På grunn av teknikker som enhetsforplantning, etter en inndeling, kan de delvise problemene imidlertid variere betydelig i kompleksitet. Dermed behandler DPLL -algoritmen vanligvis ikke hver del av søkeområdet på samme tid, noe som gir et utfordrende lastbalanseringsproblem .

Kubefase for formelen . Beslutningsheuristikken velger hvilke variabler (sirkler) som skal tildeles. Etter at grensen for heuristikk bestemmer seg for å stoppe ytterligere forgrening, løses delproblemene (rektangler) uavhengig av hverandre ved hjelp av CDCL.${\ displaystyle F}$

På grunn av ikke-kronologisk tilbakesporing er parallellisering av konfliktdrevet klausulering vanskeligere. En måte å overvinne dette på er Cube-and-Conquer- paradigmet. Det foreslår å løse i to faser. I "kube" -fasen er problemet delt inn i mange tusen, opptil millioner, seksjoner. Dette gjøres med en blikk-fremover-løsning, som finner et sett med delvise konfigurasjoner kalt "kuber". En terning kan også sees på som en sammenheng av et delsett av variabler av den opprinnelige formelen. I forbindelse med formelen danner hver av kubene en ny formel. Disse formlene kan løses uavhengig og samtidig av konfliktdrevne løsningsmenn. Ettersom disjunksjonen av disse formlene er ekvivalent med den opprinnelige formelen, rapporteres problemet å være tilfredsstillende hvis en av formlene er tilfredsstillende. Løsningen for blikket fremover er gunstig for små, men vanskelige problemer, så den brukes til å dele problemet gradvis i flere delproblemer. Disse delproblemene er lettere, men fortsatt store, noe som er den ideelle formen for en konfliktdrevet løsning. Videre vurderer løsningene med blikket fremover hele problemet, mens konfliktdrevne løsere tar beslutninger basert på informasjon som er mye mer lokal. Det er tre heuristikk involvert i terningfasen. Variablene i kubene velges av den heuristiske beslutningen. Retningen heuristisk bestemmer hvilken variabel oppgave (sann eller usann) som skal utforskes først. I tilfredsstillende problemforekomster er det fordelaktig å velge en tilfredsstillende gren først. Avskjæringsheuristen bestemmer når den skal slutte å utvide en kube og i stedet videresende den til en sekvensiell konfliktdrevet løsning. Fortrinnsvis er terningene like komplekse å løse.

Treengeling er et eksempel på en parallellløser som bruker Cube-and-Conquer-paradigmet. Siden introduksjonen i 2012 har den hatt flere suksesser ved den internasjonale SAT Solver Competition . Cube-and-Conquer ble brukt til å løse problemet med boolske pytagoranske trippler .

Lokalt søk

En strategi mot en parallell lokal søkealgoritme for SAT -løsning er å prøve flere variable flips samtidig på forskjellige behandlingsenheter. En annen er å bruke den ovennevnte porteføljemetoden, men deling av klausuler er ikke mulig siden lokale søkeløsere ikke produserer klausuler. Alternativt er det mulig å dele konfigurasjonene som produseres lokalt. Disse konfigurasjonene kan brukes til å veilede produksjonen av en ny innledende konfigurasjon når en lokal løsningsmann bestemmer seg for å starte søket på nytt.

Se også

• Uforsettelig kjerne
• Tilfredshetsmodulteorier
• Teller SAT
• Planar SAT
• Karloff - Zwick algoritme
• Kretsens tilfredshet

Merknader

Referanser

Referanser er sortert etter publiseringsdato:

Eksterne linker

• SAT Game - prøv å løse et boolsk tilfredsstillelsesproblem selv

SAT problemformat

Et SAT-problem er ofte beskrevet i DIMACS-CNF- formatet: en inndatafil der hver linje representerer en enkelt disjunksjon. For eksempel en fil med de to linjene

1 -5 4 0
-1 5 3 4 0

representerer formelen "( x ₁ ∨ ¬ x ₅ ∨ x ₄ ) ∧ (¬ x ₁ ∨ x ₅ ∨ x ₃ ∨ x ₄ )".

Et annet vanlig format for denne formelen er 7-biters ASCII- representasjonen "(x1 | ~ x5 | x4) & (~ x1 | x5 | x3 | x4)".

• BCSAT er et verktøy som konverterer inndatafiler i format som kan leses av mennesker til DIMACS-CNF-format.

Online SAT -løsere

• BoolSAT-Løser formler i DIMACS-CNF-formatet eller i et mer menneskelig vennlig format: "a og ikke b eller a". Kjører på en server.
• Logictools - Tilbyr forskjellige løsere i javascript for læring, sammenligning og hacking. Kjører i nettleseren.
• minisat-in-your-browser -Løser formler i DIMACS-CNF-format. Kjører i nettleseren.
• SATRennesPA -Løser formler skrevet på en brukervennlig måte. Kjører på en server.
• somerby.net/mack/logic - Løser formler skrevet i symbolsk logikk. Kjører i nettleseren.

SAT -løsere uten nett

• MiniSAT -DIMACS-CNF-format og OPB-format for sin ledsager Pseudo-boolske begrensningsløser MiniSat+
• Lingeling - vant en gullmedalje i en SAT -konkurranse i 2011.
  • PicoSAT - en tidligere løser fra Lingeling -gruppen.
• Sat4j -DIMACS-CNF-format. Java kildekode tilgjengelig.
• Glukose -DIMACS-CNF-format.
• RSat - vant en gullmedalje i en SAT -konkurranse i 2007.
• UBCSAT . Støtter uveide og vektede ledd, begge i DIMACS-CNF-format. C kildekoden ligger på GitHub .
• CryptoMiniSat - vant en gullmedalje i en SAT -konkurranse i 2011. C ++ - kildekoden ligger på GitHub . Prøver å sette mange nyttige funksjoner i MiniSat 2.0 -kjernen, PrecoSat ver 236 og Glucose i en pakke, og legger til mange nye funksjoner
• Spyd -Støtter bit-vektor aritmetikk. Kan bruke DIMACS-CNF-formatet eller Spear-formatet .
  • HyperSAT -Skrevet for å eksperimentere med beskjæring av B-cubing søkeplass. Vant 3. plass i en SAT -konkurranse i 2005. En tidligere og langsommere løsning fra utviklerne av Spear.
• BASolver
• ArgoSAT
• Rask SAT Solver - basert på genetiske algoritmer .
• zChaff - støttes ikke lenger.
• BCSAT -et menneskelig lesbart boolsk kretsformat (konverterer også dette formatet til DIMACS-CNF-formatet og kobler automatisk til MiniSAT eller zChaff).
• gini - Go -språk SAT -løsning med relaterte verktøy.
• gophersat -Go-språk SAT-løsning som også kan håndtere pseudo-boolske og MAXSAT-problemer.
• CLP (B)-Boolean Constraint Logic Programming, for eksempel SWI-Prolog .

SAT -applikasjoner

• WinSAT v2.04 : En Windows-basert SAT-applikasjon laget spesielt for forskere.

Konferanser

• Internasjonal konferanse om teori og anvendelser av tilfredshetstesting

Publikasjoner

• Journal om tilfredshet, boolsk modellering og beregning
• Undersøkelsesformidling

Benchmarks

• Tvunget tilfredsstillende SAT -referanser
• Verifiseringsbenchmarks for programvare
• Fadi Aloul SAT Benchmarks

SAT -løsning generelt:

• http://www.satlive.org
• http://www.satisfiability.org

Evaluering av SAT -løsere

• Årlig evaluering av SAT -løsere
• SAT løser evalueringsresultater for 2008
• Internasjonale SAT -konkurranser
• Historie

Mer informasjon om SAT:

• SAT og MAX-SAT for Lay-forskeren
• SAT/SMT etter eksempel

Denne artikkelen inneholder materiale fra en spalte i ACM SIGDA e-nyhetsbrev av Prof. Karem Sakallah
Originalteksten er tilgjengelig her