Faster Lifting for Ordered Domains with Predecessor Relations

Evaluation

• Figure 1 compares Incremental2 with Incremental [15] and Recursive [13] on immediate and second predecessor relations.The supplied caption identifies the algorithms and predecessor cases but does not provide numerical cell values.Source: Figure 1 · p. 1

Motivation

• Existing predecessor encodings are theoretically tractable but practically inefficient because they rely on complex counting and cardinality extensions.The prior approach omitted experiments on second predecessors because it barely scaled beyond domain size 4.Source: §1 · p. 1

Contribution

• Treating predecessor relations as native axiom components lets the proposed algorithm scale to hundreds of domain elements for immediate and second predecessors.The method generalizes the IncrementalWFOMC algorithm using dynamic programming.Source: §1 · p. 2

Generalization

• The algorithm extends to cyclic and general k-th predecessors and proves FO2 tractability for the general k-th predecessor relation.The general relation can encode bounded-height grids, including grid-based inference tasks such as the two-dimensional Ising model.Source: §1 · p. 2

Evaluation

• Lifted inference experiments achieve speedups of a full order of magnitude, while most combinatorics problems are solved within one second.The comparison covers prior lifted-inference benchmarks and permutation problems.Source: §1 · p. 2

Tractability background

• WFOMC tractability is known for FO2 but may fail when a linear order is directly encoded because transitivity requires three variables.This motivates using a non-logical linear order axiom.Source: §2 · p. 2

Linear order axiom

• The linear order axiom enforces ordering outside the first-order sentence, but prior findings did not directly support predecessor relations.Related work explored additional axioms and sharper boundaries between FO2 and FO3.Source: §2 · p. 2

Predecessor relations

• Earlier methods derived immediate and second predecessors through complex syntactic manipulations, preserving theoretical tractability but causing practical inefficiency.A later linear-order algorithm improved efficiency without removing the derivation bottleneck.Source: §2 · p. 2

3.1 Fist-Order Logic

• The paper uses finite-domain, function-free first-order logic with formulas, atoms, literals, sentences, ground formulas, Herbrand worlds, and models defined over a finite domain.A sentence has all variables bound, while a ground formula has no variables.Source: §3.1 · p. 2

3.2 Weighted First-Order Model Counting

• WFOMC computes the weighted sum of satisfying models using predicate-specific positive and negative weights, and domain-liftability means polynomial data complexity in domain size.The paper focuses on fixed sentences and weights while varying the domain size.Source: §3.2 · pp. 2–3

3.3 A Domain-Lifted Algorithm

• IncrementalWFOMC partitions domain elements into cells, tracks cell configurations, and computes weighted counts by dynamic programming.The final count sums T_n(k) over configurations whose entries sum to n, yielding polynomial complexity.Source: §3.3 · p. 3
• IncrementalWFOMC obtains the WFOMC by summing T_n(k) over all configurations with |k| = n, establishing polynomial-time computation in the domain size.The approach also extends to C2 with counting quantifiers and cardinality constraints.Source: §3.3 · p. 3

3.4 Linear order axiom

• The linear order axiom imposes a total order externally, because expressing transitivity directly requires three logical variables beyond FO2.Prior work transforms FO2 sentences with the axiom into computation over an ordered domain and establishes domain-liftability.Source: §3.4 · pp. 3–4

3.5 Predecessor Relations

• Predecessor relations extend the linear order axiom with Pred1 through Predk, but direct first-order encodings are unsupported by IncrementalWFOMC.Prior Pred1 and Pred2 encodings used counting quantifiers and cardinality constraints; general k-th predecessors remained open.Source: §3.5 · p. 4
• Prior work proved FO2 liftability with immediate and second predecessors while warning that counting-based encodings may not scale in practice.The counting quantifiers preserve polynomial-time complexity but can hinder practical scalability.Source: §3.5 · p. 4

• IncrementalWFOMC2 natively supports the immediate predecessor relation and has better time complexity than IncrementalWFOMC.Source: §4 · p. 4
• The dynamic-programming update records the previous element’s cell so each new element is constrained to have its immediate predecessor.The update therefore retains only the predecessor information needed to enforce Pred1.Source: §4 · p. 4
• The method distinguishes weights for nonadjacent pairs from weights for consecutive pairs linked by Pred1.The additional consecutive-pair weight captures the immediate predecessor relation during updates.Source: §4 · p. 4
• The resulting WFOMC is obtained by summing the final dynamic-programming states and multiplying by n!.Source: §4 · p. 4
• The state expansion increases records from n^p to p · n^p, improving on the O(n^c · p) complexity of the counting-quantifier encoding.Source: §4 · p. 4

• The cyclic predecessor relation makes the last element the predecessor of the first element.Source: §5 · p. 4
• The encoding introduces First and Last predicates to identify the endpoints of the ordered domain.Source: §5 · p. 4
• CirPred is encoded using Pred1 together with a Last–First disjunct.Source: §5 · p. 4

