Campus Event Calendar

Event Entry

What and Who

Conflict Resolution

Nestan Tsiskaridze
University of Manchester
AG Audience

Date, Time and Location

Friday, 17 December 2010
60 Minutes
E1 7


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
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.


Jennifer Müller
--email hidden
passcode not visible
logged in users only

Jennifer Müller, 12/16/2010 08:31 -- Created document.