Aprendizaje de cláusulas basado en conflictos

El problema de satisfacibilidad consiste en encontrar una asignación satisfactoria para una fórmula dada en forma normal conjuntiva (FNC).

Un ejemplo de dicha fórmula es:

( ( no A ) o ( no C ) ) y ( B o C ),  

o, utilizando una notación común: ^{[ 5 ]}

${\displaystyle (\lnot A\lor \lnot C)\land (B\lor C)}$

donde A , B , C son variables booleanas,${\displaystyle \lnot A}$,${\displaystyle \lnot C}$,${\displaystyle B}$, y${\displaystyle C}$son literales y${\displaystyle \lnot A\lor \lnot C}$y${\displaystyle B\lor C}$son cláusulas.

Una asignación satisfactoria para esta fórmula es, por ejemplo:

${\displaystyle A=\mathrm {Falso}, B=\mathrm {Falso}, C=\mathrm {Verdadero}}$

puesto que hace que la primera cláusula sea verdadera (ya que${\displaystyle \lnot A}$es cierto) así como el segundo (ya que${\displaystyle C}$es cierto).

Este ejemplo utiliza tres variables ( A , B , C ), y hay dos posibles asignaciones (Verdadero y Falso) para cada una de ellas. Por lo tanto, uno tiene${\displaystyle 2^{3}=8}$posibilidades. En este pequeño ejemplo, se puede usar la búsqueda por fuerza bruta para probar todas las asignaciones posibles y comprobar si satisfacen la fórmula. Pero en aplicaciones reales con millones de variables y cláusulas, la búsqueda por fuerza bruta resulta poco práctica. La responsabilidad de un solucionador SAT es encontrar una asignación satisfactoria de forma eficiente y rápida aplicando diferentes heurísticas para fórmulas CNF complejas.

Si una cláusula tiene todos sus literales o variables menos uno evaluados como Falso, entonces el literal libre debe ser Verdadero para que la cláusula sea Verdadera. Por ejemplo, si la cláusula insatisfecha a continuación se evalúa con${\displaystyle A=\mathrm {Falso} }$y${\displaystyle B=\mathrm {Falso} }$debemos tener${\displaystyle C=\mathrm {Verdadero} }$ para que la cláusula${\displaystyle (A\lor B\lor C)}$ser cierto.

La aplicación iterativa de la regla de la cláusula de unidad se denomina propagación de unidad o propagación de restricción booleana (BCP).

Consideremos dos cláusulas${\displaystyle (A\lor B\lor C)}$y${\displaystyle (\neg C\lor D\lor \neg E)}$La cláusula${\displaystyle (A\lor B\lor D\lor \neg E)}$, obtenido al fusionar las dos cláusulas y eliminar ambas${\displaystyle \neg C}$y${\displaystyle C}$, se denomina resolvente de las dos cláusulas.

La resolvente es equisatisfacible con sus premisas (es decir, la resolvente es satisfacible si y solo si ambas premisas son satisfacibles).

Se puede utilizar una notación similar al cálculo de secuencias para formalizar muchos algoritmos de reescritura, incluido CDCL. Las siguientes son las reglas que un solucionador de CDCL puede aplicar para demostrar que no existe una asignación satisfactoria o para encontrar una, es decir:${\displaystyle A=(l_{1},\neg l_{2},l_{3},...)}$y cláusula de conflicto${\displaystyle C}$. ^{[ 6 ]}

Propagar Si una cláusula en la fórmula${\displaystyle \Phi }$tiene exactamente un literal sin asignar${\displaystyle l}$en${\displaystyle A}$, con todos los demás literales en la cláusula asignados como falsos en${\displaystyle A}$, extender${\displaystyle A}$con${\displaystyle l}$Esta regla representa la idea de que una cláusula actualmente falsa con solo una variable sin definir obliga a que esa variable se defina de tal manera que toda la cláusula sea verdadera; de lo contrario, la fórmula no se cumplirá .

