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

20

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)VC

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 .

Juho
la source
Eh bien, ces gars-là le construisent en matériel. Apparemment , les approches probabilistes et heuristiques sont plus populaires; cela donnerait à penser que l'on ne peut en effet pas choisir rapidement la "meilleure" variable (ce n'est que gourmand, après tout), ou que ce choix n'est pas bon en général.
Raphael
@Raphael Vous avez peut-être raison de ne pas pouvoir le choisir très rapidement, mais je n'oserais pas dire "le choix n'est pas bon en général". J'ai peut-être mal compris votre point, mais je suis presque sûr que le choix de la «bonne» variable a un impact énorme. Merci, je vais creuser un peu plus. Je pense que l'un des auteurs des diapositives que vous avez liées (Hoos) a un livre sur le sujet.
Juho
La «bonne» serait optimale, mais y a-t-il des raisons de croire que celle qui maximise maintenant est la bonne? Après tout, le problème n'est pas résolu par les gourmands (canoniques).
Raphael

Réponses:

9

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.

Kyle Jones
la source