title: Propositional directed acyclic graph
text: # Propositional directed acyclic graph
  
  A propositional directed acyclic graph (PDAG) is a data structure that is used to represent a Boolean function. A Boolean function can be represented as a rooted, directed acyclic graph of the following form:
  
  * Leaves are labeled with $\top$ (true), $\bot$ (false), or a Boolean variable.
  * Non-leaves are $\bigtriangleup$ (logical and), $\bigtriangledown$ (logical or) and $\Diamond$ (logical not).
  * $\bigtriangleup$- and $\bigtriangledown$-nodes have at least one child.
  * $\Diamond$-nodes have exactly one child.
  
  Leaves labeled with $\top$ ($\bot$) represent the constant Boolean function which always evaluates to 1 (0). A leaf labeled with a Boolean variable $x$ is interpreted as the assignment $x=1$, i.e. it represents the Boolean function which evaluates to 1 if and only if $x=1$. The Boolean function represented by a $\bigtriangleup$-node is the one that evaluates to 1, if and only if the Boolean function of all its children evaluate to 1. Similarly, a $\bigtriangledown$-node represents the Boolean function that evaluates to 1, if and only if the Boolean function of at least one child evaluates to 1. Finally, a $\Diamond$-node represents the complementary Boolean function its child, i.e. the one that evaluates to 1, if and only if the Boolean function of its child evaluates to 0.
  
  ## PDAG, BDD, and NNF
  
  Every binary decision diagram (BDD) and every negation normal form (NNF) are also a PDAG with some particular properties. The following pictures represent the Boolean function $f(x1,x2,x3)=-x1*-x2*-x3+x1*x2+x2*x3$:
  
  | BDD for the function f | PDAG for the function f obtained from the BDD | PDAG for the function f |
  | - | - | - |
  