Propositional directed acyclic graph
# 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 |
| - | - | - |
