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

TL;DR

This paper enhances the Conflict-Driven Cylindrical Algebraic Covering algorithm by formulating and solving a set covering problem with reasons, leading to more optimized conflict clause generation in SMT solving for non-linear real arithmetic.

Contribution

It introduces a novel set covering optimization within CDCAC, including a data reduction step and an LP-based solver, improving SMT solver efficiency for non-linear real arithmetic.

Findings

The data reduction step solves many benchmark instances efficiently.

The LP-based solver effectively handles remaining optimization cases.

Integration of these techniques can significantly boost SMT solver performance.

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.