Campus Event Calendar
Event Entry
What and Who
Conflict Resolution
Nestan Tsiskaridze
University of Manchester
Talk
RG1
AG Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Friday, 17 December 2010
14:00
60 Minutes
E1 7
2.01
Saarbrücken
Abstract
We presented a new method for solving systems of linear constraints
over the rationals or reals - Conflict Resolution method. The method
works with a set of constraints and an assignment on variables. The
method is an assignment driven. The assignment is refined iteratively
trying to make it into a solution. If such a refinement is impossible,
it is due to a pair of conflicting constraints in the system. We
resolve a conflict by deriving a new constraint and adding it to the
system. Deduction of new constraints is guided by the assignment. The
refinement is done successively until either the assignment becomes a
solution of the system or the inconsistency of the initial system is
proved.
Generation of new constraints ensures that new constraints are
non-redundant (in some natural sence). The method also has a number of
properties crucial for integration into SMT solving: incrementality
and ability to generate explanations for an unsatisfiabile subset of
constraints. The method may also have an independent value for linear
programming. We implemented a solver based on our method. The solver
showed itself to be highly competitive with existing state-of-the-art
solvers and in some cases even outperforming them.
over the rationals or reals - Conflict Resolution method. The method
works with a set of constraints and an assignment on variables. The
method is an assignment driven. The assignment is refined iteratively
trying to make it into a solution. If such a refinement is impossible,
it is due to a pair of conflicting constraints in the system. We
resolve a conflict by deriving a new constraint and adding it to the
system. Deduction of new constraints is guided by the assignment. The
refinement is done successively until either the assignment becomes a
solution of the system or the inconsistency of the initial system is
proved.
Generation of new constraints ensures that new constraints are
non-redundant (in some natural sence). The method also has a number of
properties crucial for integration into SMT solving: incrementality
and ability to generate explanations for an unsatisfiabile subset of
constraints. The method may also have an independent value for linear
programming. We implemented a solver based on our method. The solver
showed itself to be highly competitive with existing state-of-the-art
solvers and in some cases even outperforming them.
Contact
Jennifer Müller
900
--email hidden
passcode not visible
logged in users only
Jennifer Müller, 12/16/2010 08:31 -- Created document.