2-satisfactibilidad

En informàtica, la 2-satisfactibilidad, 2-SAT o simplement 2SAT és un problema computacional d'assignació de valors a variables, cada una de les quals té dos valors possibles, en la finalitat de satisfer un sistema de restriccions sobre parells de variables. És un cas especial del problema general de satisfacció booleana, que pot incloure restriccions sobre més de dos variables, i dels problemes de satisfacció de restriccions, que poden permetre més de dos opcions per al valor de cada variable. Pero a diferència d'estos problemes més generals, que són NP-complets, la 2-satisfacció pot resoldre's en temps polinòmic.

Les instàncies del problema de la 2-satisfactibilidad s'expressen normalment com a fòrmules booleanas d'un tipo especial, cridades forma normal conjuntiva (2-CNF) o fòrmules de Krom. També poden expressar-se com un tipo especial de grafo dirigit, el grafo d'implicació, que expressa les variables d'una instància i les seues negacions com a vèrtiços d'un grafo, i les restriccions sobre parells de variables com a arestes dirigides. Abdós tipos d'entrades poden resoldre's en temps llineal, ya siga per mig d'un método basat en el backtracking o utilisant els components fortament conectats del grafo d'implicació. La resolució, un método per a combinar parells de restriccions en la finalitat d'obtindre restriccions vàlides adicionals, també conduïx a una solució en temps polinòmic. Els problemes de 2-satisfactibilidad proporcionen una de les dos subclasses principals de les fòrmules de forma normal conjuntiva que poden resoldre's en temps polinòmic; l'atra de les dos subclasses és la Horn-satisfactibilidad.

La 2-satisfiability pot aplicar-se a problemes de geometria i visualisació en els que una colecció d'objectes té cada u dos ubicacions potencials i l'objectiu és trobar una colocació per a cada objecte que evite solapamientos en atres objectes. Atres aplicacions inclouen l'agrupació de senyes per a minimisar la suma dels diàmetros dels grups, la programació de classes i deports, i la recuperació de formes a partir d'informació sobre les seues seccions travesseres.

En la teoria de la complexitat computacional, la 2-satisfactibilidad és un eixemple de problema NL-complet, que pot resoldre's de forma no determinista utilisant una cantitat logarítmica d'almagasenament i que es troba entre els problemes més difícils de resoldre en este llímit de recursos. El conjunt de totes les solucions a una instància de 2 satisfacció pot tindre l'estructura d'un grafo mijà, pero contar estes solucions és P-complet i, per tant, no s'espera que tinga una solució en temps polinòmic. Les instàncies aleatòries experimenten una transició de fase brusca d'instàncies resolubles a instàncies irresolubles a mida que la proporció entre restriccions i variables aumenta més allà d'1, un fenomen conjeturado pero no demostrat per a formes més complicades del problema de la satisfacibilidad. Una variació computacionalment difícil de la 2-satisfactibilidad, trobar una assignació de veres que maximizar el número de restriccions satisfetes, té un algoritme d'aproximació que la seua optimalidad depén de la conjectura de jocs únics, i una atra variació difícil, trobar una assignació satisfactòria que minimise el número de variables verdaderes, és un important cas de prova per a la complexitat parametrizada.

Representacions del problema

Un problema de 2 satisfacció pot descriure's per mig d'una expressió booleana en una forma restringida especial. Es tracta d'una conjunció (una operació booleana) de clàusules, a on cada clàusula és una disjunció (una operació booleana) de dos variables o variables negades. Les variables o les seues negacions que apareixen en esta fòrmula es coneixen com a lliterals.^[1]Per eixemple, la següent fòrmula està en forma normal conjuntiva, en sèt variables, onze clàusules i 22 lliterals:

$\begin{matrix} (x_{0} \lor x_{2}) \land (x_{0} \lor \neg x_{3}) \land (x_{1} \lor \neg x_{3}) \land (x_{1} \lor \neg x_{4}) \land \\ (x_{2} \lor \neg x_{4}) \land (x_{0} \lor \neg x_{5}) \land (x_{1} \lor \neg x_{5}) \land (x_{2} \lor \neg x_{5}) \land \\ (x_{3} \lor x_{6}) \land (x_{4} \lor x_{6}) \land (x_{5} \lor x_{6}) . \end{matrix}$

