A Strongly Exponential Separation of DNNFs from CNF Formulas

Decomposable Negation Normal Forms (DNNFs) are Boolean circuits in negation normal form where the subcircuits leading into each AND gate are defined on disjoint sets of variables. We prove a strongly exponential lower bound on the size of DNNFs for a class of CNF formulas built from expander graphs. As a corollary, we obtain a strongly exponential separation between DNNFs and CNF formulas in prime implicates form. This settles an open problem in the area of knowledge compilation (Darwiche and Marquis, 2002).


Introduction
The aim of knowledge compilation is to succinctly represent propositional knowledge bases in a format that allows for answering a number of queries in polynomial time [DM02]. Choosing a representation language generally involves a trade-off between succinctness and the range of queries that can be efficiently answered. For instance, CNF formulas are more succinct than prime implicate formulas (PIs), but the latter representation enjoys clause entailment checks in polynomial time whereas CNF formulas in general do not, unless P = NP [GKPS95,CM78]. The need to balance the competing requirements of succinctness and tractability has led to the introduction of a large variety of representation languages that strike this balance in different ways.
Decomposable Negation Normal Forms (DNNFs) are a restricted form of Boolean circuits in negation normal form (NNF) such that the subcircuits leading into an AND gate are defined on disjoint sets of variables. DNNFs are among the most succinct representation languages considered in knowledge compilation-for instance, they include variants of binary decision diagrams such as ordered binary decision diagrams (OBDDs) and even free binary decision diagrams (FBDDs, also known as read-once branching programs) as special cases. In spite of their expressive power, they still support clause entailment queries and satisfiability testing in linear time, both of which are of critical importance in practice.
In this paper, we study the relative succinctness of DNNFs and CNF formulas. On the one hand, DNNFs are known to be exponentially more succinct than CNF formulas in some cases [GKPS95]; on the other hand, it was known that CNFs do not have polynomial DNNF representations unless the polynomial hierarchy collapses [SK96,CDLS02]. The main contribution of this paper is in improving this conditional, superpolynomial lower bound to an unconditional, exponential lower bound (Theorem 5): There is a class C of CNFs such that the DNNF size of each F ∈ C is 2 Ω(size(F )) .
We prove this result by combining the combinatorial properties of expander graphs with recently developed techniques for proving lower bounds on the size of non-deterministic read-once branching programs for CNF formulas [Raz14b]. In addition to resolving an open problem by Darwiche and Marquis [DM02], our lower bound has several other implications (cf. Appendix 7): • The formulas used to prove Theorem 5 are PIs, so it immediately follows that PIs can be exponentially more succinct than DNNFs (Corollary 3). Again, this answers an open question by Darwiche and Marquis [DM02].
Related Work. To the best of our knowledge, ours is the first unconditional lower bound for general DNNFs. However, there is a rich literature on lower bounds for more restricted representation languages, such as OBDDs or FBDDs [Weg00,Juk12]. Moreover, certain subclasses of DNNFs, so-called decision-DNNFs, have been recently considered in database theory in the context of probabilistic databases. In this setting, lower bounds are obtained by a quasipolynomial simulation of decision-DNNFs by FBDDs in combination with known exponential lower bounds for FBDDs [BLRS13,BLRS14]. Pipatsrisawat and Darwiche have proposed a framework for showing lower bounds on structured DNNFs [PD10], a subclass of DNNFs in which the variables respect a common tree-ordering.
The formulas used to prove Theorem 5 are based on expander graphs and were originally introduced to establish an exponential lower bound for the OBDD size of CNFs [BS14]. The present paper leverages a recent result by Razgon [Raz14b,Theorem 4] to lift this lower bound to DNNFs; indeed, we even generalize such result, at the same time providing a significantly shorter proof based on a new combinatorial result (Theorem 3) which may be of independent interest.

