La mise en œuvre de l'algorithme GSAT - Comment sélectionner le littéral de retourner?

Question

L'algorithme GSAT est, pour la plupart, tout droit: vous obtenez une formule sous forme normale conjonctive et retourner les littéraux des clauses jusqu'à trouver une solution qui répond à la formule ou vous atteignez les max_tries / max_flips limite et trouver pas de solution.

Je suis en œuvre l'algorithme suivant:

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

Je ne parviens pas interpréter la ligne suivante:

V <- the variable whose flip yield the most important raise in the number of satisfied clauses;

est-ce pas le nombre maximum de clauses satisfaites ce que nous recherchons? Il me semble que nous essayons d'utiliser la solution ou des approximations pour trouver la solution.

J'ai pensé à des façons de le faire, mais il serait bon d'entendre d'autres points de vue (L'hypothèse est qu'une fois que la variable est retournée une fois qu'il est sélectionné.):

• Générer un espace d'état avec tous les retournements possibles et la recherche de l'espace pour un littéral que les résultats dans la meilleure approximation de l'état de but.
• sélectionnez la variable au hasard, je vais retourner en commençant par les
littéraux qui sont plus fréquentes.
• Choisissez un littéral aléatoire.

Answer 1

  

est-ce pas le nombre maximum de clauses satisfaites ce que nous recherchons?

Oui, nous sommes à la recherche d'une mission qui satisfait le nombre maximum de clauses (qui tous, de préférence). Et à cette fin, nous nous demandons « Quelle variable unique nous apportera le plus proche de cet objectif en retournant? » puis retournez.

  

Il me semble que nous essayons d'utiliser la solution ou des approximations pour trouver la solution.

En utilisant la solution serait si nous avons demandé « Quelle combinaison de multiples flips donnerait le meilleur résultat? » ou simplement « Quelle mission serait le meilleur? ». Mais ce ne est pas ce que nous faisons, nous ne recherche un pas en avant. En utilisant une approximation de la solution semble être une description précise. Cependant, il est faux de rien avec ça. C'est comment fonctionnent les stratégies cupides.

  

Générer un espace d'état avec tous les retournements possibles et la recherche de l'espace pour un littéral que les résultats dans la meilleure approximation de l'état de but.

Droit.