Lemma Learning in the Model Evolution Calculus
Alexander Fuchs and Cesare
The Model Evolution (ME) Calculus is a proper lifting
to first-order logic of the DPLL procedure,
a backtracking-based search procedure for propositional satisfiability.
Analogously to DPLL, the ME calculus is based on the idea of
incrementally building a model of the input formula
by alternating constraint propagation steps with
non-deterministic decision steps.
One of the major conceptual improvements over basic DPLL
is lemma learning,
a mechanism for generating new formulae
that prevent later in the search
combinations of decision steps guaranteed to lead to failure.
We introduce three lemma generation methods for
ME proof procedures,
with various degrees of power, effectiveness in reducing search,
and computational overhead.
Even if formally correct,
each of these methods presents complications
that do not exist at the propositional level but need to be addressed
for learning to be effective in practice for ME.
We discuss some of these issues and then present
initial experimental results on the performance
of an implementation within Darwin of the three learning procedures.
Last modified: Sun Mar 20 16:51:19 CST 2005