Threshold counting for decomposable representations

A smooth decomposable DAG has unions on a common scope and binary products on disjoint scopes. Leaves have at most one assignment. Its denotations satisfy the usual local semantics; a decreasing rank rules out cycles. Unions need not be disjoint, and different branches may use different partitions.

An occurrence in an accepting certificate supplies an outside context. Substituting any assignment accepted by that node preserves acceptance at the root. Thus a node and all its contexts form a rectangle. Descending a certificate to the cardinality threshold charges at most (K - 1)^2 inputs to a union edge and (K - 1)^3 to a product node.

The certificate-context rectangle construction is standard in the DNNF literature; see Bova, Capelli, Mengel and Slivovsky, IJCAI 2016. The threshold estimate here does not require deterministic unions or a single tree of coordinate partitions.

inductive Complexity.Frontier.DecomposableGate (N : Type u_1) : Type u_1

The three node types of a smooth decomposable representation.

• leaf {N : Type u_1} : DecomposableGate N
• union {N : Type u_1} (children : Finset N) : DecomposableGate N
• product {N : Type u_1} (left right : N) : DecomposableGate N

structure Complexity.Frontier.Decomposable (ι : Type u_1) (U : Type u_2) (N : Type u_3) : Type (max (max u_1 u_2) u_3)

A finite acyclic union/product representation, with its local denotational semantics. Literal leaves and constants satisfy leaf_small; arbitrary predicates are not free leaves. Finiteness of the node type is needed only for the size bound.

• scope : N → Set ι

  The coordinates each node is about.

• root : N

  The root node, whose scope is everything.

• scope_root : self.scope self.root = Set.univ
• gate : N → DecomposableGate N

  The gate at each node: a leaf, a union of children, or a product of two.

• rank : N → ℕ

  A rank that decreases from each node to its children.

• values (v : N) : Set (↑(self.scope v) → U)

  The partial inputs each node accepts, on its scope.

• leaf_small (v : N) : self.gate v = DecomposableGate.leaf → (self.values v).ncard ≤ 1
• union_scope (v : N) (c : Finset N) : self.gate v = DecomposableGate.union c → ∀ u ∈ c, self.scope u = self.scope v
• union_rank (v : N) (c : Finset N) : self.gate v = DecomposableGate.union c → ∀ u ∈ c, self.rank u < self.rank v
• union_values (v : N) (c : Finset N) : self.gate v = DecomposableGate.union c → ∀ (x : ι → U), (self.scope v).domRestrict x ∈ self.values v ↔ ∃ u ∈ c, (self.scope u).domRestrict x ∈ self.values u
• product_scope (v l r : N) : self.gate v = DecomposableGate.product l r → self.scope v = self.scope l ∪ self.scope r
• product_disjoint (v l r : N) : self.gate v = DecomposableGate.product l r → Disjoint (self.scope l) (self.scope r)
• product_rank (v l r : N) : self.gate v = DecomposableGate.product l r → self.rank l < self.rank v ∧ self.rank r < self.rank v
• product_values (v l r : N) : self.gate v = DecomposableGate.product l r → ∀ (x : ι → U), (self.scope v).domRestrict x ∈ self.values v ↔ (self.scope l).domRestrict x ∈ self.values l ∧ (self.scope r).domRestrict x ∈ self.values r

def Complexity.Frontier.Decomposable.accepts {ι : Type u_1} {U : Type u_2} {N : Type u_3} (P : Decomposable ι U N) (v : N) : Set (ι → U)

Acceptance by a node, viewed on full inputs.

Equations

• P.accepts v = {x : ι → U | (P.scope v).domRestrict x ∈ P.values v}

def Complexity.Frontier.Decomposable.accepted {ι : Type u_1} {U : Type u_2} {N : Type u_3} (P : Decomposable ι U N) : Set (ι → U)

The set represented by the root.

Equations

• P.accepted = P.accepts P.root

theorem Complexity.Frontier.Decomposable.accepts_congr {ι : Type u_1} {U : Type u_2} {N : Type u_3} (P : Decomposable ι U N) {v : N} {x y : ι → U} (h : Set.EqOn x y (P.scope v)) : x ∈ P.accepts v ↔ y ∈ P.accepts v

inductive Complexity.Frontier.Decomposable.Occurs {ι : Type u_1} {U : Type u_2} {N : Type u_3} (P : Decomposable ι U N) (x : ι → U) : N → Prop

A node occurs on an accepting certificate for x. At a union, any accepting child can be selected. At a product, both children occur.

• root {ι : Type u_1} {U : Type u_2} {N : Type u_3} {P : Decomposable ι U N} {x : ι → U} : x ∈ P.accepted → P.Occurs x P.root
• union {ι : Type u_1} {U : Type u_2} {N : Type u_3} {P : Decomposable ι U N} {x : ι → U} {v u : N} {c : Finset N} : P.Occurs x v → P.gate v = DecomposableGate.union c → u ∈ c → x ∈ P.accepts u → P.Occurs x u
• left {ι : Type u_1} {U : Type u_2} {N : Type u_3} {P : Decomposable ι U N} {x : ι → U} {v l r : N} : P.Occurs x v → P.gate v = DecomposableGate.product l r → P.Occurs x l
• right {ι : Type u_1} {U : Type u_2} {N : Type u_3} {P : Decomposable ι U N} {x : ι → U} {v l r : N} : P.Occurs x v → P.gate v = DecomposableGate.product l r → P.Occurs x r

