Threshold counting for decomposable DAGs

A smooth decomposable DAG (DecomposableDAG) represents a set of inputs ι → U by nodes of three kinds, each about a set of coordinates, its scope, and accepting a set of assignments of its scope:

• a leaf accepts at most one assignment, as a literal or a constant does;
• a union accepts what one of its children accepts, and each child has its scope (smoothness);
• a product of two children accepts what both accept, and their scopes split its scope into two disjoint parts (decomposability).

The root has every coordinate in its scope, and a rank decreasing from each node to its children makes the DAG acyclic. Nodes may be shared, unions need not be disjoint (the DAG need not be deterministic), and different branches may split the coordinates in different ways. Over the alphabet Bool with literal leaves, these are the smooth DNNFs of knowledge compilation [Dar01].

Certificates and rectangles. A node occurs on an accepting certificate of an input x (DecomposableDAG.Occurs) when it is the root and accepts x, a child of an occurring union that accepts x, or a child of an occurring product. If a node occurs for x, then replacing the part of x on its scope by any assignment that the node accepts keeps the input accepted (DecomposableDAG.Occurs.mem_accepted). So the assignments accepted by a node and its contexts, the parts outside its scope of the inputs for which it occurs, form a rectangle inside the accepted set (DecomposableDAG.rectangle_subset) [BCMS16].

Threshold counting. Let the accepted set be K-rectangle-free with at least K elements. Descend along a certificate of an accepted input x, from the root, to the lowest node v that accepts at least K assignments, so that the children of v on the certificate accept fewer. By rectangle-freeness v has fewer than K contexts. If v is a union, then x is determined by a child accepting it, its part on that child, and its context; if v is a product, by its parts on both children and its context. So each union edge is charged at most (K - 1) ^ 2 inputs and each product at most (K - 1) ^ 3 (DecomposableDAG.ncard_accepted_le):

|accepted| ≤ (K - 1) ^ 2 · #(union edges) + (K - 1) ^ 3 · #(products).

For dense rectangle-free sets with small thresholds, every smooth decomposable DAG is therefore exponentially large.

Main definitions

• Cslib.Circuits.DecomposableDAG: a smooth decomposable DAG.
• Cslib.Circuits.DecomposableDAG.accepted: the set it represents.
• Cslib.Circuits.DecomposableDAG.Occurs: the nodes on accepting certificates.
• Cslib.Circuits.DecomposableDAG.unionEdges, DecomposableDAG.products, DecomposableDAG.size: the size of a DAG.

Main results

• Cslib.Circuits.DecomposableDAG.rectangle_subset: a node and its contexts form a rectangle inside the accepted set.
• Cslib.Circuits.DecomposableDAG.ncard_accepted_le: threshold counting.
• Cslib.Circuits.DecomposableDAG.ncard_accepted_le_size: threshold counting, charging (K - 1) ^ 3 to every union edge and every product.

References

• A. Darwiche, Decomposable negation normal form
• S. Bova, F. Capelli, S. Mengel, F. Slivovsky, Knowledge compilation meets communication complexity

inductive Cslib.Circuits.DecomposableDAG.Gate (N : Type u_3) : Type u_3

The gate at a node of a decomposable DAG on the nodes N.

• leaf {N : Type u_3} : Gate N

  A leaf, accepting at most one assignment of its scope.

• union {N : Type u_3} (children : Finset N) : Gate N

  A union of finitely many children.

• product {N : Type u_3} (left right : N) : Gate N

  A product of two children.

structure Cslib.Circuits.DecomposableDAG (ι : Type u_3) (U : Type u_4) (N : Type u_5) : Type (max (max u_3 u_4) u_5)

A smooth decomposable DAG on the nodes N, representing a set of inputs ι → U. Each node has a scope, a set of coordinates, and accepts a set of assignments of its scope. The gate at a node is a leaf, accepting at most one assignment; a union of children, each with the scope of the node, accepting what one of them accepts; or a product of two children whose scopes split the scope of the node into two disjoint parts, accepting what both accept. The root has every coordinate in its scope, and a rank decreasing from each node to its children makes the DAG acyclic.

• scope : N → Set ι

  The coordinates that a node is about.

• root : N

  The root.

• scope_root : self.scope self.root = Set.univ

  The root is about every coordinate.

• gate : N → Gate N

  The gate at a node.

• rank : N → ℕ

  A rank that decreases from each node to its children.

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

  The assignments of its scope that a node accepts.

• values_subsingleton (v : N) : self.gate v = Gate.leaf → (self.values v).Subsingleton

  A leaf accepts at most one assignment.

• scope_union (v : N) (c : Finset N) : self.gate v = Gate.union c → ∀ u ∈ c, self.scope u = self.scope v

  The children of a union have its scope (smoothness).

• rank_union (v : N) (c : Finset N) : self.gate v = Gate.union c → ∀ u ∈ c, self.rank u < self.rank v

  The children of a union have lower rank.

• values_union (v : N) (c : Finset N) : self.gate v = Gate.union c → ∀ (x : ι → U), (self.scope v).domRestrict x ∈ self.values v ↔ ∃ u ∈ c, (self.scope u).domRestrict x ∈ self.values u

  A union accepts what one of its children accepts.

• scope_product (v l r : N) : self.gate v = Gate.product l r → self.scope v = self.scope l ∪ self.scope r

  The scope of a product is the union of the scopes of its children.

• disjoint_product (v l r : N) : self.gate v = Gate.product l r → Disjoint (self.scope l) (self.scope r)

  The scopes of the children of a product are disjoint (decomposability).

• rank_product (v l r : N) : self.gate v = Gate.product l r → self.rank l < self.rank v ∧ self.rank r < self.rank v

  The children of a product have lower rank.

