## 1. IntroductionThe propositional satisfiability problem (often called SAT) is the problem of determining whether a set of sentences in Propositional Logic is satisfiable. The problem is significant both because the question of satisfiability is important in its own right and because many other questions in Propositional Logic can be reduced to that of propositional satisfiability. In practice, many automated reasoning problems in Propositional Logic are first reduced to satisfiability problems and then by using a satisfiability solver. Today, SAT solvers are commonly used in hardware design, software analysis, planning, mathematics, security analysis, and many other areas. In the chapter, we look at several basic methods for solving SAT problems. We begin with a review of the Truth Table Method. We then introduce the Backtracking Approach, and we show how it can be improved with Simplification and Unit Propagation. We briefly mention the popular DPLL method. Finally, we talk about non-guaranteed methods, with emphasis on one particular method, called GSAT. ## 2. Truth Table MethodLet Δ = {
There is one row for each possible truth assignment. For each truth assignment, each of the sentences in Δ is evaluated. If any sentence evaluates to 0, then Δ as a whole is not satisfied by the truth assignment. If a satisfying truth assignment is found, then Δ is determined to be satisfiable. If no satisfying truth assignment is found, then Δ is unsatisfiable. In this example, every row ends with Δ not satisfied. So the truth table method concludes that Δ is unsatisfiable. The truth table method is complete because every truth assignment is checked. However, the method is impractical for all but very small problem instances. In our example with 3 propositions, there are 2 ## 3. BacktrackingLooking at the example in the preceding section, we can observe that, often times, a partial truth assignment is all that is required to determine whether the input Δ is satisfied. For example, let's consider the partial assignment { To search the space of truth assignments systematically, both partial and complete, we can set the propositions one at a time. The process can be visualized as a tree search where each branch sets the truth value of a single proposition, each interior node is a partial truth assignment, and each leaf node is a complete truth assignment. Below is a tree whose fringe represents all complete truth assignments. In basic backtracking search, we start at the root of the tree (the empty assignment where nothing is known) and work our way down a branch. At each node, we check whether the input Δ is satisfied. If Δ is satisfied, we move down the branch by choosing a truth value for a currently unassigned proposition. If Δ is falsified, then, knowing that all the (partial) truth assignments further down the branch also falsify Δ, we Let's look at an example. At each step, we show the part of the tree explored so far. A boxed node is the current node. An × mark at a node indicates that the truth assignment at that node falsifies at least one sentence in Δ. A ✓ indicates that the truth assignment at that node satisfies all the sentences in Δ. A ? indicates that the partial truth assignment at the node neither satisfies nor falsifies Δ. Let's start with the assumption that Now, let's assume that Since the current branch is closed, we backtrack to the most recent choice point where another branch can be taken. This time, let's assume that Again, Δ is falsified, and the current branch is closed. Again we backtrack to the most recent choice point where another branch can be taken. Let Let Again, our sentences are falsified, and we backtrack. Let Let Our sentences are falsified by this assignment, and we backtrack one last time. Let Once again, our sentences are falsified. Since all branches have been explored and closed, the method determines that Δ is unsatisfiable. Looking at the full search tree compared to the portion explored by the basic backtracking search, we can see that the greyed out subtrees are all pruned from the search space. In this particular example, the savings are not spectacular. But in a bigger example with more propositions, the pruned subtrees can be much bigger. ## 4. Simplification and Unit PropagationIn this section, we consider two optimizations of basic backtracking search - Suppose, for example, a proposition If a proposition Consider once again the example in the preceding section. Under the partial assignment
While simplifying sentences is helpful in and of itself, the real value of simplification is that it enables a further optimization that can drastically decrease the search space. In the course of the backtracking search, if we see a sentence that consists of single atom, say Let's redo example 1 with formula simplification and unit propagation. As we proceed through this example, we illustrate each step with the search tree on that step (on the left) and the simplified sentence set (in the table on the right). To start, let
In the simplified set of sentences, we have the unit ¬
Δ is falsified, so we backtrack to the most recent decision point, all the way back at the root. Let
In the simplified set of sentences, we have the unit
In the simplified set of sentences, we have the unit ¬
Δ is falsified on this branch, so the branch is closed. All branches are closed, so the method determines that Δ is unsatisfiable. Compared to the tree explored by the basic backtracking search, we see that the greyed out subtrees are pruned away from the search space. ## 5. DPLLThe ## 6. GSATMany practical SAT solvers based on complete search for models are routinely used to solve satisfiability problems of significant size. However, some problem instances are still impractical to solve using complete search for models. In these problem instances, it is impractical to exhaustively eliminate every truth assignment as a possible model. In such situations, one may consider incomplete search methods - methods that answer correctly when they can but sometimes fail to answer. The basic idea is to sample a subset of truth assignments. If a satisfying assignment is found, then we can conclude that the input is satisfiable. If no satisfying assignment is found, then we don't know whether the input is satisfiable. In practice, modern incomplete SAT solvers tend to be very good at finding the satisfying assignments in a reasonable amount of time when they exist, but they still lack the ability to answer definitively that an input is unsatisfiable. The first idea may be to uniformly sample a number of truth assignments from the space of all truth assignments. However, in large problem instances for with few satisfying assignments, one would expect to take a very long time before happening upon a satisfying assignment. What enables incomplete SAT solvers to work efficiently is the use of heuristics that frequently steer the search toward satisfying assignments. One family of incomplete SAT solvers uses local search heuristics to look for a truth assignment that maximizes the number of sentences it satisfies. Clearly, a set of sentences is satisfiable if and only if it is satisfied by an optimal truth assignment (optimal in terms of maximizing the number of sentences satisfied). We look at one particular method called GSAT in more detail. The GSAT method starts with an arbitrary truth assignment. Then GSAT moves from one truth assignment to the next by flipping one of the propositions to achieve the greatest increase in the number of sentences satisfied. The search stops when it reaches a truth assignment such that the number of sentences satisfied cannot be increased by flipping the truth value of one proposition (in other words, a locally optimal point is reached). Consider the set of sentences {
Only one sentence is satisfied by this assignment. However, we can improve matters by flipping the value of
Still not satisfied, but we can improve matters by flipping the value of
Unfortunately, at this point, we are stuck. No flipping of a single proposition value can increase the number of sentences satisfied. The search terminates, suggesting that the our sentences are unsatisfiable. Now, let's see what happens when we apply the method to a set or sentences that is satisfiable. Our set in this case is {
Flipping the value of
Flipping the value of
Since all three sentences are satisfied, the set as a whole is satisfied. The search terminates, concluding that the set is satisfiable. Unfortunately, local search of this sort is not guaranteed to be complete - the search may terminate without finding a satisfying assignment even though one exists. Depending on the starting assignment and the arbitrary choices in breaking ties between flipping one proposition vs another, the GSAT method may incorrectly conclude a set of sentences is unsatisfiable. To see how this can cause problems, let's look a different execution of GSAT on the same set of sentences as above. We begin with the same initial assignment as before.
This time, instead of flipping the value of
Unfortunately, at this point, we are stuck. No flipping of a proposition value can increase the number of sentences satisfied. Although a satisfying assignment exists, the search terminates without finding it. To avoid becoming stuck at a locally optimal point that is not globally optimal, one can modify the search procedure by allowing some combination of the following. - Restarting at a random truth assignment (randomized restarts).
- Flipping a proposition to move to a truth assignment that satisfies the same number of sentences (plateau moves).
- Flipping a random proposition regardless of whether the move increases the number of satisfied sentences (noisy move).
Active research and engineering efforts continue in developing search methods that can find a satisfying assignment more quickly (when one exists). ## RecapThe |