Boolean satisfiability algorithm heuristics

In computer science, there are certain classes of algorithms (heuristics) that solves types of the Boolean satisfiability problem despite there being no known efficient algorithm in the general case.

Overview

The Boolean satisfiability (or SAT) problem can be stated formally as: given a Boolean expression $B$ with $V=\{v_{0},\ldots ,v_{n}\}$ variables, finding an assignment $V^{*}$ of the variables such that $B(V^{*})$ is true. It is seen as the canonical NP-complete problem. Although no known algorithm is known to solve SAT in polynomial time, there are classes of SAT problems which do have efficient algorithms that solve them.

The classes of problems amenable to SAT heuristics arise from many practical problems in AI planning, circuit testing, and software verification. Research on constructing efficient SAT solvers has been based on various principles such as resolution, search, local search and random walk, binary decisions, and Stalmarck's algorithm. Some of these algorithms are deterministic, while others may be stochastic.

As there exist polynomial-time algorithms to convert any Boolean expression to conjunctive normal form such as Tseitin's algorithm, posing SAT problems in CNF does not change their computational difficulty. SAT problems are canonically expressed in CNF because CNF has certain properties that can help prune the search space and speed up the search process.

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

Heuristics such as 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.

Variable State Independent Decaying Sum

An influential 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

For MAX-SAT, the version of SAT in which the number of satisfied clauses is maximized, solvers also use probabilistic algorithms. If we are given a Boolean expression $B$, with $V=\{v_{0},\ldots ,v_{n}\}$ variables and we set each variable randomly, then each clause $c$, with $|c|$ variables, then the chance of $B$ being satisfied by a particular variable assignment is

Pr($c$ is satisfied) = $1-2^{-|c|}$.

This is because each variable in $c$ has probability ⁠1/2⁠ of being satisfied, and we only need one variable in $c$ to be satisfied. This works for all $|c|\geq 1$, so

Pr($c$ is satisfied) = $1-2^{-|c|}\geq {\frac {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

$\delta _{ij}={\begin{cases}0&{\text{if }}c_{i}{\text{ is satisfied}},\\1&{\text{if }}c_{i}{\text{ is not satisfied}}.\end{cases}}$

then we have that

${\begin{aligned}E[{\text{Num Clauses Satisfied}}]&=\sum _{i}E[\delta _{i}]=\sum _{i}1-2^{-|c_{i}|}\\&\geq \sum _{i}{\frac {1}{2}}={\frac {1}{2}}|i|={\frac {1}{2}}OPT\end{aligned}}$

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.

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 stochastic probabilistic solvers can also be used to find optimal approximations for Max-SAT.

Variable splitting

Main article: 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\lor b\lor c)\wedge (\neg a\lor e\lor \neg b)\wedge (a\lor \neg c\lor f)$ will become: $B^{*}=(a\lor b\lor c)\wedge (\neg a_{1}\lor e\lor \neg b)\wedge (a_{2}\lor \neg c\lor f)$, with $a,a_{1},a_{2},\ldots ,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.