-
Computational Complexity. While the SAT problem is already known to be NP-complete [
15,
16
], its generalization #SAT is believed to be even harder. Namely, #SAT is known to be #·
Pcomplete [
17
], and by direct implications from a result by Toda [
18
], any problem on the
polynomial hierarchy [
19, 20
] can be solved in polynomial-time by a machine with access to
an oracle that can output the model count for a given formula. The problem WMC is also #·
Pcomplete. But, PMC is harder under standard assumptions and complete for the class #· NP [
21
].
Common notions on counting complexity follow works by Hemaspaandra and Vollmer [
22
] and
Durand, Herman, and Kolaitis [
21
]. Complexity classes with the sharp-dot operator ‘# · X ’ are
counting classes for which the witness can be tested in decision complexity class X . Similar to
reductions in decision complexity, there are dedicated reductions between two counting problems.
A parsimonious reduction preserves the cardinality between the corresponding witness sets and is
computable in polynomial time. A subtractive reduction between two counting problems consists
of two functions. The first function may over-count and the second function determines the
precise correction for the over-count, which is then compensated by a subtraction.
Counting and its Connection to Quantitative Reasoning. To illustrate the connection, we
elaborate on an introductory example about Bayesian inference, which can be found in lectures
on Bayesian reasoning, c.f. [
23
]. Assume that we have a bag of four marbles of which each could
be either red or blue. However, we cannot see inside the box and are hence unaware of the exact
colors. According to the colors and the setting, we may have vfie potential combinations of colors.
To determine the individual colors, we are only allowed to take out one marble at a time and put
it back into the bag. While we could repeat this experiment for a very long time and obtain the
combination that has the highest probability, we assume that we repeat the experiment only three
times. Suppose that we observed the combination blue-red-blue and want to conjecture how likely
blue-red-red-red is. Therefore, we can simply illustrate the possible combinations as paths. In the
ifrst step, we can have a blue, red, red, or red marble assuming that blue-red-red-red was inside
the bag. In steps two and three, we can have the same situation as a marble is put back inside
the bag after each step. However, only a few paths are “accepting” according to the observation
that we had seen blue-red-blue in our experiment when taking three marbles. Overall, we have
3 paths out of the 43 possible paths that are consistent with the observation. If we consider the
same experiment for each of the vfie possible conjectures of marbles and sum the paths that are
consistent with the observation, we count 20 paths in total. By counting 3 paths and in total 20
paths, we obtain a probability of 3/20 for our conjecture blue-red-red-red under the observation
blue-red-blue. In that way, we can obtain the probabilities by counting.
Abstract Argumentation. When modeling problems in reasoning and artificial intelligence [
24,
25
], we oftentimes rely on more extended frameworks to enable high-level encoding and avoid
spacious encodings. A popular framework for modeling problems that are related to arguments
and their interaction is abstract argumentation [
26, 27
]. There, counting complexity has been
considered in the literature [
28, 29
]. The most recent competition also featured counting
questions [
30
], which will hopefully enable probabilistic questions in abstraction argumentation
beyond a simple enumeration.
Practical Solving. Over the last years, tremendous progress in solving has been made and a
recently established competition makes continuing improvements visible [
31
]. Today’s solvers
provide exact, high precision, or approximate solving capabilities. Some solvers extend techniques
from SAT solving by concepts such as component caching [
32
], knowledge compilation [
33
], or
approximate solving [
34
], but also techniques from parameterized algorithmics proved helpful [
35,
36
].
Conclusion. Model counters are key tools for symbolic quantitative reasoning, which allow for
faster reasoning than simple enumeration of models. We believe that key challenges for the next
years are scalability, trustworthiness, and provability correctness of practical solvers. We hope
that effective solvers for model counting make probabilistic symbolic reasoning accessible to a
variety of scientific fields such as computational biology and psychology as cognitive reasoning.