
| Acronym   | Description                                            |
|-----------|--------------------------------------------------------|
| NNF       | Negation Normal Form                                   |
| DNNF      | Decomposable Negation Normal Form                      |
| d-NNF     | Deterministic Negation Normal Form                     |
| s-NNF     | Smooth Negation Normal Form                            |
| f-NNF     | Flat Negation Normal Form                              |
| d-DNNF    | Deterministic Decomposable Negation Normal Form        |
| sd-DNNF   | Smooth Deterministic Decomposable Negation Normal Form |
| BDD       | Binary Decision Diagram                                |
| FBDD      | Free Binary Decision Diagram                           |
| OBDD      | Ordered Binary Decision Diagram                        |
| OBDD<     | Ordered Binary Decision Diagram (using order <)        |
| DNF       | Disjunctive Normal Form                                |
| CNF       | Conjunctive Normal Form                                |
| PI        | Prime Implicates                                       |
| IP        | Prime Implicants                                       |
| MODS      | Models                                                 |

Table 1: Language acronyms.

| Property           | Short Description                                                                                      |
|--------------------|--------------------------------------------------------------------------------------------------------|
| Flatness           | The height of NNF is at most 2                                                                         |
| Simple Disjunction | Every disjunction is a clause, where literals share no variables                                       |
| Simple Conjunction | Every conjunction is a term, where literals share no variables                                         |
| Decomposability    | Conjuncts do not share variables                                                                       |
| Determinism        | Disjuncts are logically disjoint                                                                       |
| Smoothness         | Disjuncts mention the same set of variables                                                            |
| Decision           | A node of the form true, false, or (X ∧ α ∨ ¬X ∧ β), where X is a variable and α, β are decision nodes |
| Ordering           | Decision variables appear in the same order on any path in the NNF Table 2: Language properties.       |