$${\displaystyle {\frac {\begin{array}{c}\{l_{1},\dots ,l_{n},l\}\in \Phi \;\;\;\neg l_{1},\dots ,\neg l_{n}\in A\;\;\;\;\;l,\neg l\notin A\end{array}}{A:=A\;l}}{\text{ (Propagar)}}}$$

Decide si un literal${\displaystyle l}$está en el conjunto de literales de${\displaystyle \Phi }$y ninguno${\displaystyle l}$ni${\displaystyle \neg l}$está en${\displaystyle A}$, luego decide sobre el valor de verdad de${\displaystyle l}$y extender${\displaystyle A}$con la decisión literal${\displaystyle \bullet l}$Esta regla representa la idea de que, si no estás obligado a realizar una tarea, debes elegir una variable para asignar y anotar cuál fue la asignación elegida, para que puedas volver atrás si la elección no dio como resultado una asignación satisfactoria .

$${\displaystyle {\frac {\begin{array}{c}l\in {\text{Lits}}(\Phi )\;\;\;l,\neg l\notin A\end{array}}{A:=A\;\bullet \;l}}{\text{ (Decidir)}}}$$

Conflicto Si existe una cláusula contradictoria${\displaystyle \{l_{1},\dots ,l_{n}\}\in \Phi }$de tal manera que sus negaciones${\displaystyle \neg l_{1},\dots,\neg l_{n}}$están en${\displaystyle A}$, establecer la cláusula de conflicto${\displaystyle C}$a${\displaystyle \{l_{1},\dots,l_{n}\}}$Esta regla representa la detección de un conflicto cuando todos los literales en una cláusula se asignan a falso bajo la asignación actual.

$${\displaystyle {\frac {\begin{array}{c}C={\text{NINGUNO}}\;\;\;\{l_{1},\dots ,l_{n}\}\in \Phi \;\;\;\neg l_{1},\dots ,\neg l_{n}\in A\end{array}}{C:=\{l_{1},\dots ,l_{n}\}}}{\text{ (Conflicto)}}}$$

Explicar si la cláusula de conflicto${\displaystyle C}$es de la forma${\displaystyle \{l\}\cup D}$, hay una cláusula antecedente${\displaystyle \{l_{1},\dots ,l_{n},\neg l\}\in \Phi }$y${\displaystyle \neg l_{1},\dots,\neg l_{n}}$se asignan antes${\displaystyle \neg l}$en${\displaystyle A}$, luego explique el conflicto resolviéndolo${\displaystyle C}$con la cláusula antecedente. Esta regla explica el conflicto al derivar una nueva cláusula de conflicto que está implícita en la cláusula de conflicto actual y en una cláusula que provocó la asignación de un literal en la cláusula de conflicto.

$${\displaystyle {\frac {\begin{array}{c}C=\{l\}\cup D\;\;\;\{l_{1},\dots ,l_{n},\neg l\}\in \Phi \;\;\;\neg l_{1},\dots ,\neg l_{n},\neg l\in A\;\;\;\;\;\neg l_{1},\dots ,\neg l_{n}{\text{ asignado antes }}\neg l\end{array}}{C:=\{l_{1},\dots ,l_{n}\}\cup D}}{\text{ (Explicar)}}}$$

Salto hacia atrás Si la cláusula de conflicto${\displaystyle C}$es de la forma${\displaystyle \{l,l_{1},\dots,l_{n}\}}$dónde${\displaystyle {\text{lev}}(\neg l_{1})\leq \dots \leq {\text{lev}}(\neg l_{n})=i<{\text{lev}}(\neg l)}$, luego retrocede al nivel de decisión${\displaystyle i}$y asignar${\displaystyle M:=M^{[i]}\neg l}$y establecer${\displaystyle C:={\text{NONE}}}$Esta regla realiza un retroceso no cronológico al volver a un nivel de decisión implícito en la cláusula de conflicto y afirmar la negación del literal que causó el conflicto en un nivel de decisión inferior .