El problema de la 2-satisfacció consistix en trobar una assignació de veres a estes variables que faça que tota la fòrmula siga verdadera. Tal assignació elegix si fer cada una de les variables verdaderes o falses, de modo que a lo manco un lliteral en cada clàusula es convertix en verdader. Per a l'expressió mostrada dalt, una possible assignació satisfactòria és la que fa que les sèt variables siguen verdaderes. Cada clàusula té a lo manco una variable no negativa, per lo que esta assignació satisfà totes les clàusules. També hi ha atres 15 formes d'assignar totes les variables per a que la fòrmula siga verdadera. Per lo tant, l'instància de 2 satisfacció representada per esta expressió és satisfactible.

Les fòrmules d'esta forma es coneixen com a fòrmules 2-CNF. El "2" en este nom significa el número de lliterals per clàusula, i "CNF" significa forma normal conjuntiva, un tipo d'expressió booleana en forma de conjunció de disjunció.^[1] També es diuen fòrmules Krom, pel treball del matemàtic de la UC Davis Melven R. Krom, l'artícul de la qual de 1967 va ser un dels primers treballs sobre el problema de la 2-satisfactibilidad.^[2]

Cada clàusula d'una fòrmula 2-CNF és llògicament equivalent a una implicació d'una variable o variable negada a l'atra. Per eixemple, la segona clàusula de l'eixemple pot escriure's de tres formes equivalents:

$(x_{0} \lor \neg x_{3}) \equiv (\neg x_{0} \Rightarrow \neg x_{3}) \equiv (x_{3} \Rightarrow x_{0}) .$

Per esta equivalència entre estos distints tipos d'operació, una instància de 2-satisfactible també pot escriure's en forma normal implicativa, en la que substituïm cada clàusula o de la forma normal conjuntiva per les dos implicacions a les que és equivalent.^[3]

Una tercera forma, més gràfica, de descriure una instància de 2-satisfactible és com un grafo d'implicació. Un grafo d'implicació és un grafo dirigit en el que hi ha un vèrtiç per variable o variable negada, i una aresta que conecta un vèrtiç en un atre sempre que les variables corresponents estiguen relacionades per una implicació en la forma normal implicativa de l'instància. Un grafo d'implicació deu ser un grafo biaixat-simètric, lo que significa que té una simetria que du cada variable a la seua negació i invertix les orientacions de totes les arestes.^[4]

Algoritmes

Es coneixen varis algoritmes per a resoldre el problema de la 2-satisfacció. Els més eficients tarden un temps llineal.^[2]^[4]^[5]

Resolució i tancament transitivo

Krom (1967) va descriure el següent procediment de decisió en temps polinòmic per a resoldre instàncies de 2-satisfactibilidad.^[2]

Supongam que una instància de 2 satisfacció conté dos clàusules que utilisen la mateixa variable x, pero que x està negada en una clàusula i no en l'atra. Llavors les dos clàusules es poden combinar per a produir una tercera clàusula, que té els atres dos lliterals en les dos clàusules; esta tercera clàusula també deu ser satisfeta sempre que les dos primeres clàusules siguen satisfetes. Açò es diu resolució. Per eixemple, podem combinar les clàusules $(a \lor b)$ i $(\neg b \lor \neg c)$ per a obtindre la clàusula $(a \lor \neg c)$ , En térmens de la forma implicativa d'una fòrmula 2-CNF, esta regla equival a trobar dos implicacions $\neg a \Rightarrow b$ i $b \Rightarrow \neg c$ i inferir per transitividad una tercera implicació $\neg a \Rightarrow \neg c$ .^[2]