theorem Complexity.Frontier.Decomposable.Occurs.accepts {ι : Type u_1} {U : Type u_2} {N : Type u_3} (P : Decomposable ι U N) {x : ι → U} {v : N} (h : P.Occurs x v) : x ∈ P.accepts v

theorem Complexity.Frontier.Decomposable.Occurs.substitute {ι : Type u_1} {U : Type u_2} {N : Type u_3} (P : Decomposable ι U N) {x : ι → U} {v : N} (h : P.Occurs x v) {y : ι → U} (hy : y ∈ P.accepts v) (hout : Set.EqOn y x (P.scope v)ᶜ) : y ∈ P.accepted

The substitution property follows from the syntax and decomposability.

def Complexity.Frontier.Decomposable.contexts {ι : Type u_1} {U : Type u_2} {N : Type u_3} (P : Decomposable ι U N) (v : N) : Set (↑(P.scope v)ᶜ → U)

Outside assignments supplied by accepting certificates through a node.

Equations

• P.contexts v = (P.scope v)ᶜ.domRestrict '' {x : ι → U | P.Occurs x v}

theorem Complexity.Frontier.Decomposable.rectangle_subset {ι : Type u_1} {U : Type u_2} {N : Type u_3} (P : Decomposable ι U N) (v : N) : rectangle (P.scope v) (P.values v) (P.contexts v) ⊆ P.accepted

theorem Complexity.Frontier.Decomposable.contexts_small {ι : Type u_1} {U : Type u_2} {N : Type u_3} (P : Decomposable ι U N) {K : ℕ} (hS : RectangleFree P.accepted K) {v : N} (hv : K ≤ (P.values v).ncard) : (P.contexts v).ncard ≤ K - 1

def Complexity.Frontier.Decomposable.stops {ι : Type u_1} {U : Type u_2} {N : Type u_3} (P : Decomposable ι U N) (K : ℕ) (v : N) : Set (ι → U)

Inputs for which threshold descent can stop at this node.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.Frontier.Decomposable.exists_stop {ι : Type u_1} {U : Type u_2} {N : Type u_3} (P : Decomposable ι U N) [Finite ι] [Finite U] {K : ℕ} (hK : 1 < K) (hS : K ≤ P.accepted.ncard) {x : ι → U} (hx : x ∈ P.accepted) : ∃ (v : N), x ∈ P.stops K v

Every accepted input has a stopping node. Rank makes the descent finite even with sharing.

def Complexity.Frontier.Decomposable.budget {ι : Type u_1} {U : Type u_2} {N : Type u_3} (P : Decomposable ι U N) (K : ℕ) (v : N) : ℕ

The local threshold budget of a node.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.Frontier.Decomposable.ncard_stops_le {ι : Type u_1} {U : Type u_2} {N : Type u_3} (P : Decomposable ι U N) [Finite ι] [Finite U] {K : ℕ} (hS : RectangleFree P.accepted K) (v : N) : (P.stops K v).ncard ≤ P.budget K v

def Complexity.Frontier.Decomposable.unionEdges {ι : Type u_1} {U : Type u_2} {N : Type u_3} (P : Decomposable ι U N) [Fintype N] : ℕ

Count outgoing union edges, including shared children once for each parent.

Equations

• P.unionEdges = ∑ v : N, match P.gate v with | Complexity.Frontier.DecomposableGate.union c => c.card | x => 0

def Complexity.Frontier.Decomposable.products {ι : Type u_1} {U : Type u_2} {N : Type u_3} (P : Decomposable ι U N) [Fintype N] : ℕ

Count binary product nodes.

Equations

• P.products = ∑ v : N, match P.gate v with | Complexity.Frontier.DecomposableGate.product left right => 1 | x => 0

theorem Complexity.Frontier.Decomposable.ncard_le {ι : Type u_1} {U : Type u_2} {N : Type u_3} (P : Decomposable ι U N) [Finite ι] [Finite U] {K : ℕ} [Fintype N] (hK : 1 < K) (hS : K ≤ P.accepted.ncard) (hrect : RectangleFree P.accepted K) : P.accepted.ncard ≤ (K - 1) ^ 2 * P.unionEdges + (K - 1) ^ 3 * P.products

Decomposable threshold counting. The denotation of a smooth decomposable DAG cannot be both large and rectangle-free unless the DAG has many nodes or edges.

theorem Complexity.Frontier.Decomposable.ncard_le_size {ι : Type u_1} {U : Type u_2} {N : Type u_3} (P : Decomposable ι U N) [Finite ι] [Finite U] {K : ℕ} [Fintype N] (hK : 1 < K) (hS : K ≤ P.accepted.ncard) (hrect : RectangleFree P.accepted K) : P.accepted.ncard ≤ (K - 1) ^ 3 * (P.unionEdges + P.products)

A simpler bound charging the same cubic budget to each union edge or product node.