19
$\begingroup$

WalkSAT and GSAT are well-known and simple local search algorithms for solving the Boolean satisfiability problem. The pseudocode for the GSAT algorithm is copied from the question Implementing the GSAT algorithm - How to select which literal to flip? and presented below.

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

Here we flip the variable that maximizes the number of satisfied clauses. How is this done efficiently? The naive method is to flip every variable, and for each step through all clauses and calculate how many of them get satisfied. Even if a clause could be queried for satisfiability in constant time, the naive method would still run in $O(VC)$ time, where $V$ is the number of variables and $C$ the number of clauses. I'm sure we can do better, hence the question:

Many local search algorithms flip the variable's assignment that maximizes the number of satisfied clauses. In practice, with what data structures is this operation supported efficiently?

This is something I feel like textbooks often omit. One example is even the famous Russell & Norvig book.

$\endgroup$
  • $\begingroup$ Well, these guys build it in hardware. Apparently, probabilistic and heuristic approaches are more popular; that would suggest that you can indeed not choose the "best" (it is only greedy, after all) variable quickly, or that this choice is no good in general. $\endgroup$ – Raphael Apr 6 '12 at 11:15
  • $\begingroup$ @Raphael Maybe you are right that one cannot choose it very quickly, but I wouldn't dare to say "the choice is no good in general". Maybe I misunderstood your point, but I'm pretty sure choosing the "right" variable has a huge impact. Thanks, I'll dig in a little deeper. I think one of the authors of the slides you linked (Hoos) has a book on the subject. $\endgroup$ – Juho Apr 6 '12 at 20:35
  • $\begingroup$ The "right" one would be optimal, but is there reason to believe that the one that maximises now is the right one? After all, the problem is not solvable by (canonical) greedy. $\endgroup$ – Raphael Apr 6 '12 at 21:06
9
$\begingroup$

The needed data structure is an occur list, a list for each variable containing the clauses the variable occurs in. These lists are built once, when the CNF is first read. They are used in steps 3 and 5 below to avoid scanning the whole CNF formula to count satisfied clauses.

A better algorithm than flipping every variable is:

  1. Make a list of only the variables that occur in the unsatisfied clauses.
  2. Choose a variable $x$ from this list.
  3. Count how many clauses that contain $x$ are satisfied.
  4. Flip $x$.
  5. Count how many clauses that contain $x$ are satisfied.
  6. Unflip $x$.
  7. Subtract the result of step 3 from step 5 and record it for $x$.
  8. Repeat steps 2-7 for the rest of the variables found in step 1.
  9. Flip the variable with the highest number recorded in step 7.

A reference for the data structure (often also known as an adjacency list) is for example Lynce and Marques-Silva, Efficient Data Structures for Backtracking SAT solvers, 2004.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.