Problema SAT

În informatică teoretică , problema SAT sau problema de satisfacție booleană este problema deciziei , care, dată fiind logica formulei propoziționale , determină dacă există o atribuire de variabile propoziționale care face formula adevărată.

Această problemă este foarte importantă în teoria complexității . A fost scoasă la lumină de teorema lui Cook , care stă la baza teoriei completitudinii NP și a problemei P = NP . Problema SAT are, de asemenea, multe aplicații, în special în ceea ce privește satisfacerea constrângerilor , planificarea clasică, verificarea modelelor , diagnosticarea și chiar configuratorul unui PC sau al sistemului de operare al acestuia: revenim la formulele propoziționale și folosim un rezolvator SAT .

Terminologie

Formule ale logicii propoziționale

Formulele logicii propoziționale sunt construite din variabile propoziționale și din conectorii booleni "și" ( ), "sau" ( ), "nu" ( ). O formulă este satisfăcătoare (spunem și satisfăcătoare ) dacă există o atribuire de variabile propoziționale care face formula logică adevărată. De exemplu : $\ teren$ $\ lor$ $\ l nu$

Formula este satisfăcătoare deoarece, dacă ia valoarea false, formula se evaluează la adevărat. ${\ displaystyle (p \ land q) \ lor \ lnot p}$ $p$
Formula este nesatisfăcătoare, deoarece nicio valoare p nu poate face formula adevărată. ${\ displaystyle (p \ land \ lnot p)}$

Clauze conjunctive și formă normală

Un literal este o variabilă propozițională (literal pozitiv) sau negarea unei variabile propoziționale (literal negativ). O clauză este o disjuncție a formei în care sunt literali. $\ Ell$ $v_ {j}$ ${\ displaystyle \ lnot v_ {j}}$ ${\ displaystyle {\ overset {n} {\ underset {i = 1} {\ bigvee}}} \ ell _ {i} = (\ ell _ {1} \ lor \ ell _ {2} \ lor \ ldots \ lor \ ell _ {n})}$ $\ ell _ {i}$

O formulă de calcul propozițională este în formă normală conjunctivă (sau formă clauzală sau CNF înseamnă Forma normală conjunctivă ) dacă este o conjuncție de clauze.

ExempluFie setul de variabile și formula .

\ {v_ {1}, v_ {2}, v_ {3} \} \

f = (v_ {1} \ lor v_ {2}) \ land (\ neg v_ {1} \ lor v_ {3}) \ land (\ neg v_ {2} \ lor \ neg v_ {1})

{\ displaystyle (v_ {1} \ lor v_ {2})}

, Și sunt clauze cu două literale de fiecare clauză.

{\ displaystyle (\ neg v_ {1} \ lor v_ {3})}

{\ displaystyle (\ neg v_ {2} \ lor \ neg v_ {1})}

Conjuncția lor este o formă conjunctivă normală.

f

Dacă formula propozițională nu este în formă normală conjunctivă, o putem transforma într-o formă normală conjunctivă echivalentă cu dimensiuni cel mult exponențiale în formula inițială. Îl putem transforma, de asemenea, într-o formă conjunctivă normală echisatisfăcătoare de dimensiune liniară în formula inițială.

Limitările problemei SAT

Considerăm restricțiile sintactice ale problemei SAT.

Problema CNF-SAT este restricționarea problemei SAT la formele normale de conectivitate.
Problema 2-SAT este restricționarea problemei SAT la formele normale conjunctive cu cel mult 2 litere per clauză.
Problema 3-SAT este restricționarea problemei SAT la formele normale conjunctive cu cel mult 3 litere per clauză.
- Exemplu exemplu: . $(v_ {1} \ lor \ neg v_ {2} \ lor v_ {3}) \ land (\ neg v_ {1} \ lor v_ {3} \ lor v_ {4})$
Problema HORN-SAT este restricționarea problemei SAT la formele normale conjunctive în care clauzele sunt clauze Horn .

Complexitate și restricții

CNF-SAT

Problema SAT este o problemă NP - completă conform teoremei lui Cook . În special, nu se cunoaște niciun algoritm determinist polinomial care să îl rezolve. În mod similar, deoarece orice formulă se poate transforma într-o formă conjunctivă normală echisatisfăcătoare de dimensiune liniară în formula inițială, problema CNF-SAT este, de asemenea, NP-completă .

