Extending Finite Model Searching with Congruence Closure Computation - Artificial Intelligence and Symbolic Computation - page 94

Extending Finite Model Searching
with Congruence Closure Computation

Jian Zhang 1 , and Hantao Zhang 2 ,

1 Laboratory of Computer Science
Institute of Software, Chinese Academy of Sciences
Beijing 100080, China
[e-mail]
2 Department of Computer Science
University of Iowa Iowa City, IA 52242, USA
[e-mail]

Abstract. The model generation problem, regarded as a special case
of the Constraint Satisfaction Problem (CSP), has many applications in
AI, computer science and mathematics. In this paper, we describe how
to increase propagation of constraints by using the ground congruence
closure algorithm. The experimental results show that using the congru-
ence closure algorithm can reduce the search space for some benchmark
problems.

1 Introduction

Compared to the research on propositional satisfiability problem, the satisfiabil-
ity of first-order formulas has not received much attention. One reason is that
the problem is undecidable in general. Since the early 1990's, several researchers
have made serious attempts to solving the finite domain version of the problem.
More specifically, the problem becomes deciding whether the formula is satis-
fiable in a given finite domain. Several model generation programs have been
constructed [6, 3, 2, 10, 14, 16]. By model generation we mean, given a set of first
order formulas as axioms, finding their models automatically. A model is an in-
terpretation of the function and predicate symbols over some domain, which
satisfies all the axioms. Model generation is very important to the automation
of reasoning. For example, the existence of a model implies the satisfiability of
an axiom set or 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
proving. Models help people understand a theory and can guide conventional
theorem provers in finding proofs.

Supported by the National Science Fund for Distinguished Young Scholars of China
under grant 60125207. Part of the work was done while the first author was visiting
the University of Iowa.
Supported in part by NSF under grant CCR-0098093.