Reproduce “Optimising Cylindrical Algebraic Coverings for use in SMT by Solving a Set Covering Problem with Reasons” on OpenResearch
Turn your favorite coding agents into research agents that review literature, develop hypotheses, and run experiments.
Universal app for Apple silicon and Intel. Requires macOS 11 or later.
About this paper
Abiola Babatunde, Matthew England, AmirHosein Sadeghimanesh
Researchers at Coventry University introduce the "Set Covering Problem with Reasons" (SCPR) to optimize conflict clause generation within the Conflict-Driven Cylindrical Algebraic Covering (CDCAC) algorithm for SMT solvers in Non-linear Real Arithmetic. Their proposed two-phase pipeline, combining a generalized Beasley reduction with a Linear Programming solver, successfully yields provably minimal conflict clauses with minimal computational overhead, solving 95.5% of instances purely by reduction and the rest optimally in under 1 millisecond.
Key insights
- The generalized Beasley reduction is highly effective for SCPR instances, solving 95.5% of real-world cases directly and significantly reducing the complexity of the remaining instances.
- Linear Programming (LP) provides a robust and highly efficient exact method for SCPR, consistently yielding optimal solutions with very low computational overhead.
- While some metaheuristics are fast, they generally offer lower accuracy compared to exact methods, suggesting that for these SMT-derived SCPR instances, exact solvers are more practical due to the high efficiency of reduction and LP.
Summary by alphaXiv.
Tip: change arxiv.org to autoarxiv.org in any arXiv abstract link to open the paper here.