The organization of this dissertation is as follows.
Chapter2 will be concerned with sound and complete SAT algorithms that are guaranteed to terminate with a correct decision on the satisfiability/unsatisfiability of a given CNF formula. We will start by describing the classical Davis-Putnam-Logemann-Loveland (DPLL) algorithm. Afterwards, an interplay between search and inference will be explicated, and we will summarize the organization of modern conflict-driven clause learning (CDCL) solver.
Chapter 3 will pitch our new thought of two efficient implementations for im-proving the current state-of-the-art CDCL solver. One focus on the special strategy of pure literal elimination which is regarded as another deduction engine of SAT al-gorithms, besides unit propagation. The other enhances the management of learning and deleting conflict-driven clauses by a breadth-extended approach. Both of these two implementation were introduced into our submission solvers that participated in the recent SAT competitions.
In Chapter4, we will discusses the encoding of pseudo-Boolean (PB) constraints in the context of a linear search satisfiability-based solver for maximum satisfiability (MaxSAT). We will present several CNF encodings of PB constraints for weighted partial MaxSAT and provide detailed proofs of the correctness for all our encodings.
Ann-level modulo totalizer, which is the newest of them, applies multiple modular arithmetic in a mixed radix base and only generates auxiliary variables for each unique combination of weights. Significantly, this encoding always produces a polynomial-size CNF in the number of input variables.
In Chapter5, we will study the coalition structure generation (CSG) problem for partition function games (PFGs) which are coalitional games with externalities.
In PFGs, each value of a coalition depends on how the other agents are partitioned.
We propose and benchmark two methods to solve CSG problem for PFGs, concisely represented by partition decision trees (PDTs). One is a depth-first branch-and-bound (DFBnB) algorithm for modified PDTs, called the MPDT algorithm, and the other is MaxSAT encoding and leaves the rest manipulation to MaxSAT solver.
Finally, Chapter6 will contain a summary of this dissertation and discussion of some future research directions that may be worth exploring.
4 http://www.claymath.org/millennium-problems/p-vs-np-problem
15
Chapter 2
SAT Algorithms
This chapter is concerned with sound1 and complete algorithms for testing satisfia-bility, i.e., algorithms that are guaranteed to terminate with a correct decision on the satisfiability/unsatisfiability of given CNF F. One can distinguish between a few approaches on which complete satisfiability algorithms have been based.
The first approach is based onexistential quantification, where one equisatisfiably eliminates variables from the F which is applied to having come from a prenex form with its clauses grounded inresolution inference rule. The Davis-Putnam (DP) algorithm [25], reduced the size of the search space considerably by this approach.
This was done by repeatedly choosing a target variable xi still appearing in the expression, applying all possible ground resolutions on xi, then eliminating all remaining clauses still containingxi or¬xi. When all variables have been eliminated, the satisfiability test is then reduced into a simple test on a trivial CNF (F =∅).
The second approach is based on systematic search in the space of truth as-signments. Loveland and Logemann attempted to implement DP but they found that ground resolution used too much random access memory (RAM), which was quite limited in those days. So they changed the way variables are eliminated by employing the splitting rule: recursively assigning values 0 and 1 to a variable and solving both resulting subproblems [24]. Their algorithm is, of course, the familiar Davis-Putnam-Logemann-Loveland (DPLL), which is marked by its modest space requirements.
The last approach is based on combining search and inference, leading to algo-rithms that currently underly most modern complete SAT solvers—conflict-driven clause learning (CDCL). Besides using DPLL, implementing a state-of-the-art CDCL
SAT solver involves a number of additional key techniques:
• Learning new clauses from conflicts during backtrack search [65].
• Exploiting structure of conflicts during clause learning [65].
• Using lazy data structures for the representation of formulae [55].
• Branching heuristics must have low computational overhead, and must receive feedback from backtrack search [55].
1 A valid argument whose premises are tautology is said to be sound.
• Periodically restarting backtrack search [33].
• Deletion strategies and policies for learnt clauses [32].
We start in the next section by describing the classical DPLL algorithm. After-wards, Section2.2 explicates an interplay between search and inference and Section 2.3summarizes the organization of modern CDCL solvers.
2.1 The DPLL Algorithm
The DPLL algorithm [24] is based on systematic search in the space of truth assignments which was developed in response to the challenges posed by the space requirements of the DP algorithm [25].
x1
1 0
x2
1 0
x3
1 0
A1 A2
x3
1 0
A3 A4
x2
1 0
x3
1 0
A5 A6
x3
1 0
A7 A8 Level 0
Level 1 Level 2
2n possible truth assignments
depth:
n= log2(8)
Figure 2.1. A search tree of enumerating all truth assignments over Boolean variablesx1, x2 andx3in decision variable order−−−−→x1x2x3 which corresponds the decision levels from top to bottom in the leftmost of figure.
Figure 2.1 depicts a search tree that enumerates the truth assignments over Boolean variablesX ={x1, x2, x3}indecision variable order−−−−→x1x2x3. Decision levels (starting from level 0) of each assignment reflects this order. The observation about this tree is that it essentially is ann-depthcomplete binary tree, wheren=|X|, i.e., the number of variables, and its leaves are in one-to-one correspondence with the truth assignments under consideration. Hence, testing satisfiability can be viewed as a process of searching for a leaf node that satisfies the given CNF. Obviously, a brute-force search for all possible assignments is in O(2n). The decision level associated with variables used for branching steps (i.e., decision assignments) is specified by the search process, and denotes the current depth of the decision stack.
A DPLL explores the tree using depth-first-search algorithm, which incorporates unit propagation (UP), also calledunit resolution. Given our notational conventions in Definition 1, a CNF F is satif F =∅. Moreover, F is unsatif ∈ F. These two properties correspond to common boundary conditions that arise in recursive algorithms on CNF. In general, a CNF F is said to imply another CNF Γ, denoted F |= Γ, iff every assignment that satisfies F also satisfies Γ. Note that if a clauseCi
is a subset of another clause Cj,Ci ⊆Cj, then Ci |=Cj. We say in this case that clause Ci subsumes clause Cj, as there is no need to have clause Cj in a CNF that also includes clause Ci. One important fact based on this discussion is that F is intrinsically unsatifF |=.
2.1 The DPLL Algorithm 17
2.1.1 Unit propagation
Example 6. Consider the following CNF:
F = (x1∨x2∨x3)∧(¬x1∨ ¬x3)∧(¬x2∨x3)
Consider also the node at Level 1 on the left branch as shown in Figure2.1, which results from assignmentA(x1) = 1, and we have:
A(F) = (¬x3)∧(¬x2∨x3) (2.1) Currently, F is neither empty (∅), nor includes the empty clause (). Therefore, we cannot yet declare early success (sat) or early failure (unsat), which is why a brute-force algorithm continues searching below Level 1.
However, that by employing UP, we can indeed declare success and end the search at this node. Firstly, we close F under UP and collect all unit clauses2 in F. Then we assume that literals are assigned to 1 to satisfy these unit clauses.
Lastly, we simplify F given these assignments and check for either that all clauses are subsumed or that the empty clause is derived.
To incorporate UP into DPLL algorithm, we introduce a function UnitPropa-gate, which applies to a CNFF and returns two results:
• L: a set of literals that were either present as unit clauses inF, or were derived fromF by UP.
• Γ: a new CNF which results from assignments forF on literals Lconditioning to assign all of them to 1. Notationally, Γ =A(F)| ∀l(l∈ L) (A(l) = 1).
Continuously consider Formula 2.1, we have L={¬x3,¬x2}and Γ =∅.
UP is a very important component of search-based SAT solving algorithms because of its efficiency that we can apply all possible UP steps in time linear in the size of given CNF. DPLL is a refinement on depth-first-search which incorporates UP as given in Algorithm1. Beyond applying UP on Line1, we have two additional changes to ordered brute-force search as shown in Figure 2.1. First of all, we no longer assume that variables are examined in the given decision variable order as we go down the search tree. Secondly, we no longer assume that a variable is assigned to 1 first, and then to 0; see Line5. The particular choice of a literal ls.t. l∈Γ can have a dramatic impact on the running time of DPLL. Many heuristics have been proposed for making this choice. Among them, a quite effective heuristic, well-known as variable state independent decaying sum (VSIDS) attempts to score each variable and select thevariable polarity (corresponding to literal and its negation) with the highest score to determine where to branch [55].
2.1.2 Chronological backtracking
DPLL (Algorithm1) is based on chronological backtracking. That is, if we try both values of a variable at Levelt, and each leads to a contradiction (conditional unsat),
2 If a clause only contains a single literal, then it is called a unit clause.
Algorithm 1:DPLL(CNF F): returns a set of literals or unsat.
1 (L,Γ)←UnitPropagate(F);
2 if Γ =∅ then returnL;
3 else if ∈Γ then returnunsat;
4 else
5 Choose a literall in Γ;
6 if I ←DPLL(A(Γ)| A(l) = 1)6=unsatthen returnI ∪ L ∪l;
7 else if I ←DPLL(A(Γ)| A(¬l) = 1)6=unsatthen return I ∪ L ∪ ¬l;
8 else returnunsat;
9 end
we move to Levelt−1, undoing all intermediate assignments in the process, and try another value at that level (if one remains to be tried). If there are no other values to try at Level t−1, we move to Level t−2, and so on. If we move all the way to Level 0, and each value there leads to a contradiction, we know that the CNF is inconsistent (ultimate unsat).
The process of moving from the current level to a lower level is known as backtracking. Moveover, if backtracking to Level tis done only after having tried both values at Level t+ 1, then it is called chronological backtracking, which is the kind of backtracking used by DPLL. The problem is that it does not take into account the information of the contradiction that triggers the backtrack.
Example 7. Consider a concrete CNF as follows:
F =C1∧C2∧C3∧C4∧C5∧C6 where
C1 = (x1∨x2) C2 = (x2∨x3)
C3 = (¬x1∨¬x4∨x5) C4 = (¬x1∨x4∨x6) C5 = (¬x1∨¬x5∨x6) C6 = (¬x1∨x4∨ ¬x6) C7 = (¬x1∨¬x5∨ ¬x6)
(2.2)
Figure 2.2 depicts the termination tree3 for DPLL on F, which is assumed that it starts first byA(x1) = 1 and explore the subtree below that node, only to find that all branches lead to contradictions. This basically means thatA(F)| A(x1) = 1 inevitably is inconsistent, because an unsat-core (highlighted in red) is included in it. Note, however, that DPLL is unable to discover this fact in the knowledge until it first backtrack to Level 0.
The key point here is that all these contradictions that are discovered deep in the search tree are actually caused by having A(x1) = 1 at Level 0. That is, the assignment for x2 at Level 1 is irrelevant here. However, chronological backtracking is not aware of this fact. As a result, it tries different values of variablex2, hoping to fix the conflict. As shown in Figure 2.2, DPLL with chronological backtracking
3 Termination tree is the subset of search tree that is actually explored during search.