Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
|
sav08:finite-model_finders [2008/03/13 12:02] vkuncak |
sav08:finite-model_finders [2008/03/13 13:22] vkuncak |
||
|---|---|---|---|
| Line 9: | Line 9: | ||
| For a given bound $k$, is there an interpretation of a given formula with a domain of size $k$? | For a given bound $k$, is there an interpretation of a given formula with a domain of size $k$? | ||
| - | This problem is decidable. | + | 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. | Finite model finder: a tool that searches for such models. | ||
| Approaches: | Approaches: | ||
| - | * encoding into SAT (popular recently because SAT solvers are good): MACE, Paradox, KodKod (used in Alloy) | ||
| * generalize SAT algorithms to search for finite domains and not just propositional ones (SEM) | * 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: | ||
| + | * symmetry breaking | ||
| + | * sort inference | ||
| + | * incremental search for different sizes of the domain | ||
| + | |||
| + | Symmetry breaking among issues of encoding into SAT. | ||
| ===== References ===== | ===== References ===== | ||
| - | * [[http://alloy.mit.edu]] | ||
| * [[http://web.mit.edu/~emina/www/kodkod.html]] | * [[http://web.mit.edu/~emina/www/kodkod.html]] | ||
| * [[http://www.cs.chalmers.se/~koen/folkung/]] | * [[http://www.cs.chalmers.se/~koen/folkung/]] | ||
| + | * [[http://alloy.mit.edu]] | ||