| Figure 1: Searching for First-Order Models |
A Davis-Putnam Program |
Abstract: This document describes the implementation and use of a Davis-Putnam procedure for the propositional satisfiability problem. It also describes code that takes statements in first-order logic with equality and a domain size n then searches for models of size n. The first-order model-searching code transforms the statements into set of propositional clauses such that the first-order statements have a model of size n if and only if the propositional clauses are satisfiable. The propositional set is then given to the Davis-Putnam code; any propositional models that are found can be translated to models of the first-order statements. The first-order model-searching program accepts statements only in a flattened relational clause form without function symbols. Additional code was written to take input statements in the language of Otter 3.0 and produce the flattened relational form. The program was successfully applied to several open questions on the existence of orthogonal quasigroups.
The Davis-Putnam procedure is widely regarded as the best method for deciding the satisfiability of a set of propositional clauses. I’ll assume that the reader is familiar with it. I list here some features of our implementation.
The data structures for clauses and for propositional variables and the algorithms are similar to the ones Mark Stickel uses in LDPP [8].
Variables are integers ≥ 1. Associated with the set of variables is an array, indexed by the variables, of variable structures. Each variable structure contains the following fields.
value.
The current value (true, false, or unassigned) of the variable.
enqueued_value.
A field to speed the bottleneck operation of unit propagation (see below).
pos_occ.
A list of pointers to clauses that contain the
variable in a positive literal.
neg_occ.
A list of pointers to clauses that contain the
variable in a negative literal.
Each clause contains the following fields.
pos.
A list of variables representing positive literals.
neg.
A list of variables representing negative literals.
active_pos.
The number of positive literals that have not been resolved away.
active_neg.
The number of negative literals that have not been resolved away.
subsumer.
A field set to the responsible variable if the clause has been
inactivated by subsumption.
When a variable is assigned a value, say true, by splitting or during
unit propagation, unit resolution is performed by traversing the
neg_occ list of the variable: for each clause that has not
been subsumed, the active_neg field is simply decremented by 1.
If active_pos+active_neg becomes 0, the empty clause has been
found and backtracking occurs. If active_pos+active_neg
becomes 1, the new unit clause is queued for unit propagation. In
addition, if subsumption is enabled, (back) subsumption is performed
by traversing the
pos_occ list of the variable: for each clause that is not
already subsumed, the subsumer field is set to the variable.
Variables must be unassigned during backtracking, and the process is
essentially the reverse of assignment.
A split causes an assignment. The unit propagation queue is then
processed (causing further assignments and possibly more units to be
queued) until empty or the empty clause is found. Each split
typically causes many assignments, so unit propagation must be done
efficiently. To avoid duplicates in the queue, and to detect
the empty clause during the enqueue operation rather than during
assignment, we set the field enqueued_value of the variable
when the corresponding literal is enqueued. That way we can quickly
tell whether a literal or its complement is already in the queue.
If the set of input clauses contains any units, unit propagation is applied. During assignment, back subumption is always applied, because assignments made during this phase are never undone.
The variable selected for splitting is the first literal in the first, shortest nonsubsumed positive clause. After the unit preprocessing, pointers to all of the non-Horn clauses (i.e., clauses with two or more positive literals) are collected into a list. In order to select a variable for splitting, the list is simply traversed. Subsumed clauses must be ignored; if subsumption is enabled, the subsumer field is checked; otherwise the clause is scanned for a literal with value true. (If all clauses in the list are subsumed, a model has been found.)
The pigeonhole problems are a set of artificial propositional problems that are used to test the efficiency of propositional theorem provers. See the sample input files that come with ANL-DP for examples. Table 1 lists the performance of ANL-DP on several instances of the pigeonhole problems. The jobs were run on a SPARC 2.
Propositional input to ANL-DP is a sequence of clauses.
(See Sec. 2.2 for input to the first-order model-searching program.)
Literals are nonzero integers (negative integers represent negative
literals), and each clause is terminated with 0.
(Hence, the entire input is just a sequence of integers.)
The input is taken from stdin (the standard input).
ANL-DP accepts the following command-line options.
-s.
Perform subsumption. (Subsumption is always performed during unit preprocessing.)
-p.
Print models as they are found.
-m n.
Stop when the n-th model is found.
-t n.
Stop after n seconds.
-k n.
Allocate at most n kbytes for storage of clauses.
-x n.
Quasigroup experiment n. See Section 2.5.
-B file.
Backup assignments to a file.
-b n.
Backup assignments every n seconds.
-R file.
Restore assignments from a file. The file typically contains just the
last line of a backup file. Other input, in particular the clauses,
must be given exactly as in the original search.
-n n.
This option is used for first-order model searches. The parameter n
specifies the domain size, and its presence tells the program to
read first-order flattened relational input clauses instead of propositional
clauses.
The first practical program for searching for small models of first-order statements was FINDER [6]. Another model-searching program is MGTP [7], which uses a somewhat different approach. The third class of programs, including LDPP [8], SATO [8], and the one described here, are based on Davis-Putnam procedures. None of these programs is clearly better than the others, and each has answered open questions about quasigroups (see Sec. 2.5).
The Davis-Putnam approach is quite elegant, because the computational engine—the Davis-Putnam code—is in no way tailored to first-order model searching. First-order clauses and a domain size n are input; then ground instances (over the domain) of the first-order clauses are generated and given to the Davis-Putnam code. Any propositional models that are found can be easily translated to first-order models (e.g., an n× n table for a binary function).
The steps, which are summarized in Figure 1, are as follows.
Figure 1: Searching for First-Order Models
¬ G(x,y) | ¬ E(z) | F(y,x,z)
¬ G(x,y) | E(z) | ¬ F(y,x,z)
¬ F(x,y,z1) | ¬ F(x,y,z2), for z1 < z2 (well-defined)and that the function is total and its value always lies in the domain (elements of the domain are named 0, 1, ⋯, n−1):
F(x,y,0) | F(x,y,1) | ⋯ | F(x,y,n−1) (closed and total).If the flattened relational clauses contain any equality literals, the n2 units for the equality relation are asserted. Nothing special needs to be done for ordinary predicate symbols.
For various reasons, the most important being to reduce the number of isomorphic models that are found, the user can specify part of the model by supplying ground clauses over the domain. For example, if a noncommutative group is being sought, with constants a and b as noncommuting elements, the user can assign 0 to the identity, 1 to a, and 2 to b. In this case, nothing is lost by making them distinct.
Symbols can be given the following properties.
quasigroup.
This can be applied to ternary relations that represent binary functions.
The multiplication table of a quasigroup has one of each element in each
row and each column.
bijection.
This can be applied to binary relations that represent unary functions.
equality.
This can be applied to binary relations. It is just equality of domain
elements.
order.
This can be applied to binary relations. This is just the less-than
relation on the domain elements.
holey.
This can be applied to ternary relations that represent binary functions.
See Sec. 2.5.2.
hole.
This can be applied to binary relations.
See Sec. 2.5.2.
The first-order searcher is part of ANL-DP, and it is invoked
as described in Sec. 1.3. The command-line option
“-n n” specifies the domain size and indicates that
the input will be given as first-order flat clauses. Here is an
example input specifying a noncommutative group.
function F 3 quasigroup
function E 1 -----
function G 2 bijection
function A 1 -----
function B 1 -----
end_of_symbols
-E v0 F v0 v1 v1 .
-E v0 -G v1 v2 F v2 v1 v0 .
E v0 -G v1 v2 -F v2 v1 v0 .
-F v0 v1 v2 -F v3 v2 v4 -F v3 v0 v5 F v5 v1 v4 .
-F v0 v1 v2 F v3 v2 v4 -F v3 v0 v5 -F v5 v1 v4 .
-F v0 v1 v2 -B v0 -A v1 -F v1 v0 v2 .
end_of_clauses
E 0
A 1
B 2
end_of_assignments
function or relation), symbol, arity (n+1
for functions), and properties (equality, order,
quasigroup, bijection, or -----).
Otter 3.0.2 [5] and later versions can take ordinary formulas or clauses and produce the flat relational clauses for input to ANL-DP. Here is an Otter input file for a noncommutative group that will produce something like the file in Sec. 2.2.
set(dp_transform).
list(usable).
f(e,x) = x.
f(g(x),x) = e.
f(f(x,y),z) = f(x,f(y,z)).
f(a,b) != f(b,a).
end_of_list.
list(passive).
properties(f(_,_), quasigroup).
properties(g(_), bijection).
assign(e, 0).
assign(a, 1).
assign(b, 2).
end_of_list.
The command set(dp_transform) tells Otter to generate
input for an ANL-DP search and then exit.
The output of Otter contains extraneous text, so it must be passed though a filter before ANL-DP can receive it. See the example files and scripts in the distribution directories.
The ordered semigroup example in the FINDER 3.0 manual [6, Sec. 4.1.5] motivated me to have ANL-DP recognize the less-than relation on domain elements. The input (in Otter form) for the ordered semigroup problems is as follows.
set(dp_transform).
list(usable).
f(f(x,y),z) = f(x,f(y,z)).
-(f(x,y) < f(x,z)) | y < z.
-(f(y,x) < f(z,x)) | y < z.
end_of_list.
(Otter recognizes < as the order relation and gives it
the property “order” in its output.)
Table 2 compares the results of FINDER and ANL-DP, both
run on SPARC 2 computers, on the ordered semigroup problems. FINDER’s
search algorithm was developed with this type of problem in mind;
ANL-DP simply adds the n2 unit clauses for the less-than relation.
I believe this distinction explains most of the disparity of the
times.
In the multiplication table of an order-n quasigroup, each row and each column are a permutation of the n elements. For these problems, we are interested only in idempotent (i.e., xx=x) models. Additional constraints are given for the seven problems listed in Table 3. (Notes: (1) For QG1 and QG2, the disjunction to the right of the implication is ordinarily a conjunction; the forms are equivalent for quasigroups, and models are found more easily with disjunction. (2) The second and third equalities for QG5 and the second equality for QG7 are dependent.) See [2] and [7] for details on the quasigroup problems.
We also used the following cycle constraint on the last column to eliminate some isomorphic models [7]:
¬ f(x,n,z), for z < x−1.
The constraint requires that cycles in the last column be made up
of contiguous elements. This constraint is specified to ANL-DP with
the command-line option “-x1”; the quasigroup operation
must be f (lower-case) for this to work.
Table 4 gives summaries of the performance of ANL-DP (C, list structure), SATO-2 (C, trie structure), and LDPP′ (Lisp, list structure) on some cases of the quasigroup problems. The SATO and LDPP figures are taken from [8]. All runs were made on a SPARC 2 or similar computer. All programs used the cycle constraint and similar selection functions for splitting. I believe that differences in the number of branches are due mostly to the order of clauses and literals. Search time is given in seconds.
Table 4: Quasigroup Problems – Comparison
ANL-DP SATO-2 LDPP′ Problem Models Branches Search Branches Search Branches Search QG1.7 8 388 2.05 376 1 389 26 .8 16 100731 852.81 102610 379 101129 3463 QG2.7 14 361 2.23 340 1 205 8 .8 2 77158 810.75 80245 341 33835 1358 QG3.8 18 1017 2.82 1072 3 573 5 .9 - 39461 155.12 48545 157 24763 208 QG4.8 - 891 2.40 925 2 602 4 .9 178 52939 209.76 52826 168 27479 228 QG5.9 - 14 .22 19 .2 15 .4 .10 - 37 .52 62 .5 38 .9 .11 5 112 2.16 111 2 125 5 .12 - 369 6.61 369 7 369 15 .13 - 9588 242.54 10764 224 12686 639 QG6.9 4 17 .25 24 .2 18 .4 .10 - 58 .54 150 .7 59 .8 .11 - 537 5.36 519 6 539 11 .12 - 7306 95.41 5728 92 7288 177 QG7.9 4 7 .19 7 .2 8 .3 .10 - 39 .38 54 .4 40 .7 .11 - 291 2.98 254 3 294 6 .12 - 1578 17.87 1281 22 1592 38 .13 64 33946 493.67 27988 592 34726 1050
Table 5 lists some additional statistics for ANL-DP on the quasigroup problems. “Generated” and “Searched” are the number of propositional clauses generated and the number remaining after subsumption and the initial unit propagation. “Create” is the time (in seconds) used to construct the propositional clauses.
Table 5: Quasigroup Problems – ANL-DP Full Statistics
Problem Models Branches Generated Searched Memory Create Search QG1.7 8 388 120954 8952 886 K 4.79 2.05 .8 16 100731 267805 28877 2061 K 10.85 852.81 QG2.7 14 361 120954 9830 886 K 4.72 2.23 .8 2 77158 267805 30902 2061 K 10.88 810.75 QG3.8 18 1017 9757 3830 303 K 0.26 2.82 .9 - 39461 15670 6966 601 K 0.39 155.12 QG4.8 - 891 9757 3830 303 K 0.25 2.40 .9 178 52939 15670 6966 601 K 0.37 209.76 QG5.9 - 14 28792 9694 894 K 0.85 0.22 .10 - 37 43946 17274 1193 K 1.39 0.52 .11 5 112 64428 28488 1786 K 2.05 2.16 .12 - 369 91363 44302 2674 K 2.93 6.61 .13 - 9588 125984 65790 3562 K 4.02 242.54 QG6.9 4 17 22231 7653 601 K 0.66 0.25 .10 - 58 33946 13579 900 K 1.02 0.54 .11 - 537 49787 22332 1493 K 1.54 5.36 .12 - 7306 70627 34662 2088 K 2.24 95.41 QG7.9 4 7 22231 5838 601 K 0.61 0.19 .10 - 39 33946 11038 900 K 1.04 0.38 .11 - 291 49787 18944 1493 K 1.48 2.98 .12 - 1578 70627 30309 2088 K 2.14 17.87 .13 64 33946 97423 45967 2683 K 3.14 493.67
The command-line option -x2 constrains models of quasigroup f
to have the property f(x+1,y+1)=f(x,y)+1, where addition is (mod n);
that is, all the diagonals count up (mod domain-size).
The command-line option -xi, where 11≤ i ≤ 19,
constrains models of quasigroup f in the following way.
Consider the square of size x=i−10 in the lower right corner and the
remaining square of size m=n−x in the upper left corner. The
diagonals of the upper left square count up (mod m), except for
diagonals that consist of the same element in m,⋯,n−1. Also,
the first m elements of the last x rows and columns count up (mod
m). For example (see [2, Example 8.1] with the input
(note that the only upper left corner is idempotent)
set(dp_transform).
list(usable).
% (3,1,2)-COLS
f(x,y)!=u | f(z,w)!=u | f(v,x)!=y | f(v,z)!= w | x=z | y=w.
end_of_list.
list(passive).
properties(f(_,_), quasigroup).
assign(f(0,0),0).
end_of_list.
and the options “-n 10 -x13 -p”, we get
Model #1 at 333.47 seconds (SPARC 10):
f | 0 1 2 3 4 5 6 7 8 9
---------------------------
0 | 0 4 1 7 9 2 8 3 6 5
1 | 8 1 5 2 7 9 3 4 0 6
2 | 4 8 2 6 3 7 9 5 1 0
3 | 9 5 8 3 0 4 7 6 2 1
4 | 7 9 6 8 4 1 5 0 3 2
5 | 6 7 9 0 8 5 2 1 4 3
6 | 3 0 7 9 1 8 6 2 5 4
|
7 | 1 2 3 4 5 6 0 7 8 9
8 | 2 3 4 5 6 0 1 8 9 7
9 | 5 6 0 1 2 3 4 9 7 8
The -xi option can also be used when searching for
quasigroups with holes.
We simply list an example. The input (compare with above input)
set(dp_transform).
list(usable).
same_hole(x,x) | f(x,x) = x.
% (3,1,2)-COLS
f(x,y)!=u | f(z,w)!=u | f(v,x)!=y | f(v,z)!= w | x=z | y=w.
end_of_list.
list(passive).
properties(f(_,_), quasigroup_holey).
properties(same_hole(_,_), hole).
% The program makes same_hole symmetric and transitive.
assign(same_hole(7,8), T). assign(same_hole(8,9), T).
end_of_list.
with the command-line options “-n10 -x13 -p” produces the following:
Model #1 at 50.07 seconds (SPARC 2):
f | 0 1 2 3 4 5 6 7 8 9
--------------------------
0 | 0 6 7 5 8 9 3 1 2 4
1 | 4 1 0 7 6 8 9 2 3 5
2 | 9 5 2 1 7 0 8 3 4 6
3 | 8 9 6 3 2 7 1 4 5 0
4 | 2 8 9 0 4 3 7 5 6 1
5 | 7 3 8 9 1 5 4 6 0 2
6 | 5 7 4 8 9 2 6 0 1 3
7 | 3 4 5 6 0 1 2 - - -
8 | 6 0 1 2 3 4 5 - - -
9 | 1 2 3 4 5 6 0 - - -
Corollary 5.2 of [3] states
The necessary condition for the existence of a pair of OMTS(v), that is, v≡ 0 or 1 (mod 3), is also sufficient except for v=3,6 and possibly excepting v∈ {9,10,12,18}.
See [3] for definitions. The input
set(dp_transform).
list(usable).
f(x,x) = x.
h(x,x) = x.
f(x,f(y,x))=y.
h(x,h(y,x))=y.
f(x,y)!=u | f(z,w)!=u | h(x,y)!=v | h(z,w)!=v | x=z | y=w.
end_of_list.
list(passive).
properties(f(_,_), quasigroup).
properties(h(_,_), quasigroup).
end_of_list.
with the options “-n9 -x1 -p” produces the following
quasigroups, which correspond to a pair of orthogonal Mendelsohn
triple systems of order 9.
Model #1 at 54.58 seconds (SPARC 2):
f | 0 1 2 3 4 5 6 7 8 h | 0 1 2 3 4 5 6 7 8
------------------------ ------------------------
0 | 0 8 5 2 7 4 3 6 1 0 | 0 2 6 4 3 1 8 5 7
1 | 8 1 7 6 3 2 5 4 0 1 | 5 1 0 8 2 3 7 6 4
2 | 3 5 2 8 6 0 4 1 7 2 | 1 4 2 6 7 8 0 3 5
3 | 6 4 0 3 8 7 1 5 2 3 | 4 5 7 3 0 6 2 8 1
4 | 5 7 6 1 4 8 2 0 3 4 | 3 8 1 0 4 7 5 2 6
5 | 2 6 1 7 0 5 8 3 4 5 | 7 0 8 1 6 5 3 4 2
6 | 7 3 4 0 2 1 6 8 5 6 | 2 7 3 5 8 4 6 1 0
7 | 4 2 8 5 1 3 0 7 6 7 | 8 6 4 2 5 0 1 7 3
8 | 1 0 3 4 5 6 7 2 8 8 | 6 3 5 7 1 2 4 0 8
An analogous search for OMTS(10) ran for several days without finding a model.
A quasigroup of type hn has order h*n and n holes of size h. Frank Bennett posed [1] the question of the existence of QG3(28). (Mark Stickel had already answered positively the question of the existence of QG3(26) [1].) The ANL-DP input
relation = 2 equality
relation same_hole 2 hole
function f 3 quasigroup_holey
end_of_symbols
f v0 v0 v0 same_hole v0 v0 .
-f v0 v1 v2 -f v1 v0 v3 f v3 v2 v1 .
-f v0 v1 v2 -f v0 v2 v1 = v0 v1 .
-f v0 v1 v2 -f v2 v1 v0 = v0 v1 .
end_of_clauses
same_hole 0 7
same_hole 1 8
same_hole 2 9
same_hole 3 10
same_hole 4 11
same_hole 5 12
same_hole 6 13
same_hole 14 15
end_of_assignments
with the options “-n16 -p” produces the following holey quasigroup.
Model #1 at 76086.21 seconds (i468 DX2/66):
f | 0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15
------------------------------------------------------
0 | - 2 3 12 1 4 5 - 10 11 14 15 13 8 6 9
1 | 3 - 6 5 15 0 14 12 - 4 11 7 10 2 9 13
2 | 11 15 - 0 10 14 12 13 7 - 5 6 3 4 1 8
3 | 2 13 1 - 9 7 4 15 11 12 - 0 14 5 8 6
4 | 5 10 7 1 - 6 9 8 14 3 15 - 2 0 13 12
5 | 13 4 11 14 0 - 8 6 15 7 9 10 - 1 2 3
6 | 4 0 15 9 14 11 - 3 12 5 2 8 7 - 10 1
7 | - 6 8 13 2 9 15 - 5 14 4 12 1 11 3 10
8 | 14 - 4 6 3 2 10 9 - 0 13 5 15 7 12 11
9 | 15 3 - 11 6 8 7 1 13 - 12 14 0 10 4 5
10 | 6 5 14 - 7 15 11 2 9 1 - 13 8 12 0 4
11 | 8 12 10 2 - 1 3 14 6 13 7 - 9 15 5 0
12 | 10 9 0 8 13 - 1 11 4 15 6 3 - 14 7 2
13 | 9 14 12 15 5 3 - 10 2 8 0 1 4 - 11 7
14 | 1 7 13 4 12 10 0 5 3 6 8 2 11 9 - -
15 | 12 11 5 7 8 13 2 4 0 10 1 9 6 3 - -
(In case the reader is wondering why the holes are irregular in the lower right corner, the reason is that preliminary runs on QG3(26) ran faster with a similar hole configuration than with a regular configuration.)
Frank Bennett posed [1] the question of whether the the quasigroup identity (QG7a) x(yx) = (yx)y implies either (xy)x = x(yx) or xy(yx) = y. He suggested looking at models of order 17 with a hole of size 5, if they exist, as possible counterexamples. The identity (QG7b) ((xy)x)y = x, which is conjugate-equivalent [2] to (QG7a), is much easier to work with, so we put ANL-DP to work with the input
relation same_hole 2 hole
function f 3 quasigroup_holey
end_of_symbols
f v0 v0 v0 same_hole v0 v0 .
-f v0 v1 v2 -f v2 v0 v3 f v3 v1 v0 .
end_of_clauses
same_hole 12 13
same_hole 13 14
same_hole 14 15
same_hole 15 16
end_of_assignments
and the options “-n17 -x1 -p”, which produced the following
Model #1 at 172914.77 seconds (SPARC 2):
f | 0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16
---------------------------------------------------------
0 | 0 2 1 16 13 11 12 8 5 15 14 7 4 6 9 10 3
1 | 16 1 3 2 10 13 9 12 15 4 6 14 5 7 8 11 0
2 | 3 16 2 0 15 9 14 10 12 7 5 13 11 8 4 6 1
3 | 1 0 16 3 8 15 11 14 6 12 13 4 10 9 5 7 2
4 | 8 13 10 15 4 6 5 16 2 14 0 12 9 3 11 1 7
5 | 13 9 15 11 16 5 7 6 14 3 12 1 8 2 10 0 4
6 | 11 12 9 14 7 16 6 4 13 0 15 2 3 10 1 8 5
7 | 12 10 14 8 5 4 16 7 1 13 3 15 2 11 0 9 6
8 | 15 6 5 12 14 1 2 13 8 10 9 16 0 4 7 3 11
9 | 7 15 12 4 0 14 13 3 16 9 11 10 1 5 6 2 8
10 | 5 14 13 6 12 3 0 15 11 16 10 8 7 1 2 4 9
11 | 14 4 7 13 2 12 15 1 9 8 16 11 6 0 3 5 10
12 | 10 11 4 5 3 2 8 9 7 6 1 0 - - - - -
13 | 9 8 6 7 11 10 3 2 0 1 4 5 - - - - -
14 | 4 5 8 9 1 0 10 11 3 2 7 6 - - - - -
15 | 6 7 11 10 9 8 1 0 4 5 2 3 - - - - -
16 | 2 3 0 1 6 7 4 5 10 11 8 9 - - - - -
The conjugate-equivalent quasigroup corresponding to (QG7a) was then generated and found to falsify the two identities in question, giving a counterexample to the problem.
This document was translated from LATEX by HEVEA.