Milan Hladík and Stefan Ratschan. Efficient solution of a class of quantified constraints with quantifier prefix exists-forall. Math. Comput. Sci., 8(3-4):329–340, 2014.
[PDF] [gzipped postscript] [postscript] [HTML]
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.
@article{HlaRat2014a,
author = "Milan Hlad\'{\i}k and Stefan Ratschan",
title = "Efficient solution of a class of quantified constraints with quantifier prefix exists-forall",
journal = "Math. Comput. Sci.",
fjournal = "Mathematics in Computer Science",
volume = "8",
number = "3-4",
pages = "329-340",
year = "2014",
doi = "10.1007/s11786-014-0195-8",
issn = "1661-8270",
url = "https://doi.org/10.1007/s11786-014-0195-8",
bib2html_dl_html = "https://link.springer.com/article/10.1007%2Fs11786-014-0195-8",
bib2html_dl_pdf = "https://rdcu.be/cnoXw",
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 = "Constraint solving, Decision procedures, Interval computation",
}
Generated by bib2html.pl (written by Patrick Riley ) on Mon Apr 15, 2024 08:26:42