3-SAT

Problema 3 - SAT este, de asemenea, NP - completă. Pentru a demonstra dificultatea NP a 3-SAT, este suficient să se demonstreze că problema CNF-SAT este polinomial reductibilă la 3 - SAT. Reducerea transformă fiecare clauză cu în . ${\ displaystyle \ ell _ {1} \ lor \ ell _ {2} \ lor \ ldots \ lor \ ell _ {n}}$ $n \ geq 3$ ${\ displaystyle (\ ell _ {1} \ lor \ ell _ {2} \ lor u_ {1}) \ land (\ ell _ {3} \ lor \ lnot u_ {1} \ lor u_ {2}) \ land \ ldots \ land (\ ell _ {n-2} \ lor \ lnot u_ {n-4} \ lor u_ {n-3}) \ land (\ ell _ {n-1} \ lor \ ell _ { n} \ lor \ lnot u_ {n-3})}$

2-SAT

Problema 2-SAT este restricționarea problemei SAT la formele normale conjunctive cu cel mult 2 litere per clauză. Această problemă este în clasa P . Sub presupunerea , nu este complet NP. Există mai mulți algoritmi polinomiali deterministi pentru a rezolva problema 2-SAT. $P \ neq NP$

Algoritmul lui Aspvall, Plass și Tarjan Algoritmul ia o formulă conjunctivă de formă normală cu cel mult 2 litere per clauză.

\ varphi

O clauză de ordinul doi este echivalentă cu implicațiile și .

v_ {1} \ lor v_ {2}

\ lnot v_ {1} \ rightarrow v_ {2}

\ lnot v_ {2} \ rightarrow v_ {1}

Pentru a rezolva 2-SAT, construim un grafic cu două direcții (numit grafic 2-SAT) conform următoarelor două reguli:

vârfurile sunt variabilele propoziționale care apar în formulă și negațiile variabilelor propoziționale care apar în formulă; $v_ {i} \,$ $\ l nu v_ {i} \,$ $v_ {i} \,$
adăugăm arcurile și pentru fiecare clauză . $(\ nu v_ {1}, v_ {2})$ $(\ nu v_ {2}, v_ {1})$ $v_ {1} \ lor v_ {2}$

Formula este satisfiable dacă și numai dacă pentru orice variabilă propozițională a , și se află în două distincte componente puternic conectate în graficul 2-SAT. Apoi folosim algoritmul lui Tarjan (sau algoritmul lui Kosaraju ) pentru a calcula componentele puternic conectate ale graficului 2-SAT.

\ varphi

v_ {i} ~

\ varphi

v_ {i} ~

\ l nu v_ {i}

Christos Papadimitriou a arătat în 1994 că problema 2-SAT este NL-completă .

HORN-SAT

Problema satisfiabilitate a unui set de clauze Horn propoziționale (adică, cu cel mult un literal pozitiv de clauza) este în clasa P . Mai precis, există un algoritm liniar în mărimea clauzelor care rezolvă problema satisfacției. Este P-complet (pentru reducerea spațiului logaritmic ).

Teorema dihotomiei lui Schaefer

Teorema lui Schaefer oferă condiții necesare și suficiente pentru ca o variantă a problemei SAT să fie în clasa P sau NP - completă . Găsim rezultatele complexității referitoare la 3-SAT (NP-complet), 2-SAT (în P), HORN-SAT (în P) ca aplicații ale acestei teoreme.

Algoritmi pentru SAT

Cea mai evidentă metodă pentru a rezolva o problemă SAT este să parcurgeți tabelul de adevăr al problemei, dar complexitatea este apoi exponențială în comparație cu numărul de variabile.

Metoda sistematică

Pentru a dovedi satisfacția CNF , este suficient să alegeți o variabilă și să demonstrați recursiv satisfacția lui sau . Procedura este recursiv mai ușoară, deoarece cu sau poate fi adesea simplificată. Apelul recursiv construiește un arbore binar de căutare . $\ phi \$ $v ~$ $v \ land \ phi$ $\ neg v \ land \ phi$ $a \ land \ phi$ $a = v \$ $a = \ neg v$

În general, există clauze de unitate la fiecare nod (CNF este de formă ), care permit reducerea spațiului de căutare. $\ phi = a \ land \ phi '$

Exemplu Luați în considerare CNF:

