Campus Event Calendar
Event Entry
What and Who
Solving linear arithmetic by conflict resolution and bound propagation
Konstantin Korovin
University of Manchester
Talk
AG 1, AG 2, AG 3, AG 4, AG 5, SWS, RG1, MMCI
Public Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Wednesday, 23 October 2013
15:00
45 Minutes
E1 4
019
Saarbrücken
Abstract
Reasoning methods based on resolution and DPLL have enjoyed many success stories
in real-life applications. One of the challenges is whether we
can go beyond and extend this technology to other domains such as arithmetic.
In our recent work we introduced two methods for solving systems of
linear inequalities called conflict resolution (CR)
and bound propagation (BP) which aim to address this challenge.
In particular, conflict resolution can be seen as a refinement
of resolution and bound propagation is analogous to DPLL
with constraint propagation, backjumping and lemma learning.
There are non-trivial issues when considering arithmetic constraints such as
termination, dynamic variable ordering and dealing with large coefficients.
In this talk I will overview our approach for solving linear arithmetic and related work.
This is a joint work with Ioan Dragan, Laura Kovacs, Nestan Tsiskaridze and Andrei Voronkov.
in real-life applications. One of the challenges is whether we
can go beyond and extend this technology to other domains such as arithmetic.
In our recent work we introduced two methods for solving systems of
linear inequalities called conflict resolution (CR)
and bound propagation (BP) which aim to address this challenge.
In particular, conflict resolution can be seen as a refinement
of resolution and bound propagation is analogous to DPLL
with constraint propagation, backjumping and lemma learning.
There are non-trivial issues when considering arithmetic constraints such as
termination, dynamic variable ordering and dealing with large coefficients.
In this talk I will overview our approach for solving linear arithmetic and related work.
This is a joint work with Ioan Dragan, Laura Kovacs, Nestan Tsiskaridze and Andrei Voronkov.
Contact
Jennifer Müller
2900
--email hidden
passcode not visible
logged in users only
Jennifer Müller, 10/21/2013 09:10 -- Created document.