Problema de satisfacibilitat booleana

En teoria de complexitat computacional, el problema de satisfacibilitat booleana (també conegut per les sigles SAT) és el problema de determinar si existeix una interpretació que satisfà una fórmula booleana donada. En altres paraules, es qüestiona si les variables d'una fórmula booleana es poden reemplaçar de forma consistent pels valors CERT o FALS de manera que la fórmula s'avalui a CERT. Per exemple, la fórmula "a AND NOT b" es pot satisfer amb els valors a = CERT i b = FALS, que fan la fórmula doni CERT. En canvi, la fórmula "a AND NOT a" no té cap valor d'entrada que pugui donar CERT i no es pot satisfer en cap cas.^[1]

Aquest problema va ser el primer problema identificat dins la classe de complexitat NP-complet, i per tant, tots els problemes dins de la classe NP son tant complexos com SAT però no més que aquest. No es coneix cap algorisme que resolgui el problema SAT de forma òptima i es creu que no existeix, tot i que no s'ha pogut demostrar. De fet, resoldre el problema SAT amb un algorisme de temps polinòmic és equivalent a demostrar que P = NP.

Tot i això, existeixen algorismes heurístics per resoldre SAT capaços de treballar amb instàncies del problema amb desenes de milers de variables i fórmules amb milions de símbols.^[2] Aquests algorismes tenen aplicacions pràctiques en problemes d'inteli·lgència artificial, disseny de circuits i demostracions automàtiques de teoremes.

Definició formal

Una fórmula de lògica proposicional, també anomenada expressió booleana, es construeix amb variables, operadors AND (conjunció, símbol ∧), OR (disjunció, símbol ∨), NOT (negació, ¬) i parèntesis. Una fórmula es pot satisfer si combinant apropiadament els valors lògics a les entrades la sortida dona CERT. El problema SAT consisteix en, donada una fórmula, veure si es pot satisfer o no. Aquest problema de decisió és cabdal en diverses àrees de les ciències de la computació, com informàtica teòrica, teoria de la complexitat, criptografia i intel·ligència artificial.

S'anomena literals a una variable o la seva negació. Una clàusula és una disjunció de literals. Una fórmula està en la seva forma normal conjuntiva (CNF) si és una conjunció de clàusules. Per exemple, x₁ és un literal positiu, ¬x₂ és un literal negatiu, x₁ ∨ ¬x₂ és una clàusula i (x₁ ∨ ¬x₂) ∧ (¬x₁ ∨ x₂ ∨ x₃) ∧ ¬x₁ és una fórmula. Fent servir les propietats de l'àlgebra de Boole, és possible transformar qualsevol fórmula en la seva equivalent en forma normal conjuntiva. Aquesta transformació pot significar una expansió exponencial.

Complexitat i versions restrictives

SAT va ser el primer problema conegut dins de NP-complet, tal com van provar Stephen Cook i Leonid Levin de forma independent els anys 1971 i 1973 respectivament.^[3]^[4] La demostració mostra que tot problema de decisió dins de NP es pot reduir al problema SAT amb CNFs, de vegades anomenat problema CNFSAT. Una propietat útil de la reducció de la demostració és que preserva el nombre de respostes acceptades. Per exemple, decidir si un graf determinat es pot colorejar amb 3 colors és un altre problema NP; si un graf te 17 possibilitats de colorejat, la fórmula SAT aconseguit de la reducció de Cook tindrà 17 assignacions vàlides.

El problema SAT és trivial si les fórmules estan en la forma normal disjuntiva, disjuncions de conjuncions de literals. Una forma es pot satisfer si i només si una de les conjuncions es satisfà, i una conjunció es pot satisfer si i només si no conté alhora x i NOT x per alguna variable x. Una fórmula així es pot resoldre en temps lineal. És més, si es restringeix el problema a que les fórmules estiguin en forma normal disjuntiva i que cada variable només aparegui un sol cop a cada conjunció, es pot comprovar tota la fórmula en temps constant. Però pot prendre un temps exponencial en temps i espai convertir un problema SAT genèric a una forma disjuntiva normal.^[1]

3-SAT

Es coneix com a problema 3-SAT (o 3CNFSAT) al SAT on es limita la fórmula a estar en forma conjuntiva normal on cada clàusula està limitada a, com a molt, tres literals. Aquest problema segueix sent NP-complet. La transformació d'una forma general a un problema 3-SAT pot fer créixer el nombre de clàusules de forma polinòmica.^[1]

Referències

↑ ^1,0 ^1,1 ^1,2 Michael., Sipser,. Introduction to the theory of computation. 3a edició. Boston, MA: Cengage Learning, 2013. ISBN 9781133187790.
↑ Ohrimenko, Olga; Stuckey, Peter J.; Codish, Michael. Propagation = Lazy Clause Generation (en anglès). Berlin, Heidelberg: Springer Berlin Heidelberg, 2007-09-23, p. 544–558. DOI 10.1007/978-3-540-74970-7_39. ISBN 9783540749691.
↑ Cook, Stephen A. «The complexity of theorem-proving procedures». Proceedings of the 3rd Annual ACM Symposium on Theory of Computing. ACM, 03-05-1971, pàg. 151–158. DOI: 10.1145/800157.805047.
↑ Trakhtenbrot, B.A. «A Survey of Russian Approaches to Perebor (Brute-Force Searches) Algorithms» (en anglès). IEEE Annals of the History of Computing, 6, 4, 10-1984, pàg. 384–400. DOI: 10.1109/mahc.1984.10036. ISSN: 1058-6180.

[:0-1] 1,0 ^1,1 ^1,2 Michael., Sipser,. Introduction to the theory of computation. 3a edició. Boston, MA: Cengage Learning, 2013. ISBN 9781133187790.

[2] Ohrimenko, Olga; Stuckey, Peter J.; Codish, Michael. Propagation = Lazy Clause Generation (en anglès). Berlin, Heidelberg: Springer Berlin Heidelberg, 2007-09-23, p. 544–558. DOI 10.1007/978-3-540-74970-7_39. ISBN 9783540749691.

[3] Cook, Stephen A. «The complexity of theorem-proving procedures». Proceedings of the 3rd Annual ACM Symposium on Theory of Computing. ACM, 03-05-1971, pàg. 151–158. DOI: 10.1145/800157.805047.

[4] Trakhtenbrot, B.A. «A Survey of Russian Approaches to Perebor (Brute-Force Searches) Algorithms» (en anglès). IEEE Annals of the History of Computing, 6, 4, 10-1984, pàg. 384–400. DOI: 10.1109/mahc.1984.10036. ISSN: 1058-6180.

[1]

[2]

[3]

[4]