Function Synthesis for Maximizing Model Counting

Thomas Vigouroux (1) , Marius Bozga (1) , Cristian Ene (1) , Laurent Mounier (1)

1 VERIMAG - IMAG - VERIMAG

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.

Mots clés: function synthesis; model counting; MAX#SAT; DQBF; DSSAT; adaptive attackers

Domaines: Cryptographie et sécurité [cs.CR]

Thomas Vigouroux, Marius Bozga, Cristian Ene, Laurent Mounier. Function Synthesis for Maximizing Model Counting. 25th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2024), Jan 2024, Londres, United Kingdom. pp.258-279, ⟨10.1007/978-3-031-50524-9_12⟩. ⟨hal-04578258⟩