Efficient Solution of a Class of Quantified Constraints with Quantifier Prefix Exists-Forall
Logic in Computer Science
2014-06-26 v3 Data Structures and Algorithms
Numerical Analysis
Abstract
In various applications the search for certificates for certain properties (e.g., stability of dynamical systems, program termination) can be formulated as a quantified constraint solving problem with quantifier prefix exists-forall. In this paper, we present an algorithm for solving a certain class of such problems based on interval techniques in combination with conservative linear programming approximation. In comparison with previous work, the method is more general - allowing general Boolean structure in the input constraint, and more efficient - using splitting heuristics that learn from the success of previous linear programming approximations.
Cite
@article{arxiv.1312.6155,
title = {Efficient Solution of a Class of Quantified Constraints with Quantifier Prefix Exists-Forall},
author = {Milan Hladík and Stefan Ratschan},
journal= {arXiv preprint arXiv:1312.6155},
year = {2014}
}