Soutenir les structures de données pour la recherche locale SAT

Question

Walksat et GSAT sont bien connus et simples algorithmes de recherche locale pour résoudre la satisfiabilité booléenne problème. Le pseudo-code de l'algorithme GSAT est copié de la question Mettre en œuvre 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

nous retourner ici la variable qui maximise le nombre de clauses satisfaites. Comment cela se fait efficacement? La méthode naïve est de retourner toutes les variables, et pour chaque étape à travers toutes les clauses et calculer combien d'entre eux se satisfait. Même si une clause pourrait être interrogé pour satisfiability en temps constant, la méthode naïve serait encore courir en $ O (VC) $ temps, où $ V $ est le nombre de variables et le nombre de clauses $ $ C. Je suis sûr que nous pouvons faire mieux, d'où la question:

  

De nombreux algorithmes de recherche locale renversent l'affectation de la variable qui maximise le nombre de clauses satisfaites. Dans la pratique, avec ce que les structures de données est cette opération pris en charge efficacement?

Ceci est quelque chose que je me sens comme les manuels omettent souvent. Un exemple est même le célèbre livre Russell & Norvig .

Answer 1

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

Un meilleur algorithme que retournement chaque variable est:

1. Faites une liste des seules variables qui se produisent dans les clauses non satisfaites.
2. Choisir une variable $ x $ de cette liste.
3. Comptez combien de clauses qui contiennent sont satisfaits $ x $.
4. Renverser $ x $.
5. Comptez combien de clauses qui contiennent sont satisfaits $ x $.
6. Unflip $ x $.
7. Soustraire le résultat de l'étape 3 de l'étape 5 et enregistrer pour $ x $.
8. Répéter les étapes 2 à 7 pour le reste des variables trouvé à l'étape 1.
9. flip la variable avec le nombre le plus élevé enregistré à l'étape 7.

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