SAT solving
Learned clause
A new clause derived from a conflict and added to the SAT problem.
Definition
Learned clause
A learned clause records a consequence of the existing clauses that blocks a conflicting combination of assignments.
Learning lets a solver reuse information gained in one branch. A good learned clause can also cause earlier propagation in other branches.
01
Example
If a = true and c = false always cause a contradiction, the solver may learn not a or c.
02
Important distinction
A heuristic guess is not a learned clause unless the solver can derive it from existing constraints.
After reading this article, you should be able to
- Define Learned clause in the sense used on this site.
- Explain how a learned clause prevents a known conflict from recurring.