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  ⊤ {\displaystyle \top } (true),  ⊥ {\displaystyle \bot } (false), or a Boolean variable.
* Non-leaves are  △ {\displaystyle \bigtriangleup } (logical and),  ▽ {\displaystyle \bigtriangledown } (logical or) and  ◊ {\displaystyle \Diamond } (logical not).
* △ {\displaystyle \bigtriangleup } \- and  ▽ {\displaystyle \bigtriangledown } -nodes have at least one child.
* ◊ {\displaystyle \Diamond } -nodes have exactly one child.

Leaves labeled with  ⊤ {\displaystyle \top } ( ⊥ {\displaystyle \bot } ) represent the constant Boolean function which always evaluates to 1 (0). A leaf labeled with a Boolean variable  x {\displaystyle x} is interpreted as the assignment  x = 1 {\displaystyle x=1} , i.e. it represents the Boolean function which evaluates to 1 if and only if  x = 1 {\displaystyle x=1} . The Boolean function represented by a  △ {\displaystyle \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  ▽ {\displaystyle \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  ◊ {\displaystyle \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

[edit]

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

## See also

[edit]

* Data structure
* Boolean satisfiability problem
* Proposition
* Boolean circuit

## References

[edit]

* M. Wachter & R. Haenni, "Propositional DAGs: a New Graph-Based Language for Representing Boolean Functions", KR'06, 10th International Conference on Principles of Knowledge Representation and Reasoning, Lake District, UK, 2006.
* M. Wachter & R. Haenni, "Probabilistic Equivalence Checking with Propositional DAGs", Technical Report iam-2006-001, Institute of Computer Science and Applied Mathematics, University of Bern, Switzerland, 2006.
* M. Wachter, R. Haenni & J. Jonczy, "Reliability and Diagnostics of Modular Systems: a New Probabilistic Approach", DX'06, 18th International Workshop on Principles of Diagnosis, Peñaranda de Duero, Burgos, Spain, 2006.

* v
* t
* e

Diagrams in logic

* Venn diagram
* Square of opposition
* Porphyrian tree
* Karnaugh map
* Binary decision diagram
* Propositional directed acyclic graph
* Sentential decision diagram
* Truth table
* Sequent calculus
* Method of analytic tableaux

*[v]: View this template
*[t]: Discuss this template
*[e]: Edit this template