{"id":"3ba905f3-39e9-495e-b236-00ef12053826","arxiv_id":"2502.00434","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"Conjunctions of constant-width OBDD-representable constraints can be compiled into d-DNNF circuits in fixed-parameter tractable time when parameterized by incidence treewidth.","lead":"This paper proves new algorithms for turning certain types of Boolean constraints, like parity and cardinality constraints, into a compact form that allows fast counting of satisfying assignments. It extends a known technique for CNF formulas to a much wider class, using the treewidth of the problem's incidence graph as the parameter.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Theorem 4's FPT compilation is conditional on Assumption 1, an unverified compilation oracle; the abstract and informal Theorem 1 omit this condition, so the advertised instantiations (parity, cardinality) are not yet proven.","rationale":"The paper's main contribution is the FPT compilation result, Theorem 4, whose proof and applicability rest entirely on Assumption 1: for every constraint type, a polynomial-time algorithm must compile each constraint into a minimal-width complete SDNNF for any given vtree. This is a genuine algorithmic oracle, not a standard complexity-theoretic consequence of the slimness definition. The abstract and Theorem 1 present the result as unconditional for constraints with bounded state count, and the proof of Theorem 4 calls the oracle for every constraint when forming the Tseitin encoding. If the oracle fails for a natural constraint family, then the FPT compilation claim for that family is void. The paper does not prove Assumption 1 for any family in the preprint; it only states in the text that it is 'reasonable' and defers the width bounds of Table 1 and the compilation algorithms to a long version. The reader's weakest_assumption identifies exactly this issue, and I agree with that assessment. A secondary, smaller gap is that the merge in Section 4.2.2 applies Lemma 10 under an inclusion condition that is not obviously implied by Lemma 9's properties (i) and (ii); while this may be repairable by a direct connectivity argument, it is another proof obligation that is not discharged. The proposed concrete test, instantiating the theorem for constant-threshold cardinality constraints with an explicit minimal-width complete SDNNF construction, would settle whether the flagship advertised example actually satisfies Assumption 1; if it does, the conditional theorem has a nontrivial instantiation, and if it does not, the central promise is unsupported. Since the reader's CONDITIONAL verdict already flags these deferred items, my stress-test does not change the verdict.","tokens_in":28653,"tokens_out":22010,"duration_ms":214503,"concrete_test":"Instantiate Theorem 4 for the family of constant-threshold cardinality constraints (x1+...+xn >= k, k constant). Provide the explicit polynomial-time construction of a minimal-width complete SDNNF for an arbitrary vtree, and verify on small examples (n up to 6, several vtrees) by brute-force minimization that the width equals the Table 1 bound O(min(n-k,k)^2) (constant for constant k). If the construction is correct, Assumption 1 is satisfied for at least the flagship advertised class; if the minimal width exceeds the claimed bound, the informal claims for cardinality constraints are unsupported.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central result, Theorem 4 (Section 3), states an FPT compilation algorithm for systems of constraints that are w-slim for complete SDNNFs, but only 'Under assumption 1'. Assumption 1 requires, for every constraint type in the system, a polynomial-time algorithm that, given any vtree, compiles every constraint into a minimal-width complete SDNNF. This oracle is exactly the step that turns the abstract's promise ('this includes parity constraints and cardinality constraints with constant threshold') into an actual algorithm. The abstract and informal Theorem 1 drop the assumption and only mention a bounded number of residual states. The proof of Theorem 4 invokes Assumption 1 for every constraint when building the Tseitin encoding; if minimal-width complete SDNNF compilation is not polynomial-time for a natural family, the FPT result does not apply to it. Moreover, the concrete width bounds in Table 1 (e.g., O(min(n-k,k)^2) for cardinality) and the algorithms satisfying Assumption 1 are deferred to an unavailable long version. Lemma 2, used to relate SDNNF- and OBDD-slimness, is a proof sketch relying on [CM19, Lemma 1]. The merge in Section 4.2.2 also cites Lemma 10 with an inclusion condition that does not follow from Lemma 9's properties (i)-(ii); though this gap may be repairable, it is another deferred obligation. Thus the paper's main theoretical promise is not self-contained.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":29022,"tokens_out":14067,"duration_ms":147527,"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":[{"comment":"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.","section":"Abstract and Section 1, Theorem 1 vs Section 3, Theorem 4 and Assumption 1"},{"comment":"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.","section":"Section 4.2.2, Lemma 10 and the merge argument"},{"comment":"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.","section":"Section 3.1, Lemma 2"}],"minor_comments":[{"comment":"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.","section":"Table 1 and Section 3.1"},{"comment":"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.","section":"Section 5, Lemma 15"},{"comment":"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.","section":"Section 6, Definition 7 and Lemmas 19–21"},{"comment":"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.","section":"Throughout"},{"comment":"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.","section":"Section 4.2.2, final paragraph"}],"recommendation":"major_revision","confidential_remarks":"This is a promising working draft whose main ideas are plausible, but the central theorem is currently conditional on an unstated oracle and at least one proof step in the treewidth-control argument is incomplete. I would be willing to review a revision that either proves Theorem 4 under the explicitly stated assumption and supplies the concrete instantiations, or restricts the paper's claims accordingly. I saw no signs of novelty or attribution problems; the CSTS framework and the rectangle-cover lower bound appear to be original contributions."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Colleague,\n\nThis one has a real result inside, but it is not quite the paper the abstract advertises. The genuinely new part is Theorem 4: systems of constraints that are w-slim for complete SDNNFs can be compiled to d-SDNNF in time 2^{O(w·tw_i(F))} poly(...). That extends the known CNF result of Bova et al. to parity, cardinality, threshold and other constraint types, and the proof route—Tseitin-encode each constraint, compile the whole CNF, then forget auxiliary variables via Lemma 8—is coherent. The CSTS characterization of literal-symmetric functions and the rectangle-cover lower bound in Section 5 are also credible contributions. The counting algorithms with FFT/Mobius acceleration are a nice bonus.\n\nNow the soft spots, in roughly the order they matter. Assumption 1 is load-bearing: for every constraint type you need a polynomial-time algorithm that compiles each instance into a minimal-width complete SDNNF for any given vtree. That is exactly the step that makes the abstract's parity/cardinality examples actual algorithms, and it is silently missing from the abstract and from informal Theorem 1. If minimal-width compilation is not poly-time for a natural family, the FPT theorem does not apply to that family. The paper asserts the assumption is reasonable and defers the Table 1 width bounds plus corresponding algorithms to a long version. That is not fatal, but it means the advertised instantiations are not yet proven in this document.\n\nSeveral smaller proof obligations are also deferred: Lemma 2 is a proof sketch with a doubly exponential bound; Lemma 9's construction is sketched; and the merge in Section 4.2.2 invokes Lemma 10 with an inclusion condition that does not follow from Lemma 9(i)-(ii) as written. The last one looks repairable, but it is another spot where the reader has to fill in work. The stress-test note is on target about all of this.\n\nI do not think the main theorem is wrong. The structure is plausible, the lower bound is substantive, and the counting algorithms are self-contained enough to be checked. But the current preprint is not self-contained: an editor should send it to referees with instructions to require the authors to align the informal statements with Theorem 4 and supply or publicly post the missing proofs.\n\nWorth your time if you work on knowledge compilation or parameterized model counting. I would read the long version when it appears.","headline":"Solid FPT compilation result beyond CNF, but the advertised generality is conditional on an unverified SDNNF compilation oracle that the abstract drops.","tokens_in":29517,"tokens_out":2636,"would_cite":true,"duration_ms":27364,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68Q17","68Q25","68R10","05C85"],"pacs":[],"model":"deepseek-v4-flash","headline":"Constant-state constraints compile to d-DNNF in FPT time","keywords":["knowledge compilation","d-DNNF","SDNNF","incidence treewidth","fixed-parameter tractability","model counting","ordered binary decision diagrams","commutative state transition systems"],"falsifier":"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.","tokens_in":2157,"feed_emoji":"🧮","tokens_out":5798,"duration_ms":129344,"temperature":0.7,"pith_summary":"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.","feed_headline":"Parity constraints beyond CNF compile fast when treewidth is bounded","feed_subtitle":"Singly exponential in incidence treewidth; counting gets even faster without compiling.","key_machinery":"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.","core_discovery":"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.","pith_inferences":["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."],"forward_implications":["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."],"supporting_citations":[{"why":"Supplies the FPT algorithm that compiles CNF formulas into d-SDNNF parameterized by incidence treewidth, used as the compilation subroutine.","marker":"[BCMS15]"},{"why":"Provides the notion of functions computable by small-width OBDDs under every variable ordering and the OBDD width-composition facts used in the slimness definitions and examples.","marker":"[Weg00]"},{"why":"Introduces SDNNF and structured decomposability, the target language and vtree structure on which the main compilation theorem is built.","marker":"[PD08]"},{"why":"Gives the existential-quantification equivalence that underlies replacing a d-DNNF over Tseitin variables by its projection to the original variables.","marker":"[DM02]"},{"why":"Supports the fact that existential forgetting over Tseitin variables preserves d-DNNF, used in Lemma 8 to erase auxiliary variables.","marker":"[KE23]"},{"why":"Establishes the W[1]-hardness of satisfiability with bounded treewidth and the dual-treewidth bound used in the lower-bound construction of Theorem 5.","marker":"[SS10]"},{"why":"Provides width-parameter lower bounds for DNNF languages used in Lemma 3 to separate SDNNF width from OBDD width and to build hard constraint examples.","marker":"[ACMS20]"},{"why":"Supplies the fast subset-convolution technique used to speed up join-node computations in the counting algorithms for one-sided constraints.","marker":"[BHKK07]"},{"why":"Gives the zeta- and Möbius-transform identity for union products used in the faster counting algorithm for clauses mixed with modulo constraints.","marker":"[SS20]"}],"fun_headline_variants":["FPT compilation of parity and cardinality constraints via treewidth","Count models of XOR clauses fast without full compilation","Singly exponential in treewidth: compile many constraints to d-DNNF","Fast model counting for symmetric constraints without compiling","Subsumes CNF: treewidth-bounded compilation for parity and more"],"cache_read_input_tokens":31616,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["FPT compilation of parity and cardinality constraints via treewidth","Count models of XOR clauses fast without full compilation","Singly exponential in treewidth: compile many constraints to d-DNNF","Fast model counting for symmetric constraints without compiling","Subsumes CNF: treewidth-bounded compilation for parity and more"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.001078,"raw_usage":{"total_tokens":4548,"prompt_tokens":1017,"completion_tokens":3531,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":633,"completion_tokens_details":{"reasoning_tokens":3446}},"tokens_in":633,"tokens_out":3531,"duration_ms":21576,"temperature":1.0,"reasoning_tokens":3446,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-09T19:00:53.868884+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[],"review_version":1}