Finite Model Finders
Consider formulas of first order logic (recall Predicate Logic Informally).
A model of is an interpretation in which is true.
We can define these notions precisely: First-Order Logic.
For a given bound , is there an interpretation of a given formula with a domain of size ?
This problem is decidable: consider domain . The number of all possible interpretations with this domain is finite.
Finite model finder: a tool that searches for such models.
- generalize SAT algorithms to search for finite domains and not just propositional ones (SEM)
- encoding into SAT (popular recently because SAT solvers are good): MACE, Paradox, KodKod (used in Alloy)
Issues when encoding into SAT:
- detecting sharing to minimizing size of propositional formula
- symmetry breaking - larger formula with fewer instances
- sort inference - smaller range of variables
- incremental search for different sizes of the domain - reusing work in SAT solver
Symmetry breaking among issues of encoding into SAT.