Boolean logic
Model
An interpretation that makes every asserted constraint true.
Definition
Model
A model assigns meanings and values that satisfy a formal query.
For a quantifier-free solver query, the visible part is often a list of variable values. Model replay evaluates those values against the original assertions.
01
Example
For x + y = 10 with x > y, x = 6 and y = 4 is a model over integers.
02
Important distinction
A plausible set of values is not a model until every assertion has been evaluated under it.
After reading this article, you should be able to
- Define Model in the sense used on this site.
- Verify a proposed model against every assertion in a small query.