Estructuras de datos de soporte para búsqueda local SAT

WalkSAT y GSAT son algoritmos de búsqueda locales bien conocidos y simples para resolver el problema de satisfacción booleana. El pseudocódigo para el algoritmo GSAT se copia de la pregunta Implementación del algoritmo GSAT: ¿cómo seleccionar qué literal voltear? y presentado a continuación.

procedure GSAT(A,Max_Tries,Max_Flips)
  A: is a CNF formula
  for i:=1 to Max_Tries do
    S <- instantiation of variables
    for j:=1 to Max_Iter do
      if A satisfiable by S then
        return S
      endif
      V <- the variable whose flip yield the most important raise in the number of satisfied clauses;
      S <- S with V flipped;
    endfor
  endfor
  return the best instantiation found
end GSAT

Aquí volteamos la variable que maximiza el número de cláusulas satisfechas. ¿Cómo se hace esto de manera eficiente? El método ingenuo es voltear cada variable, y para cada paso a través de todas las cláusulas y calcular cuántas de ellas quedan satisfechas. Incluso si se pudiera consultar la satisfacción de una cláusula en tiempo constante, el método ingenuo seguiría ejecutándose en tiempo , donde V es el número de variables y C el número de cláusulas. Estoy seguro de que podemos hacerlo mejor, de ahí la pregunta:$O(VC)$$V$$C$

Muchos algoritmos de búsqueda locales cambian la asignación de la variable que maximiza el número de cláusulas satisfechas. En la práctica, ¿con qué estructuras de datos se respalda esta operación de manera eficiente?

Esto es algo que siento que los libros de texto a menudo omiten. Un ejemplo es incluso el famoso libro de Russell y Norvig .

La estructura de datos necesaria es una lista de ocurrencia , una lista para cada variable que contiene las cláusulas en las que aparece la variable. Estas listas se crean una vez, cuando se lee el CNF por primera vez. Se utilizan en los pasos 3 y 5 a continuación para evitar escanear toda la fórmula CNF para contar cláusulas satisfechas.

Un mejor algoritmo que voltear cada variable es:

1. Haga una lista de solo las variables que ocurren en las cláusulas insatisfechas.
2. $x$
3. $x$
4. $x$
5. $x$
6. $x$
7. $x$
8. Repita los pasos 2-7 para el resto de las variables encontradas en el paso 1.
9. Voltee la variable con el número más alto registrado en el paso 7.

Una referencia para la estructura de datos (a menudo también conocida como una lista de adyacencia) es, por ejemplo, Lynce y Marques-Silva, Efficient Data Structures for Backtracking SAT soluvers, 2004.