Finite Model Computation via Answer Set Programming
Martin Gebser, Orkunt Sabuncu, Torsten Schaub
We show how Finite Model Computation (FMC) of ?rst-order theories can ef?ciently and transparently be solved by taking advantage of a recent extension of Answer Set Programming (ASP), called incre- mental Answer Set Programming (iASP). The idea is to use the incremental parameter in iASP pro- grams to account for the domain size of a model. The FMC problem is then successively addressed for increasing domain sizes until an answer set, rep- resenting a ?nite model of the original ?rst-order theory, is found. We implemented a system based on the iASP solver iClingo and demonstrate its competitiveness.