Adapting Real Quantifier Elimination Methods for Conflict Set Computation

TL;DR

This paper adapts real quantifier elimination techniques, specifically cylindrical algebraic decomposition and virtual substitution, to efficiently compute conflict sets in polynomial constraint satisfiability problems.

Contribution

It introduces a novel adaptation of existing quantifier elimination methods for conflict set computation in satisfiability modulo theories.

Findings

Effective conflict set computation demonstrated

Performance improvements shown in practical experiments

Applicable to polynomial constraint satisfiability problems

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.