Solver primo advances automated reasoning for linear real arithmetic
Vibe-Coded and Tuned: A State-of-the-Art SMT Solver for QF-LRA
Logic in Computer Science
Summary
Solving math problems with real numbers can be tricky for computers. The authors introduce primo, a new software tool that solves these problems faster and better than previous tools. They improved primo by carefully studying past methods, measuring what slows it down, and fine-tuning its settings. This shows a new way of building such solvers can make big improvements.
What this means in practice
- •For formal verification engineers: Verify software and hardware designs that involve arithmetic on real numbers more efficiently using primo.
- •For optimization software developers: Integrate primo to enhance solvers used in operations research problems involving linear real constraints.
Authors
Mikoláš Janota, Jan Jakubův
Abstract
This paper presents the SMT solver primo, which is fully vibe-coded and then parameter-tuned, achieving state-of-the-art results on linear real arithmetic (QF-LRA). The performance of primo is achieved by a systematic literature survey, repeated profiling, and parameter tuning. The resulting solver outperforms the winner of the QF-LRA track of SMT-COMP~2026. This confirms that vibe-coding of automated reasoning tools will enable us to make great strides in the future.