Krom escriu que una fòrmula és consistent si l'aplicació repetida d'esta regla d'inferència no pot generar les dos clàusules $(x \lor x)$ i $(\neg x \lor \neg x)$ per a qualsevol variable $x$ . Com ell demostra, una fòrmula 2-CNF és satisfacible si i només si és consistent. Perque, si una fòrmula no és consistent, no és possible satisfer les dos clàusules $(x \lor x)$ i $(\neg x \lor \neg x)$ simultàneament. I, si és coherent, llavors la fòrmula pot ampliar-se afegint repetidament una clàusula de la forma $(x \lor x)$ o $(\neg x \lor \neg x)$ cada volta, mantenint la coherència en cada pas, fins que incloga una clàusula d'este tipo per a cada variable. En cada u d'estos passos d'ampliació, sempre es pot afegir una d'estes dos clàusules preservant la coherència, ya que si no, l'atra clàusula es podria generar utilisant la regla d'inferència. Una volta que totes les variables tenen una clàusula d'esta forma en la fòrmula, es pot generar una assignació satisfactòria de totes les variables establint una variable $x$ a verdader si la fòrmula conté la clàusula $(x \lor x)$ i posant-la en fals si la fòrmula conté la clàusula $(\neg x \lor \neg x)$ .^[2]

Krom s'ocupava principalment de la completitud dels sistemes de regles d'inferència, més que de l'eficàcia dels algoritmes. No obstant, el seu método du a un llímit de temps polinòmic per a resoldre problemes de 2 satisfacció. Agrupant totes les clàusules que utilisen la mateixa variable i aplicant la regla d'inferència a cada parell de clàusules, és possible trobar totes les inferència possibles a partir d'una instància 2-CNF donada, i comprovar si és consistent, en un temps total $O(n 3)$ , a on $n$ és el número de variables de l'instància. Esta fòrmula resulta de multiplicar el número de variables pel número $O(n 2)$ de parells de clàusules que impliquen una variable donada, als que es pot aplicar la regla d'inferència. Aixina, és possible determinar si una instància 2-CNF donada és satisfacible en temps $O(n 3)$ . Ya que trobar una assignació satisfactòria utilisant el método de Krom implica una seqüència de comprovacions de consistència $O(n)$ , duria un temps $O(n 4)$ . Inclús, Itai & Shamir (1976) citen un llímit de temps més ràpit de $O(n 2)$ per a este algoritme, basat en un ordenament més cuidadós de les seues operacions. No obstant, inclús este llímit de temps més chicotet va ser millorat en gran mida pels algoritmes de temps llineal posteriors de Even, Itai i Shamir (1976) i Aspvall, Plass i Tarjan (1979).

En térmens del grafo d'implicació de l'instància de 2-satisfacció, la regla d'inferència de Krom pot interpretar-se com la construcció del tancament transitivo del grafo. Com observa Cook (1971), també pot vore's com una instància de l'algoritme Davis-Putnam per a resoldre problemes de satisfacibilidad utilisant el principi de resolució. La seua correcció es deduïx de la correcció més general de l'algoritme de Davis-Putnam. El seu llímit de temps polinòmic es deriva del fet de que cada pas de resolució aumenta el número de clàusules de l'instància, que està llimitat superiormente per una funció quadràtica del número de variables.^[6]

Backtracking llimitat

Even, Itai i Shamir (1976) descriuen una tècnica que implica un backtracking llimitat per a resoldre problemes de satisfacció de restriccions en variables binàries i restriccions per parells. Apliquen esta tècnica a un problema de programació d'aules, pero també observen que s'aplica a atres problemes, inclós 2-SAT.^[5]

L'idea bàsica del seu enfocament és construir una assignació de veres parcial, una variable al mateix temps. Certs passos dels algoritmes són «punts d'elecció», punts en els que una variable pot rebre qualsevol dels dos valors de veres diferents, i els passos posteriors en l'algoritme pot fer que es retrocedixca a un d'estos punts d'elecció. No obstant, només es pot tornar sobre l'elecció més recent. Totes les eleccions anteriors a la més recent són permanents.^[5]

Inicialment, no hi ha cap punt d'elecció, i totes les variables estan sense assignar. En cada pas, l'algoritme elegix la variable el valor de la qual establir, com seguix:

Si hi ha una clàusula que les seues dos variables ya estan fixades, de manera que es falsifica la clàusula, llavors l'algoritme retrocedix al seu punt d'elecció més recent, desfent les assignació que va fer des d'eixa elecció, i invertix la decisió presa en eixa elecció. Si no hi ha cap punt d'elecció, o si l'algoritme ya ha retrocedit fins al punt d'elecció més recent, llavors aborta la busca i informa de que la fòrmula 2-CNF d'entrada és insatisfactible.
Si hi ha una clàusula en la que una de les dos variables de la clàusula ya s'ha establit, i la clàusula encara podria ser verdadera o falsa, llavors l'atra variable s'establix d'una manera que obliga a la clàusula a ser verdadera.
En el restant dels casos, es garantisa que cada clàusula serà verdadera independentment de cóm s'assignen les variables restants, o be no s'ha assignat encara cap de les seues dos variables. En este cas, l'algoritme crea un nou punt d'elecció i establix qualsevol de les variables sense assignar a un valor elegit arbitrariamente.

