PaperlayerView exact revision on arXiv

Source-linked AI summary

Symmetric Weighted First-Order Model Counting

Paul Beame, Guy Van den Broeck, Eric Gribkoff, Dan Suciu

arXiv:1412.1505v3cs.DBcs.AIcs.CCcs.LO

TL;DR

The paper analyzes symmetric first-order and weighted model counting, motivated by probabilistic inference in large knowledge bases and MLNs. It develops complexity results for data and combined settings, including hardness, tractability, and decision-problem boundaries. The main results give #P1-complete data-complexity cases, polynomial time for γ-acyclic queries, and #P-completeness for combined FOk counting when k ≥ 2.

  • Problem

    The paper asks how difficult symmetric FOMC and WFOMC are, motivated by probabilistic inference with soft constraints in large knowledge bases and MLNs.

    Source: §1 · pp. 1–2

  • Method

    It analyzes data and combined complexity using reductions between MLNs and symmetric WFOMC, universal #P1-machine simulation, and fixed-vocabulary first-order reductions.

    Source: §1 · p. 2, §3.3 · p. 7

  • Results

    Data complexity is #P1-complete for an FO3 FOMC instance and a conjunctive-query WFOMC instance, polynomial for γ-acyclic queries, and combined FOk complexity is #P-complete for every k ≥ 2.

    Source: §3.1 · p. 5, §3.2 · p. 6, §3.3 · p. 7

  • Takeaways & Limitations

    Symmetry does not guarantee tractability: it permits polynomial-time evaluation for γ-acyclic queries but still supports hard counting problems and complete combined complexity.

    Source: §5 · p. 11

    The paper leaves the complexity of several FOMC and WFOMC queries open, as summarized in its list of open problems.

    Source: §5 · p. 11

Abstract

from arXiv · show

The FO Model Counting problem (FOMC) is the following: given a sentence $\Phi$ in FO and a number $n$, compute the number of models of $\Phi$ over a domain of size $n$; the Weighted variant (WFOMC) generalizes the problem by associating a weight to each tuple and defining the weight of a model to be the product of weights of its tuples. In this paper we study the complexity of the symmetric WFOMC, where all tuples of a given relation have the same weight. Our motivation comes from an important application, inference in Knowledge Bases with soft constraints, like Markov Logic Networks, but the problem is also of independent theoretical interest. We study both the data complexity, and the combined complexity of FOMC and WFOMC. For the data complexity we prove the existence of an FO$^{3}$ formula for which FOMC is #P$_1$-complete, and the existence of a Conjunctive Query for which WFOMC is #P$_1$-complete. We also prove that all $\gamma$-acyclic queries have polynomial time data complexity. For the combined complexity, we prove that, for every fragment FO$^{k}$, $k\geq 2$, the combined complexity of FOMC (or WFOMC) is #P-complete.

1. INTRODUCTION

The paper studies symmetric FOMC and WFOMC, motivated by probabilistic inference in large knowledge bases and Markov Logic Networks, and establishes sharp complexity boundaries for data and combined complexity.

1. INTRODUCTION

  • Probabilistic inference in large knowledge bases is formulated as weighted model counting, where WFOMC sums products of tuple weights over satisfying structures.The paper connects this formulation to systems containing millions or billions of uncertain tuples.Source: §1 · p. 1
  • Symmetric WFOMC assigns one common weight to all tuples of each relation, with FOMC recovered when all weights equal 1.This setting models symmetric probabilistic structures and arises naturally in MLNs.Source: §1 · pp. 1–2
  • An MLN can be reduced to symmetric WFOMC by replacing each soft constraint with a hard constraint and a new relation whose tuples have weight 1/(w−1).The reduction preserves the ratio between contributions when a constraint is false or true and is independent of the finite domain.Source: §1 · p. 2

