Abstract
Given a boolean formula \(\phi (X, Y, Z)\), the Max#SAT problem [10, 29] 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 [23] and DSSAT [19] 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.
This work was supported by the French national projects TAVA (ANR-20-CE25-0009) and SECUREVAL (ANR-22-PECY-05).
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
Actually these problems can even be reduced to SSAT instances.
- 2.
Thanks to specific parametrization and the oracles [5] used internally by BaxMC, it can be considered an exact solver on the small instances of interest in this section.
References
Audemard, G., Lagniez, J., Miceli, M.: A new exact solver for (weighted) max#SAT. In: SAT. LIPIcs, vol. 236, pp. 28:1–28:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)
Aziz, R.A., Chu, G., Muise, C., Stuckey, P.: \(\#\exists \)SAT: projected model counting. In: Heule, M., Weaver, S. (eds.) SAT 2015. LNCS, vol. 9340, pp. 121–137. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-24318-4_10
Bardin, S., Girol, G.: A Quantitative Flavour of Robust Reachability. arXiv preprint arXiv:2212.05244 (2022)
Chakraborty, S., Fried, D., Meel, K.S., Vardi, M.Y.: From weighted to unweighted model counting. In: IJCAI, pp. 689–695. AAAI Press (2015)
Chakraborty, S., Meel, K.S., Vardi, M.Y.: A Scalable Approximate Model Counter. arXiv preprint arXiv:1306.5726 (2013)
Chakraborty, S., Meel, K.S., Vardi, M.Y.: Balancing Scalability and Uniformity in SAT Witness Generator. In: DAC, pp. 60:1–60:6. ACM (2014)
Chen, P., Huang, Y., Jiang, J.R.: A sharp leap from quantified boolean formula to stochastic boolean satisfiability solving. In: AAAI, pp. 3697–3706. AAAI Press (2021)
Cheng, C., Jiang, J.R.: Lifting (D)QBF preprocessing and solving techniques to (D)SSAT. In: AAAI, pp. 3906–3914. AAAI Press (2023)
Dullien, T.: Weird machines, exploitability, and provable unexploitability. IEEE Trans. Emerg. Top. Comput. 8(2), 391–403 (2020)
Fremont, D.J., Rabe, M.N., Seshia, S.A.: Maximum model counting. In: AAAI, pp. 3885–3892. AAAI Press (2017)
Garey, M.R., Johnson, D.S.: Computers and Intractability: A Guide to the Theory of NP-Completeness. W.H. Freeman (1979)
Garey, M.R., Johnson, D.S., So, H.C.: An application of graph coloring to printed circuit testing (working paper). In: FOCS, pp. 178–183 (1975)
Gario, M., Micheli, A.: PySMT: a solver-agnostic library for fast prototyping of SMT-based algorithms. In: SMT Workshop, vol. 2015 (2015)
Henkin, L., Karp, C.R.: Some remarks on infinitely long formulas. J. Symb. Log. 30(1), 96–97 (1965). https://doi.org/10.2307/2270594
King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385–394 (1976)
Kovásznai, G.: What is the state-of-the-art in DQBF solving. In: MaCS-16. Joint Conference on Mathematics and Computer Science (2016)
Kullmann, O.: Fundaments of branching heuristics. In: Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 336, pp. 351–390. IOS Press (2021)
Lagniez, J., Marquis, P.: A recursive algorithm for projected model counting. In: AAAI, pp. 1536–1543. AAAI Press (2019)
Lee, N., Jiang, J.R.: Dependency stochastic boolean satisfiability: a logical formalism for NEXPTIME decision problems with uncertainty. In: AAAI, pp. 3877–3885. AAAI Press (2021)
Luo, Y., Cheng, C., Jiang, J.R.: A resolution proof system for dependency stochastic boolean satisfiability. J. Autom. Reason. 67(3), 26 (2023)
Papadimitriou, C.H.: Games against nature. J. Comput. Syst. Sci. 31(2), 288–301 (1985)
Peterson, G., Reif, J., Azhar, S.: Lower bounds for multiplayer noncooperative games of incomplete information. Comput. Math. Appl. 41(7–8), 957–992 (2001)
Peterson, G.L., Reif, J.H.: Multiple-person alternation. In: FOCS, pp. 348–363. IEEE Computer Society (1979)
Phan, Q., Bang, L., Pasareanu, C.S., Malacaria, P., Bultan, T.: Synthesis of adaptive side-channel attacks. In: IACR Cryptol. ePrint Arch, p. 401 (2017)
Saha, S., Eiers, W., Kadron, I.B., Bang, L., Bultan, T.: Incremental adaptive attack synthesis. arXiv preprint arXiv:1905.05322 (2019)
Smith, G.: On the foundations of quantitative information flow. In: de Alfaro, L. (ed.) FoSSaCS 2009. LNCS, vol. 5504, pp. 288–302. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-00596-1_21
Vigouroux, T., Bozga, M., Ene, C., Mounier, L.: DQMaxMC Solver (2023). https://doi.org/10.5281/zenodo.8405351
Vigouroux, T., Bozga, M., Ene, C., Mounier, L.: Function synthesis for maximizing model counting. arXiv preprint arXiv:2305.10003 (2023)
Vigouroux, T., Ene, C., Monniaux, D., Mounier, L., Potet, M.: BaxMC: a CEGAR approach to Max#SAT. In: FMCAD, pp. 170–178. IEEE (2022)
Wang, H., Tu, K., Jiang, J.R., Scholl, C.: Quantifier elimination in stochastic boolean satisfiability. In: SAT. LIPIcs, vol. 236, pp. 23:1–23:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)
Wimmer, R., Scholl, C., Wimmer, K., Becker, B.: Dependency schemes for DQBF. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 473–489. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-40970-2_29
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2024 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
Cite this paper
Vigouroux, T., Bozga, M., Ene, C., Mounier, L. (2024). Function Synthesis for Maximizing Model Counting. In: Dimitrova, R., Lahav, O., Wolff, S. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2024. Lecture Notes in Computer Science, vol 14499. Springer, Cham. https://doi.org/10.1007/978-3-031-50524-9_12
Download citation
DOI: https://doi.org/10.1007/978-3-031-50524-9_12
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-50523-2
Online ISBN: 978-3-031-50524-9
eBook Packages: Computer ScienceComputer Science (R0)