Lecture 08
This figure visualizes an implication graph with the decision levels.
We began with a conflict, kappa, and delved into a search through the implication graph to trace it back to its roots. As we explored, we discovered a clause that negates these roots. Any cut in the graph that isolates the conflict from the decision (by negating the variables on this cut) becomes an implied clause. In our case, we took it to the extreme by placing this cut to the left.
- Blue arrows: any cut which separates conflict from decisions
- Red dots: variable cuts
- Black dots: last variables which were assigned
And this gives some freedom. There is one choice which is best here.
Blue arrows are the interesting parts here: any cut which separates the conflict from decisions.
The red dots are the variable cuts, and this is the one which you should use. They have incoming edges, so they are not decisions except for the one on the lowest level (lower left). Any cut which separates the decisions and we see all the blue edges here are left of the cut, and if we follow from the cut, we go forward, we will reach the conflict.
This learned clause, the negation of red dots, is a way better-learned clause than always going to these decisions. It might already make sense because we are just trying to get the minimal reason closest to the conflict, which tells us we should not have decided at decision level 1.
This learning function only traverses the implication graph at the last decision level. Therefore, whenever it needs to traverse an arrow that leads to another decision level, the negation is immediately included in the clause.
Is it possible? Yes, because you have a decision here and always run propagation on that level to completion. If you think about our loop, it says while propagating, and only if you are not propagating and finding no conflicts, everything is populated on level n-1, then you decide. That is why this guy on the lower left needs to exist. You can do a graph search backward (from conflict) to the decision (red lower left). Black dots are the last variables assigned, so on the trail, we follow the trail backward in the topological order of the trail and find this decision and collect all the guys on the lower decision level, which is your learned clause.
This example will lead us to minimization. The dashed lines are the decision levels, where the top line is the root level.
Notation: $\text{variable} = \text{value } @ \text{ decision level}$
The UIP separates all decisions from the conflict. Why is that better? Think about how you find the back jump level. You take the second highest level in this cut, which is $n-2$ here, because there is nothing red on the yellow level. If we had this line from the previous slide, the cut would pull in these two guys from above (see the previous slide, two red dots in the middle left), even if the middle right dot would be on level $n-2$. Then the backjump level would be worse because it is higher, and you cannot jump over as many parts of the graph.
Notation: $\text{variable} = \text{value } @ \text{ decision level}$
Antecedents / Reasons
These clauses are implicitly represented in the graph. The blue line represents a hyperedge, which is a clause. You point to that clause when you assign a literal (in this case, $t=1$). You flip the incoming variables because they imply a single destination of this edge ($t=1@4$ represents the edge here).
On the bottom left, there is the implication which gives the clause on the bottom right.
Every node in this diagram representing a literal has an incoming edge, except for the units at the top and the decisions. Both of these have zero pointers as the reason. You can distinguish between them by looking at the decision level of the variable, which you store somewhere else. If the decision level is 0, then it is a unit reason. If it is not 0, then it is a decision because there are no decisions at decision level 0.
Conflicting Clauses
The conflict $\kappa$ is somewhat of an arbitrary variable. You can interpret $\kappa$ as false, resulting in $y$ and $z$ implying false.
You need to remember the following:
- There are usual clauses (like $t$ from the previous slide)
- Then there are units and decisions
- Then we need to think about the conflicts
Resolving Antecedents the First Time
Let us perform a conflict analysis. You can maintain a learned clause that we can continue resolving linearly.
The circles are clauses here. We perform resolution and combine two clauses to form a new one. Then, we use that new clause to perform resolution with another clause and continue the process until no more resolutions can be made. This is called a linear resolution chain.
This is also behind the execution semantics of Prolog. You always take the last resolved clause and resolve it with a new one you have not seen before.
We take the conflict clause (the blue clause on the bottom right, not the blue background), then we take one of its literals and resolve it with its reason.
In this case, we consider the variable $y$. We observe that whenever two clauses (in this case, the conflict clause $\color{blue} (\bar{y} \vee \bar{z})$ and the reason for $y$) overlap and have $y$ in common, $y$ occurs positively in one clause and negatively in the other. This is the way we constructed the graph.
In this particular situation, we have two clauses at the bottom. The variable $y$ occurs positively in the reason for the $y$ clause, which is $\color{red} (\bar{h} \vee \bar{i} \vee \bar{t} \vee y)$. The variable $y$ is true, while the other literals are false. This is important later. We also have the resolvent $\color{blue} (\bar{y} \vee \bar{z})$, which has all false literals, and $y$ in the opposite phase. This is why we can perform resolution between these two clauses.
This is always possible because everything in this context is false except for the literal $y$ (an assigned literal or a literal forced by a reason clause). Therefore, taking these two clauses will not yield a tautology, which would require that one is also true. The only true literal is $y$, but we are resolving it away.
The resolvent clause has all false literals.
The resolvent can be interpreted as a cut. The term “cut” refers to a partition that separates the conflict from the decisions on the left-hand side. It can be thought of as a clause; intuitively, this cut can be derived by resolution. This explains why the negation of these literals, when combined in a clause, is implied by the formula because we can resolve them.
This is now our current working resolvent. All literals are false under the current assignment. In principle, we could take any literal and resolve its reason again. We have thus four choices. However, in a real solver, you will only resolve literals in this lowest level graphically (highest decision level), so either $t$ or $z$.
This is why $t$ is in the clause on the left since $t$ occurs positively in that clause. Everything else in that clause is false. By resolving these two clauses, we can avoid a tautology. This results in a new cut, indicated by the yellow line. Graphically, we take the cut; mathematically, we obtain it by performing resolutions.
Next, we use the binary clause as the reason for $z$. Again, the cut separates the conflict from the decisions. This means that the formula implies the thing. The takeaway is that these cuts correspond to resolutions.
What is self-subsuming resolution?
$R \subseteq C$ is equivalent to saying $D \subseteq C$
The $b$ is in both parts.
The resolvent is a subset of the left clause.
We are simply removing $x$ from the formula, making it shorter. This is beneficial because a shorter formula means fewer parameters, making it easier to determine unsatisfiability.
Both clauses contain the variable $\bar{s}$. During resolution, we will find two origins for $\bar{s}$. The yellow clause is a subset of the blue clause, which subsumes the previous clause.
Why does it have to happen? If we look only at literals of the highest decision level and you are going to resolve away the reasons: $y$, then $t$, then $z$, then $x$ , and then at one point, there will be only one literal left on this decision level. Because everything can be simulated by resolution, it is clear that we need to have this situation of self-subsumption during these intermediate resolvent because otherwise, we will not get to this situation (green box).
Also, note that we could continue resolving $s$, but this one is better because it is the first UIP we sought. So this guy on the lowest decision level, if you ignore everything above, dominates this conflict. So every path from the decision here to reaching the conflict needs to go through this UIP. This is the best clause you would usually want to learn.
Another hidden aspect is that we have a learned clause (shown in blue at the bottom), and we will proceed through this clause. On decision level 4, we have variable $s$, while all the other variables are at decision level 2 or lower. This indicates that the second-highest decision level in the learned clause is 2. Consequently, we will perform a backjump to decision level 2 since decision level 3 was not useful in deriving the conflict. Although there is an arrow pointing downward from variable $l$, it was unnecessary to derive the conflict. We could have chosen $s$ as the decision on level 3, and the conflict would have been encountered.
We could continue, i.e., resolve the reason for $s$. We would also get a cut that separates the decisions. Note that we also could have learned the decisions, which corresponds to clause $(\bar{c} \wedge \bar{f} \wedge \bar{k} \wedge \bar{r})$. Assuming these four, we know we get into a conflict. But that clause would be worse than the previous one.
The name “last unique implication point” (UIP): because it’s the very last clause that satisfies this resolvent (in the process resolving literals only in this decision level) which would have only one literal on the current decision level. Called “last” because it could be when you start resolving away $s$, it could also have literals in this decision level so that you can go down to one literal in the resolvent of the current decision level. Then you resolve, add more and more, and go down again. And then you resolve more and go down again. You cannot continue this forever because you will hit the decision here (green box) at one point, and that’s a situation where it’s a UIP, the single literal in the learned clause of the current decision level. This explains why this is called “last.”
Where do we need to backtrack? This clause pulled in decision level 3 during this resolution procedure because we now have literal $l$ here. Decision level 3 is the second highest level in the clause. That’s why if we learn this clause (blue on bottom), we can only backtrack to decision level 3 while, in principle, it’s possible to backtrack to decision level 2. This seems to be a good heuristic to avoid pulling in decision levels.
You want to do as few as possible resolutions to derive this point.
Here we did the minimum number of resolutions to obtain a learned clause that has a single literal on the last decision level, and in this case, it allows us to backtrack the largest number of levels. In this case, we jump over one decision level.
Is this the end? ⇒ real insight from Niklas. You can continue doing more
We got the clause on the bottom by only resolving on decision level 4. But if we look at this $i$ (it’s in the clause), if we take its reason which is a binary clause (only says $h$ implies $i$), then we can do self-subsuming resolution again because $h$ is also in the clause
Look at the yellow cut: it’s shorter and still has the property that separates decisions from the conflict.
This is our locally minimized clause. What’s local minimization: go through your learned clause and check for literals in the learned clause, whether it has a reason where all its other literals (not the one which is forced) which are implied are also in the learned clause (just condition for self-subsuming resolution). In that case, you can remove that literal (in this case, we removed the $i$).
It’s a very cheap procedure, go over the learned clause once, check for each literal in its learned clauses, mark all the literals in the learned clause before, and then remove them. The procedure is even confluent, you can do this in any order, and you will get the smallest locally minimized clause.
Next step: Is this even possible in a more general way? Pay attention here at $h$: it depends on $e$ and $g$. $g$ is already in the good clause, but $e$ is not in the clause. This looks not good. If we resolve away $h$, this won’t do anything, but we’re adding $e$. So we replace $h$ by $e$ , which seems to be a redundant resolution. Intuition: redundant resolutions are not good. You should keep as close as possible to the conflict. However, looking at $e$, it has unit as one reason.
$h$ has $e$ in its reason and also the $g$
You could just resolve away the $e$ again because the $e$ only depends on something globally true so that you can ignore it and on the $d$ , which is in the clause. Now we see this linear resolution chain again. So we take this locally minimized clause (starting point here), then we resolve it with the reason for $h$, then we take $e$ and the reason of $e$, so $e$ goes away, and then $b$ goes away because we have a unit clause. Ultimately, we get a very short clause corresponding to this yellow cut.
This procedure is linear but needs some tricks to make it linear. Not simple depth-first search, we need to remember things that cannot be resolved away (called “poison”) and remember things that can be resolved away. Start with the original first UIP clause, and then you do this recursive minimization, which subsumes the local minimization.
This is in SATCH
Run produced 55000 conflicts, and we made this UIP deduction in all these conflicts. We derived 2.6 million literals. This means that the first UIP clause has an average size of 47. So we had this first UIP clause where we resolved on the lowest decision of the highest decision level, and then we got this first clause, which has, on average here, 47 literals. We’d also look at whether there are outliers for real-life implementation, but the average is a good metric.
Minimized: number of literals we could minimize by procedure (recursive minimization). Here 1.7 million, usually it’s not that much. 67% of the variables could be removed by minimization (quite substantial!), reducing the size of the clause by a factor of 3 without introducing new literals.
Learned: average learned clause length is 16 literals, which goes down from 47 to 15.7
In KISSAT, we can profile how long we spend on each procedure
KISSAT, less than 6.42% is spent on minimization, very little time
Analyze takes about 30% of the runtime
Mark all variables in the first UIP clause, then search for each of the literals in the UIP clause in the implication graph, and you go recursively. This is depth-first, which tries to reach already literals in the clause (in principal linear). If you hit recursively a decision not in the clause, you cannot remove the literal. Otherwise, in principle, you can remove it if you always end up with literals already in the clause.
There are several optimizations:
- Failure to remove a literal can be cached, called “poison” (you can mark it either as removable or poison), then for the second literal, you can reuse the fact that you searched this already, the first one. Then, if you try to remove the second one, you hit a literal, which was marked as not being removable on the first attempt. You can also stop early.
- If you’re pulling a decision level, if you find an antecedent in this search that contains a literal which is not pulled into the learned clause, then you can also terminate immediately
With the poison idea, you get the whole thing linear. The algorithm says: for every literal in the clause, you would need to do this search, and if you have, e.g., 10000 literals and you need to do DFS for each of them, it’s not linear anymore (10000 times the size of the implication graph), but with poison idea, you can make it linear
Interesting thing here: the memory goes down. One thing that is not on the slide here is that you kind of also learn better clauses which means the overall runtime of the solver goes down.
Running solvers ten times with random seeds, the solver would use random seeds to initialize data structures.
Local means: don’t look deep in the implication graph; only look one reason clause back
Look at 100 runs. This is for one solver with preprocessing
Recursive, local, no minimization (none) solvers were run ten times on all 100 benchmarks
Then rank the results of individual runs. Recursive wins (I would expect consistently removing the largest number of literals), local is not as good, and none is worse.
If we had picked the local algorithm seed 0 and the recursive algorithm 2, the overall result would be the opposite. We would’ve claimed that the local version is better than the recursive one. This is a real danger in SAT research: the butterfly effect. Random seed somewhere. Ordering the clauses or doing strange changes in your data structures means the clauses are traversed differently. This all corresponds to seeds in a certain sense. Then when you measure something, you might have been just lucky by your last change, which has nothing to do with the idea you’re measuring, that it’s faster. That’s the annoying part of these problems where you have timeouts and butterfly effects. In ML, you have similar problems.
0% del for none is always. None means no minimization
You also see here the effect of memory, which is predicted by the del column (the averages over ten seeds are on the previous slide)
Minimization was recently improved. If you have multiple decisions on each decision level, you can try to replace this with one dominator on the previous decision level. So similar to what you do on the highest decision level. You will only want to do this if you’re not pulling in additional decision levels. That reduces the clauses, and you get additional improvement. This procedure is called “shrinking.” Mathias Fleury and Armin Biere came up with a procedure to perform shrinking in linear time, see Efficient All-UIP Learned Clause Minimization.
Check Your Knowledge
- Can you explain what a unique implication point (UIP) is and its importance in SAT solving?
- What is the difference between the first UIP and last UIP?
- Can you describe what a learned clause is and why the length matters?
- Can you explain the concept of clause minimization in SAT solving?
- In the context of clause minimization, what is “poison?” How is it used to speed up the process?
- What is the difference between recursive and local minimization?
- How does the butterfly affect SAT solver benchmarking?