Las estructuras de soporte de datos por satélite de búsqueda local

Question

WalkSAT y GSAT son bien conocidos y simples algoritmos de búsqueda local para resolver el satisfacibilidad booleana problema. El pseudocódigo para el algoritmo GSAT se copia de la pregunta Implementación del algoritmo de GSAT -?. ¿Cómo seleccionar el que literal para voltear y se presenta 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í voltear la variable que maximiza el número de cláusulas satisfechos. ¿Cómo se hace esto de manera eficiente? El método es ingenua para voltear cada variable y para cada paso a través de todas las cláusulas y calcular cuántos de ellos consigue satisfecho. Incluso si una cláusula podría ser consultada para satisfacibilidad en tiempo constante, el método ingenuo todavía se ejecutaría en $ O (VC) $ 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:

Muchos algoritmos de búsqueda local voltear la asignación de la variable que maximiza el número de cláusulas satisfecho. En la práctica, con lo que las estructuras de datos es apoyado esta operación eficiente?

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

Answer 1

La estructura de datos necesita es un producirse , una lista para cada variable que contiene las cláusulas de la variable se usa. Estas listas se construyen una vez, cuando el CNF es la primera lectura. Se utilizan en los pasos 3 y 5 a continuación para evitar la exploración de toda la fórmula CNF para contar cláusulas satisfechos.

Un algoritmo mejor que lanzar cada variable es:

1. Haga una lista de sólo las variables que se producen en las cláusulas no satisfechas.
2. Elija una variable $ x $ de esta lista.
3. Cuenta cuantas cláusulas que contienen $ x $ esté satisfecho.
4. $ x $ tirón.
5. Cuenta cuantas cláusulas que contienen $ x $ esté satisfecho.
6. Unflip $ x $.
7. Restar el resultado del paso 3 a partir del paso 5 y registrar por $ x $.
8. Repetir los pasos 2-7 para el resto de las variables se encontró en el paso 1.
9. Voltear la variable con el mayor número registrado en el paso 7.

A de referencia para la estructura de datos (a menudo también conocida como una lista de adyacencia) es, por ejemplo Lynce y Marques-Silva, estructuras de datos eficientes para resolver Backtracking SAT, 2004.