5

In SAT solving by conflict-driven clause learning, each time a solver detects that a candidate set of variable assignments leads to a conflict, it must look at the causes of the conflict, derive a clause from this (i.e. a lemma in terms of the overall problem) and add it to the set of known clauses. This entails choosing a cut in the implication graph, from which to derive the lemma.

A common way to do this is to pick the first unique implication point.

Per https://users.aalto.fi/~tjunttil/2020-DP-AUT/notes-sat/cdcl.html

A vertex l in the implication graph is a unique implication point (UIP) if all the paths from the latest decision literal vertex to the conflict vertex go through l.

The first UIP by the standard terminology is the first one encountered when backtracking from the conflict.

In alternative terminology, a UIP is a dominator on the implication graph, relative to the latest decision point and the conflict. As such, it could be found by building the implication graph and using a standard algorithm for finding dominators.

But finding dominators can take a nontrivial amount of CPU time, and I get the impression practical CDCL solvers use a faster algorithm specific to this context. However, I have not been able to find anything more specific than 'take the first UIP'.

What is the best known algorithm for finding the first UIP?

rwallace
  • 31,405
  • 40
  • 123
  • 242
  • 1
    I found an actual description of the algorithm [here](https://efforeffort.wordpress.com/2009/03/09/linear-time-first-uip-calculation/), but I don't understand it well enough to write an answer with it. – harold May 04 '21 at 06:33

1 Answers1

3

Without getting into data structural details, we have the implication graph and the trail, which is a prefix of a topological order of the implication graph. We want to pop vertices from the trail until we arrive at a unique implication point – this will be the first.

We recognize the unique implication point by tracking the set of vertices v in the trail such that there exists a path from the last decision literal through v to the conflict literal where the vertex following v in the path does not belong to the trail. Whenever this set consists of a single vertex, that vertex is a unique implication point.

Initially, this set is the two conflicting literals, since the conflict vertex does not belong to the trail. Until the set has one vertex, we pop the vertex v most recently added to the trail. If v belongs to the set, we remove it and add its predecessors (discarding duplicates, natch).

In the example from the linked site, the evolution of the set is

{x11, -x12}
{x10, x11}
{-x9, x10}
{x8, -x9}
{x8}

and we report x8.

David Eisenstat
  • 64,237
  • 7
  • 60
  • 120