(v_ {1} \ lor \ neg v_ {2}) \ land \ neg v_ {3} \ land (v_ {3} \ lor \ neg v_ {1})

. A doua clauză ( ) este unitară și permite obținerea imediată . Putem înlocui valorile din acest CNF. Asta da :

\ neg v_ {3}

v_ {3} = {\ textit {false}}

v_ {3}

(v_ {1} \ lor \ neg v_ {2}) \ land \ neg {\ textit {false}} \ land ({\ textit {false}} \ lor \ neg v_ {1}) = (v_ {1} \ lor \ neg v_ {2}) \ land \ neg v_ {1}

. Din nou, avem o clauză unitară și obținem . Apoi, prin propagare , obținem .

v_ {1} = {\ textit {false}} ~

v_ {2} = {\ textit {false}} ~

În acest exemplu, am găsit valorile celor trei variabile fără a extinde măcar arborele de căutare. În general, spațiul de căutare poate fi redus foarte mult. Pe de altă parte, dacă o variabilă apare întotdeauna pozitiv în CNF , atunci putem pune deoarece este satisfăcătoare dacă și numai dacă este satisfăcătoare (și la fel dacă variabila apare negativ). Astfel, în exemplul anterior, apare doar negativ și atribuirea poate fi realizată. Rețineți că această atribuire face posibilă accelerarea descoperirii unei soluții, dar că soluțiile ar putea exista prin efectuarea atribuirii opuse. DPLL Algoritmul (Davis, Putnam, Davis, Logemann, Loveland) se bazează pe aceste idei. $v \$ $\ phi \$ $v = {\ textit {true}} \$ $\ phi \$ $\ phi \ land v$ $v_ {2} \$ $v_ {2} = false \$

Alegerea variabilei care trebuie dezvoltată este foarte importantă pentru performanța algoritmilor SAT. În general, alegem variabilele care apar cel mai des, dacă este posibil în clauzele de mărime 2. $v \$

Clauze de învățare prin conflicte

Principiul solvenților CDCL (Conflict-Driven Clause Clause Learning) este acela de a utiliza un mecanism pentru a învăța noi clauze în timpul unei căutări, apoi de a utiliza la maximum informațiile învățate în speranța de a îmbunătăți timpul de căutare. Din punct de vedere practic, această metodologie este foarte eficientă în rezolvarea problemelor concrete. Învățarea clauzelor este după cum urmează: atunci când apare un conflict în timpul căutării, adică atunci când se arată că o atribuire parțială este incompatibilă cu setul de clauze, putem izola un subset al acestor atribuiri și un subset al acestor clauze, care sunt responsabile pentru conflict (atribuțiile nu sunt în concordanță cu clauzele). Învățarea clauzelor face două lucruri. În primul rând, evită repetarea acelorași erori de mai multe ori în arborele de căutare. În al doilea rând, clauza învățată va intra în conflict cu starea arborelui de căutare. Prin urmare, va fi necesar să efectuați un backtracking pentru a vă asigura că cel puțin unul dintre aceste litere este adevărat.

Există diferite metode pentru a genera noi clauze dintr-o inconsecvență locală.

Metoda naivă

Să instanța de rezolvat să aibă următoarea formulă : $\ phi _ {1}$

{\ begin {array} {rcl} C_ {1} & = & x_ {1} \ lor x_ {2} \\ C_ {2} & = & \ neg x_ {1} \ lor x_ {3} \\\ end {array}}

și interpretarea parțială definită prin: . Această interpretare duce la un conflict, deoarece implică asta , în timp ce implică asta . Pentru a genera o clauză care reprezintă acest conflict, este posibil să se ia negarea de interpretare : . Cu toate acestea, această metodă are un dezavantaj major: dimensiunea clauzei este în întregime determinată de întreaga interpretare. Cu toate acestea, anumite părți ale interpretării pot fi complet independente de conflictul pe care cineva dorește să îl reprezinte. De fapt, să adăugăm formulele la instanță : și să fie interpretarea curentă . Conflictul apare din primele două clauze și deci din valorile lui și . Cu toate acestea, clauza generată de negarea interpretării va lua în considerare toate variabilele, cu excepția . Ca urmare, clauza va fi inutilă de lungă. ${\ mathcal {I}}$ $x_ {2} = {\ textit {false}}, x_ {3} = {\ textit {false}}$ $x_ {2}$ $x_ {1} = adevărat$ $x_ {3}$ $x_ {1} = false$ ${\ mathcal {I}}$ $\ neg {\ mathcal {I}} = \ neg (\ neg x_ {2} \ land \ neg x_ {3}) = x_ {2} \ lor x_ {3}$ $\ phi _ {1}$ $C _ {{i}} = x_ {i} \ lor x _ {{i + 1}}, 4 \ leq i \ leq N$ ${\ mathcal {I}} = \ {x_ {2} = false, x_ {3} = false, x _ {{4 \ leq i \ leq N}} = false \}$ $x_ {2}$ $x_ {3}$ $x_ {1}$

