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

Benchmark: SMT-LIB QF_NRA

Code structure: code structure

Detailed data: data

Installation

DNLSAT is implemented based on Z3 Prover (https://github.com/Z3Prover/z3). The compilation methid is similar to Z3.

cd code
python scripts/mk_make.py
cd build
make -j<num_threads>

Usage

cd code/build
./z3 <input_file>

Experiments

Comparison between different branching heuristics

Comparison with other SMT(NRA) solvers

Contact

Main developer: Zhonghan Wang ([email protected])

Refer to the personal page to find something more interesting.