Results on Data Complexity

  • The data-complexity boundary occurs between FO2 and FO3: FO2 is tractable, whereas an FO3 sentence yields #P1-hard FOMC.The input is only the unary-encoded domain size n, motivating the #P1 complexity class.Source: Results on Data Complexity · pp. 2–3
  • The data-complexity results establish #P1-hardness for FOMC on an FO sentence and for WFOMC on a conjunctive query, while γ-acyclic conjunctive queries are tractable.The associated decision problem for the hard conjunctive-query instance remains trivial because every conjunctive query has a model over domains of size at least 1.Source: Results on Data Complexity · p. 3

Results on the Combined Complexity

  • For combined complexity, FOMC for every FOk with k ≥ 2 is #P-complete, using Scott’s reduction for membership and Boolean-formula model counting for hardness.The vocabulary is fixed; allowing it as input would make even FO0 encode arbitrary Boolean formulas.Source: Results on the Combined Complexity · p. 3

The Associated Decision Problem

  • The associated combined decision problem is NP-complete for FO2 and PSPACE-complete for unrestricted FO.For FO2, this settles the complexity using the exponential finite-model bound and the NEXPTIME-completeness of finite satisfiability.Source: The Associated Decision Problem · pp. 3–4

2. BACKGROUND

The background defines weighted model counting through Boolean formulas and first-order lineages, then specializes it to symmetric tuple weights. It also distinguishes data from combined complexity and records assumptions about weights, probabilities, and computational representations.

Weighted Model Counting

  • Weighted Model Counting assigns weights to Boolean variables and sums the products of true and false literal weights over satisfying assignments; ordinary model counting is the special case with all weights equal to 1.Source: §2 · p. 4

Probabilities and Complexity

  • The framework covers model probabilities through normalized weighted counts and includes both data complexity, where the formula is fixed, and combined complexity, where the formula and domain size are inputs.Source: §2 · p. 4

Weighted First-Order Model Counting

  • WFOMC represents an FO sentence as a Boolean lineage over ground tuples and evaluates its weighted model count using tuple weights and complementary weights.Source: §2 · p. 4

Symmetric WFOMC

  • Symmetric WFOMC constrains each tuple’s weight to depend only on its relation name, extending fixed relation-level weights uniformly across every domain size.Source: §2 · p. 4

Weights and Representation

  • The paper permits arbitrary, including negative, weights and assumes rational inputs with polynomially representable counts; polynomial interpolation shows the complexity is unchanged between positive and arbitrary weights.Source: §2 · pp. 4–5

3. DATA COMPLEXITY

The data-complexity results establish lower and upper bounds for symmetric WFOMC through computational encodings in FO³ and polynomial-time algorithms for γ-acyclic queries. They develop model-counting correspondences and structural recurrences for the analyzed query families.

3.1 Lower Bounds

  • An FO3 sentence has #P1-complete FOMC, so the FO2 polynomial-time WFOMC result cannot extend to FOk for k > 2 unless #P1 is in PTIME.Van den Broeck et al. [37] established polynomial-time data complexity for every FO2 formula.Source: §3.1 · p. 5
  • Symmetric WFOMC is #P1-hard for a positive clause without equality and, dually, for a conjunctive query, ruling out tractability for all CQs.The reduction applies quantifier elimination, negation elimination, equality removal, inclusion-exclusion, and query duplication; the transformations preserve WFOMC using signed weights.Source: §3.1 · pp. 5–6

3.2 Upper Bounds

  • Symmetric WFOMC for γ-acyclic conjunctive queries without self-joins is in PTIME, but γ-acyclicity does not characterize tractability.The query cγ is γ-cyclic yet has PTIME data complexity because its shared variable z acts as a separator.Source: §3.2 · p. 6
  • The tractability boundary remains open: typed cycles are believed hard, β-cyclic queries yield reductions from typed cycles, and α-acyclicity is as hard as arbitrary self-join-free CQs.The paper also leaves open a complete characterization of tractable conjunctive queries without self-joins.Source: §3.2 · pp. 6–7
  • The symmetric WFOMC problem is in PTIME for the query QS4 under standard semantics, using dynamic programming beyond existing lifted-inference rules.Earlier PTIME results for QS4 assumed a bipartite-graph semantics; the paper extends the proof to standard semantics.Source: §3.2 · p. 7

