Weighted First-Order Model Counting in the Two-Variable Fragment With Counting Quantifiers

• WFOMC supports probabilistic inference in statistical relational learning, but probabilistic inference and relational WFOMC are generally intractable.Source: §1 · p. 1
• WFOMC is domain-liftable for every fixed first-order sentence containing at most two variables [Van den Broeck, 2011; Van den Broeck, Meert, and Darwiche, 2014].Source: §1 · p. 1
• Kuusisto and Lutz [2018] extended two-variable domain-liftability to one functionality constraint and identified multiple functionality constraints as a route to counting quantifiers.Source: §1 · p. 1
• The paper develops a simpler method for adding arbitrary numbers of functionality and cardinality constraints while guaranteeing polynomial-time inference.Source: §1 · pp. 1–2
• The resulting method proves domain-liftability for the two-variable fragment with counting quantifiers.Source: §1 · p. 2

2.1 Lagrange Interpolation

• Lagrange interpolation uniquely recovers a degree-d polynomial from d + 1 points with distinct x-values.Source: §2.1 · p. 2

2.2 First-Order Logic

• FO2 restricts formulas to variables {x, y}; its satisfiability is decidable and WFOMC is polynomial-time in domain size [Van den Broeck, 2011; Van den Broeck, Meert, and Darwiche, 2014].Source: §2.2 · p. 3

2.2.1 First-Order Logic With Counting Quantifiers

• Counting quantifiers express at least, at most, or exactly k satisfying elements, and can constrain binary relations to be functions or bijections.Source: §2.2.1 · p. 3

2.3 Weighted First-Order Model Counting

• WFOMC sums products of predicate weights over worlds satisfying a sentence, with unspecified predicate weights defaulting to one.Source: §2.3 · p. 4, We also define · p. 4

2.3.1 Two Useful Technical Results About WFOMC

• For rational weights, WFOMC output has numerator and denominator bit lengths polynomial in domain size and log M, independently of the number of predicates.Source: §2.3.1 · p. 4
• A formula-negation replacement using fresh predicates is available through a transformation attributed to [Beame et al., 2015].Source: §2.3.1 · pp. 4–5

2.4 Domain-Lifted Inference

• Domain liftability requires WFOMC algorithms to run polynomially in domain size and weight-representation length, and such WFOMC computes MLN partition functions and marginals.Source: §2.4 · p. 5, §2.4.1 · p. 6

2.4.1 An Application of WFOMC: Inference in Markov Logic Networks

• An MLN is a set of weighted first-order formulas whose induced world distribution uses satisfied-grounding counts and a partition-function normalizer.Source: §2.4.1 · pp. 5–6

3 Weighted Model-Counting Functions

• A relation-cardinality vector records the numbers of true ground atoms for a selected list of predicates.Source: §3 · p. 6
• A model-counting function returns the number of worlds whose selected relation-cardinality vector equals a specified vector.Source: §3 · pp. 6–7
• Weighted model-counting functions generalize model-counting functions by assigning weights according to relation cardinalities and serve as the paper’s main computational workhorses.Source: §3 · p. 7

3.1 Computing Weighted Model-Counting Functions

• The paper avoids complex-valued WFOMC by computing weighted model-counting functions through polynomial coefficient extraction.Source: §3.1 · p. 8
• Proposition 4 establishes polynomial-time computation of the corresponding weighted model-counting function whenever WFOMC is polynomial-time in domain size and weight-encoding length.Source: §3.1 · p. 8
• WFOMC can be converted into a polynomial whose monomial coefficients encode weighted model-counting values for relation-cardinality vectors.Source: §3.1 · p. 8
• Lagrange interpolation extracts the needed coefficients from |D| + 1 WFOMC evaluations, with polynomial bit complexity and runtime.Source: §3.1 · p. 9

• WFOMC remains domain-liftable when a domain-liftable sentence is conjoined with Boolean combinations of cardinality constraints.This is established for constraints of the form ψ(|R_i1| ▷◁ k_1, …, |R_im| ▷◁ k_m).Source: §4 · p. 9
• The method evaluates the associated WMC-function on polynomially many cardinality vectors whose coordinates range over feasible predicate counts.The evaluation set is D = {0, …, M_1} × ··· × {0, …, M_m}, with M_i = |∆|^arity(R_i).Source: §4 · pp. 9–10
• The resulting WFOMC is therefore computable in time polynomial in the size of the domain.Source: §4 · p. 10
• The technique also extends beyond cardinality constraints to rational-valued weight functions depending only on predicate counts.The paper notes that this broader setting is not needed for its main development.Source: §4 · p. 10

