Efficient Solution of a Class of Quantified Constraints with Quantifier Prefix Exists-Forall

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.