Intuitivamente, l'algoritme seguix totes les cadenes d'inferència despuix de fer cada una de les seues eleccions. Açò conduïx a una contradicció i a un pas arrere o, si no es deriva cap contradicció, es deduïx que l'elecció va ser correcta i conduïx a una assignació satisfactòria. Per lo tant, l'algoritme o be troba correctament una assignació satisfactòria o be determina correctament que l'entrada és insatisfactible.^[5]

Even et al. no descriuen en detalle cóm implementar este algoritme de forma eficient. Només afirmen que «utilisant estructures de senyes apropiades per a trobar les implicacions de qualsevol decisió», cada pas de l'algoritme (llevat la reculada) pot realisar-se ràpidament. No obstant, algunes entrades poden fer que l'algoritme retrocedixca moltes voltes, realisant cada volta molts passos abans de retrocedir, per lo que la seua complexitat global pot ser no llineal. Per a evitar este problema, modifiquen l'algoritme per a que, despuix d'alcançar cada punt d'elecció, comence a provar simultàneament les dos assignació per al conjunt de variables en el punt d'elecció, invertint el mateix número de passos en cada una de les dos assignació. Tan pronte com la prova d'una d'estes dos assignació crearia un atre punt d'elecció, l'atra prova es deté, de modo que en qualsevol etapa de l'algoritme només hi ha dos branques de l'arbre de reculada que encara s'estan provant. D'esta manera, el temps total empleat en realisar les dos proves per a qualsevol variable és proporcional al número de variables i clàusules de la fòrmula d'entrada els valors de la qual s'assignen permanentment. Com a resultat, l'algoritme tarda un temps llineal en total.^[5]

Components fortament conectats

Aspvall, Plass i Tarjan (1979) varen trobar un procediment de temps llineal més senzill per a resoldre instàncies de 2 satisfacció, basat en la noció de components fortament conectats de la teoria de grafos.^[4]

Es diu que dos vèrtiços d'un grafo dirigit estan fortament conectats entre sí si existix un camí dirigit d'un a un atre i viceversa. Es tracta d'una relació d'equivalència, i els vèrtiços del grafo poden dividir-se en components fortament conectats, subconjunts dins dels quals cada dos vèrtiços estan fortament conectats. Existixen varis algoritmes eficients en temps llineal per a trobar les components fortament conectades d'un grafo, basats en la busca per profunditat: L'algoritme de components fortament conectats de Tarjan^[7] i l'algoritme de components fortament conectats basat en rutes^[8]realisen cada u una única busca en profunditat. L'algoritme de Kosaraju realisa dos busques en profunditat, pero és molt senzill.

En térmens del grafo d'implicació, dos lliterals pertanyen al mateix component fortament conectat sempre que existixquen cadenes d'implicacions d'un lliteral a l'atre i viceversa. Per lo tant, els dos lliterals deuen tindre el mateix valor en qualsevol assignació satisfactòria a l'instància de 2-satisfacció donada. En particular, si una variable i la seua negació pertanyen al mateix component fortament conectat, l'instància no pot satisfer-se, perque és impossible assignar a abdós lliterals el mateix valor. Com varen demostrar Aspvall et al., es tracta d'una condició necessària i suficient: una fòrmula 2-CNF és satisfacible si i només si no hi ha cap variable que pertanyga al mateix component fortament conectat que la seua negació.^[4]

Açò conduïx immediatament a un algoritme de temps llineal per a provar la satisfabilidad de les fòrmules 2-CNF: n'hi ha prou en realisar un anàlisis de conectivitat forta en el grafo d'implicació i comprovar que cada variable i la seua negació pertanyen a components diferents. No obstant, com també varen demostrar Aspvall et al., també conduïx a un algoritme de temps llineal per a trobar una assignació satisfactòria, quan existix. El seu algoritme realisa els següents passos:

