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

Given a boolean formula ϕ(X, Y, Z), the Max#SAT problem asks for finding a partial model on the set of variables X, maximizing its number of projected models over the set of variables Y. We investigate a strict generalization of Max#SAT allowing dependencies for variables in X, effectively turning it into a synthesis problem. We show that this new problem, called DQMax#SAT, subsumes both the DQBF and DSSAT problems. We provide a general resolution method, based on a reduction to Max#SAT, together with two improvements for dealing with its inherent complexity. We further discuss a concrete application of DQMax#SAT for symbolic synthesis of adaptive attackers in the field of program security. Finally, we report preliminary results obtained on the resolution of benchmark problems using a prototype DQMax#SAT solver implementation.

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