cs.AIMay 24, 2026

Solving Combinatorial Counting Problems with Weighted First-Order Model Counting

Authors: Yuanhong Wang, Juhua Pu, Yuxu Zhou, Yuyi Wang, Ondřej Kuželka

Organizations: School of Artificial Intelligence, Jilin University, Changchun, China · State Key Laboratory of Complex & Critical Software Environment, Beihang University, China · National Research Center for Educational Materials, China · CRRC Zhuzhou Insitute, Zhuzhou, China · Tengen Intelligence Institute, China · Czech Technical University in Prague, Prague, Czech Republic

Abstract

Combinatorial counting problems pervade artificial intelligence, statistics, and discrete mathematics. Whether the task is enumerating subsets, multisets, permutations, partitions, or compositions under structural and arithmetic constraints, solving it remains a stubbornly manual exercise. Closed-form derivations are powerful but brittle, while naive encodings to propositional model counting or constraint satisfaction destroy the exchangeability that makes counting tractable in the first place. We present Cofola (COmbinatorial counting LAnguage with First-Order logic), a typed declarative language whose primitives are the combinatorial objects that recur in everyday counting questions, including sets, bags, tuples, sequences, circles, partitions, and compositions, together with natural relational and arithmetic constraints over them. A denotational semantics maps every Cofola program to a well-defined combinatorial counting problem, and a three-phase compilation pipeline (preprocessing, decomposition, and symmetry-preserving encoding) reduces this problem to a weighted first-order model counting (WFOMC) instance augmented with coefficient-extraction constraints. To stay inside known domain-liftable fragments whenever possible, the encoding groups indistinguishable entities, breaks the symmetry of unordered groupings lexicographically, and encodes sequences and circles via order axioms. On a suite of representative combinatorial counting problems, ranging from textbook math problems to multi-object scenarios that the closest prior framework cannot express, Cofola produces concise specifications and a uniform solving pipeline that is practical end-to-end.

Explore similar work

CardsList
May 5, 2026cs.LO

A Fast Model Counting Algorithm for Two-Variable Logic with Counting and Modulo Counting Quantifiers

Weighted first-order model counting (WFOMC) is a central task in lifted probabilistic inference: It asks for the weighted sum of all models of a first-order sentence over a finite domain. A long line of work has identified domain-liftable fragments of first-order logic, that is, syntactic classes for which WFOMC can be solved in time polynomial in the domain size. Among them, the two-variable fragment with counting quantifiers, C2\mathbf{C}^2, is one of the most expressive known liftable fragments. Existing algorithms for C2\mathbf{C}^2, however, establish tractability through multi-stage reductions that eliminate counting quantifiers via cardinality constraints, which introduces substantial practical overhead as the domain size grows. In this paper, we introduce IncrementalWFOMC3, a lifted algorithm for WFOMC on C2\mathbf{C}^2 and its modulo counting extension, Cmod2\mathbf{C}^2_{\text{mod}}. Instead of relying on reduction techniques, IncrementalWFOMC3 operates directly on a Scott normal form that retains counting quantifiers throughout inference. This direct treatment yields two main results. First, we derive a tighter data-complexity bound for WFOMC in C2\mathbf{C}^2, reducing the degree of the polynomial from quadratic to linear in the counting parameters. Second, we prove that Cmod2\mathbf{C}^2_{\text{mod}} is domain-liftable, extending tractability from C2\mathbf{C}^2 to a richer fragment with native modulo counting support. Finally, our empirical evaluation shows that IncrementalWFOMC3 delivers orders-of-magnitude runtime improvements and better scalability than both existing WFOMC algorithms and state-of-the-art propositional model counters.
Shixin Sun, Astrid Klipfel, Ondřej Kuželka +2
CountingFirst-Order LogicCardinalityComputableProbabilistic InferenceLogic
AskPDF
Jun 18, 2026cs.AI

CombEval: A Framework for Evaluating Combinatorial Counting in Large Language Models

We present CombEval, a dynamic benchmark for evaluating combinatorial counting in large language models. CombEval represents each problem as a typed Cofola specification over entities, combinatorial objects, object dependencies, and constraints, enabling controlled generation of natural-language counting problems with exact solver-verified answers. Unlike static collections, CombEval supports systematic variation of object type, entity scale, constraint count, and reasoning depth. We evaluate 11 LLMs under direct and code-augmented settings and find that models remain brittle on ordered objects, indistinguishable elements, relatively positional constraints, and nested object dependencies. Error analysis further identifies failures in constraint interpretation and counting principles. CombEval provides a diagnostic testbed for studying when and why LLMs fail at combinatorial reasoning. The code and generated benchmark suites are publicly available at \url{https://github.com/YuxuZhou-CN/combination-problem-generation}.
Yuxu Zhou, Ondřej Kuželka, Yuyi Wang +2
CombinationsCountingBenchmark Suite
AskPDF
Sep 1, 2020cs.AI

PyCSP3: Modeling Combinatorial Constrained Problems in Python

In this document, we introduce PyCSP33, a Python library that allows us to write models of combinatorial constrained problems in a declarative manner. Currently, with PyCSP33, you can write models of constraint satisfaction and optimization problems. More specifically, you can build CSP (Constraint Satisfaction Problem) and COP (Constraint Optimization Problem) models. Importantly, there is a complete separation between the modeling and solving phases: you write a model, you compile it (while providing some data) in order to generate an XCSP33 instance (file), and you solve that problem instance by means of a constraint solver. You can also directly pilot the solving procedure in PyCSP33, possibly conducting an incremental solving strategy. In this document, you will find all that you need to know about PyCSP33, with more than 50 illustrative models.
Christophe Lecoutre, Nicolas Szczepanski
Constraint SatisfactionPython
AskPDF