Pith. sign in

REVIEW 3 major objections 5 minor 13 references

Compilation and Fast Model Counting beyond CNF

T0 review · 3 major / 5 minor · reviewed 2026-08-09 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read Constant-state constraints compile to d-DNNF in FPT time

desk verdict Solid FPT compilation result beyond CNF, but the advertised generality is conditional on an unverified SDNNF compilation oracle that the abstract drops. read the letter →

arxiv 2502.00434 v1 pith:FGWRC6VY submitted 2025-02-01 cs.CC cs.AIcs.LO

Alexis de Colnet , Stefan Szeider , Tianwei Zhang This is my paper · ORCID
classification cs.CCcs.AIcs.LO MSC 68Q1768Q2568R1005C85
keywords knowledgecompilationd-DNNFSDNNFincidencetreewidthfixed-parametertractabilitymodelcountingorderedbinarydecisiondiagramscommutativestatetransitionsystems
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper aims to show that fixed-parameter tractable (FPT) compilation into d-DNNF circuits, the representations that make model counting linear-time, can go far beyond CNF formulas. Its central claim is that any system of constraints that stay in a constant number of states under every partial assignment, such as parity constraints, modulo constraints, and cardinality constraints with constant threshold, can be compiled in time singly exponential in the incidence treewidth of the system, plus a polynomial factor. If correct, this extends a known FPT compilation result for CNF to a broader class of constraints, and it also supplies counting algorithms that avoid compiling at all for important subfamilies. The proof route is to compile each constraint into a low-width complete SDNNF, Tseitin-encode it into CNF, and then compile the resulting CNF; the formal theorem carries an explicit assumption that such minimal-width SDNNF compilation is available in polynomial time, a premise the abstract's informal version drops.

What carries the argument

The central objects are $w$-slim functions for complete SDNNFs: a class $\mathcal{F}$ is $h$-slim when every $n$-variable function has a complete SDNNF of width at most $h(n)$ for every vtree, and the width bound $w$ is the parameter controlling the exponent in the compilation time. Three mechanisms carry the proof. First, Assumption 1 supplies a minimal-width complete SDNNF for each constraint; Lemma 9 turns the nice tree decomposition of the incidence graph into a vtree for each constraint so that the variable orderings align with the decomposition. Second, each SDNNF is Tseitin-encoded into CNF, and Lemma 11 shows that the encoding has incidence treewidth $O(w \cdot tw_i(F))$; compiling that CNF to d-SDNNF and existentially forgetting the auxiliary variables, an operation that preserves d-SDNNF by Lemma 8, recovers the original system. For the faster counting theorems, the machinery is the commutative state transition system (CSTS): a small deterministic automaton whose two transition functions commute, whose minimum number of states modulo literal-flipping is the state size of the constraint; dynamic programming over a nice tree decomposition keeps one state per constraint in each bag, and join nodes are sped up by fast convolution.

What would settle it

A concrete falsifying observation would be to take a headline family of $O(1)$-slim constraints, such as constant-threshold cardinality constraints, and determine whether compiling one constraint into a minimal-width complete SDNNF for an arbitrary vtree is polynomial-time; if this problem is NP-hard for any such family, then Assumption 1 fails and the construction behind the main compilation theorem cannot be instantiated for that family.

Watch

Extended reading notes

Core claim

