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

0430462 - ÚI 2015 RIV CH eng J - Článek v odborném periodiku
Hladík, M. - Ratschan, Stefan
Efficient Solution of a Class of Quantified Constraints with Quantifier Prefix Exists-Forall.
Mathematics in Computer Science. Roč. 8, 3-4 (2014), s. 329-340. ISSN 1661-8289
Grant CEP: GA ČR GCP202/12/J060
Grant ostatní: GA ČR(CZ) GA13-10660S
Institucionální podpora: RVO:67985807
Klíčová slova: constraint solving * decision procedures * interval computation
Kód oboru RIV: IN - Informatika

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 combinationwith conservative linear programming approximation. In comparison with previouswork, 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.
Trvalý link: http://hdl.handle.net/11104/0235395