Construir el grafo d'implicació de l'instància i trobar els seus components fortament conectats utilisant qualsevol dels algoritmes coneguts de temps llineal per a l'anàlisis de conectivitat forta.
Comprovar si algun component fortament conectat conté tant una variable com la seua negació. En cas afirmatiu, informe de que l'instància no és satisfactòria i detinga's.
Construir la condensació del grafo d'implicació, un grafo més chicotet que té un vèrtiç per cada component fortament conectat, i una aresta del component i al component j sempre que el grafo d'implicació continga una aresta uv tal que o pertanyga al component i i v pertanyga al component j. La condensació és automàticament un grafo acíclic dirigit i, com el grafo d'implicació a partir del com es va formar, és asimètric.
Ordenar topológicamente els vèrtiços de la condensació. En la pràctica, açò pot conseguir-se eficientemente com a efecte secundari del pas anterior, ya que els components són generats per l'algoritme de Kosaraju en orde topològic i per l'algoritme de Tarjan en orde topològic invers.^[9]
Per a cada component en l'orde topològic invers, si les seues variables no tenen ya assignació de veres, establix tots els lliterals del component com a verdaders. Açò també fa que tots els lliterals en el component complementari siguen falsos.

Per l'ordenació topològica inversa i a la simetria oblicua, quan s'assigna el valor verdader a un lliteral, tots els lliterals als que es pot aplegar des d'ell a través d'una cadena d'implicacions ya s'hauran assignat el valor verdader. Simétricamente, quan un lliteral x s'establix com a fals, tots els lliterals que conduïxen a ell a través d'una cadena d'implicacions ya s'hauran establit com a falsos. Per lo tant, l'assignació de veres construïda per este procediment satisfà la fòrmula donada, que també completa la prova de correcció de la condició necessària i suficient identificada per Aspvall et al.^[4]

Com mostren Aspvall et al., un procediment similar que implica ordenar topológicamente els components fortament conectats del grafo d'implicació també es pot utilisar per a evaluar fòrmules booleanas totalment quantificades en les que la fòrmula quantificada és una fòrmula 2-CNF.^[4]

Referències

↑ ^1,0 ^1,1 Prestwich, Steven (2009), "2. Codificació CNF" , en Biere, Armin; Heule, Marijn ; van Maaren, Hans; Walsh, Toby (eds.), Manual de satisfacció , Fronteres en inteligència artificial i aplicacions, vol. 185, IOS Press, págs. 75 a 98, doi : 10.3233/978-1-58603-929-5-75 , ISBN 978-1-58603-929-5, Número d'identificació del subjecte 31666330 .
↑ ^2,0 ^2,1 ^2,2 ^2,3 ^2,4 Krom, Melven R. (1967), "El problema de decisió per a una classe de fòrmules de primer orde en les que totes les disjunció són binàries", Zeitschrift für Mathematische Logik und Grundlagen der Mathematik , 13 ( 1– 2): 15– 20, doi : [1]
↑ Russell, Stuart Jonathan; Norvig, Peter (2010), Inteligència artificial: un enfocament modern , série Prentice Hall sobre inteligència artificial, Prentice Hall, pág. 282, ISBN 978-0-13-604259-4.
↑ ^4,0 ^4,1 ^4,2 ^4,3 ^4,4 ^4,5 Aspvall, Bengt; Plass, Michael F.; Tarjan, Robert E. (1979), "Un algoritme de temps llineal per a provar la veritat de certes fòrmules booleanas quantificades" (PDF) , Information Processing Letters , 8 (3): 121– 123, doi : 10.1016/0020-0190(79)90002-4.
↑ ^5,0 ^5,1 ^5,2 ^5,3 ^5,4 Even, S .; Itai, A.; Shamir, A. (1976), "Sobre la complexitat dels problemes de fluix de múltiples productes i taules de temps", SIAM Journal on Computing , 5 (4): 691– 703, doi : 10.1137/0205048.
↑ Cook, Stephen A. (1971), "La complexitat dels procediments de demostració de teoremes", Proc. 3rd ACM Symp. Theory of Computing (STOC) , págs. 151– 158, doi : 10.1145/800157.805047 , S2CID 7573663
↑ Tarjan, Robert E. (1972), "Algoritmes de busca en profunditat i de grafos llineals", SIAM Journal on Computing , 1 (2): 146– 160, doi : 10.1137/0201010 , S2CID 16467262 .
↑ Publicat per primera volta per Cheriyan, J.; Mehlhorn, K. (1996), "Algoritmes per a gràfics densos i rets en la computadora d'accés aleatori", Algorithmica , 15 (6): 521– 549, doi : [2] , S2CID 8930091 Redescubierto en 1999 per Harold N. Gabow i publicat en Gabow, Harold N. (2003), "Searching (Ch 10.1)", en Gross, JL; Yellen, J. (eds.), Discrete Math. and its Applications: Handbook of Graph Theory , vol. 25, CRC Press, págs. 953– 984 .
↑ Harrison, Paul, Ordenament topològic robust i algoritme de Tarjan en Python , consultat el 9 de febrer de 2011