Under Assumption 1, that each constraint type comes with a polynomial-time algorithm that compiles every constraint of that type into a minimal-width complete SDNNF for any given vtree, Theorem 4 gives an algorithm that, for a system $F$ of constraints all $w$-slim for complete SDNNFs, constructs in time $2^{O(w \cdot tw_i(F))}\mathrm{poly}(|F|+|\mathrm{var}(F)|+w)$ a d-SDNNF circuit for $F$. A class of functions is $w$-slim for complete SDNNFs when each function has, for every vtree, a complete SDNNF of width at most $w$; this formalizes the intuition that the constraint can be in only constantly many states after any partial assignment. The theorem subsumes the known FPT compilation of CNF to d-SDNNF and covers clauses, XORs, modulo-sum constraints, and constant-threshold cardinality constraints. A second thread shows that for literal-symmetric constraints with bounded state size, one can count models in $O(w^{2k}|G_F|)$ elementary operations from a nice width-$k$ tree decomposition, without first compiling; restricting further to one-sided constraints, or to systems of clauses with modulo constraints, the join-node computations can be accelerated with Fourier and zeta transforms, giving $\tilde{O}((2w)^k|G_F|)$ and $\tilde{O}(w^k|G_F|)$ respectively, with $O(2^k k|G_F|)$ for clauses plus XOR.

Load-bearing premise

The load-bearing premise is Assumption 1: for every constraint type in the system, a polynomial-time algorithm must exist that compiles any single constraint into a minimal-width complete SDNNF for any given vtree, and if such an oracle is missing for a natural family, the FPT compilation theorem does not apply to that family.

Editorial extensions

If this is right

  • If the main theorem is correct, every system mixing clauses, parity constraints, and constant-threshold cardinality constraints inherits FPT compilation to d-SDNNF with the same incidence-treewidth parameterization that was previously known only for CNF, assuming the minimal-width compilation oracle exists.
  • The width parameter $w$ cannot simply be dropped from the exponent: even with constraints that are $O(nk)$-slim for complete OBDDs, there are systems of incidence treewidth $O(k)$ whose d-SDNNF representations all have size $(n/k)^{\Omega(k)}$.
  • For literal-symmetric constraints with maximum state size $w$, model counting runs in $O(w^{2k}|G_F|)$ elementary operations, so counting does not have to pay the cost of constructing a compiled circuit.
  • For one-sided constraints the counting bound improves to $\tilde{O}((2w)^k|G_F|)$; for systems of clauses together with modulo constraints, including XOR constraints, it improves to $\tilde{O}(w^k|G_F|)$, and to $O(2^k k|G_F|)$ for clauses plus XOR.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • Editorial extension: the practical bottleneck is Assumption 1, so a concrete next step is to implement minimal-width complete SDNNF compilation for constant-threshold cardinality and modulo constraints and check whether the promised polynomial-time oracle holds on realistic instances.
  • A possible extension the paper leaves implicit is allowing slowly growing width $w(n)$ rather than constant width; since the running time is $2^{O(wk)}$, quasi-polynomial width would still give polynomial time for constant incidence treewidth.
  • The paper's closing question, whether CNF-encoding the constraints before compiling is provably worse than compiling the original system directly, could be tested empirically by comparing d-SDNNF sizes for mixed parity-and-cardinality systems against their Tseitin-encoded CNF compilations.
  • The fast counting algorithms suggest that bounded incidence treewidth can be exploited for model counting without any d-SDNNF construction, and this may carry over to weighted counting or projected counting for the same constant-state constraint families.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 5 minor

Summary. The paper studies fixed-parameter tractable compilation of conjunctions of non-CNF constraints into d-SDNNF, parameterized by incidence treewidth. The main claim is that systems of constraints that are w-slim for complete SDNNFs can be compiled in time 2^{O(w·k)} poly(|F|+|var(F)|+w), generalizing the known CNF result of BCMS15. The strategy is to construct for each constraint a small complete SDNNF with respect to a vtree derived from a tree decomposition of the incidence graph, Tseitin-encode all these circuits into a CNF whose incidence treewidth is controlled, compile that CNF to d-SDNNF via BCMS15, and then deterministically forget the auxiliary variables. The paper also contains a lower bound based on rectangle covers and faster FPT model-counting algorithms for CSTS-representable constraints, including clauses combined with XOR/modulo constraints.

