1
$\begingroup$

I would guess that this question is going to make some people wonder how I haven't already found a solution looking through papers -- but I do not see a clear algorithm.

In implementing CDCL, I read this site, which gives the following definition:

Consider an implication graph $(V,E)$ obtained from a trail that falsifies at least one clause. A conflict cut of the graph is a partition $W=(A,B)$ of its vertex set such that

  • ​all the decision literal vertices belong to the set $A$, and
  • ​the conflict vertex $\bot$ belongs to the set $B$.

Let $R = \{l \in A \mid l' \in B : (l, l') \in E \}$ be the reason set of the conflict cut consisting of the $A$ vertices having an edge to the $B$ set.

The learned clause corresponding to the cut is ${\huge \lor}_{l \in R} \lnot l$.

I have a trail -- a list of assigned literals (such as -5, or 4, etc.), each one annotated with whether it's a decision literal, or pointing to the clause it was implied by in unit propagation. Each one is also annotated with a decision level, effectively giving me an implication graph.

I am unsure of a generalised algorithm to get this reason set $R$ using this trail. I have a function that gives me a UIP literal in the trail, but I don't know if this helps here.

Say we decided on the UIP cut below:

UIP Cut

What kind of algorithm or process would lead me to get $\lnot x_2, x_5, \lnot x_6$ in my reason set, given I start from a conflict clause?

$\endgroup$

1 Answer 1

1
$\begingroup$

First, some observations:

  • Setting all literals in a reason set to true leads to a conflict through unit propagation.
  • One can replace a non-decision literal from a reason set with its in-neighbors in the implication graph without disturbing the above property.
  • The falsified clause $l_1 \lor \ldots \lor l_n$ that lead to the conflict immediately gives you a reason set $\{ \lnot l_1, \ldots, \lnot l_n \}$. Similarly, any reason set $R$ has a corresponding learned clause $\bigvee_{l \in R} \lnot l$.

Clause learning consists of forming a reason set that contains exactly one literal from the current decision level, because backtracking before the current decision level then makes its corresponding learned clause a unit clause, which can immediately be used for unit propagation. The one remaining literal from the current decision level is known as a unique implication point (UIP), because from the current decision level it is solely responsible for the conflict.

All one needs to do now is to take the initial reason set and repeatedly replace one of the contained non-decision literals with its in-neighbors in the implication graph. This process is guaranteed to yield a desired reason set at some point because doing all possible replacements would result in a reason set containing only decision literals, which has the desired property.

Replacing literals at random is not particularly useful, though, because you might end up replacing a UIP without having detected it due other literals that are implied by this UIP still being in the reason set. Therefore, in order to not miss any UIPs, literals should be replaced in reverse order that they appear in the trail.

All UIPs will be detected in this procedure, though modern SAT solvers tend to stop once the first UIP (i.e. appearing the most recently in the trail) is found and use its corresponding learned clause for backtracking. The simple reason for this is that you can backtrack at most up to the decision level of the second most recently assigned literal in the reason set, since before that point the learned clause is no longer unit, and the first UIP minimizes this level.

To implement this, start out with the reason corresponding to the falsified clause, and iterate the trail in reverse to ensure that literals are processed in the correct order. Process each literal that you come across that is in the reason set by removing it from the reason set and inserting its in-neighbors in the implication graph. Keeping track of how many literals in the current reason set are from the current decision level lets you efficiently detect whether the current literal is a UIP.

Finally, it's worth noting that these replacement operations are nothing more than resolution using the clauses in the formula. In your example, the falsified clause $\neg x_{11} \lor x_{12}$ corresponds to the reason set $\{x_{11}, \neg x_{12}\}$ and replacing $\neg x_{12}$ with $x_{10}$ boils down to obtaining $\neg x_{10} \lor \neg x_{11}$ by resolving $\neg x_{11} \lor x_{12}$ (the learned clause associated with the current reason set) with $\neg x_{10} \lor \neg x_{12}$ ($x_{12}$'s antecedent).

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.