SAT solving
SAT search decision
A provisional variable assignment chosen when propagation cannot continue.
Definition
SAT search decision
A SAT search decision assigns an undecided variable so that the solver can explore one branch.
Heuristics choose the variable and value because those choices affect performance. Correctness does not require the heuristic to guess well, since conflict analysis and backtracking can reverse the branch.
01
Example
When no clause forces a, the solver may choose a = true and record a new decision level.
02
Important distinction
A decision is not a derived fact and must not be placed in an unsat certificate as if the formula implied it.
After reading this article, you should be able to
- Define SAT search decision in the sense used on this site.
- Distinguish a chosen SAT assignment from a propagated assignment.