Lecture 03
DP was not useful for computers back in the 50s. The technical report they published said you are faster on paper. The second algorithm performed much better, even on 50s machines.
This algorithm trades space for time. Instead of eliminating variables, we do a case split and look at both cases separately.
Unit resolution is confluent. You can apply it arbitrarily. In the end, you end up with the same formula. The power of modern SAT solvers comes from this rule, implemented in a very sophisticated way.
BCP means binary constraint propagation.
You add a literal with a unit clause whenever you call the solver. The first call forces $l$ to be true, and the second call forces it to be false. If there is one empty clause ($\bot$ symbol), the formula is unsat. If you get to satisfiable, you could abort, backtrack and return a satisfying assignment.
We are doing a recursive call but could implement this in a loop. But the first call has to be recursive. You need to return to $F$ and remember the literal you’ve chosen. BCP you want to make fast because approximately 80% of the time is spent here.
The “pick remaining variable” part previously took 80% of the time. With a trick, it got reduced to approximately 10%. You need a good decision heuristic: pick a variable $x$ and a phase to try first, i.e., positive or negative.
The pure literal rule is also in the original paper but dropped here. It is not done in modern solvers anymore.
Picking the right variable $x$ becomes irrelevant if you already know the phase you will assign it to. To find sat examples, we need a good heuristic at $l \in { x, \lnot x}$. For unsat, this does not matter.
The worst-case time complexity of the DPLL algorithm is $\mathcal{O}(2^n)$, where $n$ is the number of variables in the formula. In the worst case, the algorithm may need to explore all possible variable assignments, equivalent to traversing a binary tree of depth $n$. However, the algorithm often performs much better in practice than this worst-case scenario.
The space complexity of the DPLL algorithm is $\mathcal{O}(n)$, as it needs to store the current partial assignment in memory, which can have up to $n$ variables. The algorithm uses a depth-first search strategy, which means it only needs to store the variables in the current branch, not the entire search space.
Modern SAT solvers based on the DPLL algorithm, called Conflict-Driven Clause Learning (CDCL) solvers, have significantly improved performance compared to the basic DPLL algorithm through various optimizations and learning techniques.
Example of BCP
$a (\bar{a} \vee b) (\bar{b} \vee c) (\bar{c} \vee d)$ ⇒ in the end, you get $d$
$(\bar{a} \vee b) (\bar{b} \vee c) (\bar{c} \vee d) \bar{d}$ ⇒ in the end, you get $\bar{a}$
Can propagate from left to right and right to left
The arrows represent hyper-edge implications. The clause encodes three types of propagation. This is the reason why CNF is used in practice. Unit propagation is confluent. You can do this in any order.
This algorithm is exponential. For every recursive call, you double the formula
The shannon expansion provides a technique for systematically exploring a problem’s search space, simplifying Boolean formulae, and helping to identify satisfiability.
The $x$-axis represents CPU time, and the $y$-axis represents the number of solved instances.
Why is KISSAT considered superior to other solvers? About two years ago (as of 2021), an idea was conceived and has now been effectively implemented. This idea revolves around target phases, which originated from a Ph.D. thesis and has significantly impacted these maple solvers.
The concept involves dividing the search process into two distinct parts: the first focuses on unsatisfiable instances, while the second concentrates on satisfiable ones. The solver seamlessly switches between these phases, employing numerous restarts. In contrast, the alternative solver, known as “stable,” is notably slower due to the absence of restarts. A substantial improvement is achieved by combining target phases with a technique inspired by local search.
Although CaDiCal integrated this approach in 2019 and successfully solved many instances, it falls short compared to the maple solvers in the cvf. The KISSAT solver effectively implements these techniques. Additionally, several other lower-level factors demonstrate the practicality of these ideas. You can refer to the accurate system description provided for a more detailed understanding of why KISSAT performs exceptionally fast.
You do not put symbols, but integers in there, corresponding to the DIMACS format. We can think of this as lists. In reality, it will be stacked (vector in C++). The arrows are references to clauses. Each arrow is a reference. Every clause gives you a row. The literals are the columns. Think of this as a sparse matrix implementation. The lists on the left contain all occurrences of the literals.
BCP example
We can represent the truth value of a variable using a signed char, which requires only one byte of storage. The encoding scheme only necessitates a single byte to represent the truth value of a variable. A negative number indicates a false assignment, a positive number denotes a true assignment, and 0 signifies an unassigned variable.
Here, $X$ means “unassigned.”
We need to call DPLL on this because we first need a decision. We cannot propagate anything at first.
We increase the decision level. The decision level means how many recursive calls we have.
Initially, 0 is the height of the trail, and we push it on the control stack. Hence “control” increases in height with 0 on the top.
Why do we have 0 in the control stack in the beginning? On decision level 0, you want to remember the start of the literals on the trail with decision level 0. Then we need to pick a variable and a value.
Then we need to pick a variable and a value. Variable 1 becomes true. In C code, true would be +1, and false would be -1.
Now we put the literal 1 on the trail. Hence “1” is on the trail with the corresponding phase. If it were false, we would put -1.
Then we need to do boolean constraint propagation. In actual implementation, we would have a pointer “propagated” on the trail, which gives you the number of literals you have already propagated. Initially, this thing is 0. Now it is one literal, 1.
Now going to this matrix and going through all clauses in which negation of literal occurs ⇒ pink line here
Boolean constraint propagation will now force 2 to be true. The resolution of 1 and -1 cancels, and we are left with 2. The only way to make this clause true is to set 2 to true.
Now we are putting 2 on the stack, and the same thing continues: we go to the negative occurrences of 2, and we have to put 3 on the trail.
Then we would propagate 3, but there is no negative clause in which 3 occurs, meaning we have arrived at a “fixpoint.”
We now have 3 assignments on the trail and must make another decision. So we increase the decision level, and record the height of the trail, thus putting 3 on top of “control.”
The big lines around the trail indicate a block on decision level 1. These are all variables that were assigned on decision level 1. None is assigned on decision level 0, so there is no unit clause. You would see something on the trail if you had a unit clause.
Then we need to pick 4, and we can propagate 5
This is linear: the height of the trail is $\text{max}(\text{num_variables})$, so you can pre-allocate it when you implement the solver, just set it to the number of variables.
The same for the control. It can never be bigger than the number of variables plus 1. Beware of the off-by-one bug.
We can implement this going down the recursion, but how do we go up, i.e., backtrack? We go backward. If we had to backtrack to decision level 1, we would go through the trail until this decision level, to which we want to backtrack and erase all the assignments.
All this shows that we can do this in linear space with no need to copy the formula
Check Your Knowledge
- What is unit resolution and how does it help simplify SAT problems?
- Explain the concept of Boolean constraint propagation (BCP) and its role in SAT solving.
- What are the key steps involved in the DPLL algorithm? How does the pure literal rule fit into this algorithm?
- Describe the time and space complexity of the DPLL algorithm. What factors contribute to these complexities?
- What is the Expansion Theorem of Shannon, and how does it relate to SAT solving?
- Explain the correctness of the DPLL algorithm. Why can we trust the algorithm to provide accurate results?
- In the context of implementing BCP in a SAT solver, how are literals and assignments typically represented?
- What are the control and trail in a SAT solver’s implementation of BCP? What roles do they play?
- How big can the control and trail become in a SAT solver’s implementation of BCP? What factors influence their sizes?