Predicate-Oriented Isomorphism Elimination in Model Finding

1 Introduction

Satis�ability checking (or model �nding) is an important problem in logic and Arti�cial Intelligence. If restricted to the propositional logic, the problem is well-known as SAT, and has been studied by many people. In this paper, we focus on �rst-order satis�ability problems. More speci�cally, we study how to �nd �nite models of �rst-order formulas. We propose two methods which use symmetries to eliminate isomorphic subspaces and prune the search tree. One technique works row-by-row; the other one processes submatrices, based on Ramsey numbers.

Symmetry breaking can be very helpful to improve the ef�- ciency of combinatorial searching. For example, it has played a key role in the solution of some previously open questions on quasigroups [Fujita et al., 1993]. But the technique used there is problem-speci�c. Other researchers have studied more general methods for using symmetries to improve the ef�ciency of model �nding. The Least Number Heuristic (LNH) [Zhang and Zhang, 1995] is such a technique. It works well on many problems (including the quasigroup problems). But it is not effective on predicates. The techniques proposed in this paper can remedy this weakness to some extent.

2 Background

We assume that the reader is familiar with the basic concepts of classical logics (including propositional and �rst-order logics). As mentioned earlier, this paper deals with the problem of �nding �nite models of �rst-order formulas. Currently, there are some automated tools available for doing this. Tools like SEM [Zhang and Zhang, 1995] search for the models directly, while other tools (like MACE2 [McCune, 2001]) translate the problem into SAT and use ef�cient SAT solvers.

✄ Supported by the NSF of China (No. 60125207).

For simplicity, we assume that there is only one domain: ☎ ✆ = ✞ 0, 1, . . . , ✟ ✠ ☛ ✌ . (But the methods can also be used on many-sorted formulas.) Suppose there is a binary predicate, ✎ , in the formulas. To give an interpretation for ✎ , we need to �nd an ✟ ✏ ✟ matrix, in which each entry (also called a cell) has a truth value (TRUE or FALSE).

A set of ground clauses, ✓ , is symmetric with respect to a set of domain elements, if ✓ remains the same under any permutation of the elements. When ✓ is obvious from the context, we also say that the elements are symmetric or interchangeable with each other. Clearly, this is an equivalence relation de�ned on a set of domain elements.

For convenience, we assume that all the domain elements are symmetric initially. We may think that there is only one equivalence class on the domain elements. This class includes every element of ☎ ✆ .

Ramsey Numbers

Ramsey numbers are well-known in graph theory. For a pair of positive integers ✔ and ✕ (✔ ✖ ☛ ✙ ✕ ✖ ☛ ), the Ramsey number ✢ ✣ ✥ ✧ ✔ ✙ ✕ ✪ is the minimumnumber of vertices such that all undirected simple graphs of order ✢ contain a clique of order ✔ or an independent set of order ✕ .

Currently we do not know the exact values of many Ramsey numbers. But we know that

and obviously, for any ✔ and ✕ , ✥ ✧ ✔ ✙ ✕ ✪ ✣ ✥ ✧ ✕ ✙ ✔ ✪ .

3 Row-by-row IsomorphismElimination

Suppose there is a model. Let us consider an interpretation for ✎ . First look at the �rst row of the matrix, that is, the value of ✎ ✧ ✺ ✙ ✽ ✪ (for ✽ ✖ ✺ ). For these ✧ ✟ ✠ ☛ ✪ truth values, either of the following propositions must hold, but not both:

1. At least ❄ ✧ ✟ ✠ ☛ ✪ ❆ ✭ ❇ cells got the value TRUE;
2. At least ❄ ✟ ❆ ✭ ❇ cells got the value FALSE.

Here ❉ ❊ ● denotes the largest integer ❍ such that ❍ ■ ❊ , and ❄ ✽ ❇ denotes the smallest integer ▲ such that ▲ ▼ ✽ .

If (1) is true, without loss of generality, we can assume that the cells

take the value TRUE. Similarly, if (2) is true, we assume that the second half of the �rst row got the value FALSE. So we have two subcases.

The above kind of �divide-and-conquer� can be repeated until the size of the equivalence class is reduced to 1. And we can get many subcases.

We call this technique the Row-by-Row (RR) strategy. Now we prove its correctness. Let ❬ ❭ denote the set of ground clauses obtained by instantiating the �rst-order clauses using all the elements in the domain ☎ ✆ .

Lemma 1. Suppose ☛ ❫ ❵ ■ ✟ ✠ ☛ , ✺ ■ ❝ ❫ ✟ ✠ ❵ , and ❬ ❭ is symmetric with respect to ✞ ✟ ✠ ❵ , . . . , ✟ ✠ ☛ ✌ . Then any model can be mapped (under certain permutation of domain elements) to one of the following two models:

