pith. machine review for the scientific record. sign in

arxiv: 2605.03391 · v1 · submitted 2026-05-05 · 💻 cs.LO · cs.AI

Recognition: unknown

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

Astrid Klipfel, Ond\v{r}ej Ku\v{z}elka, Shixin Sun, Yi Chang, Yuanhong Wang

Pith reviewed 2026-05-07 13:42 UTC · model grok-4.3

classification 💻 cs.LO cs.AI
keywords weighted first-order model countingC²counting quantifiersdomain liftabilitymodulo countinglifted inferenceScott normal form
0
0 comments X

The pith

Direct operation on Scott normal form reduces WFOMC data complexity in C² from quadratic to linear in counting parameters and proves domain-liftability for modulo counting.

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

The paper introduces IncrementalWFOMC3, an algorithm for weighted first-order model counting on the two-variable fragment with counting quantifiers that works directly on Scott normal form while keeping the counting quantifiers intact. Prior algorithms relied on multi-stage reductions to remove those quantifiers via cardinality constraints, which added overhead that grew with domain size. By avoiding those reductions the new method establishes a tighter polynomial bound whose degree is linear rather than quadratic in the counting parameters. The same direct treatment also shows that the richer fragment with native modulo counting quantifiers remains domain-liftable.

Core claim

IncrementalWFOMC3 computes the weighted sum of models for C² sentences by processing their Scott normal form directly and retaining counting quantifiers throughout inference; this yields data complexity linear in the counting parameters. The approach further proves that C²_mod, the extension that includes modulo counting quantifiers, is domain-liftable.

What carries the argument

IncrementalWFOMC3 operating directly on Scott normal form while retaining counting quantifiers throughout inference.

If this is right

  • WFOMC for C² has data complexity linear rather than quadratic in the counting parameters.
  • C²_mod is domain-liftable, so WFOMC remains polynomial in domain size for the modulo extension.
  • The algorithm avoids the overhead of prior reduction steps and therefore runs faster in practice.
  • It scales better than both earlier WFOMC procedures and state-of-the-art propositional counters.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Implementations of other lifted-inference tasks may similarly benefit from keeping quantifiers native instead of compiling them away.
  • The linear dependence on counting parameters could allow the method to handle larger parameter values arising in statistical relational models.
  • Similar direct-treatment strategies might extend tractability results to additional fragments containing other kinds of numeric quantifiers.

Load-bearing premise

That direct processing of Scott normal form while retaining counting quantifiers preserves correctness and produces the claimed polynomial bound without introducing hidden exponential costs.

What would settle it

An exhaustive enumeration on a small domain for a C² sentence with counting parameter k greater than 5 that yields a weighted count different from the output of IncrementalWFOMC3.

Figures

Figures reproduced from arXiv: 2605.03391 by Astrid Klipfel, Ond\v{r}ej Ku\v{z}elka, Shixin Sun, Yi Chang, Yuanhong Wang.

