Efficient solution of a class of quantified constraints with quantifier prefix exists-forall
From MaRDI portal
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.
Recommendations
- Solving existentially quantified constraints with one equality and arbitrarily many inequalities
- Existentially restricted quantified constraint satisfaction
- Beyond Q-resolution and prenex form: a proof system for quantified constraint satisfaction
- Consistency for Quantified Constraint Satisfaction Problems
- Solving quantifier-free first-order constraints over finite sets and binary relations
- Foundations of Information and Knowledge Systems
- Inner and Outer Approximations of Existentially Quantified Equality Constraints
- An approximative inference method for solving \(\exists \forall \)SO satisfiability problems
- scientific article; zbMATH DE number 1759450
- Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds
Cites work
- scientific article; zbMATH DE number 2080299 (Why is no real title available?)
- scientific article; zbMATH DE number 3068536 (Why is no real title available?)
- A posteriori direction selection rules for interval optimization methods
- Automatic Generation of Polynomial Loop Invariants
- Constructing invariants for hybrid systems
- Efficient handling of universally quantified inequalities
- Efficient solving of quantified inequality constraints over the real numbers
- Guaranteed tuning, with application to robust control and motion planning
- Interval Methods for Systems of Equations
- Linear interval inequalities
- Nonlinear systems.
- Providing a Basin of Attraction to a Target Region of Polynomial Systems by Computation of Lyapunov-Like Functions
- Quantifier elimination and cylindrical algebraic decomposition. Proceedings of a symposium, Linz, Austria, October 6--8, 1993
- Revised CPA method to compute Lyapunov functions for nonlinear systems
- SOSTOOLS and Its Control Applications
- Search heuristics for box decomposition methods
- Subdivision Direction Selection in Interval Methods for Global Optimization
- Termination of rewriting
- Testing positiveness of polynomials
- Verification and synthesis using real quantifier elimination
- Verification, Model Checking, and Abstract Interpretation
- Verification, Model Checking, and Abstract Interpretation
- Weak and strong solvability of interval linear systems of equations and inequalities
Cited in
(2)
This page was built for publication: Efficient solution of a class of quantified constraints with quantifier prefix exists-forall
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q475420)
