Showing cs.SCShow all
3 papers · 1 filter
cs.SC2024
DNLSAT: A Dynamic Variable Ordering MCSAT Framework for Nonlinear Real Arithmetic
Zhonghan Wang
Satisfiability modulo nonlinear real arithmetic theory (SMT(NRA)) solving is essential to multiple applications, including program verification, program synthesis and software test…
cs.SC2024
Improving NLSAT for Nonlinear Real Arithmetic
Zhonghan Wang
The Model-Constructing Satisfiability Calculus (MCSAT) framework has been applied to SMT problems over various arithmetic theories. NLSAT, an implementation using cylindrical algeb…
cs.SC2023
Efficient Local Search for Nonlinear Real Arithmetic
Zhonghan Wang, Bohua Zhan, Bohan Li +1
Local search has recently been applied to SMT problems over various arithmetic theories. Among these, nonlinear real arithmetic poses special challenges due to its uncountable solu…