• The algorithm maintains predecessor-specific cell assignments while aggregating the updated table entries into the final WFOMC.Source: §1 · p. 5
• IncrementalWFOMC2 initializes table entries for cell configurations and iteratively updates them for elements 2 through n.Source: §1 · p. 5
• Each update processes predecessor cells that already exist and multiplies the current weight by the corresponding relation weight.Source: §1 · p. 5
• Cyclic predecessor handling records the first element’s assignment and modifies the update rule to account for endpoint wraparound.Source: §1 · p. 5
• For cyclic predecessor relations, the added complexity is only a factor of p, the number of cells.Source: §1 · p. 5

• IncrementalWFOMC2 maintains the cell assignments of the last k elements to update states for general predecessor relations.Source: §6 · p. 5
• The algorithm updates only predecessor relations that already exist in the current ordered prefix.Source: §6 · p. 5
• The general method has complexity O(p^(k+1) · n^p), where p is the number of cells.Source: §6 · p. 6
• The two-variable fragment with the general linear-order axiom and predecessor relations is domain-liftable.Source: §6 · p. 6
• Even when predecessor relations are inconsecutive, complexity remains O(p^(k+1) · n^p) using the highest predecessor order k.Source: §6 · p. 6

7 Experiments

• The experiments evaluate IncrementalWFOMC2 against IncrementalWFOMC [15] and RecursiveWFOMC on shared lifted-inference settings.All experiments used a machine with four Intel Xeon Gold 5218 CPUs and 512GB of RAM.Source: §7 · p. 6

7.1 Watts-Strogatz Model

• IncrementalWFOMC2 completes Watts-Strogatz computations within a few seconds at domain size 500, whereas both baselines fail to scale beyond a dozen elements.The comparison uses the same cyclic-predecessor encoding for the baseline algorithms.Source: §7.1 · p. 6, §7 · p. 6

7.2 Combinatorics Math Problems

• Nearly all combinatorics problems finish within 100 seconds, with most solved within 1 second; RecursiveWFOMC solves about half and IncrementalWFOMC only a few.The benchmark contains 28 selected MATH dataset problems involving linear-order, immediate, or cyclic predecessor relations.Source: §7.2 · p. 6

7.3 Hidden Markov Model with High-Order Dependencies

• IncrementalWFOMC2 shows clear subexponential runtime growth with domain size on a hidden Markov model using first-, second-, and third-predecessor relations.The model represents high-order dependencies through weighted auxiliary formulas and predecessor relations.Source: §7.3 · p. 7
• On the reduced weather2 model, IncrementalWFOMC2 improves runtime by a full order of magnitude over IncrementalWFOMC and RecursiveWFOMC.The reduced comparison removes the second- and third-predecessor components because the baselines cannot support them or scale for the second predecessor.Source: §7.3 · p. 7

8 Conclusion

• IncrementalWFOMC2 natively supports immediate and cyclic predecessor relations and extends to general k-th predecessor relations.The extension proves that the FO2 fragment with the general linear-order axiom is domain-liftable.Source: §8 · p. 7
• Extensive experiments on lifted-inference and combinatorics problems demonstrate significant performance improvement over state-of-the-art algorithms.The paper identifies sitting-arrangement problems in computational economics [2] as a future application.Source: §8 · p. 7

A Encoding of A Grid with General Predecessor Relations

• Immediate predecessors encode vertical adjacency, while k-th predecessors encode horizontal adjacency in a k × n grid.The encoding uses auxiliary boundary predicates for the left, right, top, and bottom edges.Source: A Encoding of A Grid with General… · p. 9, Figure 4 · p. 9
• First and last ordered elements seed the bottom and top boundaries, which are propagated through k-th predecessor relations.Cardinality constraints enforce exactly n elements in the top and bottom rows.Source: A Encoding of A Grid with General… · p. 9
• Vertical adjacency is defined by immediate predecessor pairs that exclude top and bottom boundary elements.The relation is written as V(x,y) iff x is not top, y is not bottom, and Pred1(x,y).Source: A Encoding of A Grid with General… · p. 9
• Horizontal adjacency is defined by k-th predecessor pairs that exclude the left and right boundaries.The relation is written as H(x,y) iff y is not left, x is not right, and Predk(x,y).Source: A Encoding of A Grid with General… · p. 9
• All grid formulas remain in FO2, and bounded grid height yields polynomial-time WFOMC in the domain size.The stated polynomial-time result assumes the height k is bounded by a constant.Source: A Encoding of A Grid with General… · p. 9

B Proof of Theorem 2

• Any FO2 sentence with the general linear-order axiom is transformed into a formula using the order and predecessor predicates.The resulting WFOMC is evaluated over a domain of size n under weighting functions.Source: B Proof of Theorem 2 · p. 9
• The dynamic-programming state stores cell partitions and predecessor-related configurations whose weighted model sums are updated incrementally.The proof identifies the state value with the weighted sum of models under standard order and predecessor interpretations.Source: B Proof of Theorem 2 · pp. 9–10
• The recurrence is correct because the conjuncts introduced when extending a partition are independent of one another and of the preceding ground formula.This independence directly yields the update from T_h to T_{h+1}.Source: B Proof of Theorem 2 · pp. 9–10
• The algorithm runs in O(p^(k+1) · n^p), which is polynomial in n when the number of cells p and predecessor order k are constants.The complexity follows from an outer loop over n, cell enumeration, and state transitions over predecessor configurations.Source: B Proof of Theorem 2 · p. 10