Suporte a estruturas de dados para pesquisa local SAT

O WalkSAT e o GSAT são algoritmos de busca local bem conhecidos e simples para solucionar o problema de satisfação booleana. O pseudocódigo para o algoritmo GSAT é copiado da pergunta Implementando o algoritmo GSAT - Como selecionar qual literal ativar? e apresentado abaixo.

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

Aqui mostramos a variável que maximiza o número de cláusulas satisfeitas. Como isso é feito com eficiência? O método ingênuo é inverter todas as variáveis, e para cada etapa de todas as cláusulas e calcular quantas delas são satisfeitas. Mesmo que uma cláusula pudesse ser consultada quanto à satisfação em tempo constante, o método ingênuo ainda seria executado no tempo , onde V é o número de variáveis ​​e C o número de cláusulas. Tenho certeza de que podemos fazer melhor, daí a pergunta:$O(VC)$$V$$C$

Muitos algoritmos de busca local alteram a atribuição da variável que maximiza o número de cláusulas satisfeitas. Na prática, com quais estruturas de dados essa operação é suportada com eficiência?

Isso é algo que eu sinto que os livros freqüentemente omitem. Um exemplo é até o famoso livro de Russell & Norvig .

A estrutura de dados necessária é uma lista de ocorrências , uma lista para cada variável que contém as cláusulas em que a variável ocorre. Essas listas são criadas uma vez, quando o CNF é lido pela primeira vez. Eles são usados ​​nas etapas 3 e 5 abaixo para evitar a varredura de toda a fórmula CNF para contar cláusulas satisfeitas.

Um algoritmo melhor do que inverter todas as variáveis ​​é:

1. Faça uma lista apenas das variáveis ​​que ocorrem nas cláusulas não satisfeitas.
2. $x$
3. $x$
4. $x$
5. $x$
6. $x$
7. $x$
8. Repita as etapas 2 a 7 para o restante das variáveis ​​encontradas na etapa 1.
9. Inverta a variável com o número mais alto registrado na etapa 7.

Uma referência para a estrutura de dados (geralmente também conhecida como lista de adjacência) é, por exemplo, Lynce e Marques-Silva, Estruturas de Dados Eficientes para Solucionadores de Backtracking SAT, 2004.