Analiza conflictelor

Când se folosește această metodă, se creează un grafic pentru a reprezenta originea propagării, numit grafic de implicație. Nodurile reprezintă literali adevărați. Există două tipuri de noduri: noduri pătrate a căror valoare literală provine dintr-o alegere arbitrară și noduri rotunde a căror valoare provine dintr-o propagare. Informațiile sunt, de asemenea, asociate cu fiecare nod: nivelul nodului în cauză. Acest nivel este definit de numărul literelor alese înainte de efectuarea propagării dacă a existat propagare. În caz contrar, nivelul este definit de numărul literelor alese, inclusiv literalul curent. Arcurile interconectează literele care fac parte dintr-o clauză de propagare. Destinația unui arc este literalul propagat, sursa (sursele) fiind celelalte litere din clauză. Să instanța de rezolvat să aibă următoarea formulă : $\ phi _ {2}$

{\ displaystyle {\ begin {array} {rcl} C_ {1} & = & \ neg d \ lor f \\ C_ {2} & = & \ neg d \ lor \ neg e \ lor g \\ C_ {3 } & = & \ neg h \ lor j \\ C_ {4} & = & \ neg h \ lor i \\ C_ {5} & = & \ neg i \ lor a \\ C_ {6} & = & \ neg g \ lor \ neg i \ lor b \\ C_ {7} & = & \ neg a \ lor c \\ C_ {8} & = & \ neg b \ lor \ neg c \ end {array}}}

însoțită de interpretarea pe care nivelurile de diferite valori literale sunt specificate precum și literal care duce la incoerență: . Apoi, este posibil să trageți graficul următor din acesta. ${\ mathcal {I}} = \ {d | _ {1}, f | _ {1}, e | _ {2}, g | _ {2}, h | _ {3}, i | _ {3 }, j | _ {3}, a | _ {3}, b | _ {3}, c | _ {3} \}$ $\ neg c$

Datorită acestui grafic, este posibil să se creeze o clauză care să reprezinte cauza conflictului. Metoda utilizată este următoarea: începem prin a crea rezolvarea clauzelor care duc la un conflict. Apoi, atâta timp cât există mai mult de un literal al nivelului actual, se creează o nouă rezolvare între rezolvarea curentă și cauza unuia dintre literalele nivelului actual. În exemplul nostru, acest lucru va da (unde reprezintă rezoluția dintre clauză și clauză ) ${\ mathcal {R}} _ {1}$ ${\ mathcal {R}} _ {{i + 1}}$ ${\ mathcal {R}} _ {i}$ $C_ {i} \ vdash _ {{\ mathcal {R}}} C_ {j}$ $Acest}$ $C_ {j}$

{\ begin {array} {rcccl} {\ mathcal {R}} _ {1} & = & C_ {7} \ vdash _ {{\ mathcal {R}}} C_ {8} & = & \ neg a \ lor \ neg b \\ {\ mathcal {R}} _ {2} & = & {\ mathcal {R}} _ {1} \ vdash _ {{\ mathcal {R}}} C_ {6} & = & \ neg g \ lor \ neg i \ lor \ neg a \\ {\ mathcal {R}} _ {3} & = & {\ mathcal {R}} _ {2} \ vdash _ {{\ mathcal {R} }} C_ {5} & = & \ neg g \ lor \ neg i \\ {\ mathcal {R}} _ {4} & = & {\ mathcal {R}} _ {3} \ vdash _ {{\ mathcal {R}}} C_ {4} & = & \ neg h \ lor \ neg g. \ End {array}}

Backtracking necronologic

