• PhD Student:
• Marie Miceli
• Funding : CRIL
• PhD defended on :
• Nov 30, 2023

This thesis is about solving problems that deal with minimization and maximization in the context of model counting. Their purpose is to determine, given a Boolean propositional formula, an assignment on a deﬁned set of variables such that the number of models of the formula is either maximized or minimized. These problems, whose decision versions are NPPP-hard, are diﬃcult to solve in practice, but are nonetheless important in many applications, such as probabilistic Inference, Program Synthesis, Quantitative Information Flow, Planning Problems, Maximum Probabilistic Equivalence Checking. . . In the ﬁrst part, we introduce a new bi-objective optimization problem, identifying soft cores, which can be deﬁned as minimizing both the set of satisﬁed variables in the assignment found and the model count. The notion of soft cores is part of the Explainable AI domain, that intends to explain to users the decisions and behaviors of computer systems. Indeed, they can be used to detect which constraints prevent expected solutions from being possible, or to help modeling in debugging tools. We also link this problem to another two NPPP-complete problems: we propose a reduction from the key problem Functional E-MajSAT, and give an encoding to translate any instance into a Max#SAT one. In the second part, we propose an exact and anytime solver, d4Max, to solve the Weighted Max#SAT problem, a generalization of both the Functional E-MajSAT and Max#SAT problems. Given a weighted and quantiﬁed CNF formula, the Weighted Max#SAT problem is to ﬁnd the assignment on a deﬁned set of variables such that the weighted model count over a projected set of variables is maximized. Thus, it allows us to consider problems that deal with reasoning in uncertain environments, for example any Probabilistic Inference problems, or Exist-Random and Exist-Random-Exist SSAT benchmarks. This solver d4Max being anytime, it also answers the decision version of the Max#SAT problem, which is to determine if there exists an assignment over the set of variables such that the number of models reaches some threshold.