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
(jks@arp.anu.edu.au).
FINDER is usually better than MACE for sentential logics.
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.