Preliminaries
For every integer n ≥ 1, we let [n] denote the set {1, . . . , n}. Let X be a countable set of elements, called variables, and call the elements of {0, 1} constants. A literal is a variable in X (a positive literal) or the negation, ¬, of a variable in X (a negative literal). For a literal l ∈ {x, ¬x} for some x ∈ X, we let var(l) = x. An atom is a literal or a constant. An assignment is a function from a subset of X to the constants. We equivalently view an assignment f as {¬x : f (x) = 0} ∪ {x : f (x) = 1}; so, as a set of atoms, an assignment does not contain the constant 0 nor a pair of complementary literals.
Negation Normal Forms (NNFs). A Negation Normal Form (NNF) C on a finite set of variables vars(C) ⊆ X (also known as a De Morgan circuit ) is a node labelled directed acyclic graph (DAG), whose labelled nodes and arcs are respectively called the gates and wires of C. A NNF C has a designated sink (outdegree 0) node, referred to as the output gate of the circuit, and denoted by output(C). The source nodes of C (indegree 0), denoted by inputs(C), are referred to as the input gates of C and are labelled by a constant or a literal in {x, ¬x : x ∈ vars(C)}. The non source nodes of D, referred as internal gates, are labelled by ∧ or ∨. The label of a node v is denoted by label(v), and a node v is also called a label(v)-gate. We let atoms(C) = {label(v) : v ∈ inputs(C)}. In this paper, the size of C, in symbols size(C), is the number of wires in C.
Let G be a DAG and let v be a node in G. The subgraph of G sinked at v is the DAG whose node set is and whose arcs are exactly the arcs of G among the nodes in V ′ . Let C be an NNF, and let v be a node in the DAG G underlying C. We let sub(C, v) denote the subcircuit of C sinked at v, that is, the NNF on variables vars(C) whose underlying DAG is the subgraph of C sinked at v, with the same labels and designated sink v.
Let C be an NNF, v be a gate in C, and f be an assignment of vars(C). The value of sub(C, v) under f , in symbols sub(C, v)(f ), is defined inductively on the structure of sub(C, v) as follows: • if v is a 0-gate or an ∨-gate having fanin 0, then sub(C, v)(f ) = 0; • if v is a 1-gate or a ∧-gate having fanin 0, then sub(C, v)(f ) = 1; The value of C under f , in symbols C(f ), is equal to sub(C, output(C))(f ). We let sat(C) denote the set of all satisfying assignments (or models) of C, that is, assignments f : vars(C) → {0, 1} such that C(f ) = 1. Let C be an NNF on variables vars(C). We say that C computes the (Boolean) function F : ; moreover, C is said trivial if it computes the identically 0 (or 1) function. Two NNFs C and C ′ are equivalent if they compute the same function; in particular, vars(C) = vars(C ′ ).
Let C be an NNF. A certificate of C (sometimes also called proof tree) is an NNF T on variables vars(C) whose gates and wires are subsets of the gates and wires of C satisfying the following: output(C) = output(T ); if a gate v is in C ∩ T , and v is a ∧-gate in C with input wires from gates v 1 , . . . , v i , then the gates v 1 , . . . , v i and the wires (v 1 , v), . . . , and v is an ∨-gate in C with input wires from gates v 1 , . . . , v i , then exactly one gate w ∈ {v 1 , . . . , v i } is in T and the wire (w, v) is in T v (i ≥ 0). We let cert(C) denote the set of certificates of C.
The models and the certificates of an NNF are nicely related as follows.
Proposition 1. Let C be an NNF and let f be an assignment. The following are equivalent.
• There exists T ∈ cert(C) such that f ∈ sat(T ).
Proof. For the forward direction, let f ∈ sat(C). Call a wire (u, v) in the DAG underlying C activated by f if f satisfies the subcircuit of C sinked at u, in symbols sub(C, u)(f ) = 1. It is readily verified that there exists a certificate T for C containing only wires activated by f . Moreover, f ∈ sat(T ) because by construction sub(T, v)(f ) = 1 for all input gates v of T , and therefore sub(T, output(T ))(f ) = 1. For the backward direction, let T be a certificate of C such that f ∈ sat(T ). By induction on the structure of C, we prove that for all t ∈ T it holds that sub(T, t)(f ) = sub(C, t)(f ) = 1. Since output(C) = output(T ), we conclude that C(f ) = sub(C, output(C))(f ) = sub(T, output(T ))(f ) = 1.
If t is an input gate of T , then sub(T, t)(f ) = 1 because otherwise f does not satisfy T . We also have that t is an input gate of C, hence sub(C, t)(f ) = 1. Let t be a ∨-gate in T , with input wires from gates t 1 , . . . , t i in C; say without loss of generality that t 1 is chosen in T . By the induction hypothesis, sub(T, t 1 )(f ) = sub(C, t 1 )(f ) = 1; hence, sub(T, t)(f ) = sub(C, t)(f ) = 1. The case where t is a ∧-gate is similar.
Decomposable Negation Normal Forms (DNNFs). An NNF D is decomposable (in short, a DNNF ) if for all ∧-gates v with input wires from gates v 1 , . . . , v i and all j, j ′ ∈ [i], j = j ′ , the variable sets of the subcircuits of D sinked at v j and v j ′ are disjoint, in symbols, Conjunctive Normal Forms (CNFs). A conjunctive normal form (in short, CNF ) is a finite set of clauses, where a clause is a finite set of literals. Equivalently, we regard a CNF as an NNF where the maximum number of wires on a path from a input gate to the output gate is 2, and each ∨-gate has input wires only from input gates. A CNF F is monotone if its labels do not contain negative literals, a k-CNF if the fanin of ∨-gates is at most k, and a read k times CNF if, for every x ∈ vars(F ), the number of wires leaving nodes whose label contain the variable x is at most k.
Graphs. We refer to a standard reference for basic notions and facts in graph theory [Die05]. Let G = (V, E) be a graph.
For every S ⊆ V , we let N S,G denote the open neighbourhood of S in G, in symbols, (1) Note that a (c, d)-expander is connected; otherwise, if S is the vertex set of a (nonempty) connected component of G of minimum size, then 0 < |S| ≤ |V |/2 and 0 = |N S,G | ≥ c|S| > 0.
Theorem 1 (Section 9.2 in [AS00]). For all d ≥ 3, there exists c > 0 and a sequence of graphs If G has no isolated vertices, we view E as a CNF on the variables vars(E) = V (a trivial CNF, if E = ∅), which we call a graph CNF. Let E be a graph CNF with underlying graph G = (V, E). Note that the satisfying assignments of E correspond to vertex covers of G: If f is a satisfying assignment of E, then {x : f (x) = 1} is a vertex cover of G, and if C is a vertex cover of G, then any assignment f of vars(E) containing C satisfies E.

