NOTE: There is a new model searcher called MACE4, which is not quite backward compatible with MACE2. MACE4 usually performs much better on equational problems, and MACE2 does better when many of the clauses are multiliteral.

MACE2 is a program that searches for finite models of first-order and equational statements. For example, if you give it the axioms for a group and state that there are two noncommuting elements, it will produce a noncommutative group. MACE2 serves as a complementary companion to Otter, which searches for refutations of the same class of statement. In particular, if you have a first-order conjecture, Otter will search for a proof, and MACE2 will search for a counterexample from the same input file.

MACE2's engine is a Davis-Putnam-Loveland-Logemann (DPLL) propositional decision procedure. It is available in the Otter-3.3/MACE-2.2 package as a standalone program called ANLDP. Some details of the DPLL implementation can be found in a 1994 report A Davis-Putnam Program and Its Application to Finite First-Order Model Search: Quasigroup Existence Problems.

MACE 2.2 for is bundled with Otter 3.3

For a better introduction, see the MACE 2.0 User Manual and Guide.

Here are the example inputs from the distribution package.

Other programs that search for small first-order models:

- SEM ,
by Jian Zhang and
Hantao Zhang
({jizhang,hzhang}@cs.uiowa.edu).

SEM is usually better than MACE for larger domains. - FINDER, by
John Slaney
([email protected]).

FINDER is usually better than MACE for sentential logics.

*
These activities are projects of the
Mathematics and Computer Science Division
of
Argonne National Laboratory.
*