Seminars

NO.238 Model Counting: Theory meets Practice

Shonan Village Center

February 2 - 6, 2026 (Check-in: February 1, 2026 )

Organizers

  • Pierre Marquis
    • Universit´e d’Artois, CNRS and CRIL, France
  • Kenji Hashimoto
    • Kagawa University, Japan
  • Johannes Klaus Fichte
    • Linköping University, Sweden

Overview

Description: “Model Counting: Theory meets Practice”

1 Research Area

Propositional model counting, also known as number SAT or #SAT, asks to output the number of models of a propositional formula over the set of variables occurring in it [3]. A model is also known as total assignment to the variables of the formula that satisfies the formula. The #SAT problem is canonical for the complexity class #P [40, 33, 1] and we can employ counting to solve any problem located on the Polynomial Hierarchy (PH) by an immediate consequence of Toda’s Theorem [39]. Interestingly, #SAT remains computationally very hard on several classes of propositional formulas, where the SAT problem (deciding satisfiability only, i.e., deciding whether the model count of the input formula is different from 0 or not) becomes tractable, such as 2-CNFs [40, 7]1. Despite the computational hardness, the field has seen considerable advances in recent years and highly efficient solvers emerged, capable of solving larger problems each year [6, 32, 25, 26, 34, 11]. These solvers have immediate use in various domains, such as quantitative questions in formal verification of hardware, software, security protocols, combinatorial optimization, computational mathematics, or simulating quantum circuits. Over the last few years, various applications can be witnessed in the literature [12, 19, 42, 13, 35, 2, 37, 27, 38, 16, 30] and will impact areas such as probabilistic reasoning [10, 28, 14], parameter learning in neuro-symbolic reasoning [29, 36, 41], or computational biology. An annual event, which evaluates solvers and is organized by the community since 2020 [17], provides a snapshot of the current state-of-the-art in model counting.

Today’s, #SAT solving techniques are diverse and far more sophisticated than simply enumerating solutions with the four prevailing ones: (i) component-caching, (ii) knowledge compilation, (iii) dynamic programming, and (iv) approximate counting. These techniques appear to be inherently different, but share many similarities. Recent articles [31, 22, 15] identify connections between structure from a theoretical perspective and solving approaches. Over the last years, approximate solving showed notable progress and dominated the perception from the outside. However, the last years demonstrated significant practical improvements in exact methods and component-caching-based solving [23, 24] and knowledge compilation [26] often outperform approximate techniques. Knowledge compilation (KC), which was pioneered three decades ago [20, 8, 9], is of high practical interest as it enables repeated fast counting by transforming an input formula into an equivalent (potentially large) formula on which counting is solvable in polynomial-time. Beyond counting, KC is of high interest in fields such as knowledge representation, constraint satisfaction, algorithms, complexity theory, machine learning, and databases.

Verifiable #SAT-solving recently emerged to identify and avoid bugs, which are still quite prevalent in today’s solvers. The techniques work by either emitting a trace during solving [18] in a proof system focusing on simple constructs or showing equivalences [5, 4] between the input formula and the resulting compiled formula. Then, the trace can be mathematically verified by a program, which in turn can be audited or formally verified. Interestingly, attempts for trustworthy solvers also yield new mathematical proof systems for counting. The relation between proofs and solving is important as (i) proof systems can model aspects of solving, which allows for analyzing limitations of solvers by mathematical methods of proof complexity; and (ii) we can construct stronger proof systems, which enable to certify very sophisticated and complex solving techniques.

The need for (i) increasingly efficient, correct, and reliable solvers and (ii) robust theoretical understanding of limitations and capabilities of solving techniques is consistently on the rise, as (iii) more and harder problems need to be solved in various contexts. Although some of the research communities focus on the development of increasingly effective solving, theory, and modeling, there have been surprisingly few interactions between the communities when it comes to quantitative aspects. There remains significant unexplored potential for reaching non-trivial advances in the state-of-the-art quantitative solving. The proposed seminar aims at connecting aspects (i)–(iii) and gather leading researchers to pave the way for a fruitful cross fertilization between the topics, from theory to practice and back.

2 Topics to Be Discussed in the Seminar

During the seminar, a range of topics centered around theory and practice of propositional counting problems and extensions in symbolic AI will be covered. These include the following.

(i) Cross-fertilizing improvements from diverse solving techniques: Today’s bestperforming solvers show diverging behavior depending on the application. Approximate solving behaves well on projected instances, is often sufficiently precise if run-time is negligible, and provides rough estimations on large instances. Exact solving such as component-caching and knowledge compilation is often faster, more precise, and enables orthogonal applications. Dynamic programming can easily be parallelized. Since the underlying techniques of the present solving approaches are quite orthogonal, we will discuss questions such as: Can we together identify crucial theoretical benefits of certain algorithms? Can we integrate improvements into orthogonal techniques? Can we benefit from fast pre- and in-processing techniques that appeared in other areas such as SAT-solving or constraint programming? Can stronger solving techniques enable faster solvers? Can we extend techniques, in particular knowledge compilation, from the propositional setting to tasks that are highly relevant for verification and AI such as partial enumeration, weighted model integration, or answer-set programming?