• values_product (v l r : N) : self.gate v = Gate.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

  A product accepts what both of its children accept.

def Cslib.Circuits.DecomposableDAG.accepts {ι : Type u_1} {U : Type u_2} {N : Type u_3} (P : DecomposableDAG ι U N) (v : N) : Set (ι → U)

The inputs accepted by a node: those whose part on its scope it accepts.

def Cslib.Circuits.DecomposableDAG.accepted {ι : Type u_1} {U : Type u_2} {N : Type u_3} (P : DecomposableDAG ι U N) : Set (ι → U)

The set represented by the DAG: the inputs accepted by the root.

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

Certificates and rectangles

inductive Cslib.Circuits.DecomposableDAG.Occurs {ι : Type u_1} {U : Type u_2} {N : Type u_3} (P : DecomposableDAG ι U N) (x : ι → U) : N → Prop

A node occurs on an accepting certificate of the input x.

• root {ι : Type u_1} {U : Type u_2} {N : Type u_3} {P : DecomposableDAG ι U N} {x : ι → U} : x ∈ P.accepted → P.Occurs x P.root

  The root occurs when it accepts x.

• union {ι : Type u_1} {U : Type u_2} {N : Type u_3} {P : DecomposableDAG ι U N} {x : ι → U} {v u : N} {c : Finset N} : P.Occurs x v → P.gate v = Gate.union c → u ∈ c → x ∈ P.accepts u → P.Occurs x u

  A child of an occurring union occurs when it accepts x.

• left {ι : Type u_1} {U : Type u_2} {N : Type u_3} {P : DecomposableDAG ι U N} {x : ι → U} {v l r : N} : P.Occurs x v → P.gate v = Gate.product l r → P.Occurs x l

  The left child of an occurring product occurs.

• right {ι : Type u_1} {U : Type u_2} {N : Type u_3} {P : DecomposableDAG ι U N} {x : ι → U} {v l r : N} : P.Occurs x v → P.gate v = Gate.product l r → P.Occurs x r

  The right child of an occurring product occurs.

theorem Cslib.Circuits.DecomposableDAG.Occurs.accepts {ι : Type u_1} {U : Type u_2} {N : Type u_3} {P : DecomposableDAG ι U N} {x : ι → U} {v : N} (h : P.Occurs x v) : x ∈ P.accepts v

A node occurring for x accepts x.

theorem Cslib.Circuits.DecomposableDAG.Occurs.mem_accepted {ι : Type u_1} {U : Type u_2} {N : Type u_3} {P : DecomposableDAG ι 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

Substitution. If a node occurs for x, then any input that the node accepts and that agrees with x outside the scope of the node is accepted.

def Cslib.Circuits.DecomposableDAG.contexts {ι : Type u_1} {U : Type u_2} {N : Type u_3} (P : DecomposableDAG ι U N) (v : N) : Set (↑(P.scope v)ᶜ → U)

The contexts of a node: the parts outside its scope of the inputs for which it occurs.

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

A node and its contexts form a rectangle inside the accepted set.

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

A node accepting at least K assignments has fewer than K contexts, when the accepted set is K-rectangle-free.

Threshold counting

def Cslib.Circuits.DecomposableDAG.stops {ι : Type u_1} {U : Type u_2} {N : Type u_3} (P : DecomposableDAG ι U N) (K : ℕ) (v : N) : Set (ι → U)

The inputs for which the descent to the threshold K stops at the node v: the node occurs for the input and accepts at least K assignments, while the children of v through which the input is accepted accept fewer.

def Cslib.Circuits.DecomposableDAG.budget {ι : Type u_1} {U : Type u_2} {N : Type u_3} (P : DecomposableDAG ι U N) (K : ℕ) (v : N) : ℕ

The threshold budget of a node: (K - 1) ^ 2 for each child of a union and (K - 1) ^ 3 for a product.

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

The descent stops. If the accepted set has at least K > 1 elements, the descent from the root along a certificate of an accepted input stops at some node. The rank makes the descent finite, even with shared nodes.

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

The charge at a node. If the accepted set is K-rectangle-free, the descent stops at a node v for at most the budget of v inputs.

def Cslib.Circuits.DecomposableDAG.unionEdges {ι : Type u_1} {U : Type u_2} {N : Type u_3} (P : DecomposableDAG ι U N) [Fintype N] : ℕ

The number of union edges: the children of each union, a shared child being counted once for each of its parents.

def Cslib.Circuits.DecomposableDAG.products {ι : Type u_1} {U : Type u_2} {N : Type u_3} (P : DecomposableDAG ι U N) [Fintype N] : ℕ

The number of products.

def Cslib.Circuits.DecomposableDAG.size {ι : Type u_1} {U : Type u_2} {N : Type u_3} (P : DecomposableDAG ι U N) [Fintype N] : ℕ

The size of the DAG: its union edges and its products. Leaves are free.

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

Threshold counting for decomposable DAGs. If the set represented by a smooth decomposable DAG is K-rectangle-free and has at least K elements, then

|accepted| ≤ (K - 1) ^ 2 · #(union edges) + (K - 1) ^ 3 · #(products).

Unions need not be disjoint, and different branches may split the coordinates differently.

theorem Cslib.Circuits.DecomposableDAG.ncard_accepted_le_size {ι : Type u_1} {U : Type u_2} {K : ℕ} {N : Type u_3} (P : DecomposableDAG ι U N) [Finite ι] [Finite U] [Fintype N] (hrect : Frontier.RectangleFree P.accepted K) (hS : K ≤ P.accepted.ncard) : P.accepted.ncard ≤ (K - 1) ^ 3 * P.size

Threshold counting by size. If the set represented by a smooth decomposable DAG is K-rectangle-free and has at least K elements, then |accepted| ≤ (K - 1) ^ 3 · size.