Optimising Cylindrical Algebraic Coverings for use in SMT by Solving a Set Covering Problem with Reasons

TL;DR

The paper tackles the efficiency bottleneck in CAD-based NRA SMT solving by formulating a Set Covering Problem with Reasons (SCPR) that captures how per-cell generalisations require minimal combinations of constraints to explain unsatisfiability. It generalises Beasley reduction to SCPR and demonstrates that most CDCAC-derived instances can be reduced syntactically, while the remaining cases are solved optimally via a linear-programming formulation. This two-phase pipeline (generalised reduction followed by LP) yields provably minimal conflict clauses with negligible overhead, suggesting a practical path to speeding up SMT solvers for NRA. The work has direct implications for integrating efficient clause minimisation into CDCAC-based engines like cvc5, SMT-RAT, and Maple, potentially accelerating real algebraic reasoning in practice.

Abstract

The Conflict-Driven Cylindrical Algebraic Covering algorithm has proven well suited for performing theory validation checks in the satisfiability modulo theories paradigm for non-linear real arithmetic. CDCAC repurposes the theory underpinning classical cylindrical algebraic decomposition for SMT solving and is implemented in the SMT solvers cvc5 and SMT-RAT, as well as the computer algebra system Maple. It was previously observed that when using cylindrical algebraic decomposition for an SMT theory call, the output can be optimised by solving a single set covering problem instance that minimises the conflict clause. In this paper we consider the corresponding optimisation for CDCAC and observe that CDCAC naturally gives rise to multiple such optimisations within a single call. Each time a covering is generalised in one dimension, the resulting cell in the next dimension is labelled with theory constraints that cannot be satisfied together. We seek the smallest subset of constraints whose union covers all labels from the cells in the current covering. We call this optimisation problem a set covering problem with reasons. To simplify this problem, we introduce a data reduction step that generalises Beasley reduction for the classical set covering problem and show that this step alone solves many of the instances arising from SMT-LIB benchmarks. We then propose an exact solver based on linear programming to efficiently solve the remaining cases. Integrating these techniques into CDCAC has the potential to significantly improve SMT solver performance for non-linear real arithmetic problems.

Figures (3)

• Figure 1: A CAD for the unit circle. It consists of 13 cells: the 13 black discs identify one sample point from each. The 2 points at the intersection of the circle and the dotted lines are point-cells, the other 6 discs on the circle or dotted lines represent one-dimensional cells for those line and curve segments, with the remaining 5 cells representing two dimensional cells of the plane as identified with the different colours. Note the vertical alignment of sample points, illustrating the organisation of cells into cylinders.
• Figure 2: Following the worked example from left to right: we first analysed at $x=0$, found two unsatisfiable intervals and then generalised the finding to apply for $x \in (-1, \infty)$. A similar analysis at $x=-3$ completed the covering with 4 cells to prove unsatisfiability of $\{c_1, c_2, c_3\}$. The right most image shows the full CAD with 43 cells for the three defining polynomials as a comparison.
• Figure 3: Average run time per algorithm (logarithmic $y$-axis).