5 WFOMC with Functionality Constraints5

• Computing WFOMC for an FO2 sentence with any number of functionality constraints remains domain-liftable.A functionality constraint requires exactly one y for every x satisfying the relation ψ(x, y).Source: §5 · p. 10
• The reduction transforms the problem into one involving only cardinality constraints and an FO2 sentence, allowing Proposition 5 to complete the polynomial-time argument.Source: §5 · pp. 10–11
• Each functionality constraint ∀x∃=1y R(x,y) is equivalently replaced by ∀x∃y R(x,y) together with the cardinality constraint |R| = |∆|.The equivalence follows from the pigeon-hole principle and ensures uniqueness when every x has at least one related y.Source: §5 · pp. 10–11
• Unlike Kuusisto and Lutz [2018], the result already permits multiple functionality constraints.Source: §5 · p. 10
• For uniformly sampled functions, the computed fixed-point distribution matches the analytical formula across the displayed values.The MC-function is used to extract probabilities by retaining points satisfying |f| = |∆|, and the two approaches agree.Source: Figure 2 · p. 11, §5 · p. 12

6.1 Two Types of Constraints: ∀x∃=ky and ∃=kx∀y

• WFOMC with constraints of the forms ∀x∃=ky and ∃=kx∀y, together with cardinality constraints, is domain-liftable.The proof removes ∃=kx∀y constraints using Lemma 3 and ∀x∃=ky constraints using Lemma 2, reducing the problem to FO2 with cardinality constraints.Source: §6.1 · pp. 12–13
• The reduction introduces auxiliary predicates that encode exactly-k relations as collections of function-like predicates, with a compensating factor of (k!)^|∆|.The construction preserves weighted counts because extensions differ only by permutations and have equal weights.Source: §6.1 · pp. 12–13

6.1.1 An Illustration: Counting K-Regular Graphs

• For 2-regular graphs, the method produces counts 1, 3, 12, 70, 465, 3507, 30016, and 286884 for 3 through 10 vertices.The count for 10 vertices is obtained by dividing the MC-function by 2^|∆|, yielding 286884.Source: §6.1.1 · p. 14
• The construction adapts to k-regular graphs for general k, although the encoding complexity grows with k.The paper notes that counting k-regular graphs is nontrivial and references prior work for k = 2, 3, 4, 5.Source: §6.1.1 · p. 14

6.2 The General Case

• WFOMC for FO2 sentences containing any finite number of counting quantifiers ∃=k1, …, ∃=km is domain-liftable.The general proof reduces these sentences to the constraint forms established earlier, using auxiliary predicates and polynomial-time WFOMC for FO2 with cardinality constraints.Source: §6.2 · pp. 14–15
• Arbitrary FO2 sentences with ∃=k are handled by replacing each counting subformula with a fresh unary predicate and a two-variable definition.The resulting formula remains in FO2, has domain-independent size, and depends on the domain through cardinality constraints whose k values grow polynomially with the domain size.Source: §6.2 · p. 17

7 The Two-Variable Fragment with Counting

• WFOMC is domain-liftable for the two-variable fragment of first-order logic with counting quantifiers.The proof reduces the full quantifier set to the already established ∃=k case.Source: §7 · p. 17
• Each subformula ∃≤ky : ψ(x,y) is rewritten as a disjunction of ∀y : ¬ψ(x,y) and exact-count cases from 1 through k.The transformation preserves FO2 and has size independent of the domain size.Source: §7 · p. 17
• Each lower-bound subformula ∃≥ky : ψ(x,y) is rewritten as ¬(∃≤k−1y : ψ(x,y)), reducing it to the handled upper-bound case.This avoids a disjunction whose number of terms would grow with the domain size.Source: §7 · p. 17

8 Related Work