Figure 1
Figure 1. Figure 1: Specifically, a C2 sentence can be transformed into a normal form, called SC2 (Scott normal form with counting 2 ): Γ = Ψ ∧ ^ i∈[M]  ∀x∃ =kiy : Ri(x, y)  , (1) where Ψ is an FO2 CC sentence, each Ri/2 is a distinguished binary predicate, each ki is a non￾negative integer, and M is a non-negative integer [21]. Then the counting quantifiers in Eq. (1) can be eliminated by introducing additional cardinality… view at source ↗
Figure 1
Figure 1. Figure 1: WFOMC reductions for C2 . 3.4 1-Types and 2-Tables Before introducing IncrementalWFOMC [31], we need the notions of 1-types and 2-tables, which are commonly used in the literature studying two-variable logic [22, 39]. A unary literal is a literal containing only one variable x. A binary literal is a literal containing both variables x and y. For example, P(x) is a unary literal, and R(x, y) is a binary lit… view at source ↗
Figure 2
Figure 2. Figure 2: Illustrated models of colored graphs. Example 4. Example models of the 2-colored graph sentence ΓCG over the domain size of 5 are illustrated in Figure 2a. In these models, constants 1, 3, and 5 realize the 1-type τ1 (red), and constants 2, 4 realize the 1-type τ2 (black). The corresponding 1-type configuration is the vector k = (3, 2). 3.5 IncrementalWFOMC We sketch the algorithm IncrementalWFOMC from [31… view at source ↗
Figure 3
Figure 3. Figure 3: Model extensions of two colored graphs µ ′ 1 and µ ′ 2 with the same 1-type configuration (3, 1) by adding a new vertex 5. The sets of extended models Mµ ′ 1 ,τ1 , Mµ ′ 1 ,τ2 , Mµ ′ 2 ,τ1 , and Mµ ′ 2 ,τ2 are mutually disjoint. As the weights of all predicates are set to 1, Wµ,τl is simply the number of models in Mµ,τl . It is clear that Wµ ′ 1 ,τ1 = Wµ ′ 2 ,τ1 = 2 and Wµ ′ 1 ,τ2 = Wµ ′ 2 ,τ2 = 8, since µ … view at source ↗
Figure 4
Figure 4. Figure 4: An illustration of the incremental computation of view at source ↗
Figure 5
Figure 5. Figure 5: Runtime (log scale) comparison for counting view at source ↗
Figure 6
Figure 6. Figure 6: Runtime (log scale) comparison for counting view at source ↗
Figure 7
Figure 7. Figure 7: Runtime comparison for counting (a) 2-regular and (b) 3-regular digraphs. 23 view at source ↗
Figure 8
Figure 8. Figure 8: Runtime (log scale) comparison for counting Barabási-Albert (BA) graphs under two view at source ↗
Figure 9
Figure 9. Figure 9: Runtime comparison for three modulo counting graph families. view at source ↗
Figure 10
Figure 10. Figure 10: Runtime comparison for counting m-odd-degree graphs with undirected edges k = 2n and (a) m = 2, (b) m = 4, and (c) m = 6. Beyond runtime, we also examined the model counts of Γm-odd-degree, denoted by T(n, m, k). For some parameter settings, these counts coincide with known integer sequences in the OEIS. For instance, T(n, 0, k) counts the number of labeled even-degree graphs with n vertices and k edges a… view at source ↗
Figure 11
Figure 11. Figure 11: Correctness validation for counting (a) 2-regular, (b) 3-regular, and (c) 4-regular graphs. view at source ↗
Figure 12
Figure 12. Figure 12: Correctness validation for counting (a) 0mod2-regular, (b) 1mod2-regular, and (c) view at source ↗
Figure 13
Figure 13. Figure 13: Correctness validation for the m-odd-degree graph counting task from Section 6.3. 0 15 30 45 60 75 90 Domain Size 0 20000 40000 60000 80000 100000 Memory Usage (MB) Recursive Fast Ours (a) 3-regular 0 15 30 45 60 75 90 Domain Size 0 10000 20000 30000 40000 Memory Usage (MB) Recursive Fast Ours (b) 4-regular 0 15 30 45 60 75 90 Domain Size 0 10000 20000 30000 40000 Memory Usage (MB) Recursive Fast Ours (c)… view at source ↗
Figure 14
Figure 14. Figure 14: Peak memory usage for counting (a) 3-regular, (b) 4-regular, and (c) 5-regular graphs. view at source ↗
Figure 15
Figure 15. Figure 15: Peak memory usage comparison for counting view at source ↗
Figure 16
Figure 16. Figure 16: Peak memory results for counting (a) 2-regular and (b) 3-regular digraphs. C Reduction of M-Odd-Degree Graphs The initial, more direct formulation of the problem is as follows: Γm-odd-degree =(∀x : ¬E(x, x)) ∧ (∀x∀y : E(x, y) → E(y, x))∧ (∀x : Odd(x) ↔ ∃=1,2 y : E(x, y)) ∧ (∃ =mx : Odd(x)) ∧ (|E| = 2k). Then we used the transformations described in Section A. All predicates A, B, C, U, and P appearing bel… view at source ↗
read the original abstract

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

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The paper introduces IncrementalWFOMC3, a lifted algorithm for weighted first-order model counting (WFOMC) on the two-variable fragment with counting quantifiers (C²) and its modulo extension (C²_mod). It operates directly on Scott normal form retaining counting quantifiers, deriving a tighter data-complexity bound reducing the polynomial degree from quadratic to linear in counting parameters for C², proving domain-liftability for C²_mod, and showing empirical runtime improvements over existing methods.

Significance. If the central claims hold, this work would advance lifted probabilistic inference by providing a more efficient algorithm for an expressive fragment, with a strictly improved complexity bound and an extension to native modulo counting. The direct treatment of quantifiers avoids reduction overhead, and the empirical gains suggest practical impact for applications in AI reasoning.

major comments (2)
  1. [§4] §4 (Complexity Analysis): The claim of a linear (rather than quadratic) data-complexity bound for WFOMC in C² rests on the incremental DP maintaining state space and transition costs that scale linearly with individual counting bounds; the manuscript must explicitly show that no pairwise cardinality convolutions or products arise when combining multiple retained ∃^{=k} atoms in the Scott normal form representation.
  2. [§5] §5 (Liftability Proof): The proof that C²_mod is domain-liftable is described as existing but only outlined; because this is one of the two main results and extends tractability to a richer fragment, the full derivation is required to confirm absence of hidden exponential factors in the handling of modulo counting quantifiers.
minor comments (2)
  1. [Empirical Evaluation] The empirical evaluation should include implementation details (e.g., data structures for the incremental DP and exact counting-parameter ranges tested) to support reproducibility of the reported runtime improvements.
  2. [Preliminaries] Notation for the modulo counting quantifiers in the definition of C²_mod should be clarified with an explicit example sentence to avoid ambiguity with standard counting quantifiers.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive comments, which help strengthen the presentation of our results on IncrementalWFOMC3. We address each major comment below and will revise the manuscript accordingly.

read point-by-point responses

  1. Referee: [§4] §4 (Complexity Analysis): The claim of a linear (rather than quadratic) data-complexity bound for WFOMC in C² rests on the incremental DP maintaining state space and transition costs that scale linearly with individual counting bounds; the manuscript must explicitly show that no pairwise cardinality convolutions or products arise when combining multiple retained ∃^{=k} atoms in the Scott normal form representation.

    Authors: We agree that an explicit argument is needed to confirm the absence of pairwise convolutions. In the incremental DP of Section 4, each retained ∃^{=k} atom is processed sequentially: the state vector tracks the cumulative count for the current quantifier independently of prior ones, and transitions update a single dimension at a time via additive increments. Because the Scott normal form atoms are independent in their cardinality constraints, no convolution or product between pairs of counting bounds is performed; the overall cost remains linear in the sum of the individual bounds. We will add a dedicated lemma (with a short inductive argument) in the revised Section 4 to make this separation explicit and thereby rigorously establish the linear data-complexity bound. revision: yes

  2. Referee: [§5] §5 (Liftability Proof): The proof that C²_mod is domain-liftable is described as existing but only outlined; because this is one of the two main results and extends tractability to a richer fragment, the full derivation is required to confirm absence of hidden exponential factors in the handling of modulo counting quantifiers.

    Authors: We concur that the domain-liftability proof for C²_mod merits a complete, self-contained derivation. The outline in Section 5 indicates that modulo constraints are incorporated by extending the DP state with a constant-size residue tracker per quantifier, preserving polynomial dependence on domain size. In the revised manuscript we will expand this into a full proof: we first reduce C²_mod sentences to an equivalent Scott normal form, then show by induction on formula structure that the incremental DP computes the weighted count in time polynomial in the domain size, with the modulo operations contributing only a linear factor in the state space and no exponential blow-up. All intermediate lemmas and the final complexity statement will be included. revision: yes

Circularity Check

0 steps flagged

No circularity: linear bound and liftability follow from direct analysis of IncrementalWFOMC3 on Scott normal form

full rationale

The paper presents IncrementalWFOMC3 as a new algorithm that retains counting quantifiers in Scott normal form and analyzes its data complexity directly. The reduction from quadratic to linear degree in counting parameters and the domain-liftability of C²_mod are obtained by bounding the state space and transitions of this incremental procedure. No equation or claim reduces by construction to a fitted parameter, a self-defined quantity, or a load-bearing self-citation; the arguments rely on standard dynamic-programming size analysis applied to the retained quantifiers. The derivation is therefore self-contained against external complexity benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The central claims rest on the existence of a Scott normal form that preserves semantics for C² and C²_mod, on standard assumptions about finite domains and weight functions in WFOMC, and on the correctness of incremental counting updates; no free parameters or invented entities are introduced in the abstract.

axioms (2)
  • domain assumption Every C² sentence can be converted to an equivalent Scott normal form that retains counting quantifiers.
    Invoked to justify operating directly on the normal form without loss of generality.
  • standard math Weighted model counting over finite domains is well-defined for the given weight functions.
    Background assumption of the WFOMC task.

pith-pipeline@v0.9.0 · 5621 in / 1417 out tokens · 65874 ms · 2026-05-07T13:42:13.929089+00:00 · methodology

Review history (2 revisions) →

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

42 extracted references · 31 canonical work pages

  1. [1]

    Statistical mechanics of complex networks

    Réka Albert and Albert-László Barabási. Statistical mechanics of complex networks.Rev. Mod. Phys., 74:47–97, Jan 2002. doi: 10.1103/RevModPhys.74.47

    work page doi:10.1103/revmodphys.74.47 2002

  2. [2]

    Kostylev, Mikaël Monet, Jorge Pérez, Juan L

    Pablo Barceló, Egor V. Kostylev, Mikaël Monet, Jorge Pérez, Juan L. Reutter, and Juan Pablo Silva. The logical expressiveness of graph neural networks. In8th International Conference on Learning Representations, ICLR 2020, Addis Ababa, Ethiopia, April 26-30, 2020. OpenRe- view.net, 2020. URLhttps://openreview.net/forum?id=r1lZ7AEKvB

    2020

  3. [3]

    Symmetric weighted first- order model counting

    Paul Beame, Guy Van den Broeck, Eric Gribkoff, and Dan Suciu. Symmetric weighted first- order model counting. InProceedings of the 34th ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems, volume 31 ofSIGMOD/PODS’15, pages 313–328, Mel- bourne Victoria Australia, May 2015. ACM. ISBN 9781450327572. doi: 10.1145/2745754. 2745760. URLhttp://d...

    work page doi:10.1145/2745754 2015

  4. [4]

    Modulo counting on words and trees

    Bartosz Bednarczyk and Witold Charatonik. Modulo counting on words and trees. In Satya V. Lokam and R. Ramanujam, editors,37th IARCS Annual Conference on Foundations of Soft- ware Technology and Theoretical Computer Science, FSTTCS 2017, Kanpur, India, December 11-15, 2017, LIPIcs, pages 12:1–12:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik,

    2017

  5. [5]

    URLhttps://drops.dagstuhl.de/entities/ document/10.4230/LIPIcs.FSTTCS.2017.12

    doi: 10.4230/LIPICS.FSTTCS.2017.12. URLhttps://drops.dagstuhl.de/entities/ document/10.4230/LIPIcs.FSTTCS.2017.12

    work page doi:10.4230/lipics.fsttcs.2017.12 2017

  6. [6]

    Two variable logic with ultimately periodic counting.SIAM Journal on Computing, 53(4):884–968, 2024

    Michael Benedikt, Egor V Kostylev, and Tony Tan. Two variable logic with ultimately periodic counting.SIAM Journal on Computing, 53(4):884–968, 2024. doi: 10.1137/22M1504792. URL https://doi.org/10.1137/22m1504792

    work page doi:10.1137/22m1504792 2024

  7. [7]

    Open-world probabilistic databases: Semantics, algorithms, complexity.Artif

    İsmail İlkan Ceylan, Adnan Darwiche, and Guy Van den Broeck. Open-world probabilistic databases: Semantics, algorithms, complexity.Artif. Intell., 295:103474, June 2021. doi: 10.1016/j.artint.2021.103474

    work page doi:10.1016/j.artint.2021.103474 2021

  8. [8]

    Meel, and Moshe Y

    Supratik Chakraborty, Kuldeep S. Meel, and Moshe Y. Vardi. A scalable approximate model counter. In Christian Schulte, editor,Principles and Practice of Constraint Pro- gramming - 19th International Conference, CP 2013, Uppsala, Sweden, September 16-20,

    2013

  9. [9]

    Springer, 2013

    Proceedings, Lecture Notes in Computer Science, pages 200–216. Springer, 2013. doi: 10.1007/978-3-642-40627-0\_18. URLhttps://doi.org/10.1007/978-3-642-40627-0_18

    work page doi:10.1007/978-3-642-40627-0 2013

  10. [10]

    Sampling regular graphs and a peer-to- peer network.Comb

    Colin Cooper, Martin Dyer, and Catherine Greenhill. Sampling regular graphs and a peer-to- peer network.Comb. Probab. Comput., 16(4):557–593, 2007. doi: 10.1017/S0963548306007978. URLhttps://doi.org/10.1017/S0963548306007978

    work page doi:10.1017/s0963548306007978 2007

  11. [11]

    Amsterdam University Press

    Jörg Flum, Erich Grädel, and Thomas Wilke, editors.Logic and Automata: History and Perspectives [in Honor of Wolfgang Thomas], volume 2 ofTexts in Logic and Games, 2008. Amsterdam University Press. ISBN 978-90-5356-576-6. 27

    2008

  12. [12]

    Pu Gao and Nicholas C. Wormald. Uniform generation of random regular graphs.SIAM J. Comput., 46(4):1395–1427, 2017. doi: 10.1137/15M1052779. URLhttps://doi.org/10.1137/ 15M1052779

    work page doi:10.1137/15m1052779 2017

  13. [13]

    MIT press, 2007

    Lise Getoor and Ben Taskar.Introduction to statistical relational learning. MIT press, 2007. doi: 10.7551/mitpress/7432.001.0001

    work page doi:10.7551/mitpress/7432.001.0001 2007

  14. [14]

    On the decision problem for two-variable first-order logic , journal =

    Erich Grädel, Phokion G Kolaitis, and Moshe Y Vardi. On the decision problem for two-variable first-order logic.Bulletin of Symbolic Logic, 3(1):53–69, 1997. doi: 10.2307/421196

    work page doi:10.2307/421196 1997

  15. [15]

    Two-variable logic with counting is decidable

    Erich Grädel, Martin Otto, and Eric Rosen. Two-variable logic with counting is decidable. In Proceedings of Twelfth Annual IEEE Symposium on Logic in Computer Science, pages 306–317. IEEE Computer Society, 1997. doi: 10.1109/LICS.1997.614957. URLhttps://doi.org/10. 1109/LICS.1997.614957

    work page doi:10.1109/lics.1997.614957 1997

  16. [16]

    Lifted probabilistic inference: A guide for the database researcher.IEEE Data Eng

    Eric Gribkoff, Dan Suciu, and Guy Van den Broeck. Lifted probabilistic inference: A guide for the database researcher.IEEE Data Eng. Bull., 37(3):6–17, 2014. URLhttp://sites. computer.org/debull/A14sept/p6.pdf

    2014

  17. [17]

    Aggregate-combine-readout GNNs can ex- press logical classifiers beyond the logic C2.Proceedings of the AAAI Conference on Ar- tificial Intelligence, 40(26):21594–21601, Mar

    Stan P Hauke and Przemysław Andrzej Wałęga. Aggregate-combine-readout GNNs can ex- press logical classifiers beyond the logic C2.Proceedings of the AAAI Conference on Ar- tificial Intelligence, 40(26):21594–21601, Mar. 2026. doi: 10.1609/aaai.v40i26.39308. URL https://ojs.aaai.org/index.php/AAAI/article/view/39308

    work page doi:10.1609/aaai.v40i26.39308 2026

  18. [18]

    Hanf normal form for first-order logic with unary counting quantifiers

    Lucas Heimberg, Dietrich Kuske, and Nicole Schweikardt. Hanf normal form for first-order logic with unary counting quantifiers. InProceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’16, page 277–286, New York, NY, USA, 2016. Association for Computing Machinery. ISBN 9781450343916. doi: 10.1145/2933575.2934571. URLhttps: /...

    work page doi:10.1145/2933575.2934571 2016

  19. [19]

    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 Daniel D. Lee, Masashi Sugiyama, Ulrike von Luxburg, Isabelle Guyon, and Roman Garnett, editors,Advances in Neural Information Processing Systems 29: Annual Conference on Neural Information Processing Systems 2016, De...

    2016

  20. [20]

    arXiv preprint arXiv:1707.07763 , year=

    Seyed Mehran Kazemi, Angelika Kimmig, Guy Van den Broeck, and David Poole. Domain recursion for lifted inference with existential quantifiers.CoRR, abs/1707.07763, 2017. URL http://arxiv.org/abs/1707.07763

    work page arXiv 2017

  21. [21]

    Regular graphs and the spectra of two-variable logic with counting.SIAM J

    Eryk Kopczynski and Tony Tan. Regular graphs and the spectra of two-variable logic with counting.SIAM J. Comput., 44(3):786–818, 2015. doi: 10.1137/130943625. URLhttps: //doi.org/10.1137/130943625

    work page doi:10.1137/130943625 2015

  22. [22]

    Bridging weighted first order model counting and graph polynomials

    Qipeng Kuang, Ondřej Kuželka, Yuanhong Wang, and Yuyi Wang. Bridging weighted first order model counting and graph polynomials. In Stefano Guerrini and Barbara König, ed- itors,34th EACSL Annual Conference on Computer Science Logic (CSL 2026), volume 363 ofLeibniz International Proceedings in Informatics (LIPIcs), pages 7:1–7:23, Dagstuhl, Ger- many, 2026...

    work page doi:10.4230/lipics.csl.2026.7 2026

  23. [23]

    Weighted first-order model counting in the two-variable fragment with count- ing quantifiers.J

    Ondřej Kuželka. Weighted first-order model counting in the two-variable fragment with count- ing quantifiers.J. Artif. Intell. Res., 70:1281–1307, 2021. doi: 10.1613/JAIR.1.12320. URL https://doi.org/10.1613/jair.1.12320

    work page doi:10.1613/jair.1.12320 2021

  24. [24]

    Towards a more efficient approach for the satisfiability of two-variable logic

    Ting-Wei Lin, Chia-Hsuan Lu, and Tony Tan. Towards a more efficient approach for the satisfiability of two-variable logic. In2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1–13, 2021. doi: 10.1109/LICS52264.2021.9470502

    work page doi:10.1109/lics52264.2021.9470502 2021

  25. [25]

    Kamal Lodaya and A. V. Sreejith. Two-variable first order logic with counting quantifiers: complexity results. InDevelopments in Language Theory - 21st International Conference, DLT 2017, Liège, Belgium, August 7-11, 2017, Proceedings, Lecture Notes in Computer Science, pages 260–271. Springer, 2017. doi: 10.1007/978-3-319-62809-7\_19

    work page doi:10.1007/978-3-319-62809-7 2017

  26. [26]

    Lifted inference beyond first-order logic

    Sagar Malhotra, Davide Bizzaro, and Luciano Serafini. Lifted inference beyond first-order logic. Artif. Intell., 342:104310, May 2025. ISSN 0004-3702. doi: 10.1016/j.artint.2025.104310

    work page doi:10.1016/j.artint.2025.104310 2025

  27. [27]

    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 Ulle Endriss, Francisco S. Melo, Kerstin Bach, Alberto José Bugarín Diz, Jose Maria Alonso-Moral, Senén Barro, and Fredrik Heintz, editors,ECAI 2024 - 27th European Conference on Artificial In...

    work page doi:10.3233/faia240858 2024

  28. [28]

    Model enumeration of two-variable logic with quadratic delay complexity

    Qiaolan Meng, Juhua Pu, Hongting Niu, Yuyi Wang, Yuanhong Wang, and Ondřej Kuželka. Model enumeration of two-variable logic with quadratic delay complexity. In40th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2025, Singapore, June 23-26, 2025, pages 301–313. IEEE, 2025. doi: 10.1109/LICS65433.2025.00030

    work page doi:10.1109/lics65433.2025.00030 2025

  29. [29]

    Zettlemoyer, Kristian Kersting, Michael Haimes, and Leslie Pack Kael- bling

    Brian Milch, Luke S. Zettlemoyer, Kristian Kersting, Michael Haimes, and Leslie Pack Kael- bling. Lifted probabilistic inference with counting formulas. 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 1062–1068. AAAI Press, 2008...

    2008

  30. [30]

    Meel, and Jiong Yang

    Yash Pote, Kuldeep S. Meel, and Jiong Yang. Towards real-time approximate counting. In Toby Walsh, Julie Shah, and Zico Kolter, editors,Thirty-Ninth AAAI Conference on Artificial Intelligence, Thirty-Seventh Conference on Innovative Applications of Artificial Intelligence, Fifteenth Symposium on Educational Advances in Artificial Intelligence, AAAI 2025, ...

    work page doi:10.1609/aaai.v39i11.33231 2025

  31. [31]

    Markov logic networks.Mach

    Matthew Richardson and Pedro Domingos. Markov logic networks.Mach. Learn., 62:107–136, 2006. doi: 10.1007/S10994-006-5833-1. URLhttps://doi.org/10.1007/ s10994-006-5833-1

    work page doi:10.1007/s10994-006-5833-1 2006

  32. [32]

    Shubham Sharma, Subhajit Roy, Mate Soos, and Kuldeep S. Meel. GANAK: A scalable probabilistic exact model counter. InProceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence (IJCAI 2019), pages 1169–1176. ijcai.org, 2019. doi: 10. 24963/ijcai.2019/163. 29

    2019

  33. [33]

    Lifted inference with linear order axiom

    Jan Tóth and Ondřej Kuželka. Lifted inference with linear order axiom. InThirty-Seventh AAAI Conference on Artificial Intelligence, AAAI 2023, Thirty-Fifth Conference on Inno- vative Applications of Artificial Intelligence, IAAI 2023, Thirteenth Symposium on Educa- tional Advances in Artificial Intelligence, EAAI 2023, Washington, DC, USA, February 7- 14,...

    work page doi:10.1609/aaai.v37i10.26449 2023

  34. [34]

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

    Jan Tóth and Ondřej Kuželka. Complexity of weighted first-order model counting in the two- variable fragment with counting quantifiers: A bound to beat. InProceedings of the 21st International Conference on Principles of Knowledge Representation and Reasoning, pages 676–686, 8 2024. doi: 10.24963/kr.2024/64. URLhttps://doi.org/10.24963/kr.2024/64

    work page doi:10.24963/kr.2024/64 2024

  35. [35]

    Leslie G. Valiant. The complexity of computing the permanent.Theor. Comput. Sci., 8: 189–201, 1979. doi: 10.1016/0304-3975(79)90044-6

    work page doi:10.1016/0304-3975(79)90044-6 1979

  36. [36]

    Faster lifting for two-variable logic using cell graphs

    Timothy Van Bremen and Ondřej Kuželka. Faster lifting for two-variable logic using cell graphs. InUncertainty in Artificial Intelligence, pages 1393–1402. PMLR, 2021. URLhttps: //proceedings.mlr.press/v161/bremen21a.html

    2021

  37. [37]

    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. InAdvances in Neural Information Processing Systems 24: 25th Annual Conference on Neural Information Processing Systems 2011. Proceedings of a meeting held 12- 14 December 2011, Granada, Spain, pages 1386–1394, 2011. URLhttps://proceedings. neu...

    2011

  38. [38]

    Lifted probabilistic inference by first-order knowledge compilation

    Guy Van den Broeck, Nima Taghipour, Wannes Meert, Jesse Davis, and Luc De Raedt. Lifted probabilistic inference by first-order knowledge compilation. InProceedings of the Twenty- Second International Joint Conference on Artificial Intelligence, pages 2178–2185, 2011. doi: 10.5591/978-1-57735-516-8/IJCAI11-363

    work page doi:10.5591/978-1-57735-516-8/ijcai11-363 2011

  39. [39]

    Skolemization for weighted first-order model counting

    Guy Van den Broeck, Wannes Meert, and Adnan Darwiche. Skolemization for weighted first-order model counting. In Chitta Baral, Giuseppe De Giacomo, and Thomas Eiter, editors,Principles of Knowledge Representation and Reason- ing: Proceedings of the Fourteenth International Conference, KR 2014, Vienna, Austria, July 20-24, 2014. AAAI Press, 2014. URLhttps:/...

    2014

  40. [40]

    The MIT Press, August 2021

    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. URLhttps://doi.org/10.7551/mitpress/10548.001.0001

    work page doi:10.7551/mitpress/10548.001.0001 2021

  41. [41]

    Lifted algorithms for sym- metric weighted first-order model sampling.Artif

    Yuanhong Wang, Juhua Pu, Yuyi Wang, and Ondřej Kuželka. Lifted algorithms for sym- metric weighted first-order model sampling.Artif. Intell., 331:104114, 2024. ISSN 0004-3702. doi: https://doi.org/10.1016/j.artint.2024.104114. URLhttps://www.sciencedirect.com/ science/article/pii/S000437022400050X

    work page doi:10.1016/j.artint.2024.104114 2024

  42. [42]

    Faster lifting for ordered domains with predecessor relations

    Kuncheng Zou, Jiahao Mai, Yonggang Zhang, Yuyi Wang, Ondřej Kuželka, Yuanhong Wang, and Yi Chang. Faster lifting for ordered domains with predecessor relations. InECAI 2025 - 28th European Conference on Artificial Intelligence, volume 413 ofFrontiers in Artificial Intelligence and Applications, pages 1784–1791. IOS Press, 2025. doi: 10.3233/FAIA251008. UR...

    work page doi:10.3233/faia251008 2025