(ii) Improving theoretical understanding: While KC and its applications, in particular limitations and capabilities, have been studied extensively [9], many aspects of quantitative solving have been neglected with focus of theoretical research on decision and optimization problems and hardness results and algorithmic limitations. We aim at reviving theoretical questions on quantitative solving and will discuss: Can proof complexity provide insights into quantitative problem-solving? How could more general techniques in proof complexity look like to establish limitations in the quantitative or probabilistic setting? Are existing hardness results in counting complexity tight for counting on restricted classes of formulas and under more restrictive (natural) reductions? What are the most promising candidates? Can we construct metrics between decision and counting problems that enable fast simplification techniques? Can stronger solving techniques from the decision or optimization setting be transformed to counting? How can we identify general restrictions of KC and what are possible ways to circumvent these limitations?

(iii) Community building for practical applications: Improvements in #SAT-solving
spawned many new applications in AI and natural sciences where decision problems were insufficient. While an annual solver evaluation provides a platform for building tools and generating visibility outside of the immediate community, its focus has largely been on computational challenges. Instead, we want to discuss more general questions: How can we provide robust and easy to use solvers and make them available to a larger community? Can we provide better insights for theoretical research and theoretical understanding from solver evaluations? What does theoretical research need to obtain those insights? What extensions will be interesting for applications in AI, e.g., quantitative preferences? What extensions can we support to make model counting more interesting for natural sciences?

3 Goals and Outcomes

The main outcome will be a road map listing significant challenges. Since the “market” for counting is very large and spans many areas (artificial intelligence, logic, theoretical computer science, natural sciences), we expect to identify new use of model counting, application areas, and synergies. We will share expertise to address these challenges and solve new applications, including joint software and collaboration on data and starting new joint projects. Finally, we aim for kicking off an introductory book to make counting tools and concepts more accessible.

References

[1] Bacchus, F., Dalmao, S., and Pitassi, T. Algorithms and complexity results for #SAT and bayesian inference. In FOCS’03 (Cambridge, MA, USA, Oct. 2003), C. S. Chekuri and D. Micciancio, Eds., IEEE Computer Soc., pp. 340–351.
[2] Baluta, T., Chua, Z. L., Meel, K. S., and Saxena, P. Scalable quantitative verification for deep neural networks. In ICSE’21 (2021), pp. 312–323.
[3] Biere, A., Heule, M., van Maaren, H., and Walsh, T., Eds. Handbook of Satisfiability (2nd Edition). Frontiers in Artificial Intelligence and Applications. IOS Press, Amsterdam, Netherlands, Feb. 2021.
[4] Bryant, R. E., Nawrocki, W., Avigad, J., and Heule, M. J. H. Certified knowledge compilation with application to verified model counting. In SAT’23 (Alghero, Italy, July 2023), vol. 271 of Leibniz International Proceedings in Informatics (LIPIcs), Dagstuhl Publishing, pp. 6:1–6:20.
[5] Capelli, F. Knowledge compilation languages as proof systems. In SAT’19 (2019), vol. 11628 of Lecture Notes in Computer Science, Springer Verlag, pp. 90–99.
[6] Chakraborty, S., Meel, K. S., and Vardi, M. Y. Algorithmic improvements in approximate counting for probabilistic inference: From linear to logarithmic SAT calls. In IJCAI’16 (New York City, NY, USA, July 2016), S. Kambhampati, Ed., The AAAI Press, pp. 3569–3576.
[7] Dahllöf, V., Jonsson, P., and Wahlström, M. Counting models for 2sat and 3sat formulae. Theoretical Computer Science 332, 1 (2005), 265–291.
[8] Darwiche, A. New advances in compiling CNF to decomposable negation normal form. In Proceedings of the 16th European Conference on Artificial Intelligence (ECAI’04) (Valencia, Spain, 2004), R. López De Mántaras and L. Saitta, Eds., IOS Press, pp. 318–322.
[9] Darwiche, A., and Marquis, P. A knowledge compilation map. JAIR 17 (2002), 229–264.
[10] De Raedt, L., Kimmig, A., and Toivonen, H. Problog: A probabilistic prolog and its application in link discovery. In Proceedings of the 20th international joint conference on artificial intelligence (IJCAI’07) (2007), IJCAI, pp. 2462–2467.
[11] Dudek, J. M., Phan, V. H. N., and Vardi, M. Y. Dpmc: Weighted model counting by dynamic programming on project-join trees. In CP’20 (Louvain-la-Neuve, Belgium, Sept. 2020), H. Simonis, Ed., Springer Verlag, pp. 211–230.
[12] Dueñas-Osorio, L., Meel, K. S., Paredes, R., and Vardi, M. Y. Counting-based reliability estimation for power-transmission grids. In AAAI’17 (San Francisco, CA, USA, Feb. 2017), S. P. Singh and S. Markovitch, Eds., The AAAI Press, pp. 4488–4494.
[13] Dueñas-Osorio, L., Meel, K. S., Paredes, R., and Vardi, M. Y. Counting-based reliability estimation for power-transmission grids. In Proceedings of the 31st AAAI Conference on Artificial Intelligence (AAAI’17) (San Francisco, California, USA, 2017), S. P. Singh and S. Markovitch, Eds., The AAAI Press, pp. 4488–4494.
[14] Eiter, T., Hecher, M., and Kiesel, R. Treewidth-Aware Cycle Breaking for Algebraic Answer Set Counting. In Proceedings of the 18th International Conference on Principles of Knowledge Representation and Reasoning (11 2021), pp. 269–279.