Fast d-DNNF Compilation with sharpSAT
Christian Muise Sheila McIlraith J. Christopher Beck Eric Hsu
Department of Computer Science, University of Toronto, Toronto, Canada. M5S 3G4.
{cjmuise, sheila, eihsu}@cs.toronto.edu jcb@mie.utoronto.ca
Abstract
Knowledge compilation is a valuable tool for dealing with
the computational intractability of propositional reasoning.
In knowledge compilation, a representation in a source lan-
guage is typically compiled into a target language in order to
perform some reasoning task in polynomial time. One par-
ticularly popular target language is Deterministic Decompos-
able Negation Normal Form (d-DNNF). d-DNNF supports ef-
ficient reasoning for tasks such as consistency checking and
model counting, and as such it has proven a useful represen-
tation language for Bayesian inference, conformant planning,
and diagnosis. In this paper, we exploit recent advances in
#SAT solving in order to produce a new state-of-the-art CNF
→ d-DNNF compiler. We evaluate the properties and per-
formance of our compiler relative to C2D, the de facto stan-
dard for compiling to d-DNNF. Empirical results demonstrate
that our compiler is generally one order of magnitude faster
than C2D on typical benchmark problems while yielding a
d-DNNF representation of comparable size.
1 Introduction
To deal with the intractability of propositional reasoning
tasks, one can sometimes compile a propositional theory
from a source language into a target language that guaran-
tees tractability of the task. This compilation process, popu-
larly referred to as knowledge compilation, has proven an ef-
fective tool for dealing with many practical reasoning prob-
lems (e.g., (Darwiche and Marquis 2002)).
Perhaps the best known target language is the language
captured by Ordered Binary Decision Diagrams (OBDDs),
a data structure that is commonly used in circuit synthesis
and verification (Ranjan et al. 1995). Here we are interested
in Deterministic Decomposable Negation Normal Form (d-
DNNF), a strict superset of OBDDs that is also more suc-
cinct. d-DNNF supports efficient reasoning for tasks such as
consistency checking and model counting. d-DNNF has also
been exploited more recently for a diversity of AI applica-
tions including Bayesian reasoning (Chavira, Darwiche, and
Jaeger 2006), conformant planning (Palacios and Geffner
2006), and diagnosis (Siddiqi and Huang 2008).
The de facto standard for CNF → d-DNNF compilation
is C2D, a tool developed and refined by Darwiche and col-
leagues over a number of years.1 Although C2D is well
designed and optimized, CNF→ d-DNNF compilation can
still be slow. Knowledge compilation has traditionally been
1http://reasoning.cs.ucla.edu/c2d/
characterized as an off-line process and therefore its pro-
cessing time can often be rationalized by amortizing it over
numerous subsequent queries. However, more recent use of
d-DNNF in tasks such as planning and diagnosis has been
problem specific, challenging this characterization and em-
phasizing the need for fast compilation.
Motivated by this need, in this paper we propose a
new CNF→ d-DNNF compiler, DSHARP (available online
at http://www.haz.ca/research/dsharp/). Our
compiler builds on the research results by Huang and Dar-
wiche showing that we can extract target languages such as
d-DNNF from the trace of an exhaustive search of a propo-
sitional theory (Darwiche 2004). To this end, we construct
our compiler by appealing to a state-of-the-art #SAT solver,
sharpSAT (Thurley 2006). Our compiler exploits two signif-
icant features of sharpSAT that distinguish it from previous
CNF → d-DNNF compilers: dynamic decomposition, and
implicit binary constraint propagation.
Our objective in constructing DSHARP was to develop a
state-of-the-art CNF → d-DNNF compiler that was faster
than C2D, while preserving the size of the output. We eval-
uated the performance of our compiler on 300 problem in-
stances over eight problem domains taken from SatLib2 and
the Fifth International Planning Competition.3 DSHARP
solved more problem instances than C2D in the time al-
lowed, showing a significant improvement in run time. The
size of the resulting d-DNNF representation was maintained,
and was on average five times smaller. In addition to these
experiments, we also delved deeper into the workings of our
compiler to attempt to determine the components that con-
tributed significantly to this improved performance. To this
end we did extensive ANOVA testing, identifying several
components of our system as being critical to this impres-
sive speedup.
In Section 2, we review some basic terminology related
to d-DNNF. We follow in Section 3 with a review of the
relationship between knowledge compilation and the search
trace of an execution of the Davis, Putnam, Logemann, and
Loveland algorithm (DPLL) for determining Satisfiability
(Davis, Logemann, and Loveland 1962), and a discussion
of our approach to developing DSHARP. In Section 4 we
present our experimental results, and conclude with a dis-
cussion in Section 5.
2http://www.satlib.org/
3http://www.ldc.usb.ve/˜bonet/ipc5/

2 Preliminaries
In (Darwiche and Marquis 2002) the authors proposed a so-
called knowledge compilation map, an analysis of a num-
ber of target compilation languages with respect to two key
features: succinctness of the target language, and the class
of queries and transformations that the language supports in
polytime. The target languages that they analyzed were not
restricted to classical “flat” normal forms such as CNF or
DNF, but also include a relatively large class of languages
based on directed acyclic graphs (DAGs). This class of lan-
guages included both OBDDs and d-DNNF, and helps high-
light the benefit that can be yielded by an alternative charac-
terization of languages in terms of a graph structure.
The knowledge compilation map proposed a hierarchy of
target languages. The root of the map is Negation Normal
Form (NNF), a DAG in which the label of each leaf node
is a literal, TRUE, or FALSE, and the label of each internal
node is a conjunction (∧) or a disjunction (∨). While NNF
is technically not a target language itself (since it does not
permit a polytime clausal entailment test) there are two dis-
tinct subsets of NNF whose members are target languages–
a flat subset and a nested subset. Our interest here is with the
nested subset. We distinguish members of the nested subset
by their properties including decomposability, determinism,
and smoothness. From these properties, a subset relation is
induced among the languages. The languages are then char-
acterized with respect to the tasks they enable in polytime.
The set of tasks considered includes consistency, validity,
clausal entailment, implicant checking, equivalence, senten-
tial entailment, model counting, and model enumeration.
Here we study compilation to d-DNNF. d-DNNF is the
subset of NNF satisfying decomposability and determinism.
More precisely, let V ars(n) be the propositional variables
that appear in the subgraph rooted at n, and let4(n) denote
the formula represented by n and its descendants. Decom-
posability holds when V ars(ni) ∩ V ars(nj) = ∅ for any
two children ni and nj of an and node of n. Determinism
holds when4(ni) ∧4(nj) is logically inconsistent for any
two children ni and nj of an or node of n.
Alternatively, we can understand d-DNNF as a set of well-
formed formulae of the following form. We define NNF to
be the family of boolean formulae that are built from the
operators ∨, ∧, and ¬, with the added restriction that all ¬
operators exist only at the literal level. Decomposable Nega-
tion Normal Form (DNNF) is the subset of NNF formulae
whose members additionally have the property that the for-
mula operands of ∧ do not share variables. Finally, d-DNNF
is the subset of DNNF whose members have the additional
property that the formula operands of ∨ are inconsistent.
d-DNNF permits polytime (in the size of the represen-
tation) processing of clausal entailment, model counting,
model minimization, model enumeration, and probabilistic
equivalence testing (Darwiche 2004). The conceptualiza-
tion of d-DNNF as a directed acyclic and-or graph, helps us
understand its relation to the DPLL trace, described in the
section to follow.
:xx y
V
§^:x^ y§^ x
V
W x= ?
§
Figure 1: Partial d-DNNF from an exhaustive DPLL trace.
3 DSHARP
The primary objective of this work is to develop a state-of-
the-art CNF → d-DNNF compiler that exploits recent ad-
vances in #SAT technology, with the aim of reducing com-
pilation time while maintaining d-DNNF size relative to ex-
isting compilers. We use a result of Huang and Darwiche
that shows we can extract target languages such as d-DNNF
from the trace of an exhaustive search of a propositional the-
ory. More specifically, we exploit the exhaustive search per-
formed by the #SAT solver, sharpSAT. In Section 3.1 we
review the Huang and Darwiche result. Then in Section 3.2
we discuss how we employ the features of sharpSAT to in-
stead generate d-DNNF within our new DSHARP compiler.
3.1 d-DNNF from an Exhaustive DPLL Trace
In order to perform the CNF → d-DNNF compilation, we
use the approach introduced in (Huang and Darwiche 2005)
to record the search space of an exhaustive DPLL proce-
dure. The exhaustive DPLL algorithm consists of a DPLL
algorithm modified to find all solutions and, therefore, to
implicitly explore the entire search space. Each node in the
DPLL search tree corresponds to a decision in the exhaus-
tive DPLL search (i.e., a variable selection and a choice of
assignment to either TRUE or FALSE). Decision nodes cor-
respond to or nodes in the d-DNNF representation. For each
or node, we add and nodes as children, corresponding to the
subtrees for the decision variable’s setting, and any variable
assignments inferred by unit propagation. Figure 1 shows
an example of part of the d-DNNF at a decision node where
variable x has been chosen. The theory as it exists before
setting x is Σ, and the theory solved for each subproblem is
Σ∧x and Σ∧¬x∧ y. If any unit propagation occurs due to
the variable being set, we record the implied literals under
the appropriate and node. For example, Figure 1 shows the
literal y as an implication of setting x = FALSE.
Following this approach, we are left with an and-or tree
with the leaf nodes corresponding to literals of the theory.
The tree has all of the required properties to qualify as a
representation for the d-DNNF language: it is in negation
normal form since the negations are at the literal level, it is
decomposable because the children of and nodes are disjoint
theories, and it is deterministic since the immediate children
of every or node has both a literal and its negation making
the conjunction inconsistent.