$${\displaystyle {\frac {\begin{array}{c}C=\{l,l_{1},\dots ,l_{n}\}\;\;\;{\text{lev}}(\neg l_{1})\leq \dots \leq {\text{lev}}(\neg l_{n})=i<{\text{lev}}(\neg l)\end{array}}{C:={\text{NONE}}\;\;\;A:=A^{[i]}\;\neg l}}{\text{ (Backjump)}}}$$

Se pueden agregar cláusulas de aprendizaje a la fórmula .${\displaystyle \Phi }$Esta regla representa el mecanismo de aprendizaje de cláusulas de los solucionadores CDCL, donde las cláusulas conflictivas se vuelven a agregar a la base de datos de cláusulas para evitar que el solucionador vuelva a cometer el mismo error en otras ramas del árbol de búsqueda.

$${\displaystyle {\frac {\begin{array}{c}C\neq {\text{NONE}}\;\;\;C\notin \Phi \end{array}}{\Phi$$ :=\Phi \cup \{C\}}}{\text{ (Aprender)}}}

Estas 6 reglas son suficientes para el CDCL básico, pero las implementaciones modernas de solucionadores SAT también suelen añadir reglas heurísticas adicionales para recorrer el espacio de búsqueda de forma más eficiente y resolver los problemas SAT más rápidamente.

Las cláusulas Forget Learned se pueden eliminar de la fórmula.${\displaystyle \Phi }$para ahorrar memoria. Esta regla representa el mecanismo de olvido de cláusulas, donde se eliminan las cláusulas aprendidas menos útiles para controlar el tamaño de la base de datos de cláusulas.${\displaystyle \Phi '\models C}$indica que la fórmula${\displaystyle \Phi '}$sin la cláusula${\displaystyle C}$aún implica${\displaystyle C}$, significado${\displaystyle C}$es redundante.$${\displaystyle {\frac {\begin{array}{c}C={\text{NONE}}\;\;\;\Phi =\Phi '\cup \{C\}\;\;\;\Phi '\models C\end{array}}{\Phi$$ :=\Phi '}}{\text{ (Olvidar)}}}

Reiniciar El solucionador se puede reiniciar restableciendo la asignación.${\displaystyle A}$a la tarea vacía${\displaystyle A^{[0]}}$y estableciendo la cláusula de conflicto${\displaystyle C}$a${\displaystyle {\text{NONE}}}$Esta regla representa el mecanismo de reinicio, que permite al solucionador salir de un espacio de búsqueda potencialmente improductivo y volver a empezar, a menudo guiado por las cláusulas aprendidas. Cabe destacar que las cláusulas aprendidas se conservan incluso después de los reinicios, lo que garantiza la finalización del algoritmo .

$${\displaystyle {\frac {\begin{array}{c}\end{array}}{A:=A^{[0]}\;\;\;C:={\text{NONE}}}}{\text{ (Restart)}}}$$

El aprendizaje de cláusulas basado en conflictos funciona de la siguiente manera.

1. Selecciona una variable y asígnale el valor Verdadero o Falso. Esto se denomina estado de decisión. Recuerda la asignación.
2. Aplicar propagación de restricciones booleanas (propagación de unidades).
3. Construye el gráfico de implicación .
4. Si existe algún conflicto:
   1. Encuentra el corte en el gráfico de implicación que condujo al conflicto.
   2. Derive una nueva cláusula que sea la negación de las asignaciones que llevaron al conflicto.
   3. Retroceda de forma no cronológica ("salto hacia atrás") al nivel de decisión apropiado, donde se asignó la primera variable involucrada en el conflicto.
5. De lo contrario, continúe desde el paso 1 hasta que se hayan asignado todos los valores a las variables.