Significance. If the main result is fully established, it is a meaningful theoretical advance: it would place parity, modulo, small-threshold, and other constraints under the same incidence-treewidth umbrella as CNF, both for compilation and for faster direct model counting. The CSTS characterization in Section 3.2 is elegant and gives a clean handle on literal-symmetric constraints. The counting algorithms in Section 6, especially the FFT-based join-node speedups, are concrete and potentially useful. The lower bound in Section 5 via the adversarial rectangle-cover game is a nontrivial contribution. However, the central theorem as stated is conditional on an algorithmic assumption that is omitted from the abstract and Theorem 1, and several proof obligations are deferred to an unavailable long version. The paper is therefore not yet self-contained at the level expected of a journal submission.

major comments (3)
  1. [Abstract and Section 1, Theorem 1 vs Section 3, Theorem 4 and Assumption 1] The abstract and Theorem 1 advertise an unconditional FPT compilation result for constraints with at most w residual states, with running time 2^{O(k)} poly(|F|+|var(F)|). The proof in Section 4 proves Theorem 4 only under Assumption 1, which postulates a polynomial-time algorithm that, for every constraint type and every vtree, compiles each constraint into a minimal-width complete SDNNF. This assumption is an algorithmic oracle; it is not implied by w-slimness, and it is not proved for the families in Table 1. The table's width bounds and the claimed algorithms satisfying Assumption 1 are deferred to the long version. Consequently, the advertised instantiations (parity and constant-threshold cardinality) are not yet established by the manuscript. The statement of Theorem 1 must carry the assumption explicitly, or the paper must give direct constructions for the concrete families it promises.
  2. [Section 4.2.2, Lemma 10 and the merge argument] The proof that the Tseitin encoding H has incidence treewidth O(w·tw_i(F)) uses Lemma 10 to merge the tree decomposition (T,b) of the incidence graph of F with the tree decompositions (T,b_c) of the vtrees τ_c. Lemma 10 requires, for every bag t, the inclusion b(t)∩V_s ⊆ b'(t)∩V_s for the shared vertices. Lemma 9 only establishes the opposite-direction property bc(t)∩b(t) ⊆ b(t)∩var(c). For a variable x introduced at node t_x^c, the variable x may continue to appear in descendant bags of (T,b) below t_x^c, while the constructed bc does not put x in those descendant bags. Therefore the hypothesis of Lemma 10 is not shown to hold, and the claimed treewidth bound for the encoding is not proven. The statement in Section 4.2.2 that Lemma 11 makes the merge 'equivalent' does not repair this, since Lemma 11 also assumes a tree decomposition of τ_c with the original variables placed in the same bags as in (T,b). This gap is load-bearing for Theorem 4 and must be fixed.
  3. [Section 3.1, Lemma 2] Lemma 2 is stated as a theorem relating h-slimness for complete SDNNFs to slimness for complete OBDDs, but its proof is only a sketch. The two main steps—(1) an encoding of a width-w SDNNF circuit into a CNF of incidence pathwidth O(w), and (2) a translation of such a CNF into a π-OBDD of width 2^p—are nontrivial and are not proved in the manuscript; step (3) is deferred to [CM19, Lemma 1]. Even if this lemma is not used in the direct proof of Theorem 4, it is part of the paper's claimed characterization and should either be proved in full or explicitly marked as an imported result with a precise citation. As written, it is an unsupported theorem.
