Function synthesis for maximizing model counting
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 JanDisplayed 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 20mTalk | 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 20mTalk | 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 20mTalk | 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 20mTalk | 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 |