Prise en charge des structures de données pour la recherche locale SAT

WalkSAT et GSAT sont des algorithmes de recherche locale simples et bien connus pour résoudre le problème de satisfiabilité booléenne. Le pseudocode de l'algorithme GSAT est copié de la question Mise en œuvre de l'algorithme GSAT - Comment sélectionner le littéral à retourner? et présenté ci-dessous.

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

Ici, nous inversons la variable qui maximise le nombre de clauses satisfaites. Comment cela se fait-il efficacement? La méthode naïve consiste à retourner chaque variable et à chaque étape à travers toutes les clauses et à calculer combien d'entre elles sont satisfaites. Même si une clause pouvait être interrogée pour la satisfiabilité en temps constant, la méthode naïve s'exécuterait toujours en temps , où est le nombre de variables et le nombre de clauses. Je suis sûr que nous pouvons faire mieux, d'où la question:$O(VC)$$V$$C$

De nombreux algorithmes de recherche locaux inversent l'affectation de la variable qui maximise le nombre de clauses satisfaites. Dans la pratique, avec quelles structures de données cette opération est-elle prise en charge efficacement?

C'est quelque chose que je pense que les manuels scolaires omettent souvent. Un exemple est même le célèbre livre Russell & Norvig .

La structure de données nécessaire est une liste d'occurrences , une liste pour chaque variable contenant les clauses dans lesquelles la variable se produit. Ces listes sont construites une fois, lors de la première lecture du CNF. Ils sont utilisés dans les étapes 3 et 5 ci-dessous pour éviter de parcourir toute la formule CNF pour compter les clauses satisfaites.

Un meilleur algorithme que de retourner chaque variable est:

1. Faites une liste des seules variables présentes dans les clauses non satisfaites.
2. $x$
3. $x$
4. $x$
5. $x$
6. $x$
7. $x$
8. Répétez les étapes 2 à 7 pour le reste des variables trouvées à l'étape 1.
9. Retournez la variable avec le nombre le plus élevé enregistré à l'étape 7.

Une référence pour la structure de données (souvent également connue sous le nom de liste d'adjacence) est par exemple Lynce et Marques-Silva, Efficient Data Structures for Backtracking SAT solvers, 2004.