Pith. sign in

REVIEW 5 major objections 5 minor 54 references

Weighted First-Order Model Counting over Ordered Domains

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

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

Pith's one-line read 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…

desk verdict 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. read the letter →

arxiv 2608.10877 v1 pith:IVDDLLL6 submitted 2026-08-11 cs.LO

Jan Tóth , Qipeng Kuang , Kuncheng Zou , Václav Kůla , Yuyi Wang , Yuanhong Wang , Ondřej Kuželka This is my paper · ORCID
classification cs.LO MSC 03B7068Q1768Q25
keywords weightedfirst-ordermodelcountingdomain-liftabilitylinearorderaxiomsuccessorrelationsliftedinferencetwo-variablelogiccomplexitydynamicprogramming
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 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.

What carries the argument

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.

What would settle it

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.

Watch

Extended reading notes

Core claim

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.

Load-bearing premise

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.

Editorial extensions

If this is right

  • 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.

Reading between the lines

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

  • 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.
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

5 major / 5 minor

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.

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 (5)
  1. [§5.1–§5.3, Lemmas 8 and 9, Theorem 3] 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.
  2. [§5.3, Lemma 9] 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.
  3. [§4.1, Theorem 2] 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.
  4. [§6.2, Theorem 4] 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.
  5. [§5.1, Lemmas 6 and 7] 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.
minor comments (5)
  1. [§2.3, Lemma 2] 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.
  2. [§4.1, Algorithm 2 and Theorem 2 proof] 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.
  3. [§3.2, Lemma 4] 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.
  4. [§5.3, Equations (24)–(33)] 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.
  5. [§7, Experiments] 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.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: all main theorems are proved by explicit algorithms or reductions built on external primitives, not on the claimed conclusions.

full rationale

The paper's positive results (Theorems 1, 2, 4) are established by explicit dynamic-programming algorithms (Algorithms 1, 2, 3) built on the standard cell/2-table decomposition and domain-recursion rule, with correctness proved by induction over the domain size. The linear-order and successor axioms are treated as semantic constraints on distinguished relations; the algorithms compute weighted sums over all models satisfying those constraints, and no parameter is fitted to a target value that is later reported as a prediction. The negative result (Theorem 3) reduces WFOMC with two linear orders to a grid axiom, and then to a counting tiling problem whose #P1-hardness is imported from the external Lewis-Papadimitriou tiling encoding and the universal Turing machine of Beame et al. (2015); the authors' own Lemmas 7-9 supply the translation, not the hardness itself. Self-citations (e.g., Kuželka 2021 for eliminating counting quantifiers, Tóth and Kuželka 2024, Meng et al. 2024) are prior published results or baseline tools, disclosed and not used in place of proofs for the current claims. Experimental comparisons against independent solvers GANAK/d4 and OEIS sequences provide external checks. No equation is shown to equal its own input by construction, and no fitted quantity is renamed as a prediction. Hence the derivation chain is self-contained and non-circular.

Assumptions & free parameters 0 free parameters · 5 assumptions · 0 invented entities

No free parameters are fitted; weights and sentence are inputs, and p and k are fixed by the input. No new theoretical entities are introduced. The reductions create only fresh first-order predicates, which are syntactic and carry no independent content beyond their definitions.

assumptions (5)
  • standard math Lemma 2 (Kuzelka 2021): any C2 sentence with cardinality constraints and axioms can be reduced to FO2 WFOMC with an oracle.
    Used to extend all FO2 results to C2; cited as a prior theorem, not reproved.
  • standard math FO2 sentences can be normalized to universal form forall x forall y psi(x,y) and decomposed into independent cells/2-tables (Beame et al. 2015; Van den Broeck et al. 2014).
    Basis of all three DP algorithms and of Equation (1).
  • standard math The Lewis-Papadimitriou bounded tiling encoding (Lemma 6) maps accepting paths of a nondeterministic TM to tilings with a specified first row in a one-to-one way.
    Imported without proof; used to show the 1-1-N-M counting tiling problem is #P1-hard in Lemma 7.
  • domain assumption The linear order axiom is added semantically to the language: <= must be reflexive, antisymmetric, transitive, and total, and every total order is weighted symmetrically.
    This is the modeling construct the paper introduces; it is not expressible in FO2 and is not derived from anything.
  • domain assumption The fixed-sentence/data-complexity convention: sentence and weights are constant, only domain size n varies, so the number of cells p is constant.
    Domain-liftability is defined this way and all complexity bounds O(n^...) treat p as constant; if p grows with n the claims would fail.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Weighted First-Order Model Counting over Ordered Domains." pith.science (2026). https://pith.science/paper/IVDDLLL6