Odată ce clauza a fost învățată, aceasta va fi utilizată pentru restabilire. Ideea din spatele revenirii non-cronologice este că se va face o revenire astfel încât starea atribuțiilor să fie astfel încât să rămână doar un literal neatribuit. Astfel, datorită clauzei învățate, va fi posibilă continuarea diferitelor propagări atunci când acest lucru nu mai este posibil fără ea.

Dacă luăm exemplul prezentat în secțiunea de analiză a conflictelor, clauza învățată ne oferă două litere. Nivelurile variabilelor corespunzătoare sunt: variabilă = 3, variabilă = 2. Pentru a ști la ce nivel este necesar să vă întoarceți, trebuie să vă uitați la cel mai profund nivel (nivelul este mai adânc decât nivelul ) dintre variabilele unui nivel mai mare decât nivelul actual. Deoarece clauza învățată conține doar două litere, există un singur nivel diferit de nivelul curent: nivelul 2. Prin urmare, se efectuează o revenire până la acest nivel și, prin urmare, se lasă ca interpretare . Cu toate acestea, cu o astfel de interpretare, clauza învățată conține o singură variabilă neatribuită: în timp ce cealaltă este afectată în așa fel încât literalul să fie fals. Aceasta implică necesitatea propagării variabilei la valoarea false. $\ phi _ {2}$ ${\ mathcal {R}} _ {4} = \ neg h \ lor \ neg g$ $h$ $g$ $i + 1$ $eu$ ${\ mathcal {I}} = \ {d | _ {1}, f | _ {1}, e | _ {2}, g | _ {2} \}$ $h$ $\ neg g$ $h$

Deși în acest exemplu, revenirea se face doar la un nivel, este posibil ca acesta să crească mai multe niveluri simultan. Într-adevăr, imaginați-vă că putem adăuga N niveluri între nivelul 2 și nivelul 3, unde toate variabilele care apar acolo sunt variabile noi. Deoarece aceste niveluri nu ar avea niciun impact asupra vechiului nivel 3, revenirea ar crește brusc aceste niveluri N + 1.

Abordări prospective

Abordarea prospectivă constă în explorarea arborelui de cercetare pentru a descoperi anumite sarcini. Astfel, având în vedere un CNF , având în vedere o variabilă neinstanțiată, CNF-urile și sunt căutate . Dacă cele două CNF conduc la instanțierea aceleiași variabile cu aceeași valoare, atunci instanțierea se poate face din CNF . $\ phi \$ $v \$ $\ phi \ land v$ $\ phi \ land \ neg v$ $v '\$ $\ phi \$

Exemplu Luați în considerare CNF . Suntem interesați aici de variabilă și prospectăm variabila .

\ phi = (v_ {1} \ lor v_ {2}) \ land (v_ {1} \ lor \ neg v_ {2} \ lor v_ {3}) \ land (\ neg v_ {1} \ lor v_ { 2} \ lor v_ {4}) \ land (\ neg v_ {3} \ lor \ neg v_ {4})

v_ {2} \

v_ {1} \

Luați în considerare sarcina . Obținem și, prin urmare, atribuirea (deoarece această variabilă apare doar pozitiv).

v_ {1} = {\ textit {true}} \

(v_ {2} \ lor v_ {4}) \ land (\ neg v_ {3} \ lor \ neg v_ {4})

v_ {2} = {\ textit {true}} \

Luați în considerare sarcina . Obținem și, prin urmare, clauza de atribuire prin unitate.

v_ {1} = {\ textit {false}} \

v_ {2} \ land (\ neg v_ {2} \ lor v_ {3}) \ land (\ neg v_ {3} \ lor \ neg v_ {4})

v_ {2} = {\ textit {true}} \

În toate cazurile, această atribuire este obținută și, prin urmare, este posibilă de la CNF .

v_ {2} = {\ textit {true}} \

\ phi \

Amintiți-vă că complexitatea problemei SAT provine din dimensiunea exponențială a arborelui de căutare în comparație cu numărul de variabile. Prospectarea face posibilă reducerea considerabilă a acestui număr de variabile de la rădăcină (sau de la orice nod al arborelui) cu o complexitate suplimentară relativ scăzută în vederea reducerii arborelui de căutare.

Program dinamic

