{"id":"ae94d0df-52d5-4b01-9c9f-38c8b1a8131d","arxiv_id":"2608.10877","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"WFOMC with one linear order and its successor relations is polynomial-time in the domain size, while a second full linear order makes the problem #P1-hard.","lead":"This paper shows that weighted first-order model counting over a single ordered domain can be done in polynomial time, and that adding a second independent order makes it hard. It also provides faster algorithms for successor relations and a hybrid one-order-plus-successor case, with experiments on Markov logic networks and combinatorics problems.","discovery_kind":"new_method","skeptic_critique":null,"referee_report":{"model":"deepseek-v4-flash","summary":"The paper studies Weighted First-Order Model Counting (WFOMC) over domains equipped with linear order axioms. It claims four main results: (i) C2/FO2 with one linear order axiom is domain-liftable, via a dynamic program (Algorithm 1); (ii) FO2 with an extended linear order axiom including k-th successor relations is domain-liftable (Algorithm 2); (iii) FO2 with two linear order axioms is #P1-hard, proved by encoding a hard tiling problem through a grid axiom (Lemmas 7-9, Theorem 3); and (iv) FO2/C2 with one linear order and the successor relation of another linear order is domain-liftable (Algorithm 3, Theorem 4). The paper also reports experiments comparing the new algorithms with GANAK, d4, and RecursiveWFOMC, including matchings to OEIS sequences.","tokens_in":50684,"tokens_out":25393,"duration_ms":252310,"significance":"If the results are correct, they are significant: they extend the domain-liftability frontier to ordered domains, introduce a family of dynamic-programming algorithms with practical relevance to sequences, hidden Markov models, and grid-like structures, and they sharpen the known tractability/intractability boundary for WFOMC with order axioms. The algorithmic ideas are well connected to the existing literature on domain recursion, and the experimental validation against independent exact counters and OEIS sequences is a genuine strength. However, the hardness proof has a major uniformity gap, and the proofs of Algorithms 2 and 3 are substantially less complete than the statements require; these points must be fixed before the central claims can be accepted.","major_comments":[{"comment":"The hardness reduction is not to a fixed sentence. Lemma 8 constructs a sentence Ψ whose cardinality constraints |R1T3|=n and |R1T4|=m (Eq. (23)) depend on the inputs n,m of the 1-1-N-M tiling problem, while the domain size is (n+m+2)^2. Lemma 8 then invokes Lemma 2 to obtain an FO2 sentence without cardinality constraints, and Lemma 9 repeats this for the two-linear-order encoding. However, Lemma 2 as stated is a many-one reduction to one fixed FO2 sentence, whereas the cited result (Kuželka 2021) eliminates cardinality constraints by polynomial interpolation over several WFOMC evaluations with varying weights. Since the cardinality constants here vary with the input, the argument establishes hardness for a family of sentences parameterized by n,m, not the existence of a fixed FO2 sentence with two linear orders whose function n ↦ WFOMC(Ψ,n) is #P1-hard. Theorem 3 therefore needs a genuinely uniform fixed-sentence reduction, or the statement of the hardness notion must be revised.","section":"§5.1–§5.3, Lemmas 8 and 9, Theorem 3"},{"comment":"The claimed equality WFOMC(Ψ∧G(H,V),n^2,w,w) = WFOMC(Ψ_l∧L(≤1)∧L(≤2),n^2,w,w) \"for any weighting functions\" is not correct as written. The left-hand sentence does not contain the auxiliary predicates First_i, Last_i, S_i, Left, Right, Top, Bottom, H, and V, while the right-hand side does; arbitrary weights on those predicates change the right-hand value. The proof must specify how the weighting functions are extended to the auxiliary predicates (e.g., all auxiliary weights set to 1) and state the resulting equality up to a constant factor. As written, the reduction is underspecified at a load-bearing point.","section":"§5.3, Lemma 9"},{"comment":"The proof of Algorithm 2 is not carried out. The displayed recursion for WMC(Φ_C2) is garbled: it uses r_il where only ˆr_il and ~r_il,s are defined, it contains a duplicated product over i∈[p], and it refers to Ω_m^s in a formula whose domain is of size m+1. In addition, Algorithm 2's pseudocode leaves t'_s undefined for s > min(i−1,k). Since Theorem 2 is a central positive result, the recurrence and the induction step need to be stated cleanly and proved in full.","section":"§4.1, Theorem 2"},{"comment":"The correctness proof for Algorithm 3 is only a sketch. The key claim that the pair-product contribution is determined by the state (k,ρ) is not stated as a lemma, the transition sums for merge1/merge2 with the η factors are not formally derived, and the proof that every configuration of segments counted by h_m(k,ρ) extends uniquely under the five update types is missing. The complexity bound also requires an argument counting the inner sums over a,b,c,d; they are polynomial in p, but the announced exponent O(n^{p^2+p+1}) is not justified as written. For an algorithm with this state-space complexity, a formal induction is necessary.","section":"§6.2, Theorem 4"},{"comment":"The exact counting correspondence between accepting paths of the Turing machine and tilings is imported from a theorem usually stated for the NP-completeness of the bounded tiling problem. Since Lemma 8 converts the number of tilings to a WFOMC value by a factorial factor, any spurious tiling or missing boundary tile would invalidate the hardness argument. The paper should either provide a direct proof of the one-to-one correspondence or cite a source that states the counting version explicitly.","section":"§5.1, Lemmas 6 and 7"}],"minor_comments":[{"comment":"Lemma 2 is stated as a many-one reduction to a single FO2 sentence, but the cited work eliminates cardinality constraints by interpolation over multiple oracle calls. Please state the exact reduction type and whether the auxiliary sentence or weights may depend on the cardinality constants.","section":"§2.3, Lemma 2"},{"comment":"In the proof of Theorem 2, the same-cell formula uses set notation {a,b}∈Ω^s although Ω is defined as a set of ordered pairs; it should be (a,b)∈Ω^s.","section":"§4.1, Algorithm 2 and Theorem 2 proof"},{"comment":"Lemma 4 assumes a constant-free sentence, but this is not stated explicitly in the lemma; adding unary evidence breaks the symmetry argument, so the hypothesis should be made precise.","section":"§3.2, Lemma 4"},{"comment":"The observation that the ≤2-path decomposition has exactly n paths of length n depends on the domain size being exactly n^2 and on the boundary constraints; this step is plausible but should be expanded into a short formal argument rather than three informal observations.","section":"§5.3, Equations (24)–(33)"},{"comment":"The plots report runtimes for the propositional solvers excluding CNF construction; this is reasonable, but it should be stated once in the caption or text that the comparison is therefore only for the counting phase, not end-to-end grounding plus counting.","section":"§7, Experiments"}],"recommendation":"major_revision","confidential_remarks":"The main risk is the uniformity gap in the hardness proof: if Lemma 2 is a Turing reduction via interpolation, then the #P1-hardness of a fixed FO2 sentence with two linear orders does not follow from the construction in Lemmas 8–9. The positive results (Theorems 1, 2, and 4) are likely salvageable, but Theorem 2's recurrence and Theorem 4's correctness proof need substantial formal work. I would ask the authors to state the exact hardness notion, provide a uniform fixed-sentence reduction, or explicitly downgrade the claim to hardness of the parameterized family."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Here's what I'd want you to know before reading this one: the main results are real, and two of them are genuinely new. The paper shows WFOMC with one linear order is domain-liftable (old, and they admit it — follows from the acyclicity axiom), that adding successor relations for that order stays polynomial via a native DP (Algorithm 2), that two full linear orders make WFOMC #P1-hard via a forced grid encoding, and that one linear order plus the successor relation of a second order is again polynomial (Algorithm 3). The hardness for two orders and the hybrid tractability are the actual contributions; the rest is context.\n\nThe strengths: the DP recurrences are transparent, the experiments compare against independent exact counters (GANAK, d4) and match OEIS sequences, and the paper doesn't oversell. The disclosure that Algorithm 1 restates the acyclicity liftability is a good sign of honesty. No fitted parameters, no circularity.\n\nSoft spots, in order of severity. The proof of Algorithm 3 is a sketch — the text basically says \"existence proves the statement\" and defers correctness to a future induction. That needs a real proof. Theorem 2's update formula has a garbled product; I could not parse it as written, though the intended recurrence is clear from context. Lemma 9 doesn't specify how the weighting functions extend to the fresh auxiliary relations (First, Last, etc.) when it claims the WFOMC equality for arbitrary weights. That's a gap, probably fixable, but it needs stating. The hardness result leans on an imported tiling encoding (Lemma 6) and a forced-grid construction; these are standard-style but not machine-checked. The polynomial claims all treat the sentence as fixed, so p is constant; that's the usual data-complexity convention in this literature, though the paper could be clearer that the exponent depends on p.\n\nOverall, a solid, useful paper for anyone working on lifted inference or exact combinatorial counting. It deserves a serious referee; the fixes are tractable but necessary.","headline":"Solid paper that pins down part of the WFOMC tractability frontier for ordered domains; the two-order hardness and hybrid tractability are genuinely new, but a few proofs need tightening.","tokens_in":51243,"tokens_out":2473,"would_cite":true,"duration_ms":24103,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["03B70","68Q17","68Q25"],"pacs":[],"model":"deepseek-v4-flash","headline":"Weighted model counting over linearly ordered domains stays polynomial with one linear order and its successor relations, but becomes $\\mathsf{\\#P}_1$-hard with two independent linear orders — and stays tractable when only a second…","keywords":["weighted first-order model counting","domain-liftability","linear order axiom","successor relations","lifted inference","two-variable logic","counting complexity","dynamic programming"],"falsifier":"For small domains, compare Algorithm 2 against brute-force enumeration on a sentence with explicitly defined successor relations: any mismatch would break the bookkeeping behind Theorem 2. On the hardness side, a polynomial-time algorithm for the paper's 1-1-N-M counting tiling problem, or a domain-lifted counting procedure for the constructed two-linear-order sentence, would refute Theorem 3.","tokens_in":50580,"feed_emoji":"🧮","tokens_out":15128,"duration_ms":126402,"temperature":0.7,"pith_summary":"The paper asks when the weighted first-order model counting problem (WFOMC) — summing the weights of all models of a logical sentence over a domain — can be solved in time polynomial in the domain size when the domain is linearly ordered. It proves that adding a linear order axiom to the two-variable fragment with counting quantifiers (C2) keeps the problem tractable, and that the result survives when the axiom also exposes the immediate and $k$-th successor relations. It then identifies the boundary: two independent linear orders make WFOMC $\\mathsf{\\#P}_1$-hard, while one linear order plus the successor relation of a second order remains polynomial. The practical payoff is exact lifted inference over sequences, time series, permutations, and grid-shaped structures — problems that previously required three-variable logic and were provably intractable to count.","feed_headline":"One linear order: tractable counting; two: provably hard","feed_subtitle":"New algorithms handle time series, permutations, and grid models — and pin where ordered counting turns intractable.","key_machinery":"A family of dynamic-programming algorithms built on the domain recursion rule. The domain is enlarged one element at a time in its linear order $1 \\le 2 \\le \\cdots \\le n$, and the algorithm's state is the cell configuration $\\mathbf{k}$, where a cell (1-type) is a maximal consistent set of literals in a single variable. Pairwise interactions between cells are summarized by constants $r_{ij}$ computed from 2-tables, so each step multiplies the accumulated weighted count by cell weights and pairwise factors; because the sentence has no constants, all $n!$ orderings contribute equally, so the natural-order answer is multiplied by $n!$. Algorithm 2 additionally records the cell assignments of the last $k$ elements, exactly the information needed to fix the $k$-th successor relations, yielding time $O(p^{k+1} n^p)$ with $p$ the number of cells. Algorithm 3, for one linear order plus a second order's successor, tracks how the partial second order splits the prefix into segments (maximal $S$-chains) with head and tail cells, and applies five update rules — merge two segments, extend as head, extend as tail, or start a singleton — when the next element arrives. On the hardness side, the lever is a grid axiom that encodes a $\\mathsf{\\#P}_1$-hard tiling problem; Lemma 9's construction of Left/Right row markers plus three geometric observations forces any two linear orders to arrange the domain into exactly a square grid, with each grid corresponding to a unique model.","core_discovery":"The central assertion is that the tractability boundary for WFOMC over ordered domains sits strictly between one and two full linear orders. With a single linear order axiom, the two-variable fragment with counting quantifiers is domain-liftable: WFOMC is computed in time polynomial in the domain size, and the same holds for the extended axiom that also fixes the successor relations up to a constant order $k$. With two independent linear orders the situation flips: there are fixed two-variable sentences whose WFOMC is $\\mathsf{\\#P}_1$-hard, so counting is conditionally intractable even though satisfiability questions with one order are decidable. Between those poles sits a third result: one linear order together with the successor relation of a second, unknown order is again domain-liftable. Because a linear order can be encoded by an acyclicity constraint, the hardness transfers to two acyclic relations as well.","pith_inferences":["The parallel between the satisfiability frontier (one order decidable, two undecidable) and this counting frontier (one order domain-liftable, two $\\mathsf{\\#P}_1$-hard) suggests a transfer principle worth testing: undecidability of satisfiability over ordered domains may systematically predict WFOMC hardness, and decidability may predict liftability.","The polynomial degrees are steep — the hybrid algorithm runs in time $O(n^{p^2+p+1})$ — so 'polynomial' does not mean 'fast': for ordered fragments the real lever is shrinking the number of cell types $p$, and on small domains even propositional counters can win. This predicts that cell-reduction and caching engineering will matter as much as the asymptotic results.","The segment machinery appears to extend a further step inward from the hardness barrier: two successor relations of two unknown linear orders should remain tractable by counting segment configurations, a concrete next test the paper does not run."],"forward_implications":["Exact lifted inference for hidden Markov models, time-series rules, and other sequence-structured C2 theories becomes polynomial in the domain size whenever one linear order is available.","Grid-shaped models with constant width $k$ — including the 2-dimensional Ising model with constant interaction strength — become tractable through the $k$-th successor relations.","Permutation-counting problems from combinatorics (grouped books, non-attacking kings, shuffled decks) reduce to polynomial-time WFOMC and run on domains of hundreds of elements, where propositional model counters fail at sizes in the teens.","Any axiom that can encode a linear order, such as the acyclicity axiom, inherits the hardness: WFOMC with two acyclic relations is $\\mathsf{\\#P}_1$-hard, not merely two explicit linear orders.","The successor relation of a second linear order can be exposed while keeping domain-liftability, so the intractability barrier is the second order's global structure, not its local adjacency."],"supporting_citations":[{"why":"Supplies the $\\mathsf{\\#P}_1$-hardness framework, the universal Turing machine (Lemma 1), and the cells/2-tables decomposition of FO2 that all three algorithms rest on.","marker":"(Beame et al., 2015)"},{"why":"Establishes domain-liftability of FO2 and provides the domain recursion rule that the incremental algorithms generalize to ordered domains.","marker":"(Van den Broeck, 2011)"},{"why":"Supplies the skolemization that reduces any FO2 sentence to the universal form $\\forall x\\forall y\\, \\psi(x,y)$ used throughout as input to the algorithms.","marker":"(Van den Broeck et al., 2014)"},{"why":"Proves counting quantifiers and cardinality constraints reduce to FO2 WFOMC (Lemma 2), which extends every positive result from FO2 to C2.","marker":"(Kuželka, 2021)"},{"why":"Its bounded-tiling encoding of nondeterministic Turing machines is summarized in Lemma 6 and is the foundation of the $\\mathsf{\\#P}_1$-hardness of the 1-1-N-M counting tiling problem.","marker":"(Lewis and Papadimitriou, 1998)"},{"why":"Provides the grid-like encodings of ordered two-variable logic that the paper shows cannot support counting, motivating the exact grid axiom behind Lemma 8.","marker":"(Otto, 2001)"},{"why":"Frames the multi-order frontier with several linear orders and supplies the tiling-encoding tradition from which the two-order hardness construction departs.","marker":"(Kieronski, 2011)"}],"fun_headline_variants":["One linear order: easy counting; two: #P-hard","Ordered model counting: one order tractable, two orders hard","WFOMC with a single order is in P; with two is #P-hard","Counting over ordered domains: one order easy, two orders intractable"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The tractability theorems fix the sentence — and with it the number of cell types $p$ — and the successor bound $k$ as constants while the domain grows, and the hardness theorem assumes the tiling-to-Turing-machine encoding is exactly one-to-one so the two linear orders create no unintended models.","fun_headline_variants_meta":{"raw":{"variants":["One linear order: easy counting; two: #P-hard","Ordered model counting: one order tractable, two orders hard","WFOMC with a single order is in P; with two is #P-hard","Counting over ordered domains: one order easy, two orders intractable"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000342,"raw_usage":{"total_tokens":1929,"prompt_tokens":1040,"completion_tokens":889,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":656,"completion_tokens_details":{"reasoning_tokens":811}},"tokens_in":656,"tokens_out":889,"duration_ms":9082,"temperature":1.0,"reasoning_tokens":811,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-12T15:09:33.329369+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"For small domains, compare Algorithm 2 against brute-force enumeration on a sentence with explicitly defined successor relations: any mismatch would break the bookkeeping behind Theorem 2. On the hardness side, a polynomial-time algorithm for the paper's 1-1-N-M counting tiling problem, or a domain-lifted counting procedure for the constructed two-linear-order sentence, would refute Theorem 3.","supporting_citations":[{"cited_title":"On the completeness of first-order knowledge compilation for lifted probabilistic inference","cited_arxiv_id":null,"evidence_quote":"Establishes domain-liftability of FO2 and provides the domain recursion rule that the incremental algorithms generalize to ordered domains."},{"cited_title":"Two variable first-order logic over ordered domains","cited_arxiv_id":null,"evidence_quote":"Provides the grid-like encodings of ordered two-variable logic that the paper shows cannot support counting, motivating the exact grid axiom behind Lemma 8."},{"cited_title":"Decidability issues for two-variable logics with several linear orders","cited_arxiv_id":null,"evidence_quote":"Frames the multi-order frontier with several linear orders and supplies the tiling-encoding tradition from which the two-order hardness construction departs."}],"review_version":1}