Vertex Covers
In this section, we establish upper and lower bounds on (certain) vertex covers in a maximum degree d graph, which will be essential in proving the main result.
Proposition 2. Let C be a vertex cover of a connected graph G of maximum degree d. Then, |V | d+1 ≤ |C|. Proof. Let C be a vertex cover of a connected graph G of maximum degree d. Then, V \ C is an independent set. Since G is connected, each vertex in V \ C is incident to at least one edge with a vertex in C. Hence, there are at least |V \ C| edges between C and V \ C. Since each vertex in C has degree at most d, and we are done.
We now prove a lemma that is a key technical ingredient for the proof of our main result.
Theorem 2. Let d ≥ 3, let G = (V, E) be a graph of maximum degree d, and let I be a family of subsets of V . If I covers the vertex covers of G, then The above statement has been already proved by Razgon [Raz14b, Theorem 4], but here we give a new and shorter proof.
Our proof relies on the following theorem. Let G = (V, E) be a graph and let S ⊆ V . We denote by Theorem 3. Let G = (V, E) be a graph, S ⊆ V , and s ∈ S. Then, We define a function f s : If e contains s, then e is covered by a vertex in N s ⊆ D. Otherwise, if e does not contain s, then e is covered by a vertex in C \ {s} ⊆ D.
We now prove that f s is injective, so that from which the statement follows.
Proof. Let G = (V, E) be a graph of degree d, and let S ⊆ V . By induction on |S| ≥ 0, we prove that The base case S = ∅ is trivial. Let S = {s 1 , . . . , s n , s n+1 } where n ≥ 0. By the induction hypothesis, and we are done.
If t = min{|S| : S ∈ I}, then by Theorem 1 we have that, for all S ∈ I, Using the previous inequality, we get and we are done.
In establishing [Raz14b, Theorem 4], Razgon essentially proves that , which is slightly improved by our Theorem 3. As a consequence, also the bound in Theorem 2 slightly improves the 1 d 2 +1 log 2 1 + 1 2 d+1 −1 dependence on the maximum degree d in [Raz14b,Theorem 4]. Finally we observe that the bound in Theorem 3 is tight. It is easy to see that the vertex covers of the star of the degree d and center c, that is the graph whose edge set is {{c, r 1 }, . . . , {c, r d }}, are exactly {r 1 , . . . , r d } and {c} ∪ S for all S ⊆ {r 1 , . . . , r d }; hence R d has exactly 1 + 2 d vertex covers and exactly 2 d vertex covers containing c. If the graph G is the disjoint union of some stars of degree d, and S contains the center of each star, then G has exactly (1 + 2 d ) |S| vertex covers and exactly 2 d|S| vertex covers containing S.

