Information Technology Reference
In-Depth Information
Some of the model generation methods are based on first-order reasoning
(e.g., SATCHMO [6] and MGTP [2, 3]); some are based on constraint satisfaction
(e.g., FINDER [10], FALCON [14] and SEM [16]); while others are based on the
propositional logic (e.g., ModGen [4] and MACE [7]). These tools have been used
to solve a number of challenging problems in discrete mathematics [11, 7, 14].
Despite such successes, there is still space for improvement on the performance
of the tools.
In this paper, we study how to improve the performance of finite model
searchers by more powerful reasoning mechanisms. Specifically, we propose to
incorporate congruence closure computation into the search procedure of the
model generation tools.
2
Model Generation as Constraint Satisfaction
The finite model generation problem studied in this paper is stated as follows.
Given a set of first order clauses and a non-empty finite domain, find an inter-
pretation of all the function symbols and predicate symbols appearing in the
clauses such that all the clauses are true under this interpretation. Such an in-
terpretation is called a model . Here we assume that all the input formulas are
clauses. Each variable in a clause is (implicitly) universally quantified.
Without loss of generality, we assume that an n -element domain is the set D n
=
.Ifthearityof
each function/predicate symbol is at most 2, a finite model can be conveniently
represented by a set of multiplication tables , one for each function/predicate. For
example, a 3-element model of the clause f ( x, x )= x is like the following:
{
0, 1, ..., n −
1
}
. The Boolean domain is
{
FAL SE , T RUE
}
f
012
0
010
1
110
2
012
Here f is a binary function symbol and its interpretation is given by the above
2-dimensional matrix. Each entry in the matrix is called a cell .
In this paper, we treat the problem as a constraint satisfaction problem
(CSP), which has been studied by many researchers in Artificial Intelligence.
The variables of the CSP are the cell terms (i.e., ground terms like f (0 , 0),
f (0 , 1), etc.). The domain of each variable is D n (except for predicates, whose
domain is the Boolean domain). The constraints are the set of ground instances
of the input clauses, denoted by Ψ . The goal is to find a set of assignments to
the cells (e.g., f (0 , 1) = 2) such that all the ground clauses hold.
Theoretically speaking, any approach of constraint 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 inecient to be of any practical use. There are many other search pro-
cedures and heuristics proposed in the AI literature, e.g., forward checking and
lookahead. See [5] for a good survey.
Search WWH ::




Custom Search