Boolean logic
Satisfiable
Having at least one assignment that makes all constraints true.
Definition
Satisfiable
A formula is satisfiable if some assignment makes the complete formula true.
A solver normally reports this result as sat and may return a model. One valid model establishes satisfiability.
01
Example
x > 2 and x < 4 is satisfiable over integers because x = 3 works.
02
Important distinction
Many failed assignments do not establish unsat; one untested assignment may still work.
After reading this article, you should be able to
- Define Satisfiable in the sense used on this site.
- Establish satisfiability by giving and checking one model.