minor comments (5)
  1. [Table 1 and Section 3.1] The h-slimness bounds in Table 1 are asserted without proof, and the text says the proofs are in the long version. Since these bounds are used to justify the paper's headline examples, at least the easy cases (clauses, XOR, small-scope constraints) should be proved in the paper, and the more involved cases should be accompanied by a sketch or a concrete citation.
  2. [Section 5, Lemma 15] The proof of Lemma 15 concludes that the incidence treewidth of F_{G,k} is at most k, but it uses the cited inequality 'incidence treewidth ≤ dual treewidth + 1', which would give k+1 from the constructed dual decomposition of width k. This does not affect Theorem 5 since only O(k) is needed, but the statement should be corrected.
  3. [Section 6, Definition 7 and Lemmas 19–21] The manuscript uses several inconsistent notations: bF(t) and bC(t) are used interchangeably; the symbols fV_t, eV_t, gV_t appear with different sub- and superscripts in different formulas; and σ1(v,¯s) is defined as a set but then used as if it were a function. These notational inconsistencies make the dynamic programming proof harder to follow and should be cleaned up.
  4. [Throughout] There are numerous typographical errors, including 'coomplete' in Lemma 1, 'Th construction' in the same proof, 'problautem' in Section 5, 'a verctor' in Theorem 10, and 'Eureopean' in the ECAI reference. A careful proofreading pass is needed.
  5. [Section 4.2.2, final paragraph] The sentence 'In the detailed proof, available in the long version of the paper, we directly merge the tree decompositions ... This is equivalent to what we have just explained' is not acceptable as a substitute for a proof in a journal submission. The missing details should be included in the paper itself.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the FPT compilation theorem is a conditional reduction to external CNF-compilation and knowledge-compilation results, not a repackaging of its own assumptions.

full rationale

The main derivation, Theorem 4, is explicitly conditional on Assumption 1, which supplies polynomial-time compilation of each individual constraint into a minimal-width complete SDNNF for a given vtree. The theorem does not stop there: it constructs compatible vtrees from a tree decomposition (Lemma 9), forms a Tseitin CNF encoding, bounds the encoding's incidence treewidth (Lemmas 10-11), compiles that CNF using the external BCMS15 result, and then removes auxiliary variables while preserving d-SDNNF structure (Lemma 8). The oracle gives per-constraint SDNNFs; the theorem's content is the treewidth-preserving combination and forgetting argument, which is not already contained in the oracle. No fitted parameter is renamed as a prediction, and no definition of the target class is stated in terms of the theorem's output. The lower bound in Theorem 5 relies on the rectangle-cover theorem of dCM23 and on W[1]-hardness from SS10; although the author sets overlap with some cited works, these are external published results with different targets and assumptions, not restatements of Theorem 4 and not results that assume w-slimness or Assumption 1. The speed-ups in Section 6 are standard dynamic programming over tree decompositions using external convolution/FFT facts (SS20, Obe07). The genuine caveat is not circularity: the abstract and informal Theorem 1 omit Assumption 1, and several correctness details (Table 1 entries, some merge arguments) are deferred to a long version. Those are completeness and rigor gaps that may affect whether the advertised instantiations are proven, but they do not make any derivation equivalent to its own input by construction.

Assumptions & free parameters 0 free parameters · 3 assumptions · 1 invented entities

The main theorem is conditional on Assumption 1 (Section 3), which requires a polynomial-time minimal-width complete SDNNF compiler for each constraint type; this is an algorithmic oracle, not a proved theorem. It also relies on the h-slim bounds in Table 1, whose proofs are deferred to a long version, and on Lemma 2's sketch. No free parameters are fitted to data; w and k are input parameters.

assumptions (3)
  • ad hoc to paper Assumption 1: for every constraint type in the system, a polynomial-time algorithm exists to compile every constraint into a minimal-width complete SDNNF for any given vtree.
    The FPT compilation theorem (Theorem 4) is conditional on this algorithmic assumption, which the informal Theorem 1 in the introduction omits. It is load-bearing: without it, the algorithm is not effective.
  • domain assumption The h-slim bounds for the constraint families listed in Table 1 (clauses, XORs, sum modulo, cardinality, small scope, threshold, symmetric functions) are correct.
    The paper states 'The proof of the correctness of these values for h appear in the long version of the paper' (Section 3). These bounds are needed to apply Theorem 4 to concrete constraint families, so they are load-bearing.
  • ad hoc to paper Lemma 2, step (2): a CNF F(X,Y) with incidence pathwidth p can be compiled into an OBDD of width 2^p.
    This step is asserted inside a proof sketch and is not supported by a citation or detailed proof. It is needed for the doubly exponential gap between OBDD-slim and SDNNF-slim.
