Function synthesis for maximizing model counting
Authors:
Thomas Vigouroux,
Marius Bozga,
Cristian Ene,
Laurent Mounier
Abstract:
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…
▽ More
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.
△ Less
Submitted 12 September, 2023; v1 submitted 17 May, 2023;
originally announced May 2023.
BAXMC: a CEGAR approach to Max#SAT
Authors:
Thomas Vigouroux,
Cristian Ene,
David Monniaux,
Laurent Mounier,
Marie-Laure Potet
Abstract:
Max#SAT is an important problem with multiple applications in security and program synthesis that is proven hard to solve. It is defined as: given a parameterized quantifier-free propositional formula compute parameters such that the number of models of the formula is maximal. As an extension, the formula can include an existential prefix. We propose a CEGAR-based algorithm and refinements thereof…
▽ More
Max#SAT is an important problem with multiple applications in security and program synthesis that is proven hard to solve. It is defined as: given a parameterized quantifier-free propositional formula compute parameters such that the number of models of the formula is maximal. As an extension, the formula can include an existential prefix. We propose a CEGAR-based algorithm and refinements thereof, based on either exact or approximate model counting, and prove its correctness in both cases. Our experiments show that this algorithm has much better effective complexity than the state of the art.
△ Less
Submitted 6 February, 2023; v1 submitted 2 November, 2022;
originally announced November 2022.