• The work directly extends established domain-liftability of FO2 by allowing counting quantifiers.The paper builds technically on results from [Van den Broeck, Meert, and Darwiche, 2014].Source: §8 · p. 18
• The FO2-with-counting class and the S2FO2 and S2RU classes of Kazemi et al. [2016] are incomparable.The paper suggests that the respective techniques could be combined in future work.Source: §8 · p. 18
• Kuusisto and Lutz [2018] established domain-liftability for FO2 with at most one functionality constraint and suggested a route to counting quantifiers through multiple functionality constraints.The present paper supplies the missing details and uses reductions that do not directly rely on functionality constraints.Source: §8 · p. 18
• The paper’s methods resemble generating-function techniques from enumerative combinatorics, a connection left for future investigation.The authors specifically mention plans to study this relationship more closely.Source: §8 · p. 18

9 Conclusions

• FO2 with counting quantifiers is domain-liftable, significantly broadening WFOMC problems solvable in polynomial time.The authors identify practical efficiency of lifted algorithms after reduction as an important direction for future work.Source: §9 · p. 18

A Computing Weighted Model-Counting Functions Using DFT

• The appendix presents a discrete Fourier transform approach for computing weighted model-counting functions from WFOMC queries.The method computes the Fourier transform using polynomially many WFOMC oracle calls and then applies the inverse transform.Source: A Computing Weighted Model-Counting… · p. 19, §A.2 · pp. 19–20

A.1 Discrete Fourier Transform

• The appendix defines multidimensional DFTs over bounded integer grids determined by predicate arities and domain size.For predicate Ri, the grid bound is Mi = |∆|^arity(Ri).Source: §A.1 · p. 19, §A.2 · pp. 19–20

A.2 Computing Weighted Model-Counting Functions Using DFT

• The DFT method avoids adding explicit cardinality constraints or modifying the original formulas and predicate list.It instead changes weights by complex Fourier factors before querying the WFOMC oracle.Source: §A.2 · p. 20

B Omitted Proofs

• The appendix includes omitted proofs and additional technical material supporting the main results.The paper separately notes that complex-number representation issues are discussed in earlier work.Source: B Omitted Proofs · p. 20, §A.2 · p. 20

B.1 Proof of Proposition 1

• The number of bits needed to represent the interpolating polynomial’s coefficients grows polynomially with the bits needed to encode (x_i, y_i).This establishes the required polynomial representation bound.Source: §B.1 · p. 21

B.2 Proof of Proposition 2

• The WFOMC is a weighted sum over only polynomially many distinct possible-world weights.The weights are indexed by vectors in D, whose coordinates are bounded by predicate relation sizes.Source: §B.2 · pp. 21–22
• Each summand can be represented as a fraction whose numerator and denominator use polynomially many bits in |∆| and log M.The full WFOMC is the sum of |D| such fractions, with |D| polynomial in |∆|.Source: §B.2 · p. 22

C.1 Counting Anti-Involutive Functions

• The anti-involutive-function example illustrates that the Section 6.1 techniques encode a more complex case without much additional complexity.The later, more general techniques may trade computational speed for generality.Source: §C.1 · p. 22
• The approach computes anti-involutive functions by replacing counting-quantifier constraints with first-order sentences and cardinality constraints, then selecting MC-function values with |f| = |M| = m.The resulting counts use the diagonal MCΨ,Γ,∆(m, m), divided by the normalization factor described in the passage.Source: §C.1 · p. 23
• For n = 5 and n = 10, the figures show the MC-function alongside the resulting numbers of anti-involutive functions.The left panels show the MC-functions, while the right panels show counts from domains of sizes m and fixed codomain sizes n.Source: §C.1 · p. 23, Figure 4 · p. 23, Figure 5 · p. 23
• The MC-function is zero beyond the edge count of the complete undirected graph because the constraint forbids both directed edges between a pair of vertices.Thus, the cardinality of relation f cannot exceed the number of edges in that graph.Source: §C.1 · p. 23
• The computed results agree with the explicit formula derived by Kuusisto and Lutz [2018].The authors use this agreement as a sanity check.Source: §C.1 · p. 24
• Using an alternative transformation would preserve polynomial-time counting but could increase the polynomial exponent.The example motivates investigating more efficient transformations for particular cases.Source: §C.1 · p. 24