DNLSAT: A Dynamic Variable Ordering MCSAT Framework for Nonlinear Real Arithmetic

TL;DR

This paper introduces dnlsat, an efficient implementation of dynamic variable ordering in MCSAT for nonlinear real arithmetic, significantly improving solving speed and instance coverage in SMT(NRA).

Contribution

It presents a novel implementation of dynamic variable ordering in MCSAT, with specialized data structures and mechanisms, enhancing performance over existing SMT solvers.

Findings

Dnlsat accelerates solving speed.

It solves more satisfiable instances.

Demonstrates effectiveness through experimental results.

Abstract

Satisfiability modulo nonlinear real arithmetic theory (SMT(NRA)) solving is essential to multiple applications, including program verification, program synthesis and software testing. In this context, recently model constructing satisfiability calculus (MCSAT) has been invented to directly search for models in the theory space. Although following papers discussed practical directions and updates on MCSAT, less attention has been paid to the detailed implementation. In this paper, we present an efficient implementation of dynamic variable orderings of MCSAT, called dnlsat. We show carefully designed data structures and promising mechanisms, such as branching heuristic, restart, and lemma management. Besides, we also give a theoretical study of potential influences brought by the dynamic variablr ordering. The experimental evaluation shows that dnlsat accelerates the solving speed and solves more satisfiable instances than other state-of-the-art SMT solvers. Demonstration Video: https://youtu.be/T2Z0gZQjnPw Code: https://github.com/yogurt-shadow/dnlsat/tree/master/code Benchmark https://zenodo.org/records/10607722/files/QF_NRA.tar.zst?download=1