invented entities (1)
  • Commutative state transition system (CSTS)
    purpose: Models the behavior of literal-symmetric constraints under partial assignments; used to prove that constant-width OBDD literal-symmetric functions have constant state size (Lemma 7) and to design the dynamic programming algorithm in Section 6.
    New mathematical abstraction introduced in Definition 3; it has no empirical handle outside the paper, but it is used internally to characterize constraint families and derive algorithms.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Compilation and Fast Model Counting beyond CNF." pith.science (2026). https://pith.science/paper/FGWRC6VY

@misc{pith2026250200434,
  author       = {Pith},
  title        = {Pith review of: Compilation and Fast Model Counting beyond CNF},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/FGWRC6VY}},
  note         = {Machine review of arXiv:2502.00434}
}
read the original abstract

Circuits in deterministic decomposable negation normal form (d-DNNF) are representations of Boolean functions that enable linear-time model counting. This paper strengthens our theoretical knowledge of what classes of functions can be efficiently transformed, or compiled, into d-DNNF. Our main contribution is the fixed-parameter tractable (FPT) compilation of conjunctions of specific constraints parameterized by incidence treewidth. This subsumes the known result for CNF. The constraints in question are all functions representable by constant-width ordered binary decision diagrams (OBDDs) for all variable orderings. For instance, this includes parity constraints and cardinality constraints with constant threshold. The running time of the FPT compilation is singly exponential in the incidence treewidth but hides large constants in the exponent. To balance that, we give a more efficient FPT algorithm for model counting that applies to a sub-family of the constraints and does not require compilation.

Figures

Figures reproduced from arXiv: 2502.00434 by the authors.

Figure 2
Figure 2. CSTS for XOR, OR and “x1 + · · · + xn ≥ 2” constraints. Every complete OBDD with n variables can be reinterpreted as an STS (S (Si)1≤i≤n, f0, f1), with the two sinks from the OBDD denoted as 0A and 1A, or simply, 0 and 1, where Si is the set of decision nodes at the ith layer, f0(s), f1(s) ∈ Si+1 for s ∈ Si , i < n and f0(s), f1(s) ∈ {0, 1} for s ∈ Sn. The concept of being commutative and the extended transition fun… view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