@misc{pith2026260810877,
  author       = {Pith},
  title        = {Pith review of: Weighted First-Order Model Counting over Ordered Domains},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/IVDDLLL6}},
  note         = {Machine review of arXiv:2608.10877}
}
abstract

The Weighted First-Order Model Counting Problem (WFOMC) asks for the weighted sum of models of a first-order logical sentence over a domain. It is a fundamental problem in statistical relational learning, with applications extending to enumerative combinatorics and graph polynomials. Computing WFOMC for the three-variable fragment is $\mathsf{\#P}_1$-hard, whereas polynomial-time algorithms exist for the two-variable fragment and its extensions by cardinality constraints and counting quantifiers. In this work, we explore computing WFOMC in polynomial time over linearly ordered domains, enabling tractable reasoning across inference scenarios and combinatorial problems involving sequences. Because encoding a linear order in standard first-order logic requires three variables, negating our polynomial-time aspirations, we add a linear order axiom directly to the language. This forces one predicate to impose a total ordering on domain elements. We first prove that WFOMC with the linear order axiom can be solved in time polynomial in the domain size. We then extend this result to ordered domains with access to successor relations. While this holds when successors are explicitly defined via the linear order, we demonstrate an alternative implicit approach where successor relations are part of the axiom. This implicit method exhibits significantly better performance on all tested instances, sometimes providing exponential runtime improvements. Finally, we analyze scenarios with two distinct linear orders. We show that WFOMC over the two-variable fragment with two linear orders is $\mathsf{\#P}_1$-hard. However, we develop a polynomial-time algorithm for WFOMC with one linear order and a successor relation of another, pushing the intractability barrier further, yet still leaving the question of how close to a second full linear order one can get.

Figures

Figures reproduced from arXiv: 2608.10877 by the authors.

Figure 1
Figure 1. A grid encoded using the immediate and the [PITH_FULL_IMAGE:figures/full_fig_p019_1.png] view at source ↗
Figure 2
Figure 2. An example of the simplified Watts-Strogatz model on 6 nodes with [PITH_FULL_IMAGE:figures/full_fig_p024_2.png] view at source ↗
Figure 3
Figure 3. A sketch of the tiling problem. Solid tiles represent the area already successfully tiled, while [PITH_FULL_IMAGE:figures/full_fig_p025_3.png] view at source ↗
Figures from the paper (9 more)
Figure 4
Figure 4. Figure 4: A sketch illustrating the relationship between a logical model satisfying the grid axiom and [PITH_FULL_IMAGE:figures/full_fig_p027_4.png]
Figure 5
Figure 5. Figure 5: A possible skeleton after enforcing constraints in Equations (25) to (27), which consists of [PITH_FULL_IMAGE:figures/full_fig_p030_5.png]
Figure 6
Figure 6. Figure 6: The elements form a grid using the linear orders [PITH_FULL_IMAGE:figures/full_fig_p031_6.png]
Figure 7
Figure 7. Figure 7: An illustration of the segments (red nodes and red arrows) of the order of [PITH_FULL_IMAGE:figures/full_fig_p034_7.png]
Figure 8
Figure 8. Figure 8: Runtime comparisons and WFOMC scaling behavior for [PITH_FULL_IMAGE:figures/full_fig_p038_8.png]
Figure 9
Figure 9. Figure 9: Runtime comparisons and WFOMC scaling behavior for [PITH_FULL_IMAGE:figures/full_fig_p040_9.png]
Figure 10
Figure 10. Figure 10: Cactus plots and runtime comparisons for problems from the MATH dataset for scaled-up [PITH_FULL_IMAGE:figures/full_fig_p040_10.png]
Figure 11
Figure 11. Figure 11: Runtime comparisons and scaling behavior for problems with [PITH_FULL_IMAGE:figures/full_fig_p042_11.png]
Figure 12
Figure 12. Figure 12: A k × n grid expressed using the immediate successor relation (blue) and the k-th successor relation (red). 50 [PITH_FULL_IMAGE:figures/full_fig_p050_12.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

54 extracted references · 42 canonical work pages

  1. [1]

    Computational Complexity - A Modern Approach

    Sanjeev Arora and Boaz Barak. Computational Complexity - A Modern Approach . Cambridge University Press, 2009

    2009

  2. [2]

    Symmetric weighted first-order model counting

    Paul Beame, Guy Van den Broeck, Eric Gribkoff, and Dan Suciu. Symmetric weighted first-order model counting. In Proceedings of the 34th ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems, volume 31 of SIGMOD/PODS’15, page 313–328, Melbourne Victoria Australia, May 2015. ACM. ISBN 9781450327572. doi:10.1145/2745754.2745760. URL http://dx.d...

    arXiv 2015

  3. [3]

    Ronald V. Book. Tally languages and complexity classes. Inf. Control., 26 0 (2): 0 186--193, 1974

    work page 1974

  4. [4]

    The theory of probabilistic databases

    Roger Cavallo and Michael Pittarelli. The theory of probabilistic databases. In Proceedings of the 13th International Conference on Very Large Data Bases, VLDB '87, page 71–81, San Francisco, CA, USA, 1987. Morgan Kaufmann Publishers Inc. ISBN 093461346X

    work page 1987

  5. [5]

    Two-variable logic with counting and a linear order

    Witold Charatonik and Piotr Witkowski. Two-variable logic with counting and a linear order. In CSL , volume 41 of LIPIcs, pages 631--647. Schloss Dagstuhl - Leibniz-Zentrum f \" u r Informatik, 2015

    work page 2015

  6. [6]

    On probabilistic inference by weighted model counting

    Mark Chavira and Adnan Darwiche. On probabilistic inference by weighted model counting. Artificial Intelligence, 172 0 (6-7): 0 772--799, 2008

    2008

  7. [7]

    Probabilistic (logic) programming concepts

    Luc De Raedt and Angelika Kimmig. Probabilistic (logic) programming concepts. Mach. Learn., 100 0 (1): 0 5–47, July 2015. ISSN 0885-6125. doi:10.1007/s10994-015-5494-z. URL https://doi.org/10.1007/s10994-015-5494-z

    work page doi:10.1007/s10994-015-5494-z 2015

  8. [8]

    Introduction to statistical relational learning, volume 1

    Lise Getoor and Ben Taskar. Introduction to statistical relational learning, volume 1. MIT press Cambridge, 2007

    work page 2007

Show all 54 references
  1. [9]

    Erich Gr \"a del, Phokion G Kolaitis, and Moshe Y. Vardi. On the decision problem for two-variable first-order logic. Bulletin of symbolic logic, 3 0 (1): 0 53--69, 1997

    1997

  2. [10]

    Aggregate-combine-readout gnns are more expressive than logic c2

    Stan Hauke and Przemysław Wałęga. Aggregate-combine-readout gnns are more expressive than logic c2. arXiv preprint https://arxiv.org/pdf/2508.06091, 2025. doi:10.48550/arXiv.2508.06091

    2025 doi arXiv

  3. [11]

    Measuring mathematical problem solving with the math dataset

    Dan Hendrycks, Collin Burns, Saurav Kadavath, Akul Arora, Steven Basart, Eric Tang, Dawn Song, and Jacob Steinhardt. Measuring mathematical problem solving with the math dataset. arXiv preprint arXiv:2103.03874, 2021. doi:https://doi.org/10.48550/arXiv.2103.03874

    2021 doi arXiv

  4. [12]

    Herbrand logic

    Timothy Hinrichs and Michael Genesereth. Herbrand logic. Technical Report LG-2006-02, Stanford University, Stanford, CA, 2006. http://logic.stanford.edu/reports/LG-2006-02.pdf

    2006

  5. [13]

    Hopcroft, Rajeev Motwani, and Jeffrey D

    John E. Hopcroft, Rajeev Motwani, and Jeffrey D. Ullman. Introduction to Automata Theory, Languages, and Computation (3rd Edition). Addison-Wesley Longman Publishing Co., Inc., USA, 2006. ISBN 0321455363

    2006

  6. [14]

    New liftable classes for first-order probabilistic inference

    Seyed Mehran Kazemi, Angelika Kimmig, Guy Van den Broeck, and David Poole. New liftable classes for first-order probabilistic inference. In Proceedings of the 30th International Conference on Neural Information Processing Systems, NIPS'16, page 3125–3133, Red Hook, NY, USA, 20...

    2016

  7. [15]

    Kidambi, Guramrit Singh, Paulius Dilkas, and Kuldeep S

    Ananth K. Kidambi, Guramrit Singh, Paulius Dilkas, and Kuldeep S. Meel. Towards Practical First-Order Model Counting . In Jeremias Berg and Jakob Nordstr\" o m, editors, 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025), volume 341 o...

    2025 doi

  8. [16]

    Decidability issues for two-variable logics with several linear orders

    Emanuel Kieronski. Decidability issues for two-variable logics with several linear orders. In CSL , volume 12 of LIPIcs, pages 337--351. Schloss Dagstuhl - Leibniz-Zentrum f \" u r Informatik, 2011

    2011

  9. [17]

    Small substructures and decidability issues for first-order logic with two variables

    Emanuel Kieronski and Martin Otto. Small substructures and decidability issues for first-order logic with two variables. In LICS , pages 448--457. IEEE Computer Society, 2005

    2005

  10. [18]

    Two-variable first-order logic with equivalence closure

    Emanuel Kieronski, Jakub Michaliszyn, Ian Pratt - Hartmann, and Lidia Tendera. Two-variable first-order logic with equivalence closure. In LICS , pages 431--440. IEEE Computer Society, 2012

    2012

  11. [19]

    Koller and N

    D. Koller and N. Friedman. Probabilistic Graphical Models: Principles and Techniques. Adaptive computation and machine learning. MIT Press, 2009. ISBN 9780262013192. URL https://books.google.co.in/books?id=7dzpHCHzNQ4C

    2009

  12. [20]

    Bridging weighted first order model counting and graph polynomials

    Qipeng Kuang, Ond r ej Ku z elka, Yuanhong Wang, and Yuyi Wang. Bridging weighted first order model counting and graph polynomials. In CSL , volume 363 of LIPIcs, pages 7:1--7:23. Schloss Dagstuhl - Leibniz-Zentrum f \" u r Informatik, 2026

    2026

  13. [21]

    Weighted model counting beyond two-variable logic

    Antti Kuusisto and Carsten Lutz. Weighted model counting beyond two-variable logic. In LICS , pages 619--628. ACM , 2018

    2018

  14. [22]

    Weighted first-order model counting in the two-variable fragment with counting quantifiers

    Ond r ej Ku z elka. Weighted first-order model counting in the two-variable fragment with counting quantifiers. Journal of Artificial Intelligence Research, 70: 0 1281--1307, 2021

    2021

  15. [23]

    Tractable weighted first-order model counting with bounded treewidth binary evidence

    Václav Kůla, Qipeng Kuang, Yuyi Wang, Yuanhong Wang, and Ondřej Kuželka. Tractable weighted first-order model counting with bounded treewidth binary evidence. volume 40, pages 19198--19207, 3 2026. doi:10.1609/aaai.v40i23.38994. URL https://ojs.aaai.org/index.php/AAAI/article/...

    2026 doi

  16. [24]

    An improved decision-dnnf compiler

    Jean-Marie Lagniez and Pierre Marquis. An improved decision-dnnf compiler. In Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence (IJCAI 2017), pages 667--673, 2017. doi:10.24963/ijcai.2017/93. URL https://www.ijcai.org

    2017 doi

  17. [25]

    Probabilistic time series forecasting with shape and temporal diversity

    Vincent Le Guen and Nicolas Thome. Probabilistic time series forecasting with shape and temporal diversity. Advances in neural information processing systems, 33: 0 4427--4440, 2020

    2020

  18. [26]

    Lewis and Christos H

    Harry R. Lewis and Christos H. Papadimitriou. Elements of the theory of computation, 2nd Edition. Prentice Hall, 1998

    1998

  19. [27]

    Elements of finite model theory, volume 41

    Leonid Libkin. Elements of finite model theory, volume 41. Springer, 2004

    2004

  20. [28]

    Lifted inference beyond first-order logic

    Sagar Malhotra, Davide Bizzaro, and Luciano Serafini. Lifted inference beyond first-order logic. Artif. Intell., 342: 0 104310, 2025

    2025

  21. [29]

    Two variables and two successors

    Amaldev Manuel. Two variables and two successors. In MFCS , volume 6281 of Lecture Notes in Computer Science, pages 513--524. Springer, 2010

    2010

  22. [30]

    A more practical algorithm for weighted first-order model counting with linear order axiom

    Qiaolan Meng, Jan Tóth, Yuanhong Wang, Yuyi Wang, and Ondřej Kuželka. A more practical algorithm for weighted first-order model counting with linear order axiom. In 27th European Conference on Artificial Intelligence, Frontiers in Artificial Intelligence and Applications, page...

    2024 doi

  23. [31]

    Entscheidungsproblem reduced to the case

    Edward F Moore and Hao Wang. Entscheidungsproblem reduced to the case. Proceedings of the National Academy of Sciences, 48 0 (3): 0 365--377, 1962

    1962

  24. [32]

    The on-line encyclopedia of integer sequences

    OEIS Foundation Inc. The on-line encyclopedia of integer sequences. Published electronically at https://oeis.org, 2026. Accessed: 2026-02-05

    2026

  25. [33]

    Two variable first-order logic over ordered domains

    Martin Otto. Two variable first-order logic over ordered domains. J. Symb. Log., 66 0 (2): 0 685--702, 2001

    2001

  26. [34]

    First-order probabilistic inference

    David Poole. First-order probabilistic inference. In IJCAI , pages 985--991. Morgan Kaufmann, 2003

    2003

  27. [35]

    Markov logic networks

    Matthew Richardson and Pedro Domingos. Markov logic networks. Machine Learning, 62 0 (1–2): 0 107–136, 2 2006. ISSN 0885-6125. doi:10.1007/s10994-006-5833-1. URL https://doi.org/10.1007/s10994-006-5833-1

    2006 doi

  28. [36]

    Two-variable logic with two order relations

    Thomas Schwentick and Thomas Zeume. Two-variable logic with two order relations. Log. Methods Comput. Sci., 8 0 (1), 2012

    2012

  29. [37]

    Shubham Sharma, Subhajit Roy, Mate Soos, and Kuldeep S. Meel. Ganak: A scalable probabilistic exact model counter. In Proceedings of International Joint Conference on Artificial Intelligence (IJCAI), 2019

    2019

  30. [38]

    Mate Soos and Kuldeep S. Meel. Engineering an efficient probabilistic exact model counter. In Proceedings of the International Conference on Computer Aided Verification (CAV), 2025

    2025

  31. [39]

    On discovering interesting combinatorial integer sequences

    Martin Svato s , Peter Jung, Jan T \' o th, Yuyi Wang, and Ond r ej Ku z elka. On discovering interesting combinatorial integer sequences. In IJCAI , pages 3338--3346. ijcai.org, 2023

    2023

  32. [40]

    Complexity of weighted first-order model counting in the two-variable fragment with counting quantifiers: A bound to beat

    Jan T \' o th and Ond r ej Ku z elka. Complexity of weighted first-order model counting in the two-variable fragment with counting quantifiers: A bound to beat. In KR , pages 676--686, 11 2024. doi:10.24963/kr.2024/64

    2024 doi

  33. [41]

    Lifted reasoning for combinatorial counting

    Pietro Totis, Jesse Davis, Luc De Raedt, and Angelika Kimmig. Lifted reasoning for combinatorial counting. Journal of Artificial Intelligence Research, 76: 0 1--58, 2023

    2023

  34. [42]

    Alan M. Turing. On computable numbers, with an application to the E ntscheidungsproblem. Proceedings of the London Mathematical Society, 2 0 (42): 0 230--265, 1936. URL http://www.cs.helsinki.fi/u/gionis/cc05/OnComputableNumbers.pdf

    1936

  35. [43]

    Leslie G. Valiant. The complexity of enumeration and reliability problems. SIAM J. Comput. , 8 0 (3): 0 410--421, 1979

    1979

  36. [44]

    Lifted inference with tree axioms

    Timothy van Bremen and Ond r ej Ku z elka. Lifted inference with tree axioms. Artif. Intell., 324: 0 103997, 2023

    2023

  37. [45]

    Faster lifting for two-variable logic using cell graphs

    Timothy Van Bremen and Ond r ej Ku z elka. Faster lifting for two-variable logic using cell graphs. In Uncertainty in Artificial Intelligence, pages 1393--1402. PMLR, 2021

    2021

  38. [46]

    On the completeness of first-order knowledge compilation for lifted probabilistic inference

    Guy Van den Broeck. On the completeness of first-order knowledge compilation for lifted probabilistic inference. In Proceedings of the 24th International Conference on Neural Information Processing Systems, NIPS'11, page 1386–1394, Red Hook, NY, USA, 2011. Curran Associates In...

    2011

  39. [47]

    Conditioning in first-order knowledge compilation and lifted probabilistic inference

    Guy Van den Broeck and Jesse Davis. Conditioning in first-order knowledge compilation and lifted probabilistic inference. In Proceedings of the Twenty-Sixth AAAI Conference on Artificial Intelligence, AAAI'12, page 1961–1967. AAAI Press, 2012

    1961

  40. [48]

    Skolemization for weighted first-order model counting

    Guy Van den Broeck, Wannes Meert, and Adnan Darwiche. Skolemization for weighted first-order model counting. In Proceedings of the Fourteenth International Conference on Principles of Knowledge Representation and Reasoning, KR'14, page 111–120. AAAI Press, 2014. ISBN 1577356578

    2014

  41. [49]

    An introduction to lifted probabilistic inference

    Guy Van den Broeck, Kristian Kersting, Sriraam Natarajan, and David Poole. An introduction to lifted probabilistic inference. The MIT Press, August 2021. ISBN 978-0-262-36559-8. doi:10.7551/mitpress/10548.001.0001. URL https://doi.org/10.7551/mitpress/10548.001.0001

    2021 doi

  42. [50]

    Moshe Y. Vardi. The complexity of relational query languages (extended abstract). In STOC , pages 137--146. ACM , 1982

    1982

  43. [51]

    Efficient probabilistic inference for dynamic relational models

    Jonas Vlasselaer, Wannes Meert, Guy Van den Broeck, and Luc De Raedt. Efficient probabilistic inference for dynamic relational models. In Workshops at the Twenty-Eighth AAAI Conference on Artificial Intelligence, 2014

    2014

  44. [52]

    Proving theorems by pattern recognition—ii

    Hao Wang. Proving theorems by pattern recognition—ii. Bell system technical journal, 40 0 (1): 0 1--41, 1961

    1961

  45. [53]

    Lifted algorithms for symmetric weighted first-order model sampling

    Yuanhong Wang, Juhua Pu, Yuyi Wang, and Ondřej Kuželka. Lifted algorithms for symmetric weighted first-order model sampling. Artificial Intelligence, 331: 0 104114, 2024. ISSN 0004-3702. doi:https://doi.org/10.1016/j.artint.2024.104114. URL https://www.sciencedirect.com/scienc...

    2024

  46. [54]

    Watts and Steven H

    Duncan J. Watts and Steven H. Strogatz. Collective dynamics of `small-world' networks. Nature, 393 0 (6684): 0 440--442, June 1998. doi:10.1038/30918

    1998 doi

Pith tools

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