1. a model in which ✎ ✧ ❝ ✙ ✟ ✠ ✢ ❣ ✪ , . . . , ✎ ✧ ❝ ✙ ✟ ✠ ☛ ✪ are TRUE, where ✢ ❣ ✣ ❄ ❵ ❆ ✭ ❇ ;
2. a model in which ✎ ✧ ❝ ✙ ✟ ✠ ✢ ✐ ✪ , . . . , ✎ ✧ ❝ ✙ ✟ ✠ ☛ ✪ are FALSE, where ✢ ✐ ✣ ❄ ✧ ❵ ❙ ☛ ✪ ❆ ✭ ❇ .

Theorem 1. If ❬ ❭ is symmetric with respect to ☎ ✆ , there is a model of ❬ ❭ in ☎ ✆ if and only if a model exists in one of the subcases.

For a given row, there can be several ways of dividing the assignments into two subcases. For example, we could divide the assignments at the �rst row into these two subcases:

1. ✎ ✧ ✺ ✙ ☛ ✪ is TRUE;
2. ✎ ✧ ✺ ✙ ✽ ✪ is FALSE, for every ✽ ▼ ☛ .

4 A Technique Based on Ramsey Numbers

Now we present a search strategy based on the Ramsey numbers, which is called the RN strategy. It tries to determine the values of several submatrices, starting from the upper-left corner to the lower-right corner.

If ✎ is commutative, i.e., ✎ ✧ ❊ ✙ ✽ ✪ ✣ ✎ ✧ ✽ ✙ ❊ ✪ for any ❊ ✙ ✽ , then the matrix can be regarded as a complete graph whose edges are colored with TRUE or FALSE. When ✟ is greater than or equal to the Ramsey number ✥ ✧ ✔ ✙ ✕ ✪ , there will be a complete subgraph ♥ ♦ with color TRUE, or a complete subgraph ♥ ♣ with color FALSE. Without loss of generality, we can divide the model �nding process into two subcases:

1. For any ❍ ✙ ▲ ( ✺ ■ ❍ ✙ ▲ ❫ ✔ , ❍ a115 ✣ ▲ ), ✎ ✧ ❍ ✙ ▲ ✪ and ✎ ✧ ▲ ✙ ❍ ✪ are TRUE.
2. For any ❍ ✙ ▲ (✺ ■ ❍ ✙ ▲ ❫ ✕ , ❍ a115 ✣ ▲ ), ✎ ✧ ❍ ✙ ▲ ✪ and ✎ ✧ ▲ ✙ ❍ ✪ are FALSE.

When ✟ is a bigger number,we can apply this kind of �divideand-conquer� several times.

If ✎ is not commutative, then ✎ ✧ ❊ ✙ ✽ ✪ (❊ ❫ ✽ ) can be regarded as a complete undirected graph whose edges are colored with TRUE or FALSE. Similarly, we can also divide the model searching process into two subcases:

1. For any ❍ ✙ ▲ ( ✺ ■ ❍ ❫ ▲ ❫ ✔ ), ✎ ✧ ❍ ✙ ▲ ✪ is TRUE.
2. For any ❍ ✙ ▲ (✺ ■ ❍ ❫ ▲ ❫ ✕ ), ✎ ✧ ❍ ✙ ▲ ✪ is FALSE.

To avoid repeated search, we can put the following condition on the �rst subcase: There is no ♥ ♣ colored with FALSE.

5 Experiments

We have tested our techniques on several problems, including

• ④ Pigeon-hole
• ④ Ramsey Number Searching
• ④ Steiner Triple System

Several programs are used, e.g., SEM [Zhang and Zhang, 1995], MACE2 [McCune, 2001] and the SAT solver siege v4 (http://www.cs.sfu.ca/�loryan/personal/).

Experimental results show that, typically our techniques can reduce the search time by a factor of 2 to 8.

6 Concluding Remarks

For many structured problems, if they are speci�ed naturally using �rst-order logic, the speci�cation suggests a lot of symmetries which can be used to prune the search space. This paper proposes two techniques for using such symmetries. They are mainly aimed at predicates. One of them works row by row, and the other one processes submatrices from the upperleft corner to the lower-right corner. The two techniques may be regarded as complementary to the least number heuristic and its extension. They can be helpful to both �rst-order and propositional solvers.

Symmetries have also been studied in the SAT community. For example, Aloul et al. [Aloul et al., 2003] have obtained very impressive results on various problems in the EDA �eld. They have implemented a software package called Shatter which can add certain clauses to a SAT instance to make it easier. Such an approach typically has to search for symmetries in large CNF formulas. For some SAT instances, the search may take a long time. Compared with a propositional formulation, a speci�cation in the �rst-order logic allows one to use symmetries without searching for them.

In the future, we are going to study how to combine various techniques in a single framework. It is also interesting to compare �rst-order techniques with symmetry-breaking predicates used for SAT solvers.