SAT solving
Unknown result
A report that the solver did not decide the query.
Definition
Unknown result
Unknown is a solver result meaning that the current procedure produced neither sat nor unsat.
A solver can return unknown because the query lies outside a complete decision route, a resource limit was reached, or a required feature is unsupported. The reason should accompany the result when the interface can provide it.
01
Example
A solver that reaches its time limit before finding a model or an unsat proof can return unknown.
02
Important distinction
Unknown is not evidence that the query is difficult in principle, and it must never be treated as unsat.
After reading this article, you should be able to
- Define Unknown result in the sense used on this site.
- Interpret an unknown result without converting it into a claim about satisfiability.