# 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 complemenatary 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