13 extracted references · 12 canonical work pages

  1. [9]

    CV-width: A new complexity parameter for CNFs

    [OD14a] Umut Oztok and Adnan Darwiche. CV-width: A new complexity parameter for CNFs. In Torsten Schaub, Gerhard Friedrich, and Barry O’Sullivan, editors, ECAI 2014 - 21st European Conference on Artificial Intelligence, 18-22 August 2014, Prague, Czech Republic - Including Prestigious Applications of Intelligent Systems (PAIS

    work page 2014

  2. [10]

    On compiling CNF into Decision-DNNF

    [OD14b] Umut Oztok and Adnan Darwiche. On compiling CNF into Decision-DNNF. In Barry O’Sullivan, editor, Principles and Practice of Constraint Programming - 20th International Conference, CP 2014, Lyon, France, September 8-12,

    work page 2014

  3. [11]

    A top-down compiler for sentential decision diagrams

    [OD15] Umut Oztok and Adnan Darwiche. A top-down compiler for sentential decision diagrams. In Qiang Yang and Michael J. Wooldridge, editors, Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2015, Buenos Aires, Ar- gentina, July 25-31, 2015 , pages 3141–3148. AAAI Press,

    work page 2015

  4. [12]

    New compilation languages based on structured decomposability

    [PD08] Knot Pipatsrisawat and Adnan Darwiche. New compilation languages based on structured decomposability. In Dieter Fox and Carla P. Gomes, editors, Proceedings of the Twenty- Third AAAI Conference on Artificial Intelligence, AAAI 2008, Chicago, Illinois, USA, July 13-17, 2008 , pages 517–522. AAAI Press,

    work page 2008

  5. [13]

    A faster algorithm for propositional model counting parameterized by incidence treewidth

    [SS20] Friedrich Slivovsky and Stefan Szeider. A faster algorithm for propositional model counting parameterized by incidence treewidth. In Luca Pulina and Martina Seidl, editors, The- ory and Applications of Satisfiability Testing – SAT 2020 , pages 267–276, Cham,

    work page 2020

  6. [1994]

    An improved decision-DNNF compiler

    [LM17] Jean-Marie Lagniez and Pierre Marquis. An improved decision-DNNF compiler. In Carles Sierra, editor, Proceedings of the Twenty-Sixth International Joint Conference on Artifi- cial Intelligence, IJCAI 2017, Melbourne, Australia, August 19-25, 2017 , pages 667–673. ijcai.org,

    work page 2017

  7. [2007]

    Knowledge compilation and more with SharpSAT-TD

    [KE23] Rafael Kiesel and Thomas Eiter. Knowledge compilation and more with SharpSAT-TD. In Pierre Marquis, Tran Cao Son, and Gabriele Kern-Isberner, editors, Proceedings of the 20th International Conference on Principles of Knowledge Representation and Reasoning, KR 2023, Rhodes, Greece, September 2-8, 2023 , pages 406–416,

    work page 2023

  8. [2010]

    Tractable QBF by knowledge compilation

    [CM19] Florent Capelli and Stefan Mengel. Tractable QBF by knowledge compilation. In Rolf Niedermeier and Christophe Paul, editors, 36th International Symposium on Theoretical Aspects of Computer Science, STACS 2019, March 13-16, 2019, Berlin, Germany , volume 126 of LIPIcs, pages 18:1–18:16. Schloss Dagstuhl - Leibniz-Zentrum f¨ ur Informatik,

    work page 2019

Show all 13 references
  1. [2014]

    On compiling CNFs into structured deterministic DNNFs

    [BCMS15] Simone Bova, Florent Capelli, Stefan Mengel, and Friedrich Slivovsky. On compiling CNFs into structured deterministic DNNFs. In Marijn Heule and Sean A. Weaver, editors,Theory and Applications of Satisfiability Testing - SAT 2015 - 18th International Conference, Austi...

    2015

  2. [2015]

    Fourier meets M¨ obius: fast subset convolution

    [BHKK07] Andreas Bj¨ orklund, Thore Husfeldt, Petteri Kaski, and Mikko Koivisto. Fourier meets M¨ obius: fast subset convolution. In David S. Johnson and Uriel Feige, editors,Proceedings of the 39th Annual ACM Symposium on Theory of Computing, San Diego, California, USA, June ...

    2007

  3. [2017]

    Muise, Sheila A

    [MMBH12] Christian J. Muise, Sheila A. McIlraith, J. Christopher Beck, and Eric I. Hsu. Dsharp: Fast d-DNNF compilation with sharpSAT. In Leila Kosseim and Diana Inkpen, editors, Advances in Artificial Intelligence - 25th Canadian Conference on Artificial Intelligence, Canadia...

    2012

  4. [2019]

    New advances in compiling CNF into decomposable negation normal form

    [Dar04] Adnan Darwiche. New advances in compiling CNF into decomposable negation normal form. In Ram´ on L´ opez de M´ antaras and Lorenza Saitta, editors,Proceedings of the 16th Eureopean Conference on Artificial Intelligence, ECAI’2004, including Prestigious Ap- plicants of ...

    2004

  5. [2020]

    Expander cnfs have exponential DNNF size

    [BCMS14] Simone Bova, Florent Capelli, Stefan Mengel, and Friedrich Slivovsky. Expander cnfs have exponential DNNF size. CoRR, abs/1411.1995,

    1995 arXiv

Pith tools

Reviewed August 9, 2026 · model on record in the stance chip above.