SEM: a System for Enumerating Models

1 Introduction

A large number of problems in AI and computer ~ci­ ence can be viewed as special cases of the constraint­ satisfaction problem (CSP). Some examples are machine vision, belief maintenance, scheduling, temporal reason­ ing, graph problems, and the satisfiability problem. In this paper, we are interested in one special case of CSPs, i.e., model generation, where the constraints are ex­ pressed in predicate logic.

By model generation we mean, given a set of axioms (which are first order formulas) , find their models auto­ matically. A model is an interpretation of the function and predicate symbols over some domain, which satis­ fies all the axioms . The scope of this paper is restricted to finite models, whose domains are finite sets. Model generation is very important to the automation _of r~a­ soning. For example, the existence of a model 1mphes the consistency of a theory. A suitable model can also serve as a counterexample which shows some conjecture does not follow from some premises. In this sense, model generation is complementary to classical theorem prov­ ing. Finite models help people understand a theory, and they can also guide conventional theorem provers in find­ ing proofs. In recent years, several programs have been developed for e;enerating finite models, such as FALCON [Zhang, 1994aJ, FINDER [Slaney, 1993], MGTP-G [Fu­ jita et al., 1993], LDPP, SATO [Zhang and Stickel , 1994], ModGen [Kim and Zhang, 1994], and MACE [McCune, 1994b]. They have been used to solve a large number of open questions in mathematics (see for example, [Fujita et al., 1993; Slaney et al., 1995; Zhang and Stickel , 1 994; Zhang, 1994b]). .

*Partially supported by the National Science Foundation under Grants CCR-9202838 and CCR-9357851.

tOn leave from Chinese Academy of Sciences (Beijing).

Theoretically speaking, any approach of constramt satisfaction can be used for finite model generation. For instance, a simple backtracking algorithm can always find a finite model (if it exists). Of course, a brute-force search procedure is too inefficient to be of any practical use. In general, the performances of backtracking algo­ rithms can be improved in a number of ways such as forward checking and lookahead. There are many other search procedures and heuristics proposed in the AI liter­ ature; see [Kumar, 1992] for a good survey. However, in the special case of model generation, we have to address the following two issues:

• How can we implement constraint propagation and consistency checking efficiently? In particular , what data structures should be used?
• How can isomorphism be eliminated effectively dur­ ing the search? Two models are isomorphic if one can be obtained from the other by permuting ele­ ment names.

The first issue may be trivial for some constraint sat­ isfaction algorithms because the constraints they accept are often assumed to be unary or binary. It is true that n-ary constraints can be converted into an equivalent set of binary constraints; but this conversion usually entails the introduction of new variables and constraints , and hence an increase in problem size. This issue is particu­ larly important to model generation because in this case, the constraints are represented by complicated formulas. Experience tells us that a careful implementation can improve the performance of a program by several orders of magnitude. For instance, SATO [Zhang and Stickel , 1994] is a careful implementation of the Davis-Putnam algorithm, a well-known method for satisfiability testing in propositional logic. Because of its efficiency, SATO has been used by the second author to solve several dozens of open cases of quasigroup problems that can hardly be solved by other constraint satisfaction systems.

The second issue is obviously very important, because one model may be represented in many ways, which re­ sult in much redundancy in the search space. For propo­ sitional satisfiability, isomorphism elimination has been studied via the symmetric property of variables [Ben­ hamou and Sais, 1994]. In the study of quasigroup iden­ tity problems, a key technique used in [Fujita et al., 1993; Slaney et al., 1995] is to impose extra constraints as part of the input, so that some isomorphic models need not be considered. It appears that the method implemented in FALCON [Zhang, 1994a] is better for handling iso­ morphism. It works dynamically and does not require extra constraints. FALCON has been used by the first author to solve a variety of open problems in abstract algebra.

In this paper, we describe a new model generating tool called SEM (a System for Enumerating Models) that combines the strengths of FALCON and SATO. Like FALCON, SEM is based on first-order ground clauses, and uses the powerful isomorphism eliminating tech­ nique. It also incorporates some data structures and in­ ference mechanisms which are similar to those of SATO. As expected, SEM outperforms any other finite model generator that we know. SEM not only reproduced many results obtained by SATO and FALCON, but also solved several new problems. In particular, SEM works very well when the axiom set contains long formulas - the propositional satisfiability based systems like LDPP, SATO [Zhang and Stickel, 1994], ModGen [Kim and Zhang, 1994] and MACE [McCune, 1994b] cannot han­ dle these cases because it is too expensive to convert such formulas into propositional clauses.

In the next section, we present some basic concepts, the abstract algorithm for finding finite models, as well as some features of SEM. In Section 3, we compare SEM with other similar systems on various test problems, and illustrate the applications of SEM with several examples. We hope that these experiments will be used as a basis for further comparison between finite model generators.

2 Search for Finite Models

2.1 Basic Concepts

SEM accepts problem specifications in many-sorted first­ order logic. But only finite sorts are allowed and formu­ las should be in clause form. Let (S, F) be a signature where S is a set of sorts and F is a set of function sym­ bols. We shall use the letters (or s;) to denote a sort, and f to denote a function symbol. Each sort s E S consists of a finite number of elements, which may be designated by a list of names. Alternatively, one can simply give a positive integer (say n) as the cardinality of s, and the elements of s are assumed to be 0, 1, ... , n- 1. In the sequel, an element of some sort will be denoted by e or e;. Syntactically these elements may be regarded as con­ stant symbols. The built-in sort BOOL has two elements: TRUE and FALSE.

Function symbols are sorted. Each f E F has some fixed arity k ~ 0 and is specified by f : s1 ... sk --+ s, where s, s1, ... , Sk E S. The special predicate 'equality' is specified by EQ: s s --+ BOOL, where s is an arbitrary sort . We assume that, for any element e, EQ(e, e) evaluates to TRUE; and for any two distinct elements e;, ej ( i f- j) of the same sort, EQ( e;, ej) evaluates to FALSE. There can be other predefined functions and predicates, but for the sake of brevity, they will be neglected in this paper.

Terms are built from (sorted) variables and function symbols in the usual way. For convenience, let us call a term of the form j(e1, ... ,ek) (e; E s;) cell terms or simply cells. (Intuitively, such a term corresponds to an entry or a cell in the "multiplication table" of the function f.) We shall denote a cell term by ce or ce;. Assigning an element of some appropriate sort to each cell, we obtain an interpretation of the function symbols.

The specification of a problem consists of a set of clauses. Each clause is a disjunction of literals, and a literal is a term of the sort BOOL or its negation. All the variables in the specification are universally quantified. Our goal is to find an interpretation which makes all the clauses true, i.e., to find a (finite) model of the clauses.

2.2 Model Generation as CSP

A constraint satisfaction problem (CSP) consists of a set of variables, { V; I 1 ::=; i ::=; m }; a domain of values, D;, for each variable V;; and a collection of constraints. A solution to a CSP is an assignment of values to all the variables such that no constraint is violated. Finite model generation may be considered as a kind of CSP where the "variables" are the cells in the multiplication tables and the "constraints" are specified by the clauses.

The model finding process can be described by the recursive procedure in Figure 1. The procedure uses the following parameters:

• A: assignments (cells and their assigned values), {(ce,e) I e E sort(ce)};
• B: unassigned cells and their possible values, {(ce, D) I DC sort(ce)};
• C: constraints (i.e. the clauses).

Initially A is empty, and B contains all the cells: {(ce, D) I D = sort(ce)}. Since it is relatively expen­ sive and inconvenient to check the consistency of a set of clauses containing free variables, in the implementation of SEM, before the first call of the procedure search, the clauses are instantiated once for all, with each variable replaced by each element of the same sort.

The procedure propa(A, B, C) propagates assignment A in C: it simplifies C and may force some variables in B to be assigned. In the next subsection, we give more details about this procedure.

2.3 Constraint Propagation

The procedure propa(A, B, C) is essentially a closure op­ eration (with respect to a set of sound inference rules). It repeatedly modifies A, B, and C until no further changes can be made. When it exits, it returns the modified triple (A, B, C). The basic steps of this procedure can be described as follows.

proc search(A, B, C) { } if B = 0 then I* a model is found ·I { print(A); return; } choose and delete (ce;,D;) from B; if D; = 0 then return; I* no model ·I for e ED; do { } (A',B',C') := propa(AU {(ce;,e)} , B,C); if C' = false then continue; I* contradiction ·I else search( A', B', C');

1. For each assignment ( ce, e) in A, replace the occur­ rence of ce in C by e.
2. If there exists an empty clause in C (i.e., each of its literals becomes FALSE during the propagation), replace C by FALSE, and exit from the procedure. Otherwise, for every unit clause inC (i.e. all but one of its literals become FALSE), examine the remaining literal /.
3. If/ is a cell term ce, and (ce, D) E B, then delete (ce , D) from B and add (ce, TRUE) to A; similarly, if / is the negation of a cell term in B, i.e. ·ce, delete (ce, D) from B and add ( ce, FALSE) to A.
4. If/ is of the form EQ(ce , e) (or EQ(e, ce)), and (ce, D) E B , delete (ce, D) from B and add ( ce, e) to A; similarly, if / is of the form ·EQ(ce, e) (or ·EQ(e, ce)), and (ce, D) E B , then delete e from D.
5. For each pair (ce,D) E B, if D = 0, then replace C by FALSE, and exit from the procedure; if D = { e} (i.e. IDI = 1), then delete the pair (ce, D) from B, and add the assignment ( ce, e) to A.

Because the data (A, B, C) will be used in many re­ cursive calls, it would be much simpler to implement the procedure search if we could save a copy of (A, B, C) before modifying them in each recursive call. However, this would require a lot of storage. Instead, we record in a stack all the modifications done to (A, B , C) in each call and undo them when backtracking.

In our implementation, a term in a clause is repre­ sented by a tree in the usual way. A value is associated with each leaf node (called value node) and a function symbol is associated with each internal node. An in­ ternal node has a counter to record the number of its children nodes that are internal nodes; if this number is zero, this node corresponds to a cell, called a cell node.

Associated with each cell, there is a list of cell nodes that represent all the occurrences of that cell in the con­ straints C. When a cell is assigned a value, we simply mark each cell node in the list as a value node. If a cell node in the list has a parent node, we decrease the par­ ent's counter of internal children nodes by one. When that number becomes zero, the parent node is inserted into the cell node list ofthe corresponding cell. This kind of modifications on tree nodes is stored in a stack so that we can undo these modifications when backtracking.

Similarly, a clause has a counter to record the number of uninterpreted literals of the clause. When a literal becomes false, this number is decreased by one. When a literal becomes true, this clause is marked as "inac­ tive". This technique of counter-manipulating has been used in LDPP [Zhang and Stickel, 1994] for propositional clauses. Because of space limitation, we shall not give more details about the implementation.

2.4 The Least Number Heuristic

In the procedure search, there are several places where we can use heuristics to improve its efficiency. For ex­ ample, how to choose a variable ( ce;, D; ) from B for the next assignment; and, when (ce; , D;) is chosen, in what order should the values in D; be assigned to ce;. These issues have been studied extensively in the AI literature. They have also been considered in model generation pro­ grams like FINDER [Slaney, 1993] and MGTP [Fujita et a/., 1993]. In this paper, we focus on another kind of heuristics, i.e., how to reduce the number of values in D;. If we can delete some values from D; (without los­ ing the completeness), then there will be fewer recursive calls to search and the search space will become smaller.

In a typical model generation problem, there can be many isomorphic models. When two values e and e' are symmetric in the input constraints, given one model M, we can obtain another model M' which is isomorphic to M , by exchanging e with e'. In an exhaustive search procedure like search, it is too expensive to enumerate all the possible models. Thus isomorphism rejection is crucial to the efficiency of finite model generation.

FALCON uses the so-called least number heuristic (LNH) in the search to avoid exploring isomorphic sub­ spaces [Zhang, 1994a]. It is based on the observation that, at the early stages of the search, many element names (which have not yet been used in the search) are essentially the same. Thus when choosing a value for a new cell, we need not consider all the elements of a given sort. It makes no difference to assign the element e or e' to the cell, if neither of them has been assigned to some cell. To make this concise, we say that two elements e and e' are symmetric with respect to a set of ground clauses if the clause set remains the same when e and e' are interchanged.

Theorem. The procedure search( A, {(ce;, D;)} UB, C) can find a model iff search( A, { ( ce;, N onsymm(D;, C))} U B, C) can find one, where N onsymm( D;, C) is ob­ tained from D; such that if two values in D; are sym­ metric with respect to C, then one of the two values is deleted from D; .

In general, it is expensive to repeatedly check symme­ try of elements. But when the input clauses (before the instantiation of free variables) do not use the element names (i.e., 0, 1, ... ) or their properties (e.g. , 0 < 1) , then any two elements are symmetric with respect to the ground clauses obtained by instantiating the input clauses with element names. In this case, we can show that in search( A, {(ce;, D;)} U B, C), any two values in D; that are not used in A are symmetric with respect to C. We can simply delete all the values from D; that do not appear in A, except one (the smallest one in our implementation). This technique of exploiting partially the symmetry of values is called the least number heuris­ tic (LNH). As we will see in the next section, it is very effective in reducing isomorphic subspaces.

2.5 The System

SEM was implemented in C. The YACC tool is used for parsing. The current version has about 4000 lines of source code. The major algorithm is essentially the same as search, except that, for the sake of efficiency, we use an iterative procedure instead of a recursive one.

In SEM, the input specification for a problem consists of the following four parts:

Sorts; Functions; Variables; Clauses.

As an example, we give the specification for the pigeon­ hole problem.

Example Pigeonhole problem (10 pigeons, 9 holes). (The character '%'starts a comment in a line.)

% Sorts ( pigeon [10] ( hole [9] ) % Functions { h : pigeon -> hole } { in : pigeon hole -> BOOL } % Variables < x, y : pigeon > < z : hole > %Clauses. '-' is 'not'; 'I' is 'or'. [ in(x,h(x)) ] [ -in(x,z) I -in(y,z) I EQ(x,y) ]

3 Experimental Results

In this section, we describe some of our experiments with SEM, and illustrate the applications of finite model gen­ eration with various examples. We compare SEM with other similar systems like FALCON-2 [Zhang, 1994a], FINDER (Slaney, 1993] (version 3.0), SATO 2 (Zhang and Stickel, 1994] and MACE [McCune, 1994b] (version 1.0.0). (All these systems were implemented in C.) Since different specifications may result in different execution times, we use the sample input files provided by the de­ signers of the systems, whenever possible. For the same problem, we use the same set of axioms. All of our ex­ periments were carried out on a Spare 2 workstation. The following tables show the execution times (in sec­ onds) of the programs on various problems. Each row corresponds to one problem instance. Its first column is of the form name.n or simply n, where name is the name of a problem, and n is the size of the model. In all but the first table, we also give the number of models (denoted by m) .

3.1 The Pigeonhole Problem

As a simple example of many-sorted applications, let us consider the pigeonhole problem, which has been in­ cluded as a benchmark in most of the aforementioned systems. When not exploiting symmetry of the clauses, these systems can handle at most 11 pigeons in a rea­ sonable amount of time (say 10 minutes).

Benhamou and Sais [Benhamou a:nd Sais, 1994] pro­ posed a method for exploiting symmetry in the proposi­ tional case. In the first-order case, we can use the least number heuristic to solve the problem more quickly. Ta­ ble 1 gives the execution times of the two programs (n pigeons and n -1 holes). The SEM specification for this problem was given in §2.5. Benhamou and Sais' algo­ rithm (BS, in short) was implemented in Pascal on a SUN4/110 and the run times are taken from [Benhamou and Sais, 1 994].

3.2 Quasigroups and Latin Squares

Recently a large number of open cases of quasigroup identity problems have been solved by various programs [Zhang, 1991; Fujita et a/., 1993; Slaney et a/., 1995; Zhang and Stickel, 1994; McCune, 1994b]. A quasigroup has only one binary function, denoted by . or juxtapo­ sition. In the multiplication table of this function, each · row and each column is a permutation of all the elements.

In this subsection, we compare SEM with FINDER and SATO on the following 3 problems:

1. IQG: enumerate idempotent quasigroups, i.e. quasi­ groups satisfying the identity xx = x.
2. QG5: find idempotent quasigroups satisfying the identity (yx.y)y = x. For the sake of efficiency, we also use two additional equations, i.e. y(xy.y) = x and (y.xy)y = x.
3. RLS: enumerate reduced latin ·squares. A Latin square is called reduced if in the first row and column its elements occur in natural order. Thus a 'reduced latin square corresponds to a quasigroup satisfying the identities: xO = x and Ox = x.

For the first two problems, each program uses a differ­ ent method for handling isomorphism. SATO uses the last-column constraint [Fujita et a/., 1993; Slaney et a/., 1995], FINDER introduces the 'cycle' function in the specification [Slaney, 1993], and SEM relies on the LNH.

For the last problem, no isomorphism-rejecting heuristic is used by any program.

From Table 2, one can see that the LNH is the most powerful heuristic for eliminating isomorphism. When this heuristic is used, fewer (or the same number of) models are generated. For a fixed size, all the models are essentially the same. Take QG5.7 for example, each of the 3 models produced by the other two programs is isomorphic to the one found by SEM, under certain permutations of the elements.

3.3 Some Equational Problems

Tables 3 and 4 give some data comparing the perfor­ mances of several systems on generating some finite al­ gebras: non-commutative groups (NCG), rings with unit (RU), and Boolean algebras (BA). No isomorphism elim­ inating heuristic is used by the programs in Table 3. A '*' indicates that MACE runs out of memory.

From these tables, one can see that isomorphism rejec­ tion is very important. Without such mechanisms, it is very difficult to generate moderately large algebras. The use of LNH enables FALCON and SEM to complete the search very quickly. It can also be seen that constraint propagation in SEM is very efficient . In many cases, SEM is about 10 times faster than FALCON.

3.4 Comparison

Programs like ModGen and MACE are based on deci­ sion procedures for the propositional logic. They per­ form very well on quasigroup problems, since the prob­ lems can be represented concisely in the propositional logic. But in general, it seems inappropriate to use them to find finite models of first-order theories because too many propositional variables and clauses are needed to represent the problems. On the other hand, FINDER, FALCON and SEM are based on (ground) first-order clauses and can deal with more complicated axiom sets. However, FINDER does not have any built-in mecha­ nism for isomorphism rejection. In contrast, the LNH is quite general and powerful. Both FALCON and SEM rely on this heuristic to reduce the search space. The underlying algorithm of the two programs are virtually the same. However, FALCON was designed mainly for equational theories, and its implementation does not use so sophisticated indexing techniques like those used by the other programs.

3.5 Newly Solved Problems

SEM obtained several nontrivial results, some of which seem quite difficult for other systems to reproduce.

• On Tarski's high school identities [Burris and Lee, 1993], we completed the search for Gurevic algebras of size 8, without finding a solution.
• To prove that the fragment {B, M} of combinatory logic does not possess the fixed point property, we searched for countermodels of size up to 7. (No model has been found.)
• R. Padmanabhan asked if there is a finite model of the following set of clauses:

g(f(x,y),f(x,x)) = x f(g(x,y),g(x,x)) = x g(g(x,y),z) = g(g(y,z),x) f(f(x,y),z) = f(f(y,z),x) g(a,f(b,a)) ·- f(a,g(b,a))

Here f and g are two binary function symbols, a and b are two constant symbols. We completed the search for models of size up to 20, but did not find any one. 1

• In the study of orthogonal arrays, given three pos­ itive integers g, h and k, we'd like to know if there exists an Abelian group G of size g, which has a subgroup H of size h, and on which we can define a function m : G __. G, satisfying the following two conditions: (1) for any a, bEG, m(ab) = m(a)m(b); and (2) for 0 < i < k and a (/. H, mk(a) = a, mi(a) =F a (where m 0 (a) = a and mi+ 1 (a) = m( mi (a))). SEM successfully found ( G, H, m) for (g, h, k) = (32, 2, 3), (56, 2, 3), (27, 3, 3) , (36 , 3, 3), (48, 3, 3) , (57, 3, 3).
• In group theory, we know that (xy) 2 = x 2 y 2 im­ plies xy = yx . This can be proved with a con­ ventional theorem prover like OTTER [McCune, 1994a]. In contrast, with SEM, we can show that (xy)k = xkyk does not imply the commutativity law, for k = 3, 4, 5. SEM found the appropriate countermodels of sizes 27, 8, 8, respectively.
• SEM also found some idempotent quasigroups sat­ isfying two identities simultaneously, for example, a 13-element model of QG7 and QG9, a 13-element model of QG8 and QG9, and a 21-element model of QG5 and QG7. (The related identities are: QG7. (yx)y = x(yx); QG8. x(xy) = yx; and QG9. ((xy)y)y = x.)

For the first two problems, 2 it took several days for SEM to complete the search. However, the last two prob­ lems are not so difficult as they appear - the execution times range from less than one second to several seconds.

4 Concluding Remarks

We have described SEM, a System for Enumerating fi­ nite Models, and compared its performance with those of other similar systems. Clearly, SEM can solve a wide range of problems efficiently. As shown in this paper and other papers [Fujita et al., 1993; Slaney et al., 1995; Zhang and Stickel, 1994; Zhang, 1994a; 1994b], finite model generators are very useful tools. So far, they have been mainly used to solve problems in mathematics. But we believe that the related techniques will find applica­ tions in AI and computer science as well.

Finite model generation is closely related to search and reasoning, which are two of the most important sub­ jects in AI, and which have been studied extensively. Most existing programs are based solely on backtrack­ ing procedures. In the future, we shall experiment with more search heuristics and other non-exhaustive meth­ ods. The reliability of non-existence results is also worth studying.

1 Later we proved that this set of clauses is unsatisfiable.

2 See [Zhang, 1994b] for the clauses of these two problems.