MACE2*

Models And Counter-Examples

This page is obsolete. Mace2 is now being maintained elsewhere.

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.

Copyrights and License

See the Otter/MACE Legal Page.

* The spice, not the weapon.

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