3.3 Proofs

  • A linear-time universal #P1 counting machine U1 yields, via Lemma 3.9’s construction, an FO3 formula Φ satisfying f(n) = FOMC(Φ, n)/(n!).U1 has a unary input alphabet, runs in linear time, and computes a #P1-hard function; for runtime O(n^a), Lemma 3.9 gives k = 3a, so a = 1 yields FO3.Source: §3.3 · p. 7
  • FOMC(Θ1, n) equals the number of accepting computations on input n multiplied by n!, accounting for domain orderings.The construction uses c epochs and c tape regions, each with n steps or cells, while modifying transitions using only three variables.Source: §3.3 · p. 8
  • γ-acyclic query probabilities are computable in polynomial time by repeatedly applying graph-reduction rules and maintaining polynomial-bit intermediate results.The rules eliminate isolated variables, singleton or empty edges, duplicate edges, and edge-equivalent variables; the combined complexity of acyclic queries remains open.Source: §3.3 · p. 9
  • For fixed chain length m, recursively eliminating isolated variables and singleton relations computes the query probability in polynomial time in n, but combined complexity in n and m is open.The recurrence updates relation probabilities and restricts successive variable domains according to the number of satisfying elements.Source: §3.3 · p. 9
  • For Qn1n2, every model satisfies exactly one of Pa or Pb, enabling the weighted model count to decompose as f(n1, n2) + g(n1, n2).The exclusivity follows from a finite alternating sequence contradiction, and removing the k elements satisfying Pa yields a recurrence on n1−k.Source: §3.3 · pp. 9–10

4. COMBINED COMPLEXITY

The combined complexity studies FOMC and WFOMC when both the formula and domain size are inputs, proving #P-completeness for every FO^k fragment with k≥2. The proof combines a #P membership argument based on Scott’s reduction with a #SAT reduction encoded through constrained graph structures.

Complexity bounds

  • For every fixed k≥2, combined FOMC is #P-complete, and the #P-membership argument also applies to WFOMC.The vocabulary is fixed while Φ and n are inputs; the corresponding decision problem has NP-completeness for FO2 and PSPACE-completeness for full FO.Source: §4 · p. 10

Upper bound

  • Scott’s reduction replaces a formula with an equivalent linear-size prenex conjunction whose corresponding models preserve weights.The transformed formula has bounded quantifier depth, yielding a lineage of size O(n^ks) and placing WFOMC in #P.Source: §4 · p. 10

Lower bound

  • A #SAT instance is encoded by an FO2 sentence whose models contain a unique A-to-B path and optional C-originating S-edges representing Boolean variables.The construction uses a fixed vocabulary and enforces a path of length n while excluding alternative path lengths; each satisfying assignment corresponds to (n+1)! models.Source: §4 · pp. 10–11

Open problems

  • The combined-complexity section also records a table of formulas whose FOMC hardness remains conjectural.These open cases are separate from the established FO^k hardness result for k≥2.Source: Table 2 · p. 11

Lower bound

  • The graph constraints force a unique permutation of the domain, leaving only S(c0,ci) tuples unspecified and putting them in one-to-one correspondence with the variables of F.This establishes FOMC(ϕF,n+1)=(n+1)!·#F.Source: Figure 2 · p. 10, §4 · p. 11

Decision complexity

  • Replacing Boolean variables with ternary S-tuples over the distinguished A and B elements extends the construction from SAT to QBF.This yields NP-complete spectra for FO2 and PSPACE-complete spectra for unrestricted FO.Source: §4 · pp. 10–11

5. CONCLUSIONS

The paper studies symmetric WFOMC for probabilistic inference in Markov Logic Networks and large knowledge bases, while also establishing independent complexity-theoretic results. It proves hardness for data and combined complexity and polynomial-time solvability for γ-acyclic conjunctive queries, while leaving further cases open.

