Reasoning foundations
Solver
A program that searches for values satisfying a formal problem.
Definition
Solver
A solver decides supported constraints and may return a model or evidence for its result.
Different solvers support different languages and reasoning methods. Their result is meaningful only for the parsed problem and the semantics assigned to that language.
01
Example
A solver can return x = 4 for the constraints x > 3 and x < 6.
02
Important distinction
A parser that accepts a problem without deciding it is not a solver.
After reading this article, you should be able to
- Define Solver in the sense used on this site.
- Identify the input, result, and evidence expected from a solver call.