Knowledge Compilation
In order to compute queries on a formula, such as "is the formula satisfiable?", "how many models does the formula have?", "does the formula imply another formula" etc., one can take essentially one of two approaches:

Use tools like a SAT solver, which compute the answers to such queries online on the original input formula (or normal forms which can be efficiently computed). Usually this online computation step is the computationintensive part, but the offline part of filling the SAT solver with the formula is easy.

Offline compile the original format into a more distinct format, e.g. a DNF, a BDD, or a DNNF and then answer the queries on this compiled format. In this case, the offline compile step is the computationintensive part, but answering the queries online is efficient.
The second approach is called knowledge compilation.
As a very simple example consider that we want to know two properties of a formula: 1) is it satisfiable, and 2) if so, how many models does it have.
In order to answer these two questions with approach 1 you could fill a SAT solver with the formula, compute its satisfiability and then enumerate all models. These computations are hard (in this case in NP and #P). For approach 2 you could compile the formula in a very simple knowledge compilation format, e.g. a canonical DNF. Computing this canonical DNF is the hard part, but if you could compute it, the two questions would be trivial to answer: The formula is satisfiable, if the canonical DNF has at least one model, and the number of models are exactly the number of minterms in the DNF.
But of course it is often not feasible to compute the canonical DNF of a formula, therefore more distinct knowledge compilation formats have been researched over the years. There are many knowledge compilation forms. Check out A Knowledge Compilation Map by Darwiche and Marquis to get an overview of the different knowledge compilation forms and how they perform in the distinct properties.
Generally, there are three aspects when considering different knowledge compilation forms:
 the succinctness of the compiled format
 the class of queries that can be answered in polynomial time on the compiled form
 the class of transformations that can be applied in polynomial time on the compiled form
In LogicNG, two advanced knowledge compilation forms are implemented:
 Binary Decision Diagrams (BDD)
 Decomposable Negation Normal Forms (DNNF)
BDDs are wellstudied and have been presented by Randal E. Bryant in 1986. DNNFs, however, among other knowledge compilation formats, have been developed more recently by Darwiche. The next chapter in this documentary is on BDDs, the succeeding one on DNNFs.
For more information about knowledge compilation forms, and BDDs and DNNFs, check out chapter 2.3. in New Formal Methods for Automotive Configuration by Zengler.