Nice DNNFs
In this section, we observe that a DNNF computing a graph CNFs is equivalent to a DNNF that is nice, in that its internal gates have fanin at most 2, and its input gates are labelled by positive literals (Corollary 2). We also observe that nice DNNFs have nice certificates, in the sense that their underlying graphs are rooted binary trees whose leaves are labelled by positive literals (Proposition 6).
Proposition 3. Let D be a DNNF. There exists a DNNF D ′ equivalent to D, having fanin 2, and such that size(D ′ ) ≤ 2 · size(D).
Proof. Let D be a DNNF. An NNF D ′ equivalent to D and having fanin 2 is obtained by editing D as follows, until no gate of fanin larger than 2 exists: Let v be a ∧-gate with input wires from gates v 1 , . . . , v i with i > 2; delete the wires (v j , v) for j ∈ {2, . . . , i}; create a fresh ∧-gate w, and the wires (w, v) and (v j , w) for j ∈ {2, . . . , i}. The case where v is an ∨-gate is similar.
It is readily verified that D ′ is decomposable. Moreover, each wire in D is processed at most once (when it is an input wire of a gate having fanin larger than 2) and it generates at most 2 wires in D ′ , hence the size of D ′ is at most twice the size of D.
. An NNF is called negation free if its labels do not contain negative literals. Proof. Suppose D contains a gate u labelled with literal ¬x. Let D ′ be the DNNF on vars(D) obtained from D by relabelling u with the constant 1. We claim that an assignment satisfies D if and only if it satisfies D ′ . Let f be a satisfying assignment of D. By Proposition 1 there is a certificate T of D such that f satisfies T . We obtain a certificate T ′ of D ′ by relabelling u with the constant 1 (if u appears in T ). It is straightforward to verify that f is a satisfying assignment of T ′ . We apply Proposition 1 once more to conclude that f must be a satisfying assignment of D ′ . For the converse, let f be a satisfying assignment of D ′ , and let T ′ be a certificate of D ′ such that f satisfies T ′ . If T ′ does not contain the gate u then T ′ is also a certificate of D, and f is a satisfying assignment of D by Proposition 1. Otherwise, we obtain a certificate T of D from T ′ by relabelling u with the literal ¬x. Let f ′ be the assignment such that f (y) = f ′ (y) for all y ∈ vars(D) \ {x}, and such that f ′ (x) = 0. Since D is decomposable and T contains the gate u labelled with ¬x, no node of T can be labelled with the literal x. Thus T ′ cannot contain such a gate either, and f ′ satisfies T ′ . Since ¬x evaluates to 1 under f ′ , the certificate T is satisfied by f ′ as well. By Proposition 1, the assignment f ′ is a satisfying assignment of D. Because the function computed by D is monotone, we conclude that f must satisfy D as well. Clearly D and D ′ have the same size and maximum fanin. It follows that the desired negation free DNNF can be obtained by replacing every negative literal by the constant 1 in the labels of D. Corollary 2. Let E be a graph CNF and let D be a DNNF equivalent to E. There exists a fanin 2, constant free, and negation free DNNF D ′ equivalent to D such that size(D ′ ) ≤ 2 · size(D).
Proof. Let E be a graph CNF and let D be a DNNF equivalent to E. By Proposition 3, there exists a DNNF D 1 , equivalent to D, having fanin 2 whose size is at most twice the size of D. Since E is a monotone Boolean function, by Proposition 4, there exists a fanin 2 and negation free DNNF D 2 , equivalent to D 1 , whose size is at most the size of D 1 . Since E is a non constant Boolean function, by Proposition 5, there exists a fanin 2, negation free, and constant free DNNF D 3 , equivalent to D 2 , whose size is at most the size of D 3 . Let D ′ = D 3 . Then, D ′ is a fanin 2, constant free, and negation free DNNF, equivalent to D, whose size is at most twice the size of D.
Proposition 6. Let D be a DNNF and let T ∈ cert(D).
• If D is constant free, then the underlying graph of T is a tree.
• If D is constant free and fanin 2, then the tree underlying T has maximum degree 3.
• If D is constant free and negation free, then atoms(T ) ⊆ X.
Proof. We prove the first item (the rest is clear). Assume that the underlying graph of T is cyclic, so that in the underlying DAG there exist two distinct nodes v and w in T and two arc disjoint directed paths from v to w; in particular, w has at least two ingoing arcs in T , hence by construction w is a ∧-gate in D. By decomposability, no variables occur as labels of input gates in sub(D, v), which is impossible since D is constant free.

