Interpolants in Nonlinear Theories: A Study in Real Numbers
Explore the application of interpolants in nonlinear theories over the real numbers, delving into topics such as reasoning about continuous formulae, Craig interpolation, and branch-and-prune strategies. Discover how nonlinear theories can be both undecidable and decidable with perturbations, capturing numerical computability in the process.
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. Download presentation by click this link. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
E N D
Presentation Transcript
Interpolants in Nonlinear Theories over the Reals Sicun Gao and Damien Zufferey MIT CSAIL 2016.04.06 TACAS 1
Motivation Discrete Polynomials Continuous ?2= 1 Transcendental functions cos ? Differential equations ? ? ? ?? 2
Reasoning About Continuous Formula Linear Satisfiability Linear programming Nonlinear ?-satisfiability Interval constraint propagation (ICP) Quantifier Elimination Fourier Motzkin Quantifier Elimination CAD for polynomials Craig Interpolation LP duality (Farkas Lemma) Craig Interpolation Propositional interpolation (Pudlak) ? 3
Outline Background Interpolation ?-satisfiability Interpolation for Nonlinear Theory Proof from interval constraint propagation Interpolation system Implementation and Applications 4
Craig Interpolation I Let ? ? be unsatisfiable. A B ? is an interpolant iff ? ? ? ? is unsatisfiable fv ? fv ? fv(?) Usually, ? is computed from the unsatisfiability proof of ? ?. 5
?-Satisfiability + nonlinear theory undecidable + nonlinear theory + ?-perturbations decidable ?-sat |? ? ? ? | = 0 0 < |? ? ? ? | ? ? ? = ?( ?) ?-sat / unsat |? ? ? ? | > ? unsat ?-satisfiability captures numerical computability. 6
Branch-and-Prune ICP ICP(?1, ,??,?) S.push(?) while S not empty ? S.top() while ( ) ? prune(?,??) if ? if small enough ? else S.push(?2) return UNSAT ?1 ? ?2 return ?-SAT ?1,?2 branch(?) S.push(?1) 7
Branch-and-Prune Example Prune by B Prune by A Branch Prune by A Prune by B Prune by A Prune by B B A 8
Proof from ICP: ?,?1..? ICP(?1, ,??,?) S.push(?) while S not empty ? S.top() while ( ) ? prune(?,??) if ? if small enough ? else S.push(?1) S.push(?2) return UNSAT Selecting ?? Prune = Split + ThLem return SAT Split ?1,?2 branch(?) 9
Selecting ?? ?,?? ?,?1..? (Weakening) 10
Branching ?1 ?2 ? ? ? ? ?, ?1..? ? ? ?,?1..? ?,?1..? (Split) 11
Pruning by ?? ? ? ? ? ?,?? (ThLem) ? ? ?,?1..? (Weakening) (Split) ?,?1..? 12
ICP Produces Resolution Proofs ? ? ?1..? ? ? ?1..? ? ? ?, ?1..? ? ? ?,?1..? ?,?1..? (Split) ? ?1..? 13
Interpolation Rules ? ?,?? ?,?1..? (Weakening) ? ? ? ?,?? (ThLem) ?? ? ?1 ?2 ? ? ?, ?1..? ? ? ?,?1..? ?,?1..? (Split) ?1 ?2 if ? fv ? ? fv(?) if ? fv ? ? fv(?) if ? fv ? ? fv(?) ???(? ?,?1,?2) ?1 ?2 14
Example A? = ?2 B? = cos(?) + 0.8 15
Implementation Implemented in the dReal SMT-solver: https://github.com/dzufferey/dreal3/ https://github.com/dreal/dreal3/ Evaluation in the paper Computing interpolants for examples such as QF_NRA Control theory and robotic systems Biological systems Report interpolant size vs proof size, runtimes, etc. 16
Ordinary Differential Equations ? How can we handle: ??= ?0+ ? ? ?? 0 ? 2 0 An ODE is just a pruning operator over the domain ? ?? ?0 17
Interpolation as Weak Quantifier Elimination Kinematic chain Automatically extracted model: 30 variables poly. deg. 2, trig. fct. Simplified model: 5 variables , , , < Only approximate (?) Interpolation 18
Related Works Labelled interpolation systems, D Silva et al. 10 Linear arithmetic: : Brillout et al. 10, Griggio et al. 11 : McMillan 04, Rybalchenko & Sofronie-Stokkermans 07 Polynomials over using semi-definite prog. Dai et al. 13 Tools to compute interpolants: MathSat5, Princess, SmtInterpol, Z3 19
Conclusion Interpolation for nonlinear theories over the reals based on the framework of ?-satisfiability Link between branch-and-prune proof and propositional resolution Implementation on top of the dReal SMT solver 20
