{'fraction_non_alphanumeric': 0.04462066784148931, 'fraction_numerical': 0.012877863630201979, 'mean_word_length': 4.612858229774283, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 1, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 4, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
CCDD: A Tractable Representation for Model Counting and Uniform Sampling

Knowledge compilation concerns with the compilation of representation languages to target languages supporting a wide range of tractable operations arising from diverse areas of computer science. Tractable target compilation languages are usually achieved by restrictions on the internal nodes of the NNF. In this paper, we propose a new representation language CCDD, which introduces new restrictions on conjunction nodes to capture equivalent literals. We show that CCDD supports two key queries, model counting and uniform samping, in polytime. We present algorithms and a compiler to compile propositional formulas expressed in CNF into CCDD. Experiments over a large set of benchmarks show that our compilation times are better with smaller representation than state-of-art Decision-DNNF, SDD and OBDD[AND] compilers. We apply our techniques to model counting and uniform sampling, and develop model counter and uniform sampler on CNF. Our empirical evaluation demonstrates the following significant improvements: our model counter can solve 885 instances while the prior state of the art solved only 843 instances, representing an improvement of 43 instances; and our uniform sampler can solve 780 instances while the prior state of the art solved only 648 instances, representing an improvement of 132 instances.


Introduction
Propositional reasoning plays a key role in diverse areas ranging from artificial intelligence, computational biology, verification, and the like. The computational intractability of the basic queries such as satisfiability, clausal entailment, and model counting for propositional reasoning provided an impetus to the emergence of the knowledge compilation (KC) approach [1,2,3]. Knowledge compilation concerns with the compilation of propositional theory into target languages that support a wide range of queries including satisfiability, model counting, uniform sampling in polynomial time. Accordingly, KC-based techniques form the core of several inference techniques in the context of probabilistic databases [4], probabilistic programming [5], tractable learning [6], and for synthesis and verification of hardware and software systems [7,8].
A target language is measured across three dimensions [2,9,10]: (1) succinctness of the target language; (2) supported operations in polytime by the target language; and (3) runtime efficiency of compilation process from representation to target language. The design of target compilation languages typically focuses on propositional formulas in negation normal form where the internal nodes are either conjunction (∧) or disjunction (∨), and the leaf nodes are (true), ⊥ (false), x, ¬x for variable x. To achieve tractability, we often put restrictions on the internal nodes with respect to their children. Two of the most widely used restrictions to achieve tractability are decomposability and determinism [11,12].
Due to the ubiquity of CNF as representation language, we are often interested in compilation methods from CNF to the desired target compilation language. The restrictions to achieve tractability are designed while keeping the the runtime complexity of the compilation in consideration. In practice, we often use decision nodes to enforce determinism. In contrast, the decomposability can be enforced by a simple clustering of CNF clauses such that clauses in distinct clusters do not share variables, and thereafter a conjunction node with children corresponding to each of the clusters can be constructed. Given the intractability of satisfiability on CNF, syntactic structure-based restrictions ensure the creation of a node can be achieved in polynomial time; the need for exponentially many nodes for most interesting target languages still leads to exponential time compilation algorithms.
While the KC map studies a diverse set of operations and properties, we focus our attention on model counting (CT) and uniform sampling (US) queries owing to their widespread usage in diverse areas ranging from probabilistic inference, reliability of networks, to hardware and software model checking, etc. Decision-DNNF [13], an influential target language, has been shown to support tractable model counting and uniform sampling. Actually, it was observed by Huang and Darwiche [9] that the trace of a search-based exact model counter corresponds to Decision-DNNF. Furthermore, Sharma et al. [14] showed that a scalable uniform sampler was engineered based on the scalable knowledge compiler D4 [15] on Decision-DNNF. The starting point of our work is to investigate the following natural question: Can we design efficient techniques on model counting and uniform sampling based on a generalization of Decision-DNNF?
The primary contribution of this paper is an affirmative answer to the above question. As a first step, we observe that the widely employed restrictions, in the context of knowledge compilation, on the internal nodes, decomposability, and determinism, are not expressive enough to capture literal equivalences. Indeed, pre-/in-processing techniques are an important step in modern SAT solvers [16]. We then first propose a generalization of Decision-DNNF, called CCDD, to capture literal equivalence, and show that CCDD supports model counting and uniform sampling in polynomial time. Guided by our motivation, we now design a knowledge compiler, called Panini, to compile CNF formulas into CCDD, and apply it to model counting and uniform sampling.
To empirically measure the effectiveness of CCDD, we perform an extensive experimental evaluation over a comprehensive set of benchmarks and conduct performance comparison of our tools vis-a-vis the state of the art knowledge compilers, model counters, and uniform samplers, c2d [17], Dsharp [18], miniC2D [19], BDDC [20], D4 [15], ADDMC [21], Ganak [22], SPUR [23], and KUS [14]. Our empirical evaluation over a large set of benchmarks show that our compilation times are better with smaller representations than state-of-art Decision-DNNF, SDD, and OBDD[∧] compilers. Among the prior state of the art model counters and uniform samplers are 843 (Ganak) and 648 (SPUR), our counter and sampler solve 886 and 780, representing a significant improvement of 43 and 132 instances, respectively. Since the developments in KC techniques have demonstrated the significance of engineering improvements, we believe that the significant performance improvements of our tools open up directions of future research in the im-provement of decision heuristics, caching schemes, and the like for compilers, counters, samplers based on CCDD.
The rest of the paper is organized as follows. We present notations, preliminaries, and related work in Sections 2-3. We introduce CCDD in Section 4 to capture literal equivalence, and tractable algorithms for model counting and uniform sampling in Section 5. In Section 6, we present our tools for knowledge compilation, model counting, and uniform sampling. Next, we present detailed empirical evaluation in Section 7. Finally, we discuss the other tractable operations on CCDD in Section 8 and conclude in Section 9.

Notations and Background
In a formula or the representations discussed, x denotes a propositional variable, and literal l is a variable x or its negation ¬x, where var(l) denotes the variable. PV = {x 0 , x 1 , . . . , x n , . . .} denotes a set of propositional variables. A formula is constructed from constants true, false and propositional variables using negation operator ¬, conjunction operator ∧, disjunction operator ∨, and equality operator ↔. A clause C (resp. term T ) is a set of literals representing their disjunction (resp. conjunction). A formula in conjunctive normal form (CNF) is a set of clauses representing their conjunction. Given a formula ϕ, a variable x, and a constant b, a substitution ϕ[x → b] is a transformed formula by replacing x by b in ϕ. An assignment ω over a variable set X is a mapping from X to {true, false}. Given a literal l, we denote ω(l) by {var(l) = true} if l is positive and {var(l) = false} otherwise. The set of all assignments over X is denoted by 2 X . A model of ϕ is an assignment over Vars(ϕ) that satisfies ϕ; that is, the substitution of ϕ on the model equals to true. Let sol(ϕ) ⊆ 2 X represent the set of models of ϕ, and ϕ |= ψ iff sol(ϕ) ⊆ sol(ψ). Given a formula ϕ, the problem of model counting is to compute |sol(ϕ)|, and the problem of uniform sampling is to generate a random model in sol(ϕ) with the same probability 1 |sol(ϕ)| . We focus on subsets of Negation Normal Form (NNF) where the internal nodes are labeled with disjunction (∨) or conjunction (∧) while the leaf nodes are labeled with ⊥ (f alse), (true), or a literal. For a node v, let ϑ(v) and V ars(v) denote the formula represented by the DAG rooted at v, and the variables that label the descendants of v, respectively.
We define the well-known decomposed conjunction [2] as follows: Definition 1. A conjunction node v is called a decomposed conjunction if its children (also known as conjuncts of v) do not share variables. Formally, let w 1 , . . . , w k be the children of ∧-node v, then Vars(w i ) ∩ Vars(w j ) = ∅ for i = j.
If each conjunction node is decomposed, we say the formula is in Decomposable NNF (DNNF) [11].
If each disjunction node of a DNNF formula is deterministic, we say the formula is in deterministic DNNF (d-DNNF), and we can perform tractable model counting on it.
Binary decision is a practical property to impose determinism in the design of a compiler (see e.g., D4 [15]), and the resulting language is called Decision-DNNF [13]. Essentially, each decision node with one variable x and two children is equivalent to a disjunction node of the form (¬x∧ϕ)∨(x∧ψ), where ϕ, ψ represent the formulas corresponding to the children. If each node of an NNF formula is labeled with ⊥ or , or represents a binary decision, the formula is called a Binary Decision Diagram (BDD).
Given a linear ordering ≺, a BDD is called ordered (OBDD) [24] if each decision node u with variable x i and its decision descendant v with variable x j satisfy x i ≺ x j . Darwiche [25] generalized binary decision to sentential decision, and proposed the sentential decision diagram (SDD). Lai at al. [20] augmented OBDD with decomposed conjunction giving OBDD[∧]. Hereafter, we will use OBDD, SDD and OBDD[∧] to denote the sets of all OBDDs, SDDs and OBDD[∧]s, respectively.

Knowledge Compilation
In the context of knowledge compilation, a diverse set of operations and properties have been studied with respect to the KC map [2]. However, we focus our attention on model counting (CT) and uniform sampling (US) queries owing to their widespread usage in diverse areas ranging from probabilistic inference, reliability of networks, to hardware and software model checking, etc.
To the best of our knowledge, Decision-DNNF is the first KC language which has been shown to support both tractable CT and US [12,14]. Natually, the subsets of Decision-DNNF, e.g., OBDD, SDD, and OBDD[∧], also support both tractable CT and US. This paper generalizes Decision-DNNF to propose a new representation CCDD that also supports both tractable CT and US. On the other hand, there are some languages, e.g., Sym-DDG [26] and EADT [27], which support tractable CT but is unknown to support tractable US or not. For KC tools, there are many practical knowledge compilers so far, including c2d [17], Dsharp [18], miniC2D [19], BDDC [20], and D4 [15]. We remark that many BDD packages (e.g., CUDD [28] and BuDDy [29]) and the SDD package [30] also equip the operations to transform a CNF formula into the corresponding KC languages. In addition, some of knowledge compilers, e.g., c2d [17], Dsharp [18], miniC2D [19], and D4 [15], also implement the interface for CT and therefore can serve as scalable model counters.

Model Counting
In this paper, we focus on the design of search-based model counters. To this end, we first present the skeleton of a general search-based model counter in Algorithm 1. 1 The algorithms often maintain a cache that stores the residual sub-formulas along with their corresponding model counts. The component-based decomposition, represented in line 4, seeks to partition the ϕ into sub-formulas, referred to as components, such that each of the components is defined over a mutually disjoint set of variables. Else, we pick a variable in line 9 and recursively compute the exact model count. Huang and Darwiche observed that the trace of the execution of such a model counter could be viewed to correspond to a Decision-DNNF formula. In this context, it is worth emphasizing that Decision-DNNF supports linear time model counting, which is reflected in simple constant time computations in lines 7 and 12 during each step of the recursions wherein every step of the recursion would correspond to a node in Decision-DNNF capturing the trace of the execution of SearchCounter. In this paper, we implemented a new model counter called ExactMC based on a generalized framework of SearchCounter.
Remark on Approximate Model Counting. While this work focuses on exact model counting, it is worth remarking that there has been a long line of work in the design of efficient hashing-based approximate model counters that seek to provide (ε, δ)-guarantees [31,32,33,34,35,36].

Uniform Sampling
Uniform sampling is closely related to model counting and knowledge compilation. Recently, Achlioptas et al. [23] brought together model counting and reservoir sampling to develop a uniform sampler called SPUR on top of sharpSAT. Subsequently, Sharma et al. [14] showed that Decision-DNNF supports tractable uniform sampling and proposed a uniform sampler called KUS using D4. Furthermore, this paper shows that CCDD also supports tractable US, and a scalable uniform sampler called ExactUS is developed based on a more efficient knowledge compiler Panini than D4.
While this work focuses on uniform sampling, there are also many samplers that seek to achieve scalability at the cost of theoretical guarantees of uniformity. Chakraborty et al. [37] introduced the first practical almostuniform sampler, UniGen, which has been improved to UniGen3 [36]. Golia et al. [38] designed a sampler called CMSGen by modifying the existing stateof-the-art Conflict-Driven Clause Learning (CDCL) SAT solver CryptoMin-iSat [39]. Although no theoretical guarantee has been provided, CMSGen performs very well in practice.

Capturing Literal Equivalences by CCDD
To seek an answer to the natural question of designing a counter whose trace is a generalization of Decision-DNNF, we first investigate appropriate generalizations of Decision-DNNF. To this end, we turn to the literal equivalences, a powerful technique in SAT solving, and we design a new representation language that seeks to utilize literal equivalences. We first discuss how to capture literal equivalence from the knowledge compilation perspective, which is then manifested into a corresponding new tractable language, called CCDD. We finally show that CCDD supports linear model counting, which serves as motivation for us to design a counter whose trace corresponds to CCDD.

Capturing Literal Equivalences
Given two literals l and l , we use l ↔ l to denote literal equivalence of l and l . Given a set of literal equivalences E, let E = {l ↔ l , ¬l ↔ ¬l | l ↔ l ∈ E}; and then we define semantic closure of E, denoted by E , as equivalence closure of E . Now for every literal l under E , let [l] denote the equivalence class of l. Given E, a unique equivalent representation of E, denoted by E and called prime literal equivalences, is defined as follows: is the minimum variable appearing in [x] over the lexicographic order ≺. It can be shown that E = E .
Let ϕ be a formula and let E be a set of prime literal equivalences implied by ϕ. We can obtain another formula ϕ by performing a literal-substitution: We propose a new notion on conjunction nodes to represent literal equivalences: Definition 3. A kernelized conjunction node v is a conjunction node consisting of a distinguished child, we call the core child, denoted by ch core (v), and a set of remaining children which define equivalences, denoted by Ch rem (v), such that: 1. Every w i ∈ Ch rem (v) describes a literal equivalence, i.e., w i = x ↔ l and the union of ϑ(w i ), denoted by E v , represents a set of prime literal equivalences.

For each literal equivalence
We now show how the model count of a kernelization of formula is related to its core. For simplicity, we use a sightly more general definition for model in Propositions 1-2. Given a formula ϕ and a set of variables X ⊇ V ars(ϕ), a model of ϕ over X is an assignment over X that satisfies ϕ. In practice, when we want to count models for ϕ, we only need to make X = Vars(ϕ).
Next we show given a kernelized conjunction ϕ = ψ ∧ (x ↔ l) over X, if ψ has m models over X, then ϕ has m 2 models over X. By induction, we get Proposition 1. Without loss of generality, assume l = x . As this is a kernalized conjuction, x / ∈ Vars(ψ). Let ω ∪ {x = false} and ω ∪ {x = true} be two assignments over X, where ω is a model of ψ over X \ {x }. Since x ↔ x , exactly one of the two assignments can be a model of ϕ, so half of the models of ψ are the models of ϕ.

Defining CCDD
We begin with the widely used idea of augmenting decision diagram with conjunction in knowledge compilation [40,13,26,20]. This idea is restated in a general form, Conjunction & Decision Diagram, to cover our kernelizationintegrated languages: is a variable (v is called a decision node) or operator ∧ (called a conjunction node). Each internal node v has a set of children Ch(v). For a decision node, Ch(v) = {lo(u), hi(u)}, where lo(u) (hi(u)) is connected by a dashed (solid) edge. The formula represented by a CDD rooted at u is defined as follows: (1) Hereafter we denote a leaf node by ⊥ or , an internal node by sym(v), Ch(v) ; and a decision node is denoted by sym(v), lo(v), hi(v) sometimes. Given a CDD rooted at v (denoted by D v ), its size |D v | is defined as the number of its edges, similar to other languages in the knowledge compilation literature. If we admit only read-once decisions and decomposed conjunctions, then the subset of CDD is Decision-DNNF. We are now ready to describe an extension of Decision-DNNF that captures literal equivalence, by imposing a different constraint on conjunction: Definition 5 (Constrained CDD, CCDD). A CDD is called constrained if each decision node u and its decision descendant v satisfy sym(u) = sym(v), and each conjunction node v is either: (i) decomposed; or (ii) kernelized. The language of all constrained CDDs is called CCDD.
We use ∧ d and ∧ k to denote decomposed and kernelized conjunctions respectively. Figure 1 depicts a CCDD. Since Decision-DNNF is a subset of CCDD and is known to be complete, we obtain the following result on the completeness of CCDD: Theorem 1. Given a formula, there is at least one CCDD to represent it.

Tractable Model Counting and Uniform Sampling on CCDD
In this section, we show that CCDD can support model counting and uniform sampling in polytime. We first show how CCDD supports model counting in linear time. We perform model counting on CCDD by a bottomup traversal on the DAG as follows: where the core child of the root is the child on the left hand side Proposition 2. Given a node u in CCDD with Vars(u) ⊆ X and a node v in D u , we use CT (v) to denote the model count of ϑ(v) over X. Then CT (u) can be recursively computed in linear time in |D u |: Proof. It is easy to see the case for the leaf nodes. The case for kernelized conjunctions was discussed in Proposition 1. For a decision node u, we can see that there are only half of the models over X of its low (resp. high) child satisfying ¬sym(u) ∧ ϑ(u) (resp. sym(u) ∧ ϑ(u)), since sym(u) does not appear in ϑ(lo(u)) (resp. ϑ(hi(u))). Now we discuss the case for decomposed conjunctions. Given a decomposed conjunction u, we show that this proposition holds when |Ch(u)| = 2. For the cases |Ch(u)| > 2, we only need to iteratively use the conclusion of the case |Ch(u)| = 2. Assume that . Assume that ϑ(v) and ϑ(w) have m 1 and m 2 models over X 1 and X 2 , respectively. Then ϑ(v) and ϑ(w) have m 1 · 2 |X 2 |+|X 3 | and m 2 · 2 |X 1 |+|X 3 | models over X, respectively. ϑ(u) has m 1 · m 2 models over X 1 ∪ X 2 , and has m 1 · m 2 · 2 |X 3 | models over X. It is easy to see the following equation: Now we turn to uniform sampling, which is a new query in knowledge compilation [14]. We present the sampling algorithm on CCDD in Algorithm 2, which takes in a consistent CCDD node u, and returns a random model from sol(u). Algorithm Sample first invokes SampleSub in Algorithm 3 to get a partial assignment ω of ϑ(u). If a variable x does not appear in ω, we will assign x as a random Boolean value in lines 2-5 via a Bernoulli distribution with parameter 0.5. The main idea of Algorithm SampleSub is that according to the model count of each node in the CCDD, we perform a random search along a subtree in the CCDD, which corresponds to a partial assignment, in a top-down way. If u = , SampleSub returns the empty set in line 1. If u is a decomposed node, we sample independently from its children in line 2. If u is a kernelized node, SampleSub samples from the core child first and then samples from the remaining literal equivalences (lines 3-9). We remark that for an equivalence node, its child v represents a literal and we use ω(v) to denote the assignment on sym(v) corresponding to the literal represented by v. If u is a decision node, SampleSub assigns a random value to sym(u) according to model count ratio of low child to high child, and then samples from the chosen child (lines [10][11][12][13][14][15][16]. Note that according to Proposition 2, we can count models for all nodes of D u in linear time. We assume that we finish the calling of CT (u) before we call Sample(u). Thus, Sample(u) terminates in O(|Vars(u)|) after the model count on each node is labeled.
Proposition 3. Given a consistent CCDD node rooted at u, Sample(u) can output each model with probability 1 CT (u) . Proof. If we can prove a lemma that SampleSub(u, X) can output a partial assignment ω with probability CT (ω,X) CT (u,X) such that ϑ(u)| ω ≡ true, then it is easy to see this proposition holds. It is easy to see that this lemma holds for constant CCDDs. We assume that this lemma holds with the number of nodes |N (D u )| ≤ n. For the case with |N (D u )| = n + 1, we proceed with case analysis: • u is a decomposition node: This lemma holds since the events of sampling from two different children are independent.
• u is a kernelization node: For the case with more than one literal equivalence, we assume that v is a literal equivalence in Ch(u) \ {ch core (u)}. u is equivalent to the combination of two kernelized conjunction nodes ∧ k , { ∧ k , Ch(u) \ {v} , v} with less literal equivalences. Without loss of generality, we assume that u has only one literal equivalence v. According to the induction hypothesis, SampleSub(ch core (u), X) can output a partial assignment ω. If (sym(u) = f alse) ∈ ω, then ω = ω ∪ ω(lo(v)) satisfies ϑ(u), and CT (u,X) . The case (sym(u) = true) ∈ ω is similar to the one (sym(u) = f alse) ∈ ω. For the case sym(u) / ∈ Vars(ω), it is similar to the case where u is a decomposition node.

Scalable Compiler, Counter, and Sampler
In this section, we turn our attention to the compilation of a given model into CCDD, and performing model counting and uniform sampling in practice. We remark that in the context of knowledge compilation, there are some other languages that are generalizations of Decision-DNNF (see e.g., Sym-DDG [26]). As far as we know, however, there are no scalable model counters or uniform samplers reported, based on these languages.

Panini: Compilation to CCDD
It is standard in knowledge compilation field to design compilers that take CNF as input and output an equivalent represetation corresponding to target language. In the same spirit, our algorithm, called Panini and described in Algorithm 4, takes in a CNF formula ϕ, and returns a CCDD representing ϕ.
We first handle the base cases lines 1-2. We return ⊥ and in lines 1 and 2 if ϕ is false and true, respectively. We then turn to the discovery and usage of literal equivalences in the formula to perform model counting as presented in lines 4-12. We use a heuristic, ShouldKernelize, to determine whether we should spend time in detecting and using literal equivalence because those steps are themselves possibly costly. We discuss ShouldKernelize further in Section 6.4. When ShouldKernelize returns true, we turn to call DetectLitEqu to discover literal equivalences in the formula in line 5 and if a non-trivial literal equivalence is discovered, we proceed to perform the compilation with respect to kernelized conjunction in lines 7-10. In particular, we first invoke ConstructCore to perform literal-substitution (see Section 4.1) to obtain the formula,φ, corresponding to the core child, and then recursively call Panini overφ.
If no non-trivial literal equivalence is found in line 5, then the rest of the algorithm follows the template of a Decision-DNNF compiler. We first invoke Decompose in line 13 to determine if the formula ϕ can be decomposed into components. In other words, we seeks to partition the ϕ into sub-formulas such that each of the components is defined over a mutually disjoint set of variables. If such a decomposition is not found, we pick a variable x and recursively invoke Panini on the residual formulas ϕ[x → f alse] and ϕ[x → true].
We now employ a simple example to show how kernelization helps us to reduce the size of resulting DAG. For simplicity, we assume PickGoodVar gives variables in the lexicographic order, and ShouldKernelize always returns true or always returns false.

end
Without Kernelization If ShouldKernelize is false, Panini will generate the CCDD in Figure 3a.
With Kernelization If ShouldKernelize is true, we can detect two literal equivalences x 1 ↔ ¬x 4 and x 2 ↔ ¬x 5 , and thus the residual sub-formula is equivalent to (x 1 ⊕ x 2 ⊕ x 3 = 1). After running lines 18-20, we have two other literal equivalences x 2 ↔ ¬x 3 and x 2 ↔ x 3 . The result corresponds to the CCDD in Figure 3b.

ExactMC: A Scalable Model Counter
As discussed in Sections 4-5, CCDD has two key properties: CCDD is complete, i.e., every formula can be represented using CCDD and it supports linear model counting. Thus, we can immediately obtain a model counter by invoking Panini and Algorithm CT . However, we observe that it often costs much memory to store a CCDD for a complex CNF formula. We do not need to actually generate the CCDD, but only need to perform search with respect to CCDD to perform model counting. This observation motivates us to design an individual model counter, ExactMC, whose trace corresponds to CCDD. Algorithm 5, ExactMC, takes in a CNF formula ϕ and the set of variables X (initialized to Vars(ϕ)), and returns |sol(ϕ)|. ExactMC is based on the architecture of search-based model counters, as shown in Algorithm 1.
We first handle the base cases lines 1-2 corresponding to the first two cases in Proposition 2. Since we are interested in computing the number of satisfying assignments over X, we return 2 |X| in line 2 in case ϕ is true. We then turn to the discovery and usage of literal equivalences in the formula to perform model counting as presented in lines 4-11. When ShouldKernelize returns true, we turn to DetectLitEqu to discover literal equivalences in the formula in line 5 and if a non-trivial literal equivalence is discovered, we proceed to perform exact model counting with respect to kernelized conjunction in lines 7-8 (corresponding to the fourth case in Proposition 2, where | E | is equal to the number of children minus one). In particular, we first invoke ConstructCore to perform literal-substitution (see Section 4.1) to obtain the formula,φ, corresponding to the core child, and then recursively call ExactMC overφ.
If no non-trivial literal equivalence is found in line 5, then the rest of the algorithm follows the template of search-based model counters. We first invoke Decompose in line 12 to determine if the formula ϕ can be decomposed into components. If such a decomposition is not found, we pick a variable x and recursively invoke ExactMC on the residual formulas ϕ[x → f alse] and ϕ[x → true]. We remark that lines 14-15 and lines 17-20 correspond to the third and fifth cases in Proposition 2, respectively.

ExactUS: A Scalable Uniform Sampler
Since CCDD is complete and supports tractable model counting and uniform sampling, we can immediately obtain a uniform sampler by invoking Algorithms Panini, CT , and Sample. The workflow of our uniform sampler, called ExactUS, is as follows: • First, we invoke Panini to transform a CNF formula into an equivalent CCDD; Algorithm 5: ExactMC(ϕ, X) • Second, we invoke CT to label model count for each node in the CCDD; and • Finally, we invoke Algorithm Sample s times on the CCDD to generate s identically and independently distributed samples.
Among the above three steps, the first one is often the most time-consuming but can be performed offline. The compiling time is amortized over online callings of Algorithm Sample for sample generation. In practice, this setting facilitates the end-user (e.g., verification engineer who typically invokes a sampler repeatedly till a bug is triggered [41]).

Implementation
Since the core contribution of our work lies in the on-the-fly construction and usage of kernelized conjunction nodes, we now discuss the implementation details that are crucial for runtime efficiency of our tools. As is the case for most heuristics in SAT solving and related communities, we selected parameters empirically. Given the original formula ϕ, we will use #NonUnitVars to denote the number of variables appearing in the non-unit clauses of ϕ.
ShouldKernelize As mentioned earlier, the detection and usage of literal equivalences can be significantly advantageous but our preliminary experiments indicated the need for caution. In particular, we observed that the implicit construction of kernelized conjunction node over the trace was not helpful for easy instances. To this end, we rely on the number of variables as a proxy for the hardness of a formula, in particular at every level of recursion, we classify a formula ϕ to be easy if |V ars(ϕ)| ≤ easy bound , where easy bound is defined by min(128, #NonUnitVars/2). If the formula ϕ is classified as easy, then ShouldKernelize returns false. Else, we consider the search path from the last kernelization (if no kernelization, then the root) to the current node. If the number of unit clauses on the path is greater than 48 and also greater than twice the number of decisions on the path, ShouldKernelize returns true. The intuition behind the usage of unit clauses is that unit clauses are often useful to simplify the current sub-formula and thus possibly lead to many literal equivalences.
In the other cases, ShouldKernelize returns false. We empirically determine the heuristic to have good performance.
DetectLitEqu Recall, we need to check for a chosen pair of literals l 1 and l 2 , whether l 1 ↔ l 2 is a literal equivalence implied by ϕ in De-tectLitEqu. For an efficient check, we rely on using implicit Boolean Constraint Propagation (i-BCP) for the assignments l 1 ∧¬l 2 and ¬l 1 ∧l 2 . The usage of i-BCP in model counting dates back to sharpSAT [42]. We perform some simplications on each component in order to detect more literal equivalences which includes removing literals from clauses, and unnecessary clauses. In particular, we designed a pre-processor called PreLite 2 to perform the initial kernalization on the original formula.
Prime Literal Equivalences We employ union-find sets to represent prime literal equivalences, which allows us to efficiently compute prime literal equivalences from a set of literal equivalences.

Decision Heuristics
We combine the widely used heuristic minfill [44] and a new dynamic ordering, which we call dynamic combined largest product (DLCP) to pick good variables. Given a variable, the DLCP value is the product of the weighted sum of negative appearances and positive appearances of the variable. Given an appearance, the heuristic considers the following cases: (i) if it is in an original binary clause, the weight is 2; (ii) if it is in a learnt binary clause, the weight is 1; (iii) if it is in an original non-binary clause with m literals, the weight is 1 m ; otherwise, (iv) the weight is 0. If the minfill treewidth is greater than a crossover constant min(128, #NonUnitVars/c), we use DLCP, otherwise, minfill. We choose c = 5 for compilation and c = 7 for counting. We observed in the experiments that for an instance with high treewidth, DLCP is often useful to lead to a sub-formula with many literal equivalences after assigning some variables.

Experimental Evaluation
We implemented prototypes of Panini, ExactMC, ExactUS in C++. We evaluated these tools 3 on a comprehensive set of 1114 benchmarks 4 from a wide range of application areas, including automated planning, Bayesian networks, configuration, combinatorial circuits, inductive inference, model checking, program synthesis, and quantitative information flow (QIF) analysis. These instances have been employed in the past to evaluate model domain (#)  Table 2: Compilation statistics on selected instances, where "-" denotes timeout or out of memory, "#knodes" denotes the total number of kernelized nodes, and the other columns are about compilation size counting and knowledge compilation techniques [15,45,20,46,47]. The experiments were run on a cluster 5 where each node has 2xE5-2690v3 CPUs with 24 cores and 96GB of RAM. Each instance was run on a single core with a timeout of 3600 seconds and 4GB memory.

Knowledge Compilation
We compared Panini with state-of-the-art compilers for the following target languages: (i) SDD with miniC2D [19]; (ii) OBDD[∧] with BDDC [20]; (iii) Decision-DNNF with c2d [17], Dsharp [18] and D4 [15]. We used the widely employed pre-processing tool pmc [43] for all the instances, which preserves the equivalence between input instance and pre-processed instance and is quite helpful for improving the efficiency of knowledge compilers. We employed the minfill heuristic for variable ordering in BDDC, miniC2D, and c2d, which has been shown to significantly improve runtime and space performance [18,20]. Dsharp and D4 employ their own custom variable ordering heuristics, which were shown to improve their performance [18,15]. Table 1 shows the total performance of the six compilers compiling from CNF to the target language. Overall, Panini compiled 37, 89, 21, 212, and 35 more instances than BDDC, miniC2D, c2d, Dsharp, and D4, respectively. We remark that Panini compiled 58, 168, 43, 251, and 44 more instances than BDDC, miniC2D, c2d, Dsharp, and D4 respectively without the usage of pmc. Figures 4a and 4b show the cactus plots for runtime and compilation sizes (in terms of edges in the DAG) for all six compilers. The x-axis gives the number of benchmarks; and the y-axis is compiling time (resp. compilation sizes), i.e., a point (x, y) in Figure 4a shows that x benchmarks took less than or equal to y seconds to compile. The results show that Panini can give start-of-the-art compilation both in runtime and compiled size. We show the space performance of CCDD on some selected instances in Table 2. The experimental results show that CCDD has obvious space advantage and there are many kernelized nodes in the compiled forms.

Model Counting
We compared ExactMC with state-of-the-art exact counters from each of the three paradigms: compilation-based, search-based or variable eliminationbased. Compilation-based counters include c2d and D4 based on Decision-DNNF. For search-based counters, we compared with Ganak [46] and SharpSAT-TD [48], the winners of the unweighted tracks in model counting competitions 2020 and 2021 6 , respectively. We remark that Ganak is a recent probabilistic exact model counter that implicitly combines Decision-DNNF approach with probabilistic hashing to provide exact model count with a given confidence 1−δ (we used the default δ = 0.05). Note that probabilistic exact is a stronger notion than another related notion of probabilistic approximate counting [49]. Also, perhaps it is worth remarking that Ganak and SharpSAT-TD builds on and was shown to significantly improve upon the prior state of the art searchbased counter, sharpSAT [50]. For variable elimination-based counters, we compared with ADDMC [21].
We used the widely employed pre-processing tool B+E [51] for all the instances, which was shown more powerful in model counting than pmc [51,46], but does not preserve the equivalence between input instance and pre-processed instance. We remark that B+E can often simplify almost all of the literal equivalences in the original formula detected by i-BCP. We emphasize that the literal equivalences in ExactMC is a "in-processing technology", and since B+E is already used, the literal equivalences used in ExactMC are basically the ones appearing in the sub-formulas. Consistent with recent studies, we excluded the preprocessing time from the solving time for each tool as preprocessed instances were used on all solvers. We emphasize that the usage of pre-processing favors other competing tools than ExactMC, except SharpSAT-TD where a pre-processor similar to B+E has been integrated. To see the effect of B+E, Ganak, c2d, SharpSAT-TD, D4, ADDMC, and ExactMC solved 173, 117, 2, 170, 283, and 54 less instances without the pre-processing, respectively. Similarly, we employed the minfill heuristic for variable ordering in c2d. D4, Ganak, and SharpSAT-TD employ their own custom variable ordering heuristics, which were shown to improve their performance [15,46].   Table 4: Counting statistics on selected instances using Decision-DNNF-based and CCDDbased counters, where "-" denotes timeout or out of memory, "#kers" denotes the total number of kernelizations, and the other columns are about solving time in seconds solved 133, 43, 48, 47, and 51 more instances than ADDMC, Ganak, c2d, SharpSAT-TD, and D4, respectively. Upon closer inspection of the performance of various tools across different domains, we observe that ExactMC performed the best on seven out of nine domains. Figure 5 shows the cactus plot for runtime for all the six tools. The x-axis gives the number of benchmarks; and the y-axis is running time, i.e., a point (x, y) in Figure 5 shows that x benchmarks took less than or equal to y seconds to solving. The results show that ExactMC can improve the state-of-the-art model counting across all three paradigms. We remark that all of Ganak, c2d, SharpSAT-TD, and D4 perform searches with respect to Decision-DNNF. In order to show the effect of kernelization, we compared ExactMC with the virtual best solver of c2d, D4, Ganak, and SharpSAT-TD (VBS-DecDNNF). We found that even in such an extreme case, ExactMC solved one more instance than VBS-DecDNNF.
We present the effect of kernelization on some selected instances and solving times in Table 4. The experimental results show that for some instances (e.g., blasted case138), even a small number of kernelizations are very useful to accelerate solving. Furthermore, it is worth noticing that we are able to perform a large number of kernelizations in the benchmarks, showing that substantial literal equivalence can occur in sub-formulas despite the use of pre-processing, e.g. sygus 09A-1 (Program-Synthesis). We also conducted experiments where kernelization was disabled in ExactMC (without lines 4-12 in Algorithm 5). We found that the resulting counter solved 17 less instances than the original version of ExactMC, and the average PAR-2 score increased to 1603 from 1505. 7

Uniform Sampling
To the best of our knowledge, SPUR and KUS are the only two tools that can perform sampling on CNF formulas with theoretical guarantees of uniformity. SPUR    pre-process the instances as it preserves equivalence. Table 5 shows the performance of SPUR, KUS, and ExactUS. Overall, ExactUS solved 132 and 186 more instances than SPUR and KUS, respectively, and performed the best on all the (nine) domains. We remark that ExactUS solved 157 and 201 more instances than SPUR and KUS, respectively, without the usage of pmc. Figure 6 shows the cactus plot for runtime for all three samplers. The results also demonstrate the significant improvement of ExactUS compared with SPUR and KUS.

Discussion on Tractability of CCDD
We highlight that our focus in this paper is primarily on improving the scalability of model counters and uniform samplers. However, encouraged by the significant performance improvement by ExactMC over existing solvers as shown in our experimental results, we investigate further into the underlying language, CCDD. To this end, we study CCDD from a knowledge compilation perspective characterize the tractability of CCDD. We refer the reader to Darwiche and Marquis's seminal work [2] for definitions of different standard operations in the literature. We focus on the five queries: implicant check, model counting, consistency check, validity check, and model enumeration.
We first show that CCDD supports tractable implicant check: Proposition 4. Given a consistent term T and a CCDD node u, we use IM (T, u) to denote whether T |= ϑ(u). Then IM (T, u) can be recursively performed in linear time: Proof. The constant, and decomposed and kernelized conjunction cases are obvious, and thus we focus on the decision case. Note that a literal equivalence is a special decision node. For the case where ¬sym(u) ∈ T , each model of T is not a model of sym(u) ∧ ϑ(hi(u)), and thus T |= ϑ(u) iff T |= ϑ(lo(u)). The case where sym(u) ∈ T is similar. Otherwise, T |= ϑ(u) iff ¬sym(u) ∧ T |= ¬sym(u) ∧ ϑ(lo(u)) and sym(u) ∧ T |= sym(u) ∧ ϑ(hi(u)) iff T |= ϑ(lo(u)) and T |= ϑ(hi(u)).
Since CCDD supports model counting in linear time, we obtain that CCDD supports consistency check, validity check, and model enumeration in polynomial time.
Theorem 2. CCDD supports model counting, consistency check, validity check, and implicant check in time polynomial in the DAG size, and supports model enumeration in time polynomial in both the DAG size and model count.
According to the notation in the knowledge compilation map [2], we know that CCDD satisfies CT, CO, VA, IM, and ME, respectively. We mention that if we restrict the number of ∧ k -nodes in each path from the root to a leaf, to be a constant t, we can obtain a subset of CCDD. This subset is still a superset of Decision-DNNF, and supports the same tractable operations as Decision-DNNF. We remark that another representation in the knowledge compilation literature called EADT [27] uses a generalization of literal equivalence; however, EADT is a tree-structured representation and therefore is not a generalization of Decision-DNNF, which is a DAG-based representation.

Conclusion
This paper proposed the notion of kernelization to capture literal equivalence in knowledge compilation. Combining kernelization, decomposition and ordered decision, this paper identified the new language CCDD. CCDD supports two key queries, model counting and uniform sampling in polynomial time. We designed tractable algorithms for model counting and uniform sampling on CCDD. To facilitate the usage of CCDD in practice, we developed the prototype compiler Panini to compile CNF formulas into CCDD. Experimental results show that our compilation times are better with smaller representations than state-of-art Decision-DNNF, SDD, and OBDD[∧] compilers. For model counting and uniform sampling, our techniques also significantly outperform the state-of-the-art tools. Since kernelization is orthogonal to other notions such as determinism and decomposability, we expect kernelization will help the knowledge compilation community to identify more interesting languages.