/usr/share/doc/mace2/mace2.html

<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN"
            "http://www.w3.org/TR/REC-html40/loose.dtd">
<HTML>
<HEAD>
<TITLE>MACE 2.0 Reference Manual and Guide
</TITLE>

<META http-equiv="Content-Type" content="text/html; charset=US-ASCII">
<META name="GENERATOR" content="hevea 1.10">
<STYLE type="text/css">
.li-itemize{margin:1ex 0ex;}
.li-enumerate{margin:1ex 0ex;}
.dd-description{margin:0ex 0ex 1ex 4ex;}
.dt-description{margin:0ex;}
.toc{list-style:none;}
.thefootnotes{text-align:left;margin:0ex;}
.dt-thefootnotes{margin:0em;}
.dd-thefootnotes{margin:0em 0em 0em 2em;}
.footnoterule{margin:1em auto 1em 0px;width:50%;}
.caption{padding-left:2ex; padding-right:2ex; margin-left:auto; margin-right:auto}
.title{margin:2ex auto;text-align:center}
.center{text-align:center;margin-left:auto;margin-right:auto;}
.flushleft{text-align:left;margin-left:0ex;margin-right:auto;}
.flushright{text-align:right;margin-left:auto;margin-right:0ex;}
DIV TABLE{margin-left:inherit;margin-right:inherit;}
PRE{text-align:left;margin-left:0ex;margin-right:auto;}
BLOCKQUOTE{margin-left:4ex;margin-right:4ex;text-align:left;}
TD P{margin:0px;}
.boxed{border:1px solid black}
.textboxed{border:1px solid black}
.vbar{border:none;width:2px;background-color:black;}
.hbar{border:none;height:2px;width:100%;background-color:black;}
.hfill{border:none;height:1px;width:200%;background-color:black;}
.vdisplay{border-collapse:separate;border-spacing:2px;width:auto; empty-cells:show; border:2px solid red;}
.vdcell{white-space:nowrap;padding:0px;width:auto; border:2px solid green;}
.display{border-collapse:separate;border-spacing:2px;width:auto; border:none;}
.dcell{white-space:nowrap;padding:0px;width:auto; border:none;}
.dcenter{margin:0ex auto;}
.vdcenter{border:solid #FF8000 2px; margin:0ex auto;}
.minipage{text-align:left; margin-left:0em; margin-right:auto;}
.marginpar{border:solid thin black; width:20%; text-align:left;}
.marginparleft{float:left; margin-left:0ex; margin-right:1ex;}
.marginparright{float:right; margin-left:1ex; margin-right:0ex;}
.theorem{text-align:left;margin:1ex auto 1ex 0ex;}
.part{margin:2ex auto;text-align:center}
</STYLE>
</HEAD>
<BODY >
<!--HEVEA command line is: /usr/bin/hevea mace2.tex -->
<!--CUT DEF section 1 --><DIV CLASS="center">

Argonne National Laboratory<BR>
9700 South Cass Avenue<BR>
Argonne, IL 60439<P><BR>

</P><HR SIZE=2><P><BR>
ANL/MCS-TM-249<BR>
</P><HR SIZE=2><P><BR>
<BR>
<BR>
<BR>
<BR>
<BR>
<BR>

<FONT SIZE=5><B>MACE 2.0 Reference Manual and Guide</B></FONT></P><P><BR>

by<BR>

<FONT SIZE=5><I>William McCune</I></FONT><BR>
</P><P><BR>
<BR>
<BR>
<BR>
<BR>
<BR>
<BR>
<BR>
<BR>
<BR>
<BR>

Mathematics and Computer Science Division</P><P><BR>
<BR>
</P><P>Technical Memorandum No. 249</P><P><BR>
<BR>
<BR>
<BR>
<BR>
<BR>
<BR>

May 2001
</P></DIV><P>This work was supported by the Mathematical,
Information, and Computational Sciences Division subprogram of the
Office of Advanced Scientific Computing Research, U.S. Department of
Energy, under Contract W-31-109-Eng-38.
</P><P>

Argonne National Laboratory, with facilities in the states of Illinois
and Idaho, is owned by the United States Government and operated by The
University of Chicago under the provisions of a contract with the
Department of Energy.</P><P><BR>
<BR>
<BR>
<BR>
<BR>
<BR>
<BR>
<BR>
<BR>
<BR>
<BR>
<BR>
<BR>
<BR>
</P><DIV CLASS="center">
<B>DISCLAIMER</B>
</DIV><P>This
report was prepared as an account of work sponsored by an agency of the United States Government. Neither the United States
Government nor any agency thereof, nor The University of Chicago, nor any of
their employees or officers, makes any warranty, express or implied, or assumes any legal liability or
responsibility for the accuracy, completeness, or usefulness of any
information, apparatus, product, or process disclosed, or represents that its use
would not infringe privately-owned rights.
Reference herein to any specific commercial product, process, or service by trade name,
trademark, manufacturer, or otherwise, does not necessarily constitute
or imply its endorsement, recommendation, or favoring by the United
States Government or any agency thereof. The views and opinions of document
authors expressed herein do not necessarily state or reflect those of the
United States Government or any agency thereof, Argonne National
Laboratory, or The University of Chicago.

</P><!--TOC section Contents-->
<H2 CLASS="section"><!--SEC ANCHOR -->Contents</H2><!--SEC END --><UL CLASS="toc"><LI CLASS="li-toc">
Abstract
</LI><LI CLASS="li-toc"><A HREF="#htoc1">1&#XA0;&#XA0;Introduction</A>
</LI><LI CLASS="li-toc"><A HREF="#htoc2">2&#XA0;&#XA0;A Little Motivation</A>
</LI><LI CLASS="li-toc"><A HREF="#htoc3">3&#XA0;&#XA0;How to Tell MACE What to Do</A>
<UL CLASS="toc"><LI CLASS="li-toc">
<A HREF="#htoc4">3.1&#XA0;&#XA0;The Formulas</A>
</LI><LI CLASS="li-toc"><A HREF="#htoc5">3.2&#XA0;&#XA0;Constraints in the Input</A>
</LI><LI CLASS="li-toc"><A HREF="#htoc6">3.3&#XA0;&#XA0;Command-Line Options</A>
</LI></UL>
</LI><LI CLASS="li-toc"><A HREF="#htoc7">4&#XA0;&#XA0;Language Accepted by MACE</A>
<UL CLASS="toc"><LI CLASS="li-toc">
<A HREF="#htoc8">4.1&#XA0;&#XA0;Differences from Otter&#X2019;s Language</A>
</LI><LI CLASS="li-toc"><A HREF="#htoc9">4.2&#XA0;&#XA0;A Quick Review of the Language Otter Accepts</A>
</LI></UL>
</LI><LI CLASS="li-toc"><A HREF="#htoc10">5&#XA0;&#XA0;How MACE Works</A>
</LI><LI CLASS="li-toc"><A HREF="#htoc11">6&#XA0;&#XA0;Differences from Previous Versions</A>
</LI><LI CLASS="li-toc"><A HREF="#htoc12">7&#XA0;&#XA0;Calling MACE From Other Programs</A>
</LI><LI CLASS="li-toc"><A HREF="#htoc13">8&#XA0;&#XA0;The ANLDP Propositional Decision Procedure</A>
</LI><LI CLASS="li-toc">References
</LI></UL><TABLE CLASS="title"><TR><TD><H1 CLASS="titlemain">MACE 2.0 Reference Manual and Guide</H1><H3 CLASS="titlerest"><EM>William McCune</EM></H3></TD></TR>
</TABLE><BLOCKQUOTE CLASS="abstract"><B>Abstract: </B>
MACE is a program that searches for finite models
of first-order statements. The statement to be modeled is
first translated to clauses, then to relational
clauses; finally for the given domain size, the ground
instances are constructed. A Davis-Putnam-Loveland-Logeman
procedure decides the propositional problem, and any models found
are translated to first-order models.
MACE is a useful complement to the theorem prover Otter,
with Otter searching for proofs and MACE looking for
countermodels.
</BLOCKQUOTE><!--TOC section Introduction-->
<H2 CLASS="section"><!--SEC ANCHOR --><A NAME="htoc1">1</A>&#XA0;&#XA0;Introduction</H2><!--SEC END --><P>MACE (Models And CounterExamples) is a program that searches
for small finite models of first-order statements.
It is frequently used along with our first-order theorem prover
Otter&#XA0;[<A HREF="#otter3"></A>, <A HREF="#otter-web"></A>], with Otter searching for
proofs and MACE looking for countermodels. The two programs
accept almost the same language, so the same input file can
usually be used for both programs.</P><P>MACE has been used for many applications including quasigroup existence
problems&#XA0;[<A HREF="#dp-quasi"></A>], ortholattice problems&#XA0;[<A HREF="#ortholattice"></A>], and
lattice and Boolean algebra problems&#XA0;[<A HREF="#wm-rp:monograph"></A>, <A HREF="#monograph-web"></A>].
Other successful programs that look for finite models of first-order
statements are SEM&#XA0;[<A HREF="#sem"></A>] and FINDER&#XA0;[<A HREF="#finder"></A>].
A related class of programs can produce finite models when the
search for a refutation fails. Examples of these are
SATCHMO&#XA0;[<A HREF="#satchmo"></A>] and MGTP&#XA0;[<A HREF="#mgtp"></A>].</P><P>At its core, MACE has a Davis-Putnam-Loveland-Logeman propositional
decision procedure named ANLDP. ANLDP can be used directly to decide
propositional (SAT) problems given in conjunctive normal form
(see Section&#XA0;<A HREF="#anldp">8</A>).
Section&#XA0;<A HREF="#history">6</A> gives differences between
MACE 2.0 and previous versions.
The MACE Web site is <TT>http://www.mcs.anl.gov/AR/mace</TT>.</P><!--TOC section A Little Motivation-->
<H2 CLASS="section"><!--SEC ANCHOR --><A NAME="htoc2">2</A>&#XA0;&#XA0;A Little Motivation</H2><!--SEC END --><P>Say you&#X2019;ve just invented group theory by writing down
the following three axioms,
</P><TABLE CLASS="display dcenter"><TR VALIGN="middle"><TD CLASS="dcell">
&#XA0;&#XA0;&#XA0;&#XA0;&#XA0;

</TD><TD CLASS="dcell"><TABLE CELLSPACING=6 CELLPADDING=0><TR><TD ALIGN=right NOWRAP><I>e</I>&#XA0;*&#XA0;<I>x</I></TD><TD ALIGN=left NOWRAP>&#XA0;=&#XA0;<I>x</I></TD><TD ALIGN=right NOWRAP>&nbsp;</TD><TD ALIGN=left NOWRAP>&nbsp;</TD><TD ALIGN=right NOWRAP>&nbsp;</TD><TD ALIGN=left NOWRAP>&nbsp;</TD><TD ALIGN=right NOWRAP>&nbsp;</TD><TD ALIGN=left NOWRAP>&nbsp;</TD><TD ALIGN=right NOWRAP>&nbsp;</TD><TD ALIGN=left NOWRAP>&nbsp;</TD><TD ALIGN=right NOWRAP>&nbsp;</TD></TR>
<TR><TD ALIGN=right NOWRAP>
<I>g</I>(<I>x</I>)&#XA0;*&#XA0;<I>x</I></TD><TD ALIGN=left NOWRAP>&#XA0;=&#XA0;<I>e</I></TD><TD ALIGN=right NOWRAP>&nbsp;</TD><TD ALIGN=left NOWRAP>&nbsp;</TD><TD ALIGN=right NOWRAP>&nbsp;</TD><TD ALIGN=left NOWRAP>&nbsp;</TD><TD ALIGN=right NOWRAP>&nbsp;</TD><TD ALIGN=left NOWRAP>&nbsp;</TD><TD ALIGN=right NOWRAP>&nbsp;</TD><TD ALIGN=left NOWRAP>&nbsp;</TD><TD ALIGN=right NOWRAP>&nbsp;</TD></TR>
<TR><TD ALIGN=right NOWRAP>
(<I>x</I>&#XA0;*&#XA0;<I>y</I>)&#XA0;*&#XA0;<I>z</I></TD><TD ALIGN=left NOWRAP>&#XA0;=&#XA0;<I>x</I>&#XA0;*&#XA0;(<I>y</I>&#XA0;*&#XA0;<I>z</I>)
</TD><TD ALIGN=right NOWRAP>&nbsp;</TD><TD ALIGN=left NOWRAP>&nbsp;</TD><TD ALIGN=right NOWRAP>&nbsp;</TD><TD ALIGN=left NOWRAP>&nbsp;</TD><TD ALIGN=right NOWRAP>&nbsp;</TD><TD ALIGN=left NOWRAP>&nbsp;</TD><TD ALIGN=right NOWRAP>&nbsp;</TD><TD ALIGN=left NOWRAP>&nbsp;</TD><TD ALIGN=right NOWRAP>&nbsp;</TD></TR>
</TABLE></TD></TR>
</TABLE><P>
and you are wondering whether all groups are commutative.
You prepare the following input file, named <TT>group.in</TT>.
</P><DIV CLASS="center">

<TABLE BORDER=1 CELLPADDING=1 CELLSPACING=0><TR><TD ALIGN="left"><PRE CLASS="verbatim">set(auto).
list(usable).
  e * x = x.                  % left identity
  g(x) * x = e.               % left inverse
  (x * y) * z = x * (y * z).  % associativity
  a * b != b * a.             % denial of commutativity
end_of_list.
</PRE></TD></TR>
</TABLE>
</DIV><P>
Now you give the input file to Otter to search for a proof
(actually a refutation).
</P><PRE CLASS="verbatim">    % otter &lt; group.in &gt; group.out
</PRE><P>
and to MACE to look for a countermodel (actually a model) of size 4,
as follows.
</P><PRE CLASS="verbatim">    % mace -n4 -p -c &lt; group.in &gt; group4.out
</PRE><P>
Both programs fail immediately. But looking at the Otter
output makes you suspect that not all groups are commutative,
so you go forward, looking for larger countermodels.
The command
</P><PRE CLASS="verbatim">    % mace -n6 -p -c &lt; group.in &gt; group6.out
</PRE><P>
succeeds, and the output file contains the following
noncommutative group of order 6.
</P><PRE CLASS="verbatim">    ======================= Model #1 at 1.13 seconds:
    e: 0
    a: 1
    b: 2
    *:   | 0 1 2 3 4 5
       --+------------
       0 | 0 1 2 3 4 5
       1 | 1 0 3 2 5 4
       2 | 2 4 0 5 1 3
       3 | 3 5 1 4 0 2
       4 | 4 2 5 0 3 1
       5 | 5 3 4 1 2 0
       
    g:     0 1 2 3 4 5
       ---------------
           0 1 2 4 3 5
</PRE><P>
Hmmm, very interesting: I wonder what happens if we add <I>x</I>*<I>x</I>=<I>e</I>
to our theory.</P><!--TOC section How to Tell MACE What to Do-->
<H2 CLASS="section"><!--SEC ANCHOR --><A NAME="htoc3">3</A>&#XA0;&#XA0;How to Tell MACE What to Do</H2><!--SEC END --><P>Three kinds of input determine how MACE works.
First, the clauses or formulas in the input file specify
the theory for which you seek a model.
Second, special commands in the input file put
constraints on the models.
Third, command-line options give general constraints
on the search.</P><!--TOC subsection The Formulas-->
<H3 CLASS="subsection"><!--SEC ANCHOR --><A NAME="htoc4">3.1</A>&#XA0;&#XA0;The Formulas</H3><!--SEC END --><P>MACE reads the input (from stdin) and takes formulas and clauses from
the lists <TT>usable</TT>, <TT>sos</TT>, <TT>demodulators</TT>, and 
<TT>passive</TT> as its basic theory.<SUP><A NAME="text1" HREF="#note1">1</A></SUP>
Like Otter, MACE immediately transforms any first-order formulas
to clauses.</P><P>MACE is a bit more restrictive than Otter in the language it accepts,
and it interprets some symbols differently. See Section&#XA0;<A HREF="#language">4</A>.</P><!--TOC subsection Constraints in the Input-->
<H3 CLASS="subsection"><!--SEC ANCHOR --><A NAME="htoc5">3.2</A>&#XA0;&#XA0;Constraints in the Input</H3><!--SEC END --><P>Constraints are specified in an optional
list <TT>mace_constraints</TT> in the input file.<SUP><A NAME="text2" HREF="#note2">2</A></SUP>
(If you give Otter an input file containing a <TT>mace_constraints</TT> list,
Otter ignores it.)
Two kinds of constraint are accepted:
assignments for the models and
properties of relations or functions.
Here is an example list that shows all of the types of constraint.
</P><PRE CLASS="verbatim">    list(mace_constraints).
      assign(e, 0).                   % constant symbol
      assign(g(2), 1).                % function symbol
      assign(3*4, 2).                 % function symbol
      assign(P(1), T).                % relation symbol
      assign(Q(0,3), F).              % relation symbol
      property(same(_,_), equality).
      property(lt(_,_), order).
      property(g(_), bijection).
      property(_*_, quasigroup).
    end_of_list.
</PRE><P>
The assignments simply give function values or relation values
for particular members of the domain.<SUP><A NAME="text3" HREF="#note3">3</A></SUP>
Members of the domain
are always named 0, 1, &#X2026;, <I>n</I>&#X2212;1, where <I>n</I> is the domain size.
The Boolean constants (relation values) are named <TT>T</TT> and
<TT>F</TT>. Note that assigning values to constants can also
be done with the <TT>-c</TT> command-line option (see the next subsection).
The following properties of function and relation symbols can be specified
in the <TT>mace_constraints</TT> list.
</P><DL CLASS="description"><DT CLASS="dt-description">
</DT><DD CLASS="dd-description"><TT>equality</TT><BR>
This applies to binary relation symbols.
It is necessary only if a nonstandard equality symbol is being used,
because any binary relation recognized by Otter as an equality symbol
is also recognized by MACE as an equality symbol.
See Section&#XA0;<A HREF="#syntax">4.2</A>.
</DD><DT CLASS="dt-description"></DT><DD CLASS="dd-description"><TT>order</TT><BR>
This applies to binary relation symbols.
It is necessary only if a nonstandard order symbol is being used.
MACE (but not Otter) automatically recognizes binary &lt; as
an order relation.
The &#X201C;order&#X201D; is the obvious order on
the members of the domain: 0&lt;1&lt;&#X2026;&lt;<I>n</I>&#X2212;1.
See the example input files
<TT>ordered_semi.in</TT> and <TT>cd.in</TT>
included in the MACE distribution package.
</DD><DT CLASS="dt-description"></DT><DD CLASS="dd-description"><TT>bijection</TT><BR>
This applies to unary function symbols.
The list of function values is a permutation of the domain.
</DD><DT CLASS="dt-description"></DT><DD CLASS="dd-description"><TT>quasigroup</TT><BR>
This applies to binary function symbols.
If you write down the table for a finite quasigroup,
each row and each column is a permutation of the
domain.
</DD></DL><!--TOC subsection Command-Line Options-->
<H3 CLASS="subsection"><!--SEC ANCHOR --><A NAME="htoc6">3.3</A>&#XA0;&#XA0;Command-Line Options</H3><!--SEC END --><DL CLASS="list"><DT CLASS="dt-list">

<TT>-n </TT><TT><I>n</I></TT></DT><DD CLASS="dd-list">
This gives the starting domain size for the search.
The default value is 2. If you also give an <TT>-N</TT> option,
MACE will iterate domain sizes up through the <TT>-N</TT>
value.
Otherwise, MACE will search only for the <TT>-n</TT> value.
For example,
<DIV CLASS="center">
<TABLE CELLSPACING=6 CELLPADDING=0><TR><TD CLASS="hbar" COLSPAN=3></TD></TR>
<TR><TD ALIGN=center NOWRAP>Options</TD><TD ALIGN=center NOWRAP>&#XA0;</TD><TD ALIGN=center NOWRAP>Search</TD></TR>
<TR><TD CLASS="hbar" COLSPAN=3></TD></TR>
<TR><TD ALIGN=center NOWRAP><TT>-n4</TT></TD><TD ALIGN=center NOWRAP>&nbsp;</TD><TD ALIGN=center NOWRAP>4</TD></TR>
<TR><TD ALIGN=center NOWRAP><TT>-N6</TT></TD><TD ALIGN=center NOWRAP>&nbsp;</TD><TD ALIGN=center NOWRAP>2,3,4,5,6</TD></TR>
<TR><TD ALIGN=center NOWRAP><TT>-n4 -N6</TT></TD><TD ALIGN=center NOWRAP>&nbsp;</TD><TD ALIGN=center NOWRAP>4,5,6</TD></TR>
<TR><TD CLASS="hbar" COLSPAN=3></TD></TR>
</TABLE>
</DIV>
</DD><DT CLASS="dt-list"><TT>-N </TT><TT><I>n</I></TT></DT><DD CLASS="dd-list">
This gives the ending domain size for the search.
The default is the value of the <TT>-n</TT> option.
</DD><DT CLASS="dt-list"><TT>-c</TT></DT><DD CLASS="dd-list">
This says that constants in the input should be assigned
unique elements of the domain. If the number of constants
in the input is greater than the domain size <I>n</I>, the first
<I>n</I> constants are given values, and the rest are unconstrained.
This is a useful option because it eliminates lots
of isomorphism from the search. But it can block all models,
especially when used with other constraints.
</DD><DT CLASS="dt-list"><TT>-p</TT></DT><DD CLASS="dd-list">
(Lower case.) This option tells MACE to print models in a nice
tabular form as they are found. This format is meant
for human consumption.
</DD><DT CLASS="dt-list"><TT>-P</TT></DT><DD CLASS="dd-list">
(Upper case.) This option tells MACE to print models in an easily parsable
form. This format has an Otter-like syntax and can be read by
most Prolog systems.
</DD><DT CLASS="dt-list"><TT>-I</TT></DT><DD CLASS="dd-list">
This option tells MACE to print models in IVY form.
This format is a Lisp S-expression and is meant to be read
by IVY&#XA0;[<A HREF="#ivy"></A>], our proof and model checker.
</DD><DT CLASS="dt-list"><TT>-m </TT><TT><I>n</I></TT></DT><DD CLASS="dd-list">
This tells MACE to stop after finding <I>n</I> models. The default is 1.
</DD><DT CLASS="dt-list"><TT>-t </TT><TT><I>n</I></TT></DT><DD CLASS="dd-list">
This tells MACE to stop after about <I>n</I> seconds. The default is unlimited.
<EM>MACE ignores any </EM><EM><TT>assign(max_seconds, n)</TT></EM><EM> commands
that might be in the input file. Such commands are used by Otter only.</EM>
</DD><DT CLASS="dt-list"><TT>-k </TT><TT><I>n</I></TT></DT><DD CLASS="dd-list">
This tells MACE to stop if it tries to allocate more than <I>n</I>
kilobytes ofmemory. The default is 48000 (about 48 megabytes).
<EM>MACE ignores any </EM><EM><TT>assign(max_mem, n)</TT></EM><EM> commands
that might be in the input file. Such commands are used by Otter only.</EM>
</DD><DT CLASS="dt-list"><TT>-x</TT></DT><DD CLASS="dd-list">
This is a special-purpose constraint designed to reduce
isomorphism in quasigroup problems.
It applies only to binary function <TT>f</TT>.
See&#XA0;[<A HREF="#dp-quasi"></A>].
</DD><DT CLASS="dt-list"><TT>-h</TT></DT><DD CLASS="dd-list">
This tells MACE to print a summary of these command-line options.
</DD></DL><!--TOC section Language Accepted by MACE-->
<H2 CLASS="section"><!--SEC ANCHOR --><A NAME="htoc7">4</A>&#XA0;&#XA0;Language Accepted by MACE</H2><!--SEC END --><P> <A NAME="language"></A></P><P>MACE accepts nearly the same input as Otter.
First we list the main differences from Otter; then we give a short
review of Otter&#X2019;s language.</P><!--TOC subsection Differences from Otter&#X2019;s Language-->
<H3 CLASS="subsection"><!--SEC ANCHOR --><A NAME="htoc8">4.1</A>&#XA0;&#XA0;Differences from Otter&#X2019;s Language</H3><!--SEC END --><OL CLASS="enumerate" type=1><LI CLASS="li-enumerate">
MACE does not accept function symbols with arity
greater than three or relation symbols with arity greater
than four.
</LI><LI CLASS="li-enumerate">MACE does not allow symbols with different arities,
for example, <TT>f(f,x)</TT>.
</LI><LI CLASS="li-enumerate">MACE does not allow a symbol to be used as both a
relation symbol and a function symbol.
</LI><LI CLASS="li-enumerate">MACE ignores answer literals. In fact, MACE removes all
answer literals before it starts looking for models.
</LI><LI CLASS="li-enumerate">The natural numbers <TT>0,1,2,&#X2026;</TT> are ordinary
constants to Otter, but they have special meanings to MACE.
In particular, MACE interprets them as elements of the domain.
If you ask MACE to look for a model of size <I>n</I>, and there are constants
&#X2265; <I>n</I> in the input, MACE will get confused and quit with an error message.
</LI><LI CLASS="li-enumerate">On the other hand,
the evaluable (&#X201C;dollar&#X201D;) functions and relations, for example <TT>$SUM</TT>
and <TT>$LT</TT>, have special meanings to Otter, but they are treated by
MACE as ordinary symbols. As a result, an input file containing
evaluable symbols can produce both a refutation with Otter and a model
with MACE. Here is an example.
</LI></OL><DIV CLASS="center">

<TABLE BORDER=1 CELLPADDING=1 CELLSPACING=0><TR><TD ALIGN="left"><PRE CLASS="verbatim">set(hyper_res).
list(sos).
  -P(x) | P($SUM(x,x)).
  P(1).
  -P(2).
end_of_list.
</PRE></TD></TR>
</TABLE>
</DIV><!--TOC subsection A Quick Review of the Language Otter Accepts-->
<H3 CLASS="subsection"><!--SEC ANCHOR --><A NAME="htoc9">4.2</A>&#XA0;&#XA0;A Quick Review of the Language Otter Accepts</H3><!--SEC END --><P> <A NAME="syntax"></A></P><P>See the Otter manual&#XA0;[<A HREF="#otter3"></A>] for a thorough description of the language.</P><!--TOC paragraph Clauses vs.&#XA0;Formulas.-->
<H5 CLASS="paragraph"><!--SEC ANCHOR -->Clauses vs.&#XA0;Formulas.</H5><!--SEC END --><P> You can use either clauses
or formulas. (Most people use clauses. If you use formulas,
they are immediately translated to clauses.) Here are some
corresponding examples.
</P><PRE CLASS="verbatim">    list(usable).           % clauses
      -P(x) | -Q(x) | R(x).
      -P(x) | -Q(x) | S(x).
      f(e,x) = x.
      f(g(x),x) = e.
    end_of_list.

    formula_list(usable).   % formulas
      all x (P(x) &amp; Q(x) -&gt; R(x) &amp; S(x)).
      exists e ((all x (f(e,x) = x)) &amp;
                (all x exists y (f(y,x) = e))).
    end_of_list.
</PRE><!--TOC paragraph Variables vs.&#XA0;Constants in Clauses.-->
<H5 CLASS="paragraph"><!--SEC ANCHOR -->Variables vs.&#XA0;Constants in Clauses.</H5><!--SEC END --><P>
Clauses do not have explicit quantifiers, so we need a rule to
distinguish variables from constants. The default rule is that
symbols starting with <TT>u</TT> through <TT>z</TT> are variables. If
the command <TT>set(prolog_style_variables)</TT> is in effect, symbols
starting with upper-case letters are variables.</P><!--TOC paragraph Equality Symbols.-->
<H5 CLASS="paragraph"><!--SEC ANCHOR -->Equality Symbols.</H5><!--SEC END --><P>
How do we recognize binary relations as equality relations? The
default rule is that the symbol <TT>=</TT> and symbols matching the
pattern [<TT>Ee</TT>][<TT>Qq</TT>].* are equality symbols. If the
input contains the command <TT>set(tptp_eq)</TT>, then <TT>equal</TT> is
the one and only equality symbol.</P><!--TOC paragraph Infix Notation.-->
<H5 CLASS="paragraph"><!--SEC ANCHOR -->Infix Notation.</H5><!--SEC END --><P>
One can declare binary symbols to be infix and to have a precedence
and associativity so that some parentheses can be omitted. Many symbols
such as <TT>=</TT> and <TT>*</TT> have built-in declarations.</P><!--TOC section How MACE Works-->
<H2 CLASS="section"><!--SEC ANCHOR --><A NAME="htoc10">5</A>&#XA0;&#XA0;How MACE Works</H2><!--SEC END --><P>The methods used by MACE are described in detail in&#XA0;[<A HREF="#dp-quasi"></A>].
Here is a summary.</P><P>For a given domain size, MACE transforms the (first-order) input into
an equivalent propositional problem. This is possible because,
for a fixed finite domain, the first-order problem is decidable.
The propositional problem is then given to a DPLL
(Davis-Putnam-Loveland-Logeman) procedure. If satisfiability is
detected, the propositional model is transformed into a first-order
model of the original problem.</P><P>Consider the following input file.
</P><DIV CLASS="center">

<TABLE BORDER=1 CELLPADDING=1 CELLSPACING=0><TR><TD ALIGN="left"><PRE CLASS="verbatim">list(usable).
  even(a).
  -even(x) | even(s(s(x))).
  -even(s(a)).
end_of_list.
</PRE></TD></TR>
</TABLE>
</DIV><P>
MACE first flattens the clauses into a relational form.
This step involves replacing each <I>n</I>-ary function with an <I>n</I>+1-ary relation.
MACE&#X2019;s output for this example contains something like
</P><PRE CLASS="verbatim">    Processing clause: -a(v0) | even(v0).
    Processing clause: -s(v0,v1) | -s(v1,v2) | -even(v0) | even(v2).
    Processing clause: -a(v0) | -s(v0,v1) | -even(v1).
</PRE><P>
If we ask for models of size 3, MACE generates propositional
clauses corresponding to all instances of the transformed clauses
over the set {0,1,2}. The output also contains the statements
</P><PRE CLASS="verbatim">    Function s/2 well-defined and closed.
    Function a/1 well-defined and closed.
</PRE><P>
which indicate that MACE has generated
propositional clauses asserting that the new <I>n</I>+1-ary relations
are functions. The DPLL procedure finds a model of the
set of propositional clauses, and the propositional model
is transformed into the following first-order model.
</P><PRE CLASS="verbatim">    a: 2        even:  0 1 2          s:     0 1 2
                   ---------             ---------
                       T F T                 0 0 1
</PRE><!--TOC paragraph Scalability.-->
<H5 CLASS="paragraph"><!--SEC ANCHOR -->Scalability.</H5><!--SEC END --><P> Unfortunately, this method does not scale well
as the domain increases or as the size of clauses increases.
Consider a distributivity axiom, <I>x</I> * (<I>y</I> + <I>z</I>) = (<I>x</I> + <I>y</I>) * (<I>x</I> + <I>z</I>).
The transformation to relational form produces the following two clauses.
</P><PRE CLASS="verbatim">    -+(v0,v1,v2) -+(v0,v3,v4) -*(v4,v2,v5) -+(v3,v1,v6) *(v0,v6,v5)
    -+(v0,v1,v2) -+(v0,v3,v4) *(v4,v2,v5) -+(v3,v1,v6) -*(v0,v6,v5)
</PRE><P>
For a domain of 6, each of these (7-variable) clauses produces 6<SUP>7</SUP>=279,936
propositional clauses. MACE can usually handle this many clauses,
but it&#X2019;s hard to fight exponential behavior. The program SEM&#XA0;[<A HREF="#sem"></A>]
is usually better than MACE for large clauses or large domains.</P><!--TOC section Differences from Previous Versions-->
<H2 CLASS="section"><!--SEC ANCHOR --><A NAME="htoc11">6</A>&#XA0;&#XA0;Differences from Previous Versions</H2><!--SEC END --><P> <A NAME="history"></A></P><P>Major changes from earlier versions of MACE are listed here.</P><OL CLASS="enumerate" type=1><LI CLASS="li-enumerate">
Previous versions of MACE called Otter to parse the input
and to produce an intermediate form that was given to a program
named ANLDP. MACE 2.0 is self-contained, making it easier to install and run.
</LI><LI CLASS="li-enumerate">Previous versions of MACE worked for a fixed domain size, and
there was a separate script (mace-loop) to iterate through
domain sizes and calling MACE.
</LI><LI CLASS="li-enumerate">Previous versions of MACE used Otter&#X2019;s <TT>passive</TT> list
for constraints (assignments and properties). MACE 2.0 uses the new
list <TT>mace_constraints</TT> for that purpose; clauses in <TT>passive</TT>
are now taken as part of the theory.
</LI><LI CLASS="li-enumerate">MACE 2.0 allows answer literals in the clauses. (Answer literals
are removed by MACE before the search for models.)
</LI><LI CLASS="li-enumerate">Previous versions of MACE could handle sorted logic (with
disjoint domains). MACE 2.0 cannot. Most of the code for
sorted logic is still in place, so it is possible that
future versions will handle sorted logic. <P>Sorted logic can sharply cut down the search time. Consider
a domain of size 12 that can be partitioned into 8 and 4.
A 2-variable relational clause, with one variable for each sort,
produces 144 propositional clauses with unsorted logic
and 32 clauses in the sorted case.
Let us know if you need sorted logic.
</P></LI><LI CLASS="li-enumerate">Previous versions of MACE had a checkpointing feature whereby
the state of the search was periodically backed up to a file,
and the search could be resumed from one of those states.
MACE 2.0 does not have this feature.
</LI></OL><!--TOC section Calling MACE From Other Programs-->
<H2 CLASS="section"><!--SEC ANCHOR --><A NAME="htoc12">7</A>&#XA0;&#XA0;Calling MACE From Other Programs</H2><!--SEC END --><P>MACE returns an exit code when it terminates.
This makes it convenient to call MACE from other programs.
Here is a list of MACE&#X2019;s exit codes.
(This list changes from time to time; the current
list can be found in the source file <TT>Mace.h</TT>.)
</P><DL CLASS="description"><DT CLASS="dt-description">
</DT><DD CLASS="dd-description"><TT>11 (ABEND_EXIT)</TT>
This usually indicates an error in the
input (not all input errors are covered by
<TT>INPUT_ERROR_EXIT</TT> below).
Occasionally it is caused by a bug in MACE.
When you get this exit code, look in the output for an error message.
</DD><DT CLASS="dt-description"></DT><DD CLASS="dd-description"><TT>12 (UNSATISFIABLE_EXIT)</TT>
MACE completed its search and determined that
no models exist within the given domain size(s) and other constraints.
<EM>It does not mean that the input clauses are unsatisfiable.</EM>
</DD><DT CLASS="dt-description"></DT><DD CLASS="dd-description"><TT>13 (MAX_SECONDS_EXIT)</TT>
MACE terminated because of the time limit given on
command line (with <TT>-t</TT>).
</DD><DT CLASS="dt-description"></DT><DD CLASS="dd-description"><TT>14 (MAX_MEM_EXIT)</TT>
MACE terminated because of the memory limit given
on the command line (with <TT>-k</TT>).
</DD><DT CLASS="dt-description"></DT><DD CLASS="dd-description"><TT>15 (MAX_MODELS_EXIT)</TT>
MACE terminated because it found the number of
models requested on the command line (with <TT>-m</TT>).
</DD><DT CLASS="dt-description"></DT><DD CLASS="dd-description"><TT>16 (ALL_MODELS_EXIT)</TT>
MACE completed its search and found all models
(at least one) within the given constraints.
</DD><DT CLASS="dt-description"></DT><DD CLASS="dd-description"><TT>17 (SIGINT_EXIT)</TT>
MACE terminated because it received the interrupt signal.
</DD><DT CLASS="dt-description"></DT><DD CLASS="dd-description"><TT>18 (SEGV_EXIT)</TT>
MACE crashed.
</DD><DT CLASS="dt-description"></DT><DD CLASS="dd-description"><TT>19 (INPUT_ERROR_EXIT)</TT>
Errors were found in the input.
The output file should point to the error(s).
</DD></DL><P>Say we have a list of equations containing a binary function
symbol <TT>f</TT>, and we wish to remove the equations
that have a noncommutative model of size &#X2264; 4.
If we put the equations in a file, with one equation on
each line, for example,
</P><DIV CLASS="center">

<TABLE BORDER=1 CELLPADDING=1 CELLSPACING=0><TR><TD ALIGN="left"><PRE CLASS="verbatim">f(f(x,f(f(z,x),x)),f(z,f(y,x))) = z.
f(f(f(x,f(z,x)),x),f(z,f(y,x))) = z.
f(f(f(f(y,x),z),x),f(f(u,y),x)) = x.
f(f(f(f(y,x),z),x),f(f(y,u),x)) = x.
</PRE></TD></TR>
</TABLE>
</DIV><P>
we can write a simple program to loop through the
equations, calling MACE for each and printing those
that have no noncommutative models of size &#X2264; 4.
Here is an example Perl program that does the job.
</P><DIV CLASS="center">
<FONT SIZE=2>
</FONT><TABLE BORDER=1 CELLPADDING=1 CELLSPACING=0><TR><TD ALIGN="left"><PRE CLASS="verbatim"><FONT SIZE=2>#!/usr/local/bin/perl5

$mace = "/home/mccune/bin-linux/mace"; # MACE binary
$unsatisfiable_exit = 12;  # exit code of interest
$input = "/tmp/mace$$";    # temporary input file

while ($equation = &lt;STDIN&gt;) {
    open(FH, "&gt;$input") || die "Cannot open file $input";
    print FH "list(usable). $equation f(0,1)!=f(1,0). end_of_list.\n";
    close(FH);
    $rc = system("$mace -N4 &lt; $input &gt; /dev/null 2&gt; /dev/null");
    $rc = $rc / 256;    # This gets the actual exit code.
    if ($rc == $unsatisfiable_exit) { print $equation; }
}
system("/bin/rm $input");
</FONT></PRE></TD></TR>
</TABLE>
</DIV><P>
If our data file is named <TT>identities</TT> and our Perl script
is named <TT>commute4_filter</TT>, then the command</P><PRE CLASS="verbatim">    % commute4_filter &lt; identities &gt; candidates
</PRE><P>
will remove two of the four equations within a few seconds.</P><!--TOC section The ANLDP Propositional Decision Procedure-->
<H2 CLASS="section"><!--SEC ANCHOR --><A NAME="htoc13">8</A>&#XA0;&#XA0;The ANLDP Propositional Decision Procedure</H2><!--SEC END --><P> <A NAME="anldp"></A></P><P>If you have a propositional (SAT) problem in conjunctive normal
form, you can call MACE&#X2019;s DPLL procedure directly with the
program ANLDP.
ANLDP is included in the MACE distribution package.</P><P>Input to ANLDP is a sequence of integers (no comments are allowed).
The propositional variables are <TT>1,2,3,&#X2026;</TT>.
Positive integers are positive literals,
negative integers are negative literals,
and 0 marks the ends of clauses.
For example, here is an (unsatisfiable) input consisting of
four 2-literal clauses.
</P><PRE CLASS="verbatim">    1 2 0
    1 -2 0
    -1 2 0
    -1 -2 0
</PRE><P>
The command-line options of ANLDP are a subset of MACE&#X2019;s:
</P><DL CLASS="list"><DT CLASS="dt-list">

<TT>-p</TT></DT><DD CLASS="dd-list">
(Lower case.) This tells ANLDP to print models as they are found.
</DD><DT CLASS="dt-list"><TT>-m </TT><TT><I>n</I></TT></DT><DD CLASS="dd-list">
This tells ANLDP to stop after finding <I>n</I> models. The default is 1.
</DD><DT CLASS="dt-list"><TT>-t </TT><TT><I>n</I></TT></DT><DD CLASS="dd-list">
This tells ANLDP to stop after about <I>n</I> seconds. The default is unlimited.
</DD><DT CLASS="dt-list"><TT>-k </TT><TT><I>n</I></TT></DT><DD CLASS="dd-list">
This tells ANLDP to stop if it tries to allocate more than <I>n</I> kilobytes
of memory. The default is 48000 (about 48 megabytes).
</DD><DT CLASS="dt-list"><TT>-s</TT></DT><DD CLASS="dd-list">
This tells ANLDP to perform unit subsumption as it searches.
(Unit subsumption is always performed on the input.)
When ANLDP gets a new unit (by splitting or by unit propagation),
two operations are ordinarily performed: (1) unit resolution, to
remove complementary literals from all clauses, and (2) unit
subsumption, to mark as subsumed all clauses containing the
unit as a literal. Because of our data structures, unit subsumption
nearly always costs more time than it saves. But this option
allows you to use unit subsumption if you wish.
</DD></DL><P>ANLDP is an implementation of the Davis-Putnam-Loveland-Logeman
procedure. Efficient data structures and algorithms are used,
but the procedure is otherwise standard.
When the time comes to select the next propositional variable
for splitting, ANLDP simply takes the first variable of the first shortest
positive clause.
Details of the implementation can be found in&#XA0;[<A HREF="#dp-quasi"></A>].</P><!--BEGIN NOTES document-->
<HR CLASS="footnoterule"><DL CLASS="thefootnotes"><DT CLASS="dt-thefootnotes">
<A NAME="note1" HREF="#text1">1</A></DT><DD CLASS="dd-thefootnotes">
One can argue that the hot list should also be considered as
part of the basic theory, because Otter uses the hot list to
make inferences. MACE ignores the hot list, however, because hot list
clauses almost always occur also in usable or sos, and MACE
suffers if it gets duplicate clauses. I suppose MACE could
get around this by doing a subsumption check.

</DD><DT CLASS="dt-thefootnotes"><A NAME="note2" HREF="#text2">2</A></DT><DD CLASS="dd-thefootnotes">
Previous versions of MACE used the <TT>passive</TT> list for constraints.

</DD><DT CLASS="dt-thefootnotes"><A NAME="note3" HREF="#text3">3</A></DT><DD CLASS="dd-thefootnotes">
Why not place assignments in with the clauses that specify the theory?
This can be done, but such assignments might not make sense if
the input is also being used for Otter.

</DD></DL>
<!--END NOTES-->
<!--CUT END -->
<!--HTMLFOOT-->
<!--ENDHTML-->
<!--FOOTER-->
<HR SIZE=2><BLOCKQUOTE CLASS="quote"><EM>This document was translated from L<sup>A</sup>T<sub>E</sub>X by
</EM><A HREF="http://hevea.inria.fr/index.html"><EM>H</EM><EM><FONT SIZE=2><sup>E</sup></FONT></EM><EM>V</EM><EM><FONT SIZE=2><sup>E</sup></FONT></EM><EM>A</EM></A><EM>.</EM></BLOCKQUOTE></BODY>
</HTML>
mace2 3.3f-1.1 / usr / share / doc / mace2 / mace2.html
