SAT solving
Conflict
A clause made false by the current partial assignment.
Definition
Conflict
A conflict occurs when every literal in a clause is false under the current assignments.
The conflict shows that the current branch cannot extend to a model. CDCL uses the implication trail to find which earlier choices caused it.
01
Example
The clause a or b conflicts with the assignments a = false and b = false.
02
Important distinction
A conflict rejects one search branch. It establishes global unsat only when search and learning rule out every branch.
After reading this article, you should be able to
- Define Conflict in the sense used on this site.
- Find the clause responsible for a conflict in a partial assignment.