ANL/MCS-TM-249
MACE 2.0 Reference Manual and Guide
by
William McCune
Mathematics and Computer Science Division
Technical Memorandum No. 249
May 2001
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.
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.
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.
MACE 2.0 Reference Manual and GuideWilliam McCune |
Abstract: 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.
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 [, ], 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.
MACE has been used for many applications including quasigroup existence problems [], ortholattice problems [], and lattice and Boolean algebra problems [, ]. Other successful programs that look for finite models of first-order statements are SEM [] and FINDER []. A related class of programs can produce finite models when the search for a refutation fails. Examples of these are SATCHMO [] and MGTP [].
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 8). Section 6 gives differences between MACE 2.0 and previous versions. The MACE Web site is http://www.mcs.anl.gov/AR/mace.
Say you’ve just invented group theory by writing down the following three axioms,
|
and you are wondering whether all groups are commutative. You prepare the following input file, named group.in.
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.
|
Now you give the input file to Otter to search for a proof (actually a refutation).
% otter < group.in > group.out
and to MACE to look for a countermodel (actually a model) of size 4, as follows.
% mace -n4 -p -c < group.in > group4.out
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
% mace -n6 -p -c < group.in > group6.out
succeeds, and the output file contains the following noncommutative group of order 6.
======================= 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
Hmmm, very interesting: I wonder what happens if we add x*x=e to our theory.
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.
MACE reads the input (from stdin) and takes formulas and clauses from the lists usable, sos, demodulators, and passive as its basic theory.1 Like Otter, MACE immediately transforms any first-order formulas to clauses.
MACE is a bit more restrictive than Otter in the language it accepts, and it interprets some symbols differently. See Section 4.
Constraints are specified in an optional list mace_constraints in the input file.2 (If you give Otter an input file containing a mace_constraints 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.
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.
The assignments simply give function values or relation values for particular members of the domain.3 Members of the domain are always named 0, 1, …, n−1, where n is the domain size. The Boolean constants (relation values) are named T and F. Note that assigning values to constants can also be done with the -c command-line option (see the next subsection). The following properties of function and relation symbols can be specified in the mace_constraints list.
| Options | Search | |
| -n4 | 4 | |
| -N6 | 2,3,4,5,6 | |
| -n4 -N6 | 4,5,6 | |
MACE accepts nearly the same input as Otter. First we list the main differences from Otter; then we give a short review of Otter’s language.
set(hyper_res).
list(sos).
-P(x) | P($SUM(x,x)).
P(1).
-P(2).
end_of_list.
|
See the Otter manual [] for a thorough description of the language.
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.
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) & Q(x) -> R(x) & S(x)).
exists e ((all x (f(e,x) = x)) &
(all x exists y (f(y,x) = e))).
end_of_list.
Clauses do not have explicit quantifiers, so we need a rule to distinguish variables from constants. The default rule is that symbols starting with u through z are variables. If the command set(prolog_style_variables) is in effect, symbols starting with upper-case letters are variables.
How do we recognize binary relations as equality relations? The default rule is that the symbol = and symbols matching the pattern [Ee][Qq].* are equality symbols. If the input contains the command set(tptp_eq), then equal is the one and only equality symbol.
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 = and * have built-in declarations.
The methods used by MACE are described in detail in []. Here is a summary.
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.
Consider the following input file.
list(usable).
even(a).
-even(x) | even(s(s(x))).
-even(s(a)).
end_of_list.
|
MACE first flattens the clauses into a relational form. This step involves replacing each n-ary function with an n+1-ary relation. MACE’s output for this example contains something like
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).
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
Function s/2 well-defined and closed.
Function a/1 well-defined and closed.
which indicate that MACE has generated propositional clauses asserting that the new n+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.
a: 2 even: 0 1 2 s: 0 1 2
--------- ---------
T F T 0 0 1
Unfortunately, this method does not scale well as the domain increases or as the size of clauses increases. Consider a distributivity axiom, x * (y + z) = (x + y) * (x + z). The transformation to relational form produces the following two clauses.
-+(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)
For a domain of 6, each of these (7-variable) clauses produces 67=279,936 propositional clauses. MACE can usually handle this many clauses, but it’s hard to fight exponential behavior. The program SEM [] is usually better than MACE for large clauses or large domains.
Major changes from earlier versions of MACE are listed here.
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.
MACE returns an exit code when it terminates. This makes it convenient to call MACE from other programs. Here is a list of MACE’s exit codes. (This list changes from time to time; the current list can be found in the source file Mace.h.)
Say we have a list of equations containing a binary function symbol f, and we wish to remove the equations that have a noncommutative model of size ≤ 4. If we put the equations in a file, with one equation on each line, for example,
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.
|
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 ≤ 4. Here is an example Perl program that does the job.
#!/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 = <STDIN>) {
open(FH, ">$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 < $input > /dev/null 2> /dev/null");
$rc = $rc / 256; # This gets the actual exit code.
if ($rc == $unsatisfiable_exit) { print $equation; }
}
system("/bin/rm $input");
|
If our data file is named identities and our Perl script is named commute4_filter, then the command
% commute4_filter < identities > candidates
will remove two of the four equations within a few seconds.
If you have a propositional (SAT) problem in conjunctive normal form, you can call MACE’s DPLL procedure directly with the program ANLDP. ANLDP is included in the MACE distribution package.
Input to ANLDP is a sequence of integers (no comments are allowed). The propositional variables are 1,2,3,…. 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.
1 2 0
1 -2 0
-1 2 0
-1 -2 0
The command-line options of ANLDP are a subset of MACE’s:
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 [].
This document was translated from LATEX by HEVEA.