POPL 2024
Sun 14 - Sat 20 January 2024 London, United Kingdom
Mon 15 Jan 2024 12:00 - 12:20 at Marconi Room - Session 2: SAT, SMT and Automated Reasoning Chair(s): David Monniaux

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 solution space and potential need to solve higher-degree polynomials. As a consequence, existing work on local search only considered fragments of the theory. In this work, we analyze the difficulties and propose ways to address them, resulting in an efficient search algorithm that covers the full theory of nonlinear real arithmetic. In particular, we present two algorithmic improvements: incremental computation of variable scores and temporary relaxation of equality constraints. We also discuss choice of candidate moves and a look-ahead mechanism in case when no critical moves are available. The resulting implementation is competitive on satisfiable problem instances against complete methods such as MCSAT in existing SMT solvers.

Mon 15 Jan

Displayed time zone: London change

11:00 - 12:30
Session 2: SAT, SMT and Automated ReasoningVMCAI at Marconi Room
Chair(s): David Monniaux Université Grenoble Alpes - CNRS - Grenoble INP - Verimag
11:00
20m
Talk
Function synthesis for maximizing model counting
VMCAI
Thomas Vigouroux VERIMAG - UGA, Marius Bozga CNRS; Université Grenoble Alpes, Cristian Ene Verimag, Grenoble, Laurent Mounier Université Grenoble Alpes
Pre-print
11:20
20m
Talk
Boosting Constrained Horn Solving by Unsat Core Learning
VMCAI
Parosh Aziz Abdulla Uppsala University, Sweden, Chencheng Liang Uppsala University, Philipp Rümmer University of Regensburg and Uppsala University
11:40
20m
Talk
On the Verification of a Subgraph Construction Algorithm
VMCAI
Lucas Böltz Univerity of Koblenz, Viorica Sofronie-Stokkermans University of Koblenz, Hannes Frey University of Koblenz
12:00
20m
Talk
Efficient Local Search for Nonlinear Real Arithmetic
VMCAI
Zhonghan Wang State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Bohua Zhan Institute of Software, Chinese Academy of Sciences, Bohan Li State Key Laboratory of Computer Science Institute of Software, Chinese Academy of Sciences, Beijing, China, Shaowei Cai Institute of Software at Chinese Academy of Sciences