Boolean logic
Unsatisfiable
Having no assignment that makes all constraints true.
Definition
Unsatisfiable
A formula is unsatisfiable if every possible assignment violates at least one constraint.
Solvers report this result as unsat. Unlike sat, unsat cannot be established by displaying one assignment, so a checkable proof or exhaustive argument is needed.
01
Example
a and not a is unsat because either value of a makes one part false.
02
Important distinction
Unknown means the solver did not decide the query. It does not mean unsat.
After reading this article, you should be able to
- Define Unsatisfiable in the sense used on this site.
- Explain why one counterexample assignment cannot establish unsat.