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

TL;DR

This paper presents an efficient implementation of dynamic variable orderings of MCSAT, called dnlsat, and shows carefully designed data structures and promising mechanisms, such as branching heuristic, restart, and lemma management.

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

Figures (3)

• Figure 1: Overall Structure of dnlsat.
• Figure 2: The number of solved instances by different branching heuristics within distinct time limits.
• Figure 3: The number of solved instances by SMT solvers within different time limits.