LARA

Finite Model Finders

Consider formulas of first order logic (recall Predicate Logic Informally).

A model of $F$ is an interpretation in which $F$ is true.

We can define these notions precisely: First-Order Logic.

For a given bound $k$, is there an interpretation of a given formula with a domain of size $k$?

This problem is decidable: consider domain $\{1,\ldots,n\}$. The number of all possible interpretations with this domain is finite.

Finite model finder: a tool that searches for such models.

Approaches:

  • 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.

References