DNNFs Models
In this section, we prove two lemmas to which we critically appeal in the proof of the main result.
The first lemma (Lemma 1) allows to derive, given a DNNF D and a gate v in D, a DNNF D ′ whose models are exactly the models of D minus those models that correspond (in the sense of Proposition 1) to certificates of D using the gate v.
Let D be a constant free DNNF and let v ∈ D \ {output(D)}. Let elimgate(D, v) denote the DNNF obtained from D as follows. Let paths(D, v) be the set of directed paths from v to output(D) in the DAG underlying D; display each P in paths(D, v) by (w 0 , w 1 , . . . , w p ), where w 0 = v, w p = output(D), and p ≥ 1.
If there exists P = (w 0 , w 1 , . . . , w p ) in paths(D, v) such that w j is an ∧-gate for every j ∈ [p] = {1, . . . , p}, then elimgate(D, v) is the DNNF formed by a single 0-gate (computing the constant 0). Otherwise, for every P = (w 0 , w 1 , . . . , w p ) in paths(D, v) there exists j ∈ [p] such that w j is an ∨-gate; let e P = (w j−1 , w j ) denote the wire in P such that j is the smallest index in [p] where w j is an ∨-gate. Then, elimgate(D, v) is obtained from D by deleting the wires {e P : P ∈ paths(D, v)} in D. The process might create 0-gates in the form of fanin-0 ∨-gates, and undesignated sinks. Proof. Let f be a satisfying assignment of D such that f does not satisfy any certificate T of D with v ∈ T . Let T be a certificate of D such that f satisfies T ; such a certificate exists by Proposition 1. Clearly, v ∈ T . We claim that all wires in T are kept in passing from D to elimgate(D, v); therefore, T is a certificate of elimgate (D, v), and since f satisfies T , by Proposition 1, it also holds that f satisfies elimgate(D, v).
We prove the claim. Assume for a contradiction that a wire (u ′ , u) of T is deleted in passing from D to elimgate(D, v). Then, by definition of elimgate(D, v), there is a path from v to u ′ whose nodes are all ∧-gates. Since (u ′ , u) is a wire of T and thus u ′ is a gate of T , we have, by definition of certificates, that v is in T , which is a contradiction.
Conversely, let f be a satisfying assignment of elimgate(D, v). By Proposition 1, there exists a certificate T of elimgate(D, v) such that f satisfies T ; then, T does not contain 0-gates. In particular, T does not contain 0-gates that arise, in passing from D to elimgate(D, v), as fanin-0 ∨-gates on some directed path in D from v to output(D). Therefore, every gate w ∈ T is either a ∧-gate in D, so that the gate itself and all its input wires are kept in elimgate(D, v) by construction, or is a ∨-gate in D for which at least one of its input wires is kept in elimgate(D, v), and is used by T . Hence, T is a certificate for D. The node v does not have a directed path to output(D) in elimgate(D, v), because at least one wire is deleted on each such path in passing from D to elimgate(D, v); hence, v ∈ T . Since f satisfies T , by Proposition 1, f satisfies D.
The second lemma (Lemma 2) essentially establishes that if the models of a DNNF D computing a graph CNF have to satisfy a clause {x, x ′ }, and for some gate v in D it is the case that an input gate labelled x has a directed path to v in the DAG underlying D but no input gate labelled x ′ has such a directed path to v, then all certificates of D using the gate v hit x or all certificates of D using the gate v hit x ′ .
First, we observe that x ∈ atoms(T ) \ atoms(sub(T, v)). Otherwise, assume that x ∈ atoms(T ) \ atoms(sub(T, v)), and let w be the gate of D lying in inputs(T ) \ inputs(sub(T, v)) labelled x. By hypothesis, x ∈ atoms(sub(D, v)). Let w ′ be the gate of D in inputs(sub (D, v)) labelled x. Then, it is possible to construct a certificate S for the constant free DNNF sub(D, v) such that the gate w ′ is an input gate of S, and therefore x ∈ atoms(S); the underlying graph of S is a tree by Proposition 6. Now, the tree R obtained by replacing in T the subtree rooted at v by S is a certificate of D; in R, there exists an internal gate u such that both w and w ′ have a directed path to u in R; hence, u has fanin at least 2, so that u is a ∧-gate in D, which contradicts the decomposability of D (at u by variable x).
Second, since atoms(sub(T ′ , v)) ⊆ atoms(sub(D, v)), and x ′ ∈ atoms(sub(D, v)) by hypothesis, it holds that x ′ ∈ atoms(sub(T ′ , v)). Therefore, Now, the tree S obtained by replacing in T the subtree rooted at v by the subtree rooted at v in T ′ is a certificate of D; moreover, {x, x ′ } ∩ atoms(S) = ∅, contradicting the hypothesis that all certificates of D have a nonempty intersection with {x, x ′ }.