Samer și Szeider au propus un program dinamic algoritm FTP în care lățimea arborelui graficului asociată cu formula care urmează să fie testată. Avantajul acestui algoritm este că poate face și contorizarea evaluărilor și, prin urmare, rezolva problema #SAT. De asemenea, poate fi paralelizat . Este implementat în instrumentul gpuSAT (paralelizarea este implementată prin GPU).

Căutare locală

Pornind de la o alocare a tuturor variabilelor, încercăm să modificăm anumite evaluări pentru a reduce numărul de clauze nesatisfăcute. Acest algoritm suferă de mai multe defecte: poate cădea în minime locale și nu este în măsură să dovedească nesatisfacție, dar este foarte eficient în probleme nestructurate (adică deseori probleme generate aleatoriu). În caz de eșec după o lungă perioadă de timp, este posibil să alegeți o nouă alocare aleatorie pentru a evita minimele locale.

Aplicații

Este posibil să reduceți (traduceți) unele probleme de inteligență artificială la problema SAT pentru a rezolva în mod eficient aceste probleme.

Diagnostic

Diagnosticul sistemelor statice constă în determinarea dacă un sistem se comportă la dat vina observarea intrărilor și ieșirilor sistemului. Modelul sistemului poate fi tradus într-un set de constrângeri (disjuncții): pentru fiecare componentă a sistemului, se creează o variabilă care este evaluată ca fiind adevărată dacă componenta are un comportament anormal ( Ab normal ). Observațiile pot fi traduse și printr-un set de disjuncții. Alocarea găsită de algoritmul de satisfacție este un diagnostic. $vs.$ $ABC)$

Planificare clasică

Problema clasică de planificare este de a găsi o secvență de acțiuni care să conducă de la o stare a sistemului la un set de stări. Având în vedere o lungime maximă a planului și un set de variabile de stare booleene utilizate pentru a descrie starea sistemului, creăm variabile propoziționale pentru orice variabilă . Variabila este adevărată dacă variabila de stare este adevărată după numărul acțiunii . De asemenea, creăm variabile pentru orice și orice acțiune . Variabila este adevărată dacă numărul acțiunii este . Apoi este posibil să se transforme modelul sistemului într-un set de clauze. De exemplu, dacă acțiunea face ca variabila să treacă la adevărat atunci când este falsă , atunci CNF va conține o clauză (care este tradusă prin clauză ). Alocarea găsită de algoritmul de satisfacție poate fi imediat tradusă într-un plan. $nu$ $V$ $v ^ {i}$ $i \ in \ {0, \ dots, n \}$ $v \ în V$ $v_ {i}$ $eu$ $a ^ {i}$ $i \ in \ {1, \ dots, n \}$ $la$ $a ^ {i}$ $eu$ $la$ $la$ $v_ {1}$ $(\ neg v ^ {0}) \ Rightarrow a ^ {1} \ Rightarrow v ^ {1}$ ${\ displaystyle v ^ {0} \ lor \ neg a ^ {1} \ lor v ^ {1}}$

Planificarea clasică prin SAT este foarte eficientă dacă știm lungimea n a planului . Dacă această valoare nu este cunoscută, se pot căuta planuri pentru o valoare incrementală, care este uneori costisitoare (în special deoarece CNF nu este satisfăcător până la n - 1).

Verificarea modelului

O abordare similară a fost utilizată pentru verificarea modelului . Principala diferență este că verificarea modelului se aplică traiectoriilor de lungime infinită spre deosebire de planificare. Cu toate acestea, dacă spațiul de stare al sistemului este finit, orice traiectorie infinită se bucură într-un anumit punct și putem limita dimensiunea traiectoriilor pe care este necesar să le verificăm. Modelul verificarea mărginite profită de această proprietate pentru a transforma problema de verificare de model într - o serie de probleme satisfiabilitate.

Criptografie

Complexitatea problemei SAT este o componentă esențială a securității oricărui sistem criptografic.

De exemplu, o funcție hash securizată constituie o cutie neagră care poate fi formulată în timp și spațiu finit ca o conjuncție de clauze normale, ale căror variabile booleene corespund direct valorilor posibile ale datelor de intrare ale funcției. și fiecare dintre biții de rezultat trebuie să răspundă la un test de egalitate boolean cu biții de date ai oricărui bloc de date de intrare. Funcțiile securizate de hash sunt utilizate în special în sistemele de autentificare (cunoașterea datelor secrete de intrare utilizate pentru a produce valoarea hash) și semnătură (împotriva oricărei modificări „ușoare” sau falsificări a datelor de intrare, care sunt cunoscute împreună cu funcția hash în sine și rezultatul acestuia).

