Lifted Inference with Linear Order Axiom

• WFOMC supports probabilistic inference in statistical relational learning and other applications, including conjecturing recursive formulas in enumerative combinatorics.Source: §1 · p. 1
• FO2 WFOMC is computable in time polynomial in domain size, whereas FO3 WFOMC is #P1-complete in general [Beame et al., 2015].Source: §1 · p. 1
• Prior work established domain-liftability for several FO2 extensions, including counting quantifiers and the tree axiom [Kuˇzelka, 2021; van Bremen and Kuˇzelka, 2021b].Source: §1 · pp. 1–2
• A linear order axiom forces a predicate to define a total ordering of domain elements, but this constraint is inexpressible using only two variables.Source: §1 · p. 2
• The paper introduces a dynamic programming algorithm showing that C2 with a linear order remains domain-liftable, with running time polynomial in domain size.Source: §1 · p. 2
• The authors also apply the result to exact inference in a Markov Logic Network on a random graph model related to Watts–Strogatz graphs.Source: §1 · p. 2

2.1 First-Order Logic

• The paper assumes finite-domain, function-free first-order logic with at most two variables and restricts FO2 sentences to be constant-free.Source: §2.1 · p. 3

2.2 Weighted Model Counting and Lifted Formulation

• WFOMC computes the weighted sum of models of a relational formula over a domain of size n using predicate-level positive and negative weights.Source: §2.2 · p. 3

2.3 Cells and Domain-Liftability of the Two-Variable Fragment

• A cell is a maximally consistent set of one-variable literals, and assigning domain elements to cells decomposes conditioned WFOMC into independent symmetric parts.Source: §2.3 · p. 4
• The FO2 cell-based formulation is domain-liftable because its multinomial expression can be evaluated in time polynomial in n, with skolemization extending the result beyond universal FO2.Source: §2.3 · p. 5

2.4 Cardinality Constraints and Counting Quantifiers

• Counting quantifiers generalize existential quantification, while cardinality constraints specify bounds or exact counts of predicate atoms; C2 is domain-liftable via reduction to FO2 with cardinality constraints.Source: §2.4 · p. 5

2.5 Linear Order Axiom

• A linear-order axiom requires a designated predicate to satisfy the linear-order axioms, so models can be viewed as sequences whose elements may be divided into ordered regions.Source: §2.5 · pp. 5–6
• Transitivity is problematic because it requires three variables; the algorithm therefore handles the order specially while restricting valid cells using the remaining reflexivity condition.Source: §2.5 · p. 5
• The order predicate is treated as a structural constraint with positive and negative weights fixed to one, and the paper denotes the constraint by Linear(R).Source: §2.5 · pp. 5–6

3.1 New Algorithm

• IncrementalWFOMC enlarges the domain one element at a time, storing weighted counts for possible p-vectors in tables reused at the next size.Theorem 1 states that it computes WFOMC for universally quantified FO2 sentences in prenex normal form in polynomial time in n.Source: §3 · p. 6, §3.1 · pp. 7, 9

3.2 Enforcing a Linear Order

• For a fixed ordered domain, the algorithm modifies rij so extensions retain only worlds satisfying the order, preserving polynomial-time WFOMC computation.Symmetry over domain permutations lets the full result be obtained from one ordering by multiplying by n!.Source: §3.2 · pp. 10–11
• FO2 extended by a linear order axiom is domain-liftable, using skolemization, fixed-order computation, and multiplication by n!.The overall computation remains polynomial in the domain size.Source: §3.2 · p. 11

A Worked Example of IncrementalWFOMC

• The worked example tracks a three-way head, middle, and tail split, yielding T2[(1, 1, 0)] = w1w2(r12 + r21) and an explicit T3 entry.The example constructs valid cells and applies the incremental table updates while leaving most weights symbolic.Source: A Worked Example of IncrementalWFOMC · pp. 12–13
• The worked example obtains WFOMC for one ordering and multiplies by n!; with unit weights, the combinatorial check gives 10 sequence splits.The value for ordering 1 ≤ 2 ≤ 3 is multiplied by n! = 6, while the unit-weight calculation confirms 10 splits.Source: A Worked Example of IncrementalWFOMC · p. 14

3.3 Domain-Liftability of C2 with Linear Order

• C2 with a linear order axiom is domain-liftable because its WFOMC reduces to FO2 with cardinality constraints and uses the new polynomial-time oracle.Theorem 5 states that C2 extended by a linear order axiom is domain-liftable; its proof is omitted as a near-restatement of prior work.Source: §3.3 · pp. 14–15

Predecessor Relation

• With a linear-order-enforcing ≤, theory ΨPred uses auxiliary Perm to encode Pred, correctly defines immediate predecessors for n ≥ 2, and has exactly n! models.Source: Predecessor Relation · pp. 15–16

Predecessor of the Predecessor

• The encoding uses two permutation cycles and alternating node colors, correctly defines the immediate predecessor-of-immediate-predecessor relation for every n ≥ 4, and has exactly 2n! models.Because the coloring sequence can start with either red or blue, the weighted model count is divided by 2.Source: Predecessor of the Predecessor · pp. 17–18
• Extending the order axiom with Pred and Pred2 preserves polynomial-time WFOMC for arbitrary C2 sentences, while generalization to the k-th predecessor remains unproven.The Pred2 result follows by reducing to ΨPred2 and dividing by 2; the authors describe the encoding as theoretically interesting but of little practical interest.Source: Predecessor of the Predecessor · p. 19

4 Experiments

• The implementation processes counting constraints by explicitly computing symbolic polynomials in one algorithm run rather than using repeated WFOMC calls and interpolation.Nemo.jl is used for polynomial representation and manipulation.Source: §4 · pp. 19–20

4.1 Inference in Markov Logic Networks

• IncrementalWFOMC supports exact lifted probabilistic inference for Markov Logic Networks using C2 with a linear order axiom.The implementation is evaluated on a random graph model similar to Watts and Strogatz.Source: §4.1 · p. 20

Our Model

• The graph model starts with a cyclic chain, adds m random shortcut edges, and uses a weighted rule encouraging friends of smokers to smoke.Hard constraints define the graph structure, while the smoking rule is the sole soft constraint.Source: Our Model · p. 21

Inference

• Inference queries the probability of exactly k smokers rather than an individual’s smoking probability, which is identical for every domain member.The model is reduced to WFOMC before answering the query.Source: Inference · p. 22
• Compared with a random graph having the same number of edges, the proposed model increasingly favors extreme smoker counts as the weight grows.For smaller weights both models approach the binomial distribution, while the proposed model more strongly prefers nobody or everybody smoking.Source: Inference · p. 22

5 Conclusion

• WFOMC for C2 extended with a linear order axiom can be computed in time polynomial in the domain size.This establishes domain-liftability for the extended language.Source: §5 · p. 22
• The computation is performed by the new IncrementalWFOMC algorithm.Source: §5 · p. 22

Appendix A Performance Measurements

• The measurements include head-and-tail examples, head-middle-tail examples, and formulas that count possible predecessor relations.The predecessor experiment enumerates n! domain orderings.Source: Appendix A · p. 26
• Watts–Strogatz-like inference timings are averaged over m values and use symbolic weights to obtain the full smoker-count distribution in one call.Polynomial coefficients correspond to unnormalized probabilities for each smoker count.Source: Appendix A · p. 26
• Figure 4 reports execution times for several IncrementalWFOMC problems averaged over multiple executions.Experiments used a single thread on an AMD EPYC 7742 system with 512 GB of RAM.Source: Figure 4 · p. 26, Appendix A · p. 26