First-UIP conflict analysis
also: first uip, uip, implication graph
The procedure that turns a conflict into a learned clause. Walk the implication graph backwards from the conflicting clause, resolving away literals assigned at the current decision level until exactly one remains: that unique implication point gives the clause that is both strong and cheap to derive, and its second-highest level says how far to backjump.
The step that turns a conflict into a clause. Start from the clause that is falsified and repeatedly resolve it with the reason for the most recently assigned literal in it, always eliminating a literal assigned at the current decision level:
Stop as soon as exactly one literal of the current decision level remains. That literal is the first unique implication point: the single node through which every path from the decision to the conflict passes, in the implication graph.
Stopping there rather than continuing to the decision itself is a deliberate trade. Resolving all the way back gives the decision clause, which is weaker and longer; the first UIP is the cheapest cut that still blocks the conflict, and it is consistently the best-performing choice in practice.
The learned clause also says where to go: backjump to the second-highest decision level among its literals. At that level the clause is unit, so the search immediately propagates rather than re-deciding.
see also
referenced by
read more