Securitatea funcției hash depinde de posibilitatea recuperării unui bloc de date de intrare arbitrar (posibil diferit de blocul de date secret pentru care a fost obținută o anumită valoare hash) făcând posibilă egalizarea valorii binare returnate de funcția hash. O metodă de explorare sistematică a tuturor valorilor posibile ale datelor de intrare și pentru care funcția hash este aplicată ca un oracol, face posibilă satisfacerea problemei unei valori hash egale cu cea căutată, dar complexitatea ei algoritmică va să fie exponențial (în funcție de dimensiunea maximă de biți a datelor de intrare a funcției hash)

Încercarea de a egaliza o valoare hash cu variabile de intrare de valoare necunoscută este o problemă SAT (și întrucât, în practică, datele de intrare pentru funcția hash constă din mai mulți biți, va fi o problemă n -SAT cu n destul de mare (și în orice caz mai mare sau egal cu 3) Știm atunci că această problemă este reductibilă în timp polinomial la o problemă 3 - SAT, care este NP-completă.

Securitatea funcției hash va fi puternic legată de faptul imposibilității de a o reduce mai simplu (decât de un algoritm NP-complet de suficientă complexitate) prin reducerea formei conjunctive a clauzelor care o definesc pur și simplu, pentru a izola subseturi de variabile de intrare de dimensiuni mai mici, dar suficiente pentru a determina o parte din rezultatul funcției hash a cărei ordine n va fi apoi mult mai mică și să nu mai trebuiască să exploreze doar valorile posibile ale acestor numai subseturi de variabile pentru a satisface condiția de egalitate a rezultatului, fără a fi nevoie să testați toate celelalte variabile a căror valoare poate fi setată în mod arbitrar la anumite valori determinate de un algoritm mai simplu (învățarea clauzelor, abordări prospective de mai sus).

Logica modală

Problema SAT poate fi utilizată ca subrutină pentru a rezolva problema de satisfacție logică modală.

Extensii

Există extensii la problema SAT.

Formula booleană cuantificată
Teoriile modulului de satisfacție (SMT)
UNIQUE-SAT: admite o formulă propozițională o atribuire unică a variabilelor propoziționale?
MAX-SAT: având în vedere un set de clauze, găsiți numărul maxim de clauze care pot fi satisfăcute.
Problema satisfacției constrângerii
Satisfacție în logica modală , logica de ordinul întâi , logica de ordinul doi ...

Istoric

Martin Davis și Hilary Putnam își oferă algoritmul pentru problema SAT în 1960, apoi îmbunătățit de George Logemann și Donald Loveland (în) ( Algoritm Davis-Putnam-Logemann-Loveland ). Momentul a fost dat atunci când Stephen Cook a folosit-o ca paradigmă a problemelor NP-complete . Un alt impuls a fost dat în 2002, când a început competiția SAT între software-ul de rezolvare a problemelor SAT.

Note și referințe

Inês Lynce și Joël Ouaknine , „ Sudoku ca o problemă SAT ”, în Proc. al nouălea simpozion internațional de inteligență artificială și matematică , Springer,1 st ianuarie 2006( citiți online , consultat la 10 mai 2016 )
Stephen A. Cook a „ Complexitatea procedurilor teoremei-dovedind “ Computing Surveys (CSUR) , ACM, '71 STOC,1 st ianuarie 1971, p. 151–158 ( DOI 10.1145 / 800157.805047 , citit online , accesat la 30 decembrie 2015 )
Boris A. Trakhtenbrot , „ A Survey of Russian Approaches to Perebor (Brute-Force Searches) Algorithms ”, Annals of the History of Computing , vol. 6,1 st octombrie 1984, p. 384-400 ( ISSN 0164-1239 , DOI 10.1109 / MAHC.1984.10036 , citit online , accesat la 30 decembrie 2015 )
(în) A. Biere , A. Beer , Mr. Heule și H. van Maaren , Handbook of Satisfiability: Volume 185 Frontiers in Artificial Intelligence and Applications , Amsterdam, IOS Press,15 februarie 2009, 966 p. ( ISBN 978-1-58603-929-5 și 1-58603-929-6 , citiți online )
„ Satisfăcător ” , pe CNRTL .
„ Satisfăcător ” , pe Larousse .
(în) Bengt Aspvall, Michael F. Plass și Robert E. Tarjan, " Un algoritm în timp liniar pentru testarea adevărului unor formule booleene cuantificate ", Information Processing Letters , 8, p. 121-123 (1979), [ citește online ] .
William F. Dowling și Jean H. Gallier , „ Algoritmi în timp liniar pentru testarea satisfacției formulelor de corn propozițional ”, The Journal of Logic Programming , vol. 1,1 st octombrie 1984, p. 267-284 ( DOI 10.1016 / 0743-1066 (84) 90014-1 , citit online , accesat la 31 decembrie 2015 )
Neil D. Jones și William T. Laaser , „ Probleme complete pentru timpul polinom determinist ”, Theoretical Computer Science , vol. 3, n o 1,Octombrie 1976, p. 105-117 ( ISSN 0304-3975 , DOI 10.1016 / 0304-3975 (76) 90068-2 , citit online , accesat la 6 septembrie 2018 )
Thomas J. Schaefer (1978). „Complexitatea problemelor de satisfacție” STOC 1978 : 216-226 p. ( DOI : 10.1145 / 800133.804350 ).
(ro) Martin Davis și Hillary Putnam, „A Computing Procedure for Quantification Theory”, Communications of the ACM , 7, p. 201-215 (1960) [ citește online ]
(ro) Martin Davis, George Logemann și Donald Loveland, „Un program mașină pentru demonstrarea teoremelor”, Comunicări ale ACM , 5, p. 394-397 (1962), [ citește online ]
Clasament în timpul SAT Challenge 2012, categoria Aplicații | Sat Challenge 2012
(în) Stefan Szeider , Teoria și aplicațiile testării satisfacției , Springer Berlin Heidelberg,2004( ISBN 978-3-540-20851-8 și 9783540246053 , DOI 10.1007 / 978-3-540-24605-3_15 , citiți online ) , p. 188–202
Jean-Marie Lagniez , Daniel Le Berre , Tiago de Lima și Valentin Montmirail , „ A Shorts Recursive for CEGAR: Application To the Modal Logic K Satisfiability Problem ”, Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence , International Joint Conferences despre Organizația Inteligenței Artificiale,august 2017, p. 674-680 ( ISBN 9780999241103 , DOI 10.24963 / ijcai.2017 / 94 , citite online , accesat 1 st septembrie 2018 )
(în) Thomas Caridroit, Jean-Marie Lagniez Daniel Le Berre, Tiago Lima Valentin Montmirail " A SAT-Based Approach for Solving the Modal Logic S5 Satisfiability Problem " , Proceedings of the Thirty-First {AAAI} Conference on Artificial Intelligence, San Francisco, California, {SUA.} , 4-9 februarie 2017, p. 3864–3870 ( citește online )
(en-SUA) R. Sebastiani și M. Vescovi , „ Raționament automatizat în logica modală și de descriere prin codificarea SAT: studiul de caz al K (m) / ALC-Satisfiabilitatea ” , Journal of Artificial Intelligence Research , vol. 35,25 iunie 2009, p. 343-389 ( ISSN 1076 - 9757 , DOI 10.1613 / jair.2675 , citite online , accesat 1 st septembrie 2018 )
Site-ul web al concursului SAT .

Vezi și tu

Bibliografie

René Cori și Daniel Lascar , Logică matematică I. Calcul propozițional, algebre booleene, calcul predicat [ detaliu ediții ]
J.-M. Alliot, T. Schiex, P. Brisset și F. Garcia, Inteligență artificială și calcul teoretic , Cépaduès, 2002 ( ISBN 2-85428-578-6 )
L. Sais, Problema SAT: Progrese și provocări , 2008 ( ISBN 2746218860 )
Sharad Malik și Lintao Zhang Satisfacție booleană: de la duritatea teoretică la succesul practic , Comunicări ale ACM, (2009) Vol. 52 nr. 8, paginile 76-82.
John Franco și John Martin, Manual de satisfacție , IOS Press ( citiți online ) , „Capitolul 1: O istorie a satisfacției”

Articole similare

Link extern

„ Site-ul oficial al concursului SAT ”

„ Jocul SAT, un joc în care trebuie să găsești o evaluare care să satisfacă o formulă booleană ”