Campus Event Calendar
Event Entry
What and Who
A Symbiosis of Interval Constraint Propagation and Cylindrical Algebraic Decomposition
Ulrich Loup
RWTH Aachen
Talk
AG 1, AG 2, AG 3, AG 4, AG 5, SWS, RG1, MMCI
MPI Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Wednesday, 17 April 2013
15:00
60 Minutes
E1 4
019
Saarbrücken
Abstract
This talk is a report on two kinds of symbioses: On the one hand, this work is
a tight cooperation between the university of Freiburg and RWTH Aachen
University. On the other hand, our work is a tight combination of two methods
to solve non-linear real-arithmetic formulas, each having drawbacks, but being
very powerful when combined.
The first method is based on interval-constraint propagation (ICP) and is
implemented in the satisfiability-modulo-theories (SMT) solver iSAT developed
in Freiburg. In this approach, interval arithmetic is used in order to
contract initial bounds to the input variables until either unsatisfiability
is deduced or the interval size is below a certain threshold. In that case,
the method terminates with an interval box whose satisfiability status is
unknown to iSAT.
The other method, in turn, always terminates with a satisfiability result: the
cylindrical algebraic decomposition (CAD) method, a procedure being able to
construct one representative for every maximal connected component of the
solution space where the input formula does not change its truth value.
However, the number of these representatives is doubly exponential in the
number of input variables.
A symbiosis of iSAT and our CAD implementation combines the advantages of both
methods resulting in a fast and complete solver. In particular, the interval
box determined by iSAT provides precious extra information to guide
the CAD-method search routine: We use the interval box to prune the
CAD search space forming a search “tube” rather than a search tree. This
proves to be particularly beneficial for a CAD implementation designed to
search a satisfying assignment pointedly, as opposed to search and exclude
conflicting regions, as it is currently pursued in Microsoft's solver Z3.
a tight cooperation between the university of Freiburg and RWTH Aachen
University. On the other hand, our work is a tight combination of two methods
to solve non-linear real-arithmetic formulas, each having drawbacks, but being
very powerful when combined.
The first method is based on interval-constraint propagation (ICP) and is
implemented in the satisfiability-modulo-theories (SMT) solver iSAT developed
in Freiburg. In this approach, interval arithmetic is used in order to
contract initial bounds to the input variables until either unsatisfiability
is deduced or the interval size is below a certain threshold. In that case,
the method terminates with an interval box whose satisfiability status is
unknown to iSAT.
The other method, in turn, always terminates with a satisfiability result: the
cylindrical algebraic decomposition (CAD) method, a procedure being able to
construct one representative for every maximal connected component of the
solution space where the input formula does not change its truth value.
However, the number of these representatives is doubly exponential in the
number of input variables.
A symbiosis of iSAT and our CAD implementation combines the advantages of both
methods resulting in a fast and complete solver. In particular, the interval
box determined by iSAT provides precious extra information to guide
the CAD-method search routine: We use the interval box to prune the
CAD search space forming a search “tube” rather than a search tree. This
proves to be particularly beneficial for a CAD implementation designed to
search a satisfying assignment pointedly, as opposed to search and exclude
conflicting regions, as it is currently pursued in Microsoft's solver Z3.
Contact
Jennifer Müller
2900
--email hidden
passcode not visible
logged in users only
Jennifer Müller, 04/15/2013 09:21 -- Created document.