Efficient Solution of a Class of Quantified Constraints with Quantifier Prefix Exists-Forall |
| |
Authors: | Milan Hladík Stefan Ratschan |
| |
Affiliation: | 1. Charles University, Prague, Czech Republic 2. Institute of Computer Science, Academy of Sciences of the Czech Republic, Prague, Czech Republic
|
| |
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. |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|