Computing Finite Models by Reduction to Function-Free Clause Logic

Abstract. Recent years have seen considerable interest in procedures for com-puting finite models of first-order logic specifications. One of the major paradigms, MACE-style model building, is based on reducing model search to a sequence of propositional satisfiability problems and applying (efficient) SAT solvers to them. A problem with this method is that it does not scale well, as the propositional for-mulas to be considered may become very large. We propose instead to reduce model search to a sequence of satisfiability prob-lems made of function-free first-order clause sets, and to apply (efficient) theo-rem provers capable of deciding such problems. The main appeal of this method is that first-order clause sets grow more slowly than their propositional counter-parts, thus allowing for more space efficient reasoning. In the paper we describe the method in detail and show how it is integrated into one such prover, Darwin, our implementation of the Model Evolution calculus. The results are general, however, as our approach can be used in principle with any system that decides the satisfiability of function-free first-order clause sets. To demonstrate its practical feasibility, we tested our approach on all satisfiable problems from the TPTP library. Our methods can solve a significant subset of these problems, which overlaps but is not included in the subset of problems solvable by state-of-the-art finite model builders such as Paradox and Mace4.