Main results

  • The paper proves #P1-hardness for an FO sentence under FOMC and for a conjunctive query under symmetric WFOMC.It also establishes polynomial-time WFOMC for γ-acyclic conjunctive queries and #P-completeness for FO2 in combined complexity.Source: §5 · p. 11

Motivation

  • Symmetric WFOMC is motivated by probabilistic inference in Markov Logic Networks and applications to modern large knowledge bases.The paper treats the problem as both practically motivated and independently theoretically significant.Source: §5 · p. 11

Open problems

  • The paper ends with open problems consisting of formulas for which FOMC hardness is conjectured but unresolved.Thus, the reported complexity classification does not cover every listed formula.Source: §5 · p. 11

A.1 Proof of Lemma 3.3: Removing Exists

The proof removes existential quantifiers from weighted model-counting formulas by adding a fresh relation with unit and negative weights. Good worlds preserve the original count, while bad worlds cancel in pairs.

Quantifier elimination

  • The construction replaces the first existential quantifier in prenex Φ with a universal condition using a fresh relational symbol A.A records which assignments satisfy the remaining quantified subformula.Source: §A.1 · p. 13

Weight preservation

  • Good worlds have the same weight as their projections onto the original vocabulary because A receives weight 1.Their total contribution is exactly WFOMC(Φ,n,w,¯w).Source: §A.1 · p. 13

Cancellation

  • Bad worlds cancel pairwise when the status of A(a) is flipped, since the two worlds have opposite weights from A’s −1 weight.This proves equality between the original and transformed WFOMC values.Source: §A.1 · p. 13

A.2 Proof of Lemma 3.4: Removing Negation

The proof removes negated subformulas by replacing them with fresh relations and enforcing consistency through an auxiliary relation with negative weight. Invalid worlds then cancel pairwise.

Negation elimination

  • A negated subformula ¬ψ(x) is replaced by a fresh relation A(x), while auxiliary relation B(x) and constraints enforce the intended complement behavior.A and B are assigned weights that support cancellation without changing the original WFOMC value.Source: §A.2 · p. 13

Cancellation

  • Good worlds project to worlds of the original formula with equal weight, whereas bad worlds cancel because B(a) can be toggled freely with opposite weights.Repeating this process establishes the lemma for all negated subformulas.Source: §A.2 · p. 13

A.3 Proof of Lemma 3.5: Removing Equality

The proof removes equality by replacing it with a weighted predicate and recovering the desired coefficient through finite differences. The coefficient of degree n equals the original WFOMC value.

A.3 Proof of Lemma 3.5: Removing Equality

  • Replacing equality with E yields a polynomial f(z) of degree n^2 whose monomials all have degree at least n.The lower-degree bound follows because the transformed sentence asserts ∀xE(x,x).Source: §A.3 · p. 13
  • The coefficient of z^n in f(z) equals WFOMC(Φ, n, w, ¯w), because exactly n E-tuples force E to represent equality.Source: §A.3 · p. 13
  • Finite differences with step δ recover this coefficient using n + 1 evaluations of f.The construction defines successive differences by ∆k+1f(z) = (∆kf)(z + δ) − (∆kf)(z).Source: §A.3 · p. 13

B. A #P1-HARD SENTENCE Θ1

The sentence Θ1 encodes accepting computations of a linear-time, multi-tape counting Turing machine over a unary input. The construction adapts the encoding to multiple tapes, bounded epochs and regions, and FO3.

B. A #P1-HARD SENTENCE Θ1

  • Θ1 reduces a linear-time, multi-tape counting Turing machine with unary input to first-order model counting.The target machine can be a #P1-complete counting machine.Source: B. A #P1-HARD SENTENCE Θ1 · p. 13
  • The resulting sentence belongs to FO3 while encoding the machine computation needed for the hardness reduction.Source: B. A #P1-HARD SENTENCE Θ1 · p. 13
  • The construction uses c epochs of n steps and c regions of n cells to represent runtimes and spaces of length c·n on domains of size n.Source: B. A #P1-HARD SENTENCE Θ1 · p. 13

B.1 Signature

