GET IN TOUCH
MC 2026
Workshop on Counting, Sampling, and Synthesis 2026
Registration
Purpose
The Workshop on Counting, Sampling, and Synthesis is an event for researchers in model counting and sampling. It covers advanced topics such as weighted and projected counters/samplers and various domains such as SAT, SMT, ASP, and CP. The workshop has expanded its focus to include the role of model counters, samplers, and solvers in the area of automated synthesis. The goal of the workshop is to facilitate the exchange of cutting-edge theoretical and practical insights, with a particular emphasis on innovative solver technologies and their real-world applications. Additionally, the workshop provides an opportunity for developers of model counters to showcase their work and share detailed competition results, to encourage discussions that bridge theory and practice.
Venue
This year’s event will be held alongside other workshops at FLoC 2026 (affiliated with the SAT 2026) conference. For more information, please visit the FLoC 2026 website.
Date
Day: Saturday, July 25th, 2026
Schedule (tent.)
| Time | Title | Author(s)/ Presenter |
|---|---|---|
| 09:00-09:15 | Opening | Johannes Fichte, Kuldeep Meel, Markus Hecher |
| 09:15-09:45 | Tutorial: Proof Complexity and Model Counting We survey the area of proof complexity of model counting. Several proof systems for model counting have been suggested since 2019, most of which are inspired by solving approaches. The survey explains the different systems, static and line based, and discusses the simulation order of the systems and known separations. Many proof systems are based on Decision-DNNFs, which are suitably annotated. We also discuss how these proof systems relate to state-of-the-art #SAT solving approaches. In the end, we discuss future directions for the field. |
Olaf Beyersdorff |
| 09:45-10:15 | Proof Systems That Tightly Characterise Model Counting Algorithms Several proof systems for model counting have been introduced in recent years, mainly in an attempt to model #SAT solving and to allow proof logging of solvers. We reexamine these different approaches and show that: (i)~with moderate adaptations, the conceptually quite different proof models of the dynamic system MICE and the static system of annotated Decision-DNNFs are equivalent and (ii)~they tightly characterise state-of-the-art #SAT solving. Thus, these proof systems provide a precise and robust proof-theoretic underpinning of current model counting. We also propose new strengthenings of these proof systems that might lead to stronger model counters. |
Olaf Beyersdorff, Tim Hoffmann, Kaspar Kasche |
| 10.15-11.00 | +++++++++ ☕ Coffee Break +++++++++ | |
| 11:00-11:30 | Proof Logging for Projected Enumeration (and Counting?) Problems in VeriPB When a certifying solver claims that a solution is optimal or that a problem is unsatisfiable, it demonstrates this convincingly by giving a proof log which can be checked by an independent (and ideally formally verified) proof checker. Such an approach should also be viable for enumeration problems (“I have listed all solutions explicitly”) and counting problems (“there are exactly 42 solutions”), but the currently most popular proof logging systems contain several vital features which are incompatible with this goal. We explain how the VeriPB system can be modified for enumeration and counting proofs whilst retaining as much as possible of its powerful “strengthening” and “deletion” features. We implement this extension both inside VeriPB’s user-friendly proof checker and elaborator and the formally verified CakePB backend, and use this to obtain formally verified enumerations of solutions for a range of constraint solving and graph problem instances. |
Tan Yong Kiam, Ciaran Mccreesh, Andy Oertel, Jakob Nordström |
| 11:30-12:00 | From Tensor Networks to Tractable Circuits, and back Tensor networks and circuits are widely used data structures to represent pseudo-Boolean functions. These two formalisms have been studied primarily in separate communities, and this paper aims to establish equivalences between them. We show that some classes of tensor networks that are appealing in practice correspond to classes of circuits with specific properties that have been studied in knowledge compilation as tractable circuits. In particular, we prove that matrix product states (tensor trains) coincide with nondeterministic edge-valued decision diagrams and that tree tensor networks exactly correspond to structured-decomposable circuits. These correspondences enable direct transfer of structural and algorithmic results; for example, canonicity and tractability guarantees known for circuits yield analogous guarantees for the associated tensor networks, and vice versa. |
Alexis de Colnet |
| 12:00-12:30 | Knowledge Compilation for Boolean and Presburger Functional Synthesis Given a relational specification \varphi(X, Y_1, … Y_n), functional synthesis concerns the construction of functions (or terms) F_1(X), … F_n(X) such that \varphi(X, F_1, … F_n) is semantically equivalent to \exists Y_1, … Y_n \varphi(X, Y_1, … Y_n). Such functions are also called Skolem functions, and their algorithmic synthesis has many applications, including in program synthesis, QBF-SAT certificate generation, circuit repair, reactive synthesis, planning and the like. The synthesis problem is intractable unless long-standing complexity-theoretic conjectures are falsified. Fortunately, polynomial-time synthesis algorithms can be designed if \varphi is represented in special normal forms. In this talk, we present some such normal forms when \varphi is a formula in propositional logic or in Presburger arithmetic. We show that normal forms originally studied in AI and formal verification, and others like Synthesis Negation Normal Form (SynNNF) and Subset And-Unrealizable Normal Form (SAUNF) lead to efficient functional synthesis in the Boolean setting. Then, we also discuss a new normal form, Presburger Synthesis Normal Form (or PSyNF)for Presburger specifications that allows us to efficiently extract Skolem functions as Presburger terms. We discuss properties of and relations between these normal forms, and show that every universal representation that admits polynomial-time synthesis is polynomially reducible to SAUNF (for Boolean functional synthesis), and to PSyNF (for Presburger functional synthesis with one output). |
S. Akshay, Supratik Chakraborty |
| 12.30-14.00 | +++++++++ 🍽️ Lunch +++++++++ | |
| 14:00-14:30 | A Novel Reduction from #SAT to #2SAT Based on Symmetry: Simply Drop the Large Clauses The counting problem #2SAT is complete for #P under Turing (many-call) reductions, which dates back to the seminal work by Valiant from 1979. Arguably, this reduction is the opposite from being simple as it is a sophisticated chain of transformation from #SAT, via several variations of the problem of computing the permanent, to the task of counting matchings in graphs, and then finally to #2SAT. In contrast, we give a simple classroom reduction that makes only two calls instead of polynomially many calls that can be then merged into a single call with arithmetic postprocessing (AC0). |
Markus Hecher |
| 14:30-15:00 | Counting Complexity of ASP Answer Set Programming (ASP) is a mature and widely used framework for modeling and solving problems in AI, knowledge representation and reasoning, and combinatorial search. Counting answer sets is of growing importance for analyzing search spaces, navigating ASP programs, and enabling probabilistic reasoning. While Truszczýnski established a complete hierarchy for the computational complexity of ASP decision and reasoning problems (skeptical and credulous), a corresponding systematic treatment of counting problems has been missing so far. We close this gap by providing an almost complete characterisation of the counting complexity landscape for ASP. |
Max Bannach, Johannes Fichte, Johanna Groven, Markus Hecher |
| 15:00-15:30 | Counting for Explanations: Evaluating Domain Theories and Constraint Encodings in Probabilistic Abductive Reasoning As machine learning models such as Random Forests are increasingly deployed in high-stakes environments, the need for formal and rigorous explainability has become paramount. Probabilistic abductive explanations offer a robust framework for this by identifying minimal feature subsets that guarantee a specific prediction with a high probability. However, computing these explanations is notoriously complex. A highly promising approach to solving this is transforming the explanation search into a propositional model counting problem. In this paper, we investigate the practical challenges and algorithmic nuances of this transformation. Specifically, we study the overarching impact of the domain theory formulation and closely examine the role of the majority voting constraint inherent to Random Forests. Because this majority rule acts as a critical cardinality constraint within the propositional logic framework, its representation significantly influences computational performance. We systematically explore various encoding techniques for this cardinality constraint and empirically analyze how different encodings impact the overall effectiveness and efficiency of the underlying model counter. By evaluating these design choices, this work provides critical insights into optimizing the translation of tree-ensemble explainability into tractable model counting instances, paving the way for more scalable formal explanation tools. |
Jean-Marie Lagniez, Markus Hecher |
| 15.30-16.00 | +++++++++ ☕ Coffee Break +++++++++ | |
| 16:00-16:30 | What Should #SMT Count? Model counting has a clear semantics in propositional logic, but its extension to SMT is less canonical. In this talk, we discuss two different interpretations of “#SMT”. In a strong sense, #SMT counts or measures the theory-level solution space, leading to problems such as volume computation, weighted model integration, and symbolic integration. In a weaker sense, the task is to count theory-consistent Boolean assignments over the atoms of the formula, yielding a Boolean-theory interface closer to AllSMT and T-#SAT. These two views correspond to different mathematical objects and algorithmic challenges. While theory-level counting depends on the measure induced by the background theory, predicate-space counting exposes the combinatorial structure of SMT formulas. The talk is intended as a perspective on the landscape of counting modulo theories, a direction that remains comparatively underexplored. |
Giuseppe Spallitta |
| 16:30-17:00 | LP-Based Weighted Model Integration over Non-Linear Real Arithmetic Weighted model integration (WMI) is a relatively recent formalism that has received significant interest as a technique for solving probabilistic inference tasks with complicated weight functions. Existing methods and tools are mostly focused on linear and polynomial functions and provide limited support for WMI of rational or radical functions, which naturally arise in several applications. In this work, we present a novel method for approximate WMI, which provides more effective support for the wide class of semi-algebraic functions that includes rational and radical functions, with literals defined over non-linear real arithmetic. Our algorithm leverages Farkas’ lemma and Handelman’s theorem from real algebraic geometry to reduce WMI to solving a number of linear programming (LP) instances. The algorithm provides formal guarantees on the error bound of the obtained approximation and can reduce it to any user-defined value epsilon. Furthermore, our approach is perfectly parallelizable. Finally, we present extensive experimental results, demonstrating the superior performance of our method on a range of WMI tasks for rational and radical functions when compared to state-of-the-art tools for WMI, in terms of both applicability and tightness. |
S. Akshay, Supratik Chakraborty, Soroush Farokhnia, Amir Goharshady, Harshit Jitendra Motwani, Đorđe Žikelić |
| 17:00-17:30 | Bridging Weighted First Order Model Counting and Graph Polynomials The Weighted First-Order Model Counting Problem (WFOMC) asks to compute the weighted sum of models of a given first-order logic sentence over a given domain. It can be solved in time polynomial in the domain size for sentences from the two-variable fragment with counting quantifiers, known as C2. This polynomial-time complexity is known to be retained when extending C2 by one of the following axioms: linear order axiom, tree axiom, forest axiom, directed acyclic graph axiom or connectedness axiom. An interesting question remains as to which other axioms can be added to the first-order sentences in this way. We provide a new perspective on this problem by associating WFOMC with graph polynomials. Using WFOMC, we define Weak Connectedness Polynomial and Strong Connectedness Polynomials for first-order logic sentences. It turns out that these polynomials have the following interesting properties. First, they can be computed in polynomial time in the domain size for sentences from C2. Second, we can use them to solve WFOMC with all of the existing axioms known to be tractable as well as with new ones such as bipartiteness, strong connectedness, having k connected components, etc. Third, the well-known Tutte polynomial can be recovered as a special case of the Weak Connectedness Polynomial, and the Strict and Non-Strict Directed Chromatic Polynomials can be recovered from the Strong Connectedness Polynomials. |
Ondrej Kuzelka |
| 17:30-18:00 | Quantifying Sensitivity for Tree Ensembles: A symbolic and compositional approach Decision tree ensembles (DTE) are a popular model for a wide range of AI classification tasks, used in multiple safety critical domains, and hence verifying properties on these models has been an active topic of study over the last decade. One such verification question is the problem of sensitivity, which asks, given a DTE, whether a small change in subset of features can lead to misclassification of the input. In this work, our focus is to build a quantitative notion of sensitivity, tailored to DTEs, by discretizing the input space of the model and enumerating the regions which are susceptible to sensitivity. We propose a novel algorithmic technique that can perform this computation efficiently, within a certified error and confidence bound. Our approach is based on encoding the problem as an algebraic decision diagram (ADD), and further splitting it into subproblems that can be solved efficiently and make the computation compositional and scalable. We evaluate the performance of our technique over benchmarks of varying size in terms of number of trees and depth, comparing it against the performance of model counters over the same problem encoding. Experimental results show that our tool EnSensCount achieves significant speedup over other approaches and can scale well with the increasing sizes of the ensembles. |
Ajinkya Naik, Chaitanya Garg, S. Akshay, Ashutosh Gupta, Kuldeep S. Meel |
| 18:00-18:15 | Closing |
Contact
If you have any questions about the workshop, the best way to contact the organizers is by emailing mcw at modelcounting.org.
Team
Organizers
- Johannes K. Fichte (Linköping University, Sweden)
- Markus Hecher (French National Centre for Scientific Research (CNRS), University d’Artois (CRIL), France)
- Kuldeep S. Meel (Georgia Institute of Technology, USA)