Adapting real quantifier elimination methods for conflict set computation

DOI10.1007/978-3-319-24246-0_10MaRDI QIDQ2964460zbMATH OpenOpenAlexFDO

Authors Maximilian Jaroschek, Pablo Federico Dobal, Pascal Fontaine

Publication date 27 February 2017

Published in Frontiers of Combining Systems (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1511.01123

zbMATH Keywords

conflict setcylindrical algebraic decompositionreal quantifier eliminationSMTvirtual substitution

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Quantifier elimination, model completeness, and related topics (03C10) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Abstract: The satisfiability problem in real closed fields is decidable. In the context of satisfiability modulo theories, the problem restricted to conjunctive sets of literals, that is, sets of polynomial constraints, is of particular importance. One of the central problems is the computation of good explanations of the unsatisfiability of such sets, i.e. obtaining a small subset of the input constraints whose conjunction is already unsatisfiable. We adapt two commonly used real quantifier elimination methods, cylindrical algebraic decomposition and virtual substitution, to provide such conflict sets and demonstrate the performance of our method in practice.

Recommendations

• NP-completeness of small conflict set generation for congruence closure
• Fully incremental cylindrical algebraic decomposition
• scientific article; zbMATH DE number 1302474
• A Quantifier Elimination Algorithm for Linear Real Arithmetic
• A survey of some methods for real quantifier elimination, decision, and satisfiability and their applications

Cites work

• An incremental algorithm for computing cylindrical algebraic decompositions
• Combining decision procedures by (model-)equality propagation
• Constructing a single cell in cylindrical algebraic decomposition
• scientific article; zbMATH DE number 1263423 (Why is no real title available?)
• scientific article; zbMATH DE number 1157666 (Why is no real title available?)
• Model-based theory combination
• Partial cylindrical algebraic decomposition for quantifier elimination
• QEPCAD B
• Quantifier elimination for real algebra -- the quadratic case and beyond
• Real quantifier elimination is doubly exponential
• Simplification by Cooperating Decision Procedures
• Simplification of quantifier-free formulae over ordered fields
• Simplify: a theorem prover for program checking
• Solving non-linear arithmetic
• The complexity of linear problems in fields
• The complexity of quantifier elimination and cylindrical algebraic decomposition
• Verification of clock synchronization algorithms: experiments on a combination of deductive tools

Cited in

(2)

• Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings
• Fully incremental cylindrical algebraic decomposition

Describes a project that uses

Uses Software

• QEPCAD
• REDUCE
• REDLOG
• SIMPLIFY
• SMT-RAT

This page was built for publication: Adapting real quantifier elimination methods for conflict set computation

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2964460)