LocModGen - Model Generation by Local Search

Manfred Kerber
Computer Science, The University of Birmingham
Birmingham B15 2TT, England

Humans use semantic information in their proof search, and typically they know important models of mathematical concepts. Models can be used to direct proof search in systems such as Scott [Slaney94a] or the semantically guided clause graph procedure [AI2002-clausegraph]. Model generation itself can be computationally very hard and typically complete methods are used, which are built on variants of the Davis-Putnam-Loveland-Logemann method. Such model generators are Mace (Models And Counter-Examples) [McCune03] and Finder [Slaney94]. In this abstract we propose a method using a local search approach. Such approaches have proved successful in constraint satisfaction and propositional logic model generation. We adopt the method for the generation of finite models of first-order clauses.

The approach we are proposing takes as input a first-order clause set, FCLAUSE, and the intended cardinality of the model, n. In a first step the first-order clause set is translated to a propositional logic one, C. Then a random initial interpretation I is generated and the number of clauses satisfied in C is calculated. This interpretation is modified until the process is either stuck and restarted, or a model is found (see Figure 1).

1. Flow diagram

Compared to the actual PHP-implementation, which can be run for some few examples from http://www.cs.bham.ac.uk/~mmk/demos/LocModGen, there are some simplifications in the abstract description. Typically the procedure tries to make small positive steps (S+), by modifying one single element in the interpretation. The change is taken over only if it increases the number of satisfied propositional logic clauses. If the procedure does not make any progress for a while - measured by a counter j - it tries to make a big positive step (B+), in which the change is taken over only if it increases the number of satisfied propositional logic clauses. If neither is successful for a number of steps (e.g., 100 steps) it makes a big arbitrary step (B*). If all this is not successful after a number of steps (e.g., 150 steps), the procedure restarts (RESTART). There are two resource constraints, the maximal number of steps allowed and the maximum time spent on the search. If the process runs out of resources, it will return the best interpretation found so far.

For transforming first-order clauses to propositional logical ones, it is necessary to fix the cardinality n of the universe. It is assumed that the universe is given in the form of the first n natural numbers, {1,... ,n}. We add constant symbols ,... , to the syntax, which stand for 1,... ,n, respectively, (in order to simplify notation we will write simply 1,... ,n). All clauses are replaced by their variable-free counterparts, that is, each variable is systematically replaced by each of its possible values in {1,... ,n}. For instance the clause P(x,a),Q(y,f(x)) with n=3 will be replaced by the following nine clauses

While we know how to interpret the elements 1,2,3,... ,n, and the binary predicate symbol equal, which has a fixed interpretation to model equality, the other symbols, a, f, P, and Q in the example, can be interpreted in an arbitrary way.

While the method presented here has the disadvantage that we cannot use it to prove that there is no model, we can use it to define a notion of "near-model", which tells that an interpretation satisfies k out of m propositional logical clauses. Such near models may be used as a heuristic in adaptations of the methods described in [Slaney94a] and [AI2002-clausegraph]. The method presented here can also be directly adapted to deal with higher-order formulae.


© 2005, Manfred Kerber
The URL of this page is http://www.cs.bham.ac.uk/~mmk/papers/05-ARW.html.
Also available as pdf ps.gz bib .