Supporting data structures for SAT local search

Question

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.

Answer 1

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.