  We introduced decomposable negation normal form (DNNF) recently as a
tractable form of propositional theories, and provided a number of powerful
logical operations that can be performed on it in polynomial time. We also
presented an algorithm for compiling any conjunctive normal form (CNF) into
DNNF and provided a structure-based guarantee on its space and time complexity.
We present in this paper a linear-time algorithm for converting an ordered
binary decision diagram (OBDD) representation of a propositional theory into an
equivalent DNNF, showing that DNNFs scale as well as OBDDs. We also identify a
subclass of DNNF which we call deterministic DNNF, d-DNNF, and show that the
previous complexity guarantees on compiling DNNF continue to hold for this
stricter subclass, which has stronger properties. In particular, we present a
new operation on d-DNNF which allows us to count its models under the
assertion, retraction and flipping of every literal by traversing the d-DNNF
twice. That is, after such traversal, we can test in constant-time: the
entailment of any literal by the d-DNNF, and the consistency of the d-DNNF
under the retraction or flipping of any literal. We demonstrate the
significance of these new operations by showing how they allow us to implement
linear-time, complete truth maintenance systems and linear-time, complete
belief revision systems for two important classes of propositional theories.
