[Solved]: Supporting data structures for SAT local search

Problem Detail: 

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.

Asked By : Juho

Answered By : Kyle Jones

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.

Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/1058