This is a project which is currently making use of HPC facilities at Newcastle University. It is active.
For further information about this project, please contact:
This project will use high-performance computing to evaluate the performance and scalability of Satisfiability Modulo Theories (SMT) solving for quantifier-free linear real arithmetic (QF_LRA) using exact linear programming (LP) techniques. The cvc5 SMT solver will be extended to integrate exact LP solvers, namely SoPlex and QSopt_ex, with delta-complete decision procedures, following an approach inspired by prior work on LP-based SMT solving but replacing floating-point approximations with exact arithmetic, while still exploiting floating-point operations where possible. Large-scale experimental evaluation will be conducted on the Satisfiability Modulo Theories Library (SMT-LIB) QF_LRA benchmark suite, comprising 1,753 instances of varying size and structural complexity. High-performance computing (HPC) resources will enable massively parallel solver runs, systematic configuration sweeps, and fine-grained performance profiling across solver variants. The study will compare the modified cvc5 against baseline cvc5, as well as established SMT solvers such as Z3 and Yices, measuring runtime, robustness, and decision accuracy.