New Techniques that Improve MACE-style Finite Model Finding
(Citations: 62)
We describe a new method for finding finite models of unsorted first-order logic clause sets. The method is a MACE-style method, i.e. it "flattens" the first-order clauses, and for increasing model sizes, instanti- ates the resulting clauses into propositional clauses which are consecutively solved by a SAT-solver. We enhance the standard method by using 4 novel techniques: term definitions, which reduce the number of variables in flat- tened clauses, incremental SAT, which enables reuse of search information between consecutive model sizes, static symmetry reduction, which reduces the number of isomorphic models by adding extra constraints to the SAT problem, and sort inference, which allows the symmetry reduction to be ap- plied at a finer grain. All techniques have been implemented in a new model finder, called Paradox, with very promising results.

Published in 2003.