Boolean satisfiability algorithm heuristics

Branching heuristics in conflict-driven algorithms

One of the cornerstone Conflict-Driven Clause Learning SAT solver algorithms is the DPLL algorithm. The algorithm works by iteratively assigning free variables, and when the algorithm encounters a bad assignment, then it backtracks to a previous iteration and chooses a different assignment of variables. It relies on a Branching Heuristic to pick the next free variable assignment; the branching algorithm effectively makes choosing the variable assignment into a decision tree. Different implementations of this heuristic produce markedly different decision trees, and thus have significant effect on the efficiency of the solver.

Early branching Heuristics (Bohm's Heuristic, Maximum Occurrences on Minimum sized clauses heuristic, and Jeroslow-Wang heuristic) can be regarded as greedy algorithms. Their basic premise is to choose a free variable assignment that will satisfy the most already unsatisfied clauses in the Boolean expression. However, as Boolean expressions get larger, more complicated, or more structured, these heuristics fail to capture useful information about these problems that could improve efficiency; they often get stuck in local maxima or do not consider the distribution of variables. Additionally, larger problems require more processing, as the operation of counting free variables in unsatisfied clauses dominates the run-time.

Another heuristic called Variable State Independent Decaying Sum (VSIDS) attempts to score each variable. VSIDS starts by looking at small portions of the Boolean expression and assigning each phase of a variable (a variable and its negated complement) a score proportional to the number of clauses that variable phase is in. As VSIDS progresses and searches more parts of the Boolean expression, periodically, all scores are divided by a constant. This discounts the effect of the presence of variables in earlier-found clauses in favor of variables with a greater presence in more recent clauses. VSIDS will select the variable phase with the highest score to determine where to branch.

VSIDS is quite effective because the scores of variable phases is independent of the current variable assignment, so backtracking is much easier. Further, VSIDS guarantees that each variable assignment satisfies the greatest number of recently searched segments of the Boolean expression.

Stochastic solvers

MAX-SAT (the version of SAT in which the number of satisfied clauses is maximized) solvers can also be solved using probabilistic algorithms. If we are given a Boolean expression B , with V = { v 0 , … , v n } variables and we set each variable randomly, then each clause c , with | c | variables, has a chance of being satisfied by a particular variable assignment Pr( c is satisfied) = 1 − 2 − | c | . This is because each variable in c has 1 2 probability of being satisfied, and we only need one variable in c to be satisfied. This works ∀   | c | ≥ 1 , so Pr( c is satisfied) = 1 − 2 − | c | ≥ 1 2 .

Now we show that randomly assigning variable values is a 1 2 -approximation algorithm, which means that is an optimal approximation algorithm unless P = NP. Suppose we are given a Boolean expression B = { c i } i = 1 n and

This algorithm cannot be further optimized by the PCP theorem unless P = NP.

Other Stochastic SAT solvers, such as WalkSAT and GSAT are an improvement to the above procedure. They start by randomly assigning values to each variable and then traverse the given Boolean expression to identify which variables to flip to minimize the number of unsatisfied clauses. They may randomly select a variable to flip or select a new random variable assignment to escape local maxima, much like a simulated annealing algorithm.

2-SAT heuristics

Unlike general SAT problems, 2-SAT problems are tractable. There exist algorithms that can compute the satisfiability of a 2-SAT problem in polynomial time. This is a result of the constraint that each clause has only two variables, so when an algorithm sets a variable v i , the satisfaction of clauses, which contain v i but are not satisfied by that variable assignment, depend on the satisfaction of the second variable in those clauses, which leaves only one possible assignment for those variables.

Backtracking

Suppose we are given a Boolean expressions:

With B 1 , the algorithm can select v 1 = true , so to satisfy the second clause, the algorithm will need to set v 3 = false , and resultantly to satisfy the first clause, the algorithm will set v 2 = false .

If the algorithm tries to satisfy B 2 in the same way it tried to solve B 1 , then the third clause will remain unsatisfied. This will cause the algorithm to backtrack and set v 1 = false and continue assigning variables further.

Graph reduction

2-SAT problems can also be reduced to running a depth-first search on a strongly connected components of a graph. Each variable phase (a variable and its negated complement) is connected to other variable phases based on implications. In the same way when the algorithm above tried to solve

However, when the algorithm tried solve

which is a contradiction.

Once a 2-SAT problem is reduced to a graph, then if a depth first search finds a strongly connected component with both phases of a variable, then the 2-SAT problem is not satisfiable. Likewise, if the depth first search does not find a strongly connected component with both phases of a variable, then the 2-SAT problem is satisfiable.

Weighted SAT problems

Numerous weighted SAT problems exist as the optimization versions of the general SAT problem. In this class of problems, each clause in a CNF Boolean expression is given a weight. The objective is the maximize or minimize the total sum of the weights of the satisfied clauses given a Boolean expression. weighted Max-SAT is the maximization version of this problem, and Max-SAT is an instance of weighted MAX-SAT problem where the weights of each clause are the same. The partial Max-SAT problem is the problem where some clauses necessarily must be satisfied (hard clauses) and the sum total of weights of the rest of the clauses (soft clauses) are to be maximized or minimized, depending on the problem. Partial Max-SAT represents an intermediary between Max-SAT (all clauses are soft) and SAT (all clauses are hard).

Note that the stochasitic probabilistic solvers can also be used to find optimal approximations for Max-SAT.

Variable splitting

Variable splitting is a tool to find upper and lower bounds on a Max-SAT problem. It involves splitting a variable a into new variables for all but once occurrence of a in the original Boolean expression. For example, given the Boolean expression: B = ( a ∨ b ∨ c ) ∧ ( ¬ a ∨ e ∨ ¬ b ) ∧ ( a ∨ ¬ c ∨ f ) will become: B ∗ = ( a ∨ b ∨ c ) ∧ ( ¬ a 1 ∨ e ∨ ¬ b ) ∧ ( a 2 ∨ ¬ c ∨ f ) , with a , a 1 , a 2 , … , a n being all distinct variables.

This relaxes the problem by introducing new variables into the Boolean expression, which has the effect of removing many of the constraints in the expression. Because any assignment of variables in B can be represented by an assignment of variables in B ∗ , the minimization and maximization of the weights of B ∗ represent lower and upper bounds on the minimization and maximization of the weights of B .

Partial Max-SAT

Partial Max-SAT can be solved by first considering all of the hard clauses and solving them as an instance of SAT. The total maximum (or minimum) weight of the soft clauses can be evaluated given the variable assignment necessary to satisfy the hard clauses and trying to optimize the free variables (the variables that the satisfaction of the hard clauses does not depend on). The latter step is an implementation of Max-SAT given some pre-defined variables. Of course, different variable assignments that satisfy the hard clauses might have different optimal free variable assignments, so it is necessary to check different hard clause satisfaction variable assignments.

Data structures for storing clauses

As SAT solvers and practical SAT problems (e.g. circuit verification) get more advanced, the Boolean expressions of interest may exceed millions of variables with several million clauses; therefore, efficient data structures to store and evaluate the clauses must be used.

Expressions can be stored as a list of clauses, where each clause is a list of variables, much like an adjacency list. Though these data structures are convenient for manipulation (adding elements, deleting elements, etc.), they rely on many pointers, which increases their memory overhead, decreases cache locality, and increases cache misses, which renders them impractical for problems with large clause counts and large clause sizes.

When clause sizes are large, more efficient analogous implementations include storing expressions as a list of clauses, where each clause is represented as a matrix that represents the clauses and the variables present in that clause, much like an adjacency matrix. The elimination of pointers and the contiguous memory occupation of arrays serve to decrease memory usage and increase cache locality and cache hits, which offers a run-time speed up compared to the aforesaid implementation.