On Weighted Maximum Model Counting: Complexity and Fragments

Maximum model counting <tex xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">$(\text{MAX}\#\exists \text{SAT})$</tex> is a recently introduced extension of projected model counting <tex xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">$(\#\exists \text{SAT})$</tex> that maximizes over a set of variables <tex xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">$X$</tex> the number of assignments over a set <tex xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">$Y$</tex> that can be extended to a satisfying assignment over <tex xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">$Z$</tex>. It is known that <tex xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">$\text{MAX}\#\exists \text{SAT}$</tex> also generalizes weighted <tex xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">$\#\exists \text{SAT}$</tex> and MAXSAT if weights are introduced to the problem. However, for the latter a non-trivial gadget is needed. We propose a more generic weighting scheme that evaluates a fitness term and a probability term simultaneously. In this setting, <tex xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">$\text{MAX}\#\exists \text{SAT}$</tex> extends weighted MAXSAT and <tex xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">$\#\exists \text{SAT}$</tex> without the need of gadgets. As MAXSAT is the canonical problem of cost-optimal reasoning and <tex xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">$\#\exists \text{SAT}$</tex> can be seen as canonical problem of probabilistic reasoning, <tex xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">$\text{MAX}\# 3\text{SAT}$</tex> with the proposed weighting scheme naturally fills the role as canonical problem for cost-optimal probabilistic reasoning. We study the problem from a complexity-theoretic point of view for unary weights and prove that the decision version is <tex xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">$\mathrm{D}_{2}^{\mathrm{P}}{-}$</tex> complete. We then focus on structural parameters and provide an ETH lower bound with respect to the inputs treewidth, as well as a treewidth-aware reduction from <tex xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">$\text{MAX}\#\exists \text{SAT}$</tex> to <tex xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">$\text{MAX}\#\exists \text{SAT}$</tex>.