Campus Event Calendar
Event Entry
What and Who
Towards a Lifted Version of DPLL(T)
Peter Baumgartner
NICTA, Canberra, Australia
Logic & Computation Program
Talk
AG 1, AG 2, AG 3, AG 4, AG 5, SWS, RG1, RG2
MPI Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Wednesday, 11 July 2007
15:00
-- Not specified --
E1 4
Rotunde 6.OG
Saarbrücken
Abstract
The purpose of this talk is to discuss investigations into (partially)
lifting to the first-order level the well-known DPLL(T) approach to
Satisfiability Modulo Theories (SMT).
DPLL(T) is one of the most successful approaches to build automated
theorem provers for reasoning modulo a background theory T for the
case of quantifier-free input formulas. It is based on combining a
DPLL-type propositional SAT solver with a solver for quantifier-free
conjunctions of T-literals, the T-solver.
Resorting to a propositional SAT solver poses some limitations,
though. These are grounded on the SAT solver's inability to analyze
the term structure of the given formula (naturally, the SAT solver has
to work on propositional abstractions of the given formula). For
instance, treating non-quantifier free formulas is done by eager
translation into propositional logic, which does not work well in many
cases.
We view at this problem from an angle that is very natural with our
work done in the past. We have been developing a first-order logic
version of the DPLL procedure, the Model Evolution calculus (ME). One
may thus ask if it is possible to replace in a DPLL(T) solver the DPLL
procedure by ME, thus obtaining an "ME(T)" solver. We present a basic
approach for doing that and discuss its consequences. Basically, the
term structure can be analyzed by the ME calculus now, which can be
exploited in a beneficial way, e.g., for non-quantifier free input
problems. The talk will present the main ideas behind that. These
ideas seem not limited to the ME calculus, and it should not be too
difficult to apply them to hyper resolution or hyper tableaux calculi.
lifting to the first-order level the well-known DPLL(T) approach to
Satisfiability Modulo Theories (SMT).
DPLL(T) is one of the most successful approaches to build automated
theorem provers for reasoning modulo a background theory T for the
case of quantifier-free input formulas. It is based on combining a
DPLL-type propositional SAT solver with a solver for quantifier-free
conjunctions of T-literals, the T-solver.
Resorting to a propositional SAT solver poses some limitations,
though. These are grounded on the SAT solver's inability to analyze
the term structure of the given formula (naturally, the SAT solver has
to work on propositional abstractions of the given formula). For
instance, treating non-quantifier free formulas is done by eager
translation into propositional logic, which does not work well in many
cases.
We view at this problem from an angle that is very natural with our
work done in the past. We have been developing a first-order logic
version of the DPLL procedure, the Model Evolution calculus (ME). One
may thus ask if it is possible to replace in a DPLL(T) solver the DPLL
procedure by ME, thus obtaining an "ME(T)" solver. We present a basic
approach for doing that and discuss its consequences. Basically, the
term structure can be analyzed by the ME calculus now, which can be
exploited in a beneficial way, e.g., for non-quantifier free input
problems. The talk will present the main ideas behind that. These
ideas seem not limited to the ME calculus, and it should not be too
difficult to apply them to hyper resolution or hyper tableaux calculi.
Contact
Roxane Wetzel
900
--email hidden
passcode not visible
logged in users only
Roxane Wetzel, 07/03/2007 15:09
Roxane Wetzel, 07/03/2007 15:08 -- Created document.
Roxane Wetzel, 07/03/2007 15:08 -- Created document.