Este artícul conté una traducció derivada de «2-satisfactibilidad» de Wikipedia en castellà publicada baix la Llicència de documentació lliure de GNU i la Llicència Creative Commons Reconeiximent-CompartirIgual 4.0 Internacional.

[:0-1] 1,0 ^1,1 Prestwich, Steven (2009), "2. Codificació CNF" , en Biere, Armin; Heule, Marijn ; van Maaren, Hans; Walsh, Toby (eds.), Manual de satisfacció , Fronteres en inteligència artificial i aplicacions, vol. 185, IOS Press, págs. 75 a 98, doi : 10.3233/978-1-58603-929-5-75 , ISBN 978-1-58603-929-5, Número d'identificació del subjecte 31666330 .

[:1-2] 2,0 ^2,1 ^2,2 ^2,3 ^2,4 Krom, Melven R. (1967), "El problema de decisió per a una classe de fòrmules de primer orde en les que totes les disjunció són binàries", Zeitschrift für Mathematische Logik und Grundlagen der Mathematik , 13 ( 1– 2): 15– 20, doi : [1]

[3] Russell, Stuart Jonathan; Norvig, Peter (2010), Inteligència artificial: un enfocament modern , série Prentice Hall sobre inteligència artificial, Prentice Hall, pág. 282, ISBN 978-0-13-604259-4.

[:2-4] 4,0 ^4,1 ^4,2 ^4,3 ^4,4 ^4,5 Aspvall, Bengt; Plass, Michael F.; Tarjan, Robert E. (1979), "Un algoritme de temps llineal per a provar la veritat de certes fòrmules booleanas quantificades" (PDF) , Information Processing Letters , 8 (3): 121– 123, doi : 10.1016/0020-0190(79)90002-4.

[:3-5] 5,0 ^5,1 ^5,2 ^5,3 ^5,4 Even, S .; Itai, A.; Shamir, A. (1976), "Sobre la complexitat dels problemes de fluix de múltiples productes i taules de temps", SIAM Journal on Computing , 5 (4): 691– 703, doi : 10.1137/0205048.

[6] Cook, Stephen A. (1971), "La complexitat dels procediments de demostració de teoremes", Proc. 3rd ACM Symp. Theory of Computing (STOC) , págs. 151– 158, doi : 10.1145/800157.805047 , S2CID 7573663

[7] Tarjan, Robert E. (1972), "Algoritmes de busca en profunditat i de grafos llineals", SIAM Journal on Computing , 1 (2): 146– 160, doi : 10.1137/0201010 , S2CID 16467262 .

[8] Publicat per primera volta per Cheriyan, J.; Mehlhorn, K. (1996), "Algoritmes per a gràfics densos i rets en la computadora d'accés aleatori", Algorithmica , 15 (6): 521– 549, doi : [2] , S2CID 8930091 Redescubierto en 1999 per Harold N. Gabow i publicat en Gabow, Harold N. (2003), "Searching (Ch 10.1)", en Gross, JL; Yellen, J. (eds.), Discrete Math. and its Applications: Handbook of Graph Theory , vol. 25, CRC Press, págs. 953– 984 .

[9] Harrison, Paul, Ordenament topològic robust i algoritme de Tarjan en Python , consultat el 9 de febrer de 2011

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]