The signature of Θ1 represents an ordered domain together with machine states, head positions, tape contents, movement, and unchanged-cell information.

B.1 Signature

  • The signature includes a strict order, successor relation, and predicates identifying the minimum and maximum domain elements.Source: §B.1 · pp. 13–14
  • State predicates encode the machine state at each time and epoch, while head predicates encode tape-head positions within regions.Source: §B.1 · p. 14
  • Tape, movement, and frame predicates encode symbols, relative head movement, and cells unchanged between consecutive steps.Source: §B.1 · p. 14

B.2 Sentences

The sentences of Θ1 enforce a valid ordered domain, well-formed machine configurations, transition behavior, and acceptance. For each fixed domain order, models correspond one-to-one with accepting computations.

B.2 Sentences

  • The axioms make < a strict linear order and define Min, Max, and Succ relative to that order.Source: §B.2 · p. 14
  • Configuration axioms require exactly one state at each time, exactly one head position per tape, and exactly one symbol at each tape position.Source: §B.2 · p. 14
  • Initial-configuration axioms place the machine in q1 with specified heads and unary input followed by zeros.Source: §B.2 · p. 14
  • Transition axioms encode machine updates within epochs and across epoch boundaries, while preserving unaffected tape cells and other heads.Source: §B.2 · pp. 14–15
  • Movement and frame predicates are defined explicitly, and the machine is required to terminate in an accepting state.Source: §B.2 · p. 15
  • Θ1 uses at most three logical variables per sentence, so the construction lies in FO3.Source: §B.2 · p. 15
  • For a fixed domain order, Θ1-models correspond one-to-one to accepting computations, and dividing by the n! possible orders recovers the computation count.Source: §B.2 · p. 15

C. PTIME DATA COMPLEXITY FOR FO2

The proof establishes polynomial-time data complexity for FO2 by reducing formulas to universally quantified sentences with unary and binary relations, then exploiting symmetry and independence. The resulting probability depends only on cell cardinalities and constant-time local probabilities.

Reduction

  • FO2 formulas are reduced to equivalent universally quantified formulas whose relational symbols have arity at most two and whose quantifier-free core is ψ(x, y).The reduction combines Scott’s reduction, an arity-lowering transformation, and existential-quantifier elimination; zero-arity symbols are handled by Shannon expansion.Source: C. PTIME DATA COMPLEXITY FOR FO2 · p. 15

Binary case

  • For purely binary formulas, events associated with distinct unordered pairs of domain elements are independent because they depend on disjoint ground tuples.This independence would fail when unary atoms share elements across assignments.Source: C. PTIME DATA COMPLEXITY FOR FO2 · pp. 15–16
  • By symmetry, p1 = Pr(ψ(a, b)) is independent of a, b and p2 = Pr(ψ(c, c)) is independent of c, both computable in O(1), and Pr(ϕ) = Pr(ϕ∗) = p(F) = p^n(n−1)/2.Source: C. PTIME DATA COMPLEXITY FOR FO2 · p. 16

Illustrations

  • Concrete examples show that restricted formulas can be evaluated by brute force after substituting cell-specific unary truth values into the remaining binary formulas.The examples define probabilities such as rij, sℓ, and tℓ for representative assignments and use them in the factorized expression.Source: C. PTIME DATA COMPLEXITY FOR FO2 · p. 16

Unary and binary case

  • With unary and binary relations, domain elements are partitioned into 2^m unary types, and the formula is split according to the cells containing x and y.Unary predicates become fixed truth values within each cell, leaving formulas involving only binary predicates.Source: C. PTIME DATA COMPLEXITY FOR FO2 · p. 16
  • The resulting events are independent across distinct cell pairs, so their probabilities factor using cell cardinalities and constant-time probabilities for the induced binary formulas.Symmetry ensures the expression depends only on n1, ..., n2^m, not on the identities of the cells; summing over partitions yields the polynomial-time computation.Source: C. PTIME DATA COMPLEXITY FOR FO2 · p. 16
Loading 1412.1505v3…