Lower Bound
In this section we prove the main result, an exponential separation between CNFs and DNNFs (Theorem 5).
Outline. We provide an informal outline of the proof. We separate CNFs and DNNFs by a class of graph CNFs naturally corresponding to a family of expander graphs (Theorem 1). Without loss of generality, the DNNF size of a graph CNF can be measured on DNNFs having fanin 2 and not containing negations or constants (Corollary 2); in particular, input gates are variables (or equivalently vertices of the underlying graphs). Let E be a graph CNF whose underlying graph (V, E) is an expander, and let D be a DNNF equivalent to E. In view of an application of Theorem 2, we construct a family of subsets of V covering the set of satisfying assignments of E, as follows. In each step, we pick a gate in D, and then we edit D so as to remove all certificates through that gate. As long as D has certificates, it follows from Proposition 2 that it must have at least |V |/(d + 1) distinct variables (vertices) labelling its input gates. We find a gate v in D such that the variables occurring below v in D are at least |V |/(d + 1) and at most |V |/2 (Lemma 3, Claim 1); this is sufficient and necessary to appeal to the expansion of the graph underlying E, and find in such a graph a matching of size proportional in |V | between variables occurring below v in D and variables not occurring below v in D (Lemma 3, Claim 2). We then argue using Lemma 2 that there is an equally large subset of vertices covering the satisfying assignments corresponding (in the sense of Proposition 1) to certificates through v (Lemma 3, Claim 3). We now remove the certificates through v from D, by following every path from v to the output gate of D until we find a wire that leads to an ∨-gate, and by deleting this wire. By Lemma 1, performing these deletions eliminates a satisfying assignment of D if and only if it corresponds to a certificate through v. The iteration terminates once the resulting DNNF is unsatisfiable. At termination, we have found a family of substes of V , each of size proportional in |V |, that covers all satisfying assignments of E; by Theorem 2, this family has size exponential in |V |. Since there is a bijection between the substes of V in the family and a subset of gates in the original DNNF D, the latter must have exponential size in |V | as well.
Proof. We now prove the main result. The following is the main technical lemma.
, and let D be a fanin 2, constant free, and negation free DNNF computing the CNF E. There exist K ⊆ D and a family I of subsets of vertices in G such that: (i) |K| ≥ |I|; (ii) I covers the vertex covers of G; (iii) min{|I| : I ∈ I} ≥ min{1,c} 2d 2 |V |.
Proof. We construct K ⊆ D and a family I of subsets of vertices in G as follows. Let D 0 = D, K 0 = ∅, and I 0 = ∅. For i ≥ 0, we define D i , K i , and I i maintaining the following invariants: (I1) D i is a fanin 2, constant free, and negation free nontrivial DNNF; At i = 0, the invariant (I1) holds by the hypotheses on D and the fact that the CNF E is neither unsatisfiable nor valid; the invariant (I2) holds trivially because K 0 = ∅. Let i ≥ 1, and assume that the invariant holds at i − 1.
Proof of Claim 1. Let (w 1 , . . . , w s ) be a directed path in D from an input gate w s to the output gate w 1 = output(D i−1 ) such that for all j ∈ [s − 1] if w j has input wires from gates w j+1 and w in D i−1 (by hypothesis, w j has fanin at most 2), then |atoms(sub(D i−1 , w))| ≤ |atoms(sub(D i−1 , w j ))|.
By (I1), it holds that D i−1 is nontrivial, so that there exists a satisfying assignment f ∈ sat(D i−1 ). By (I2), sat(D i−1 ) ⊆ sat(D). By Proposition 1, there exists a certificate T ∈ cert(D i−1 ) such that f extends T . Since D i−1 is constant free and negation free, atoms(T ) ⊆ V .
We observe that atoms(T ) contains a vertex cover of G. To see this, assume by way of contradiction that no vertex cover of G is contained in atoms(T ). Let g be the assignment defined by g(x) = 1 if and only if x ∈ atoms(T ). Since g extends T , we have that g ∈ sat(D i−1 ) by Proposition 1. Consequently, g ∈ sat(D). Since D computes E, it holds that g ∈ sat(D) if and only if {x : g(x) = 1} is a vertex cover of G. But by definition {x : g(x) = 1} ⊆ atoms(T ), a contradiction.
As G is a (c, d)-expander, G is connected and has maximum degree at most d, we have by Proposition 2, that any vertex cover of G has size at least |V | d+1 . Hence, |atoms(T )| ≥ |V | d+1 . Therefore, we have that If we have |atoms(D i−1 )| ≤ |V | 2 , we may choose v i = w 1 = output(D i−1 ) and are done. Otherwise, where the first inequality holds as d ≥ 3. Hence, there exists an index j in [s − 1] such that by construction, where the last inequality holds as d ≥ 3. We choose v i = w j .
Let v i be the gate in D i−1 given by Claim 1. If elimconst(elimgate(D i−1 , v i )), that is, the result of first eliminating gate v i and then constants in D i−1 , computes the constant 0 function, then the construction terminates with K = K i−1 and I = I i−1 . Otherwise, put Note that D i satisfies (I1) by inspection of the elimination operation. Moreover, D i satisfies (I2) as follows: Claim 2. There exists a matching M i in G between atoms(sub(D i , v i )) and V \ atoms(sub(D i , v i )) such that Proof of Claim 2. Let S = atoms(sub(D i , v i )). Since |S| ≤ |V |/2 and G is a (c, d)-expander, by (1) we have that Recall that |S| ≥ |V |/(d + 1) by Claim 1. We construct a matching M i between between S and V \ S in G as follows. Pick an edge {v, w} ∈ E with v ∈ S and w ∈ N S ⊆ V \ S; add {v, w} to M i ; delete v from S, w from N S , the vertices in S with no neighbors in N S after the deletion of w, and the vertices in N S with no neighbors in S after the deletion of v; iterate on the updated S and N S , until either S = ∅ or N S = ∅. At each step, we delete at most d vertices in S and at most d vertices in N S .
Hence, we iterate for at least 2d 2 |V |, and we are done.
Let M i be the matching in G given by Claim 2.
Claim 3. There exists a subset I i of vertices in G such that |I i | = |M i | and, for all certificates T of D such that v i ∈ T , and all vertex covers C of G such that atoms(T ) ⊆ C, it holds that I i ⊆ C.
Proof of Claim 3. We construct a set I i ⊆ V as follows. Let {x, x ′ } ∈ M i . By construction, x ∈ S = atoms(sub(D i , v i )) and x ′ ∈ N S . Since M i ⊆ E and D computes E, it holds that {x, x ′ } ∩ atoms(T ) = ∅ for all T ∈ cert(D); otherwise, by Proposition 1, an assignment extending T and sending both x and x ′ to 0 would satisfy E, contradiction. By the invariant, any certificate of D i is also a certificate of D; hence {x, x ′ } ∩ atoms(T ) = ∅ for all T ∈ cert(D i ). Then, by applying Lemma 2 to D i , x ∈ atoms(T ) for all T ∈ cert(D i ) such that v i ∈ T , or x ′ ∈ atoms(T ) for all T ∈ cert(D i ) such that v i ∈ T . If x ∈ atoms(T ) for all T ∈ cert(D i ) such that v i ∈ T , then add x to I i ; otherwise, add x ′ to I i .
By construction, I i contains exactly one vertex for each edge in M i , hence |I i | = |M i |. Finally, let T be a certificate for D such that v i ∈ T . We observe that I i ⊆ atoms(T ). Indeed, let w ∈ I i , and let {w, w ′ } ∈ M i be the corresponding edge in M i . By construction, all certificates containing v i have w as an atom; in particular, w ∈ atoms(T ). We conclude that, for all vertex covers C of G such that atoms(T ) ⊆ C, it holds that I i ⊆ C. Put: We conclude checking that the sets K = {v 1 , . . . , v L } and I, returned by the above construction, satisfy (i)-(iii) as required.
(i) The mapping sending v i ∈ K to I i ∈ I (i ∈ [L]) is, by construction, a surjective function from K to I. Hence, |K| ≥ |I|.
(ii) Let C be any vertex cover of G. As D computes E, the assignment f defined by f (v) = 1 if and only if v ∈ C satisfies D, that is, f ∈ sat(D). By (I2), there exists i ∈ [L] such that f ∈ sat(D i−1 ) and f ∈ sat(D i ). By construction, there exists a certificate T ∈ cert(D) such that v i ∈ T and f ∈ sat(T ); that is, atoms(T ) ⊆ {v ∈ V : f (v) = 1} = C. So, by Claim 3, I i ⊆ C. Thus every vertex cover of G contains some set in I; that is, I covers the vertex covers of G.  Proof. First note that E = ∅, because |V | ≥ 2 and (c, d)-expanders are connected. Let D be a DNNF equivalent to the graph CNF E. By Corollary 2, there exists a fanin 2, constant free, and negation free DNNF D ′ equivalent to D such that 2·size(D) ≥ size(D ′ ). By Lemma 3, there exist K ⊆ D ′ and a family I of subsets of vertices in G such that |K| ≥ |I|, I covers the vertex covers of G, and min{|I| : I ∈ I} ≥ min{1, c}|V |/2d 2 . Putting h(c, d) = min{1,c}·f (d) Now observe that |E| ≤ d|V |, because G has maximum degree d; thus the CNF E has at most d|V | clauses, each of at most 2 literals, so that d|V | + 2d|V | = 3d|V | ≥ size(E). Therefore, where g(c, d) is as in the statement, and we conclude that DNNF(E) ≥ 2 g(c,d)·size(E)−1 .
Theorem 5. There exist a class C of CNF formulas and a constant c > 0 such that DNNF(F ) ≥ 2 c·size(F ) for each formula F ∈ C. Indeed, C is a class of read 3 times monotone 2-CNFs.
Proof. By Theorem 1, there exists a family G = {G i = (V i , E i ) : i ∈ N} of (e, 3)-expander graphs such that |V i | ≥ 2 for all i ∈ N and |V i | → ∞ as i → ∞ (e > 0). Every graph in G is connected; in particular, it does not contain isolated vertices. Therefore E i is a CNF for every i ∈ N, and indeed E i is a read 3 times monotone 2-CNF.
Since |V i | → ∞ as i → ∞ and each graph in G satisfies (1), there exists an infinite subset I ⊆ N such that size(E i ) < size(E i+1 ) for all i ∈ I. Choose c > 0 and j ∈ I large enough such that g(e, 3) · size(E j ) − 1 ≥ c · size(E j ), where g(·, ·) is as in the statement of Theorem 4. It follows from Theorem 4 that DNNF(E j ) ≥ 2 g(e,3)·size(Ej)−1 ≥ 2 c·size(Ej) ; we take C = {E i : i ∈ I and i ≥ j}, and the statement is proved.

Corollaries
In this section we will prove the corollaries of Theorem 5 we sketched in the introduction.
Let F be a CNF-formula. We say that a clause C is entailed by F if every satisfying assignment of F also satisfies C. We say that a clause C ′ subsumes C, if C ′ ⊆ C. A CNF F is in prime implicates form (short PI) if every clause that is entailed by F is subsumed by a clause that appears in F and no clause in F is subsumed by another. Note that CNFs in PI form can express all Boolean functions but it is known that encoding in PI form may generally be exponentially bigger than general CNF [DM02].
Lemma 4. Every monotone 2-CNF formula is in PI form.
Proof. Let F be a monotone 2-CNF formula. We first note that trivially no clause in a 2-CNF subsumes another. Now let C be a clause entailed by F and assume by way of contradiction that C is not subsumed by any clause of F , that is, every clause in F contains a positive literal not in C. Let C ′ be the clause we get from C by deleting all negative literals. We claim that C ′ is entailed by F . To see this, consider a satisfying assignment f of F . Let f ′ be the assignment we get from f by setting the variables that are negated in C to 1. Since F is monotone, this is still a satisfying assignment of F and thus of C. Consequently, C is satisfied by one of its positive literals in f ′ and thus in f . Thus f satisfies C ′ and it follows that F entails C ′ . Now let f be the assignment that sets all variables in C ′ to 0 and all other variables to 1. Since C and thus also C ′ is not subsumed by any clause of F , the assignment f satisfies F . But by construction f does not satisfy C ′ which is a contradiction.
Remember that the formulas of Theorem 5 are monotone 2-CNF formulas. Then we directly get the promised separation from Lemma 4 and Theorem 5.
Corollary 3. There exist a class C of CNFs in PI form and a constant c > 0 such that, for every formula F in C, every DNNF equivalent to F has size at least 2 c·size(F ) .
It follows that L 1 can be exponentially more succinct than L 2 for any two representation languages L 1 ⊇ PI and L 2 ⊆ DNNF. In particular, this holds if L 1 ∈ {PI, CNF, NNF} and L 2 ∈ {d-DNNF, DNNF}. Here, d-DNNF denotes the language of deterministic DNNFs, that is, DNNFs where subcircuits leading into DNNFs where subcircuits leading into a common ∨-gate never simulataneously evaluate to 1. This answers several questions concerning the relative succinctness of common representation languages [DM02].
We also observe that DNNFs are not closed under negation.
Lemma 5. There exist a class D of 2-DNF formulas and a constant c > 0 such that, for every formula D in D, every DNNF equivalent to ¬D has size at least 2 c·size(D) .
Proof. Let C be the class of 2-CNFs from Theorem 5. Let D be the class of 2-DNFs we get by negating the formulas in C. Now negating D gives the class C again, for which we have the lower bound from Theorem 5.
Observing that DNF is a restricted form of DNNF, we get the following non-closure result which was only known conditionally before.
Corollary 4. There exist a class D of DNNFs and a constant c > 0 such that, for every formula D in D, every DNNF equivalent to ¬D has size at least 2 c·size(D) .

Conclusion
We proved an unconditional exponential separation between the representational power of CNFs and that of DNNFs and discussed its consequences in the area of knowledge compilation [DM02]. Let us close by mentioning directions for future research.
In order to prove the lower bound of Theorem 5, we generalized arguments concerning paths in branching programs to the tree-shaped certificates of DNNFs. It would be interesting to know whether other lower bounds for branching programs can be lifted to (suitably restricted) versions of DNNFs along similar lines.
Recent progress notwithstanding [BLRS13], several separations between well-known representation languages are known to hold only conditionally [DM02]. For instance, it is known that DNFs cannot be compiled efficiently into so-called deterministic DNNFs unless the polynomial hierarchy collapses [SK96,CDLS02]. It would be interesting to show this separation unconditionally.
Finally, there is a long line of research proving upper bounds for DNNFs and restrictions (see [Raz14a,OD14a,OD14b] for some recent contributions). We believe that these results should be complemented by lower bounds as in [Raz14a,Raz14b], and hope that the ideas developed in this paper will contribute to this project.