# Boolean algebra cheat sheet

## Operator Precedence

First operators in this list bind stronger:

1. $\neg$ (Negation)
2. $\wedge$ (And)
3. $\oplus$ (Xor)
4. $\vee$ (Or)
5. $\rightarrow$ (Implication)
6. $\leftrightarrow$ (Equivalence)

From this point on we will use multiplication ($\cdot$) instead of $\wedge$ and $+$ instead of $\vee$. Also, instead of writing $\neg a$ we will write $\bar{a}$. Sometimes the equality sign ($=$) is used to denote syntactic equality, but here we will denote sematic equivalence with $=$.

## Axioms

\begin{aligned} \left.\begin{aligned} a + b &= b + a \\ a \cdot b &= b \cdot a \end{aligned}\right\rbrace &\text{commutativity} \\ \left.\begin{aligned} a(b + c) &= ab + ac \\ a + bc &= (a + b)(a + c) \end{aligned}\right\rbrace &\text{distributivity} \\ \left.\begin{aligned} a + 0 &= a \\ a \cdot 1 &= a \end{aligned}\right\rbrace &\text{neutral elements} \\ \left.\begin{aligned} a + \bar{a} &= 1 \\ a \cdot \bar{a} &= 0 \end{aligned}\right\rbrace &\text{complement} \end{aligned}

## Basic laws

\begin{aligned} \left.\begin{aligned} a + a &= a \\ a \cdot a &= a \end{aligned}\right\rbrace &\text{idempotency} \\ \left.\begin{aligned} a + 1 &= 1 \\ a \cdot 0 &= 0 \end{aligned}\right\rbrace &\text{killer elements} \\ \left.\begin{aligned} a + ab &= a \\ a(a + b) &= a \end{aligned}\right\rbrace &\text{absorbtion} \\ \left.\begin{aligned} (a + b) + c &= a + (b + c) \\ (a \cdot b) \cdot c &= a \cdot (b \cdot c) \end{aligned}\right\rbrace &\text{associativity} \\ \left.\begin{aligned} \overline{a + b} &= \bar{a} \cdot \bar{b} \\ \overline{a \cdot b} &= \bar{a} + \bar{b} \end{aligned}\right\rbrace &\text{De Morgan} \\ \left.\begin{aligned} \bar{\bar{a}} &= a \end{aligned}\right\rbrace &\text{involution} \\ \left.\begin{aligned} ab + bc + \bar{a}c &= ab + \bar{a}c \\ (a + b)(b + c)(\bar{a} + c) &= (a + b)(\bar{a} + c) \end{aligned}\right\rbrace &\text{consensus} \end{aligned}

## Implication properties

### Simplification rules

\begin{aligned} 0 \rightarrow a &= 1 \\ 1 \rightarrow a &= a \\ a \rightarrow 1 &= 1 \\ a \rightarrow 0 &= \bar{a} \\ a \rightarrow \bar{a} &= \bar{a} \\ a \rightarrow a &= 1 \\ a \cdot b \rightarrow a &= 1 \\ a \rightarrow a \cdot b &= a \rightarrow b \\ a \rightarrow (a \rightarrow b) &= a \rightarrow b \\ a \rightarrow (b \rightarrow a) &= 1 \\ (a \rightarrow b) \rightarrow a &= a \\ (a \rightarrow b)(b \rightarrow c) \rightarrow (a \rightarrow c) &= 1 \end{aligned}

### Rewrite rules

\begin{aligned} a \rightarrow b &= \bar{a} + b \\ \overline{a \rightarrow b} &= a\bar{b} \\ a \rightarrow b &= \bar{b} \rightarrow \bar{a} \\ a \rightarrow b \cdot c &= (a \rightarrow b)(a \rightarrow c) \\ a \rightarrow b + c &= (a \rightarrow b) + (a \rightarrow c) \\ (a + b) \rightarrow c &= (a \rightarrow c)(b \rightarrow c) \\ a \rightarrow (b \rightarrow c) &= a \cdot b \rightarrow c \\ (a \rightarrow b) \rightarrow c &= (\bar{a} \rightarrow c)(b \rightarrow c) \end{aligned}

### Implication in an operator basis

\begin{aligned} \bar{a} &= a \rightarrow 0 \\ a \cdot b &= \overline{a \rightarrow \bar{b}} \\ a \cdot b &= (a \rightarrow (b \rightarrow 0)) \rightarrow 0 \\ a + b &= (a \rightarrow b) \rightarrow b \end{aligned}

## XOR and equivalence properties

\begin{aligned} a \oplus 0 &= a \\ a \oplus 1 &= \bar{a} \\ a \oplus a &= 0 \\ a \oplus b &= a\bar{b} + \bar{a}b \\ a \oplus b &= \bar{a} \oplus \bar{b} \\ a \oplus b &= \bar{a} \leftrightarrow b = a \leftrightarrow \bar{b} \\ a \oplus b &= \overline{a \leftrightarrow b} \\ a \cdot (b \oplus c) &= ab \oplus ac \\ a + b &= ab \oplus a \oplus b \\ a \rightarrow b &= ab \oplus a \oplus 1 \\ a \leftrightarrow b &= a \oplus b \oplus 1 \\ a \leftrightarrow a &= 1 \\ a \leftrightarrow \bar{a} &= 0 \\ a \leftrightarrow b &= (a \rightarrow b)(b \rightarrow a) \\ a \leftrightarrow b &= a \cdot b + \bar{a} \cdot \bar{b} \\ a \leftrightarrow b &= (\bar{a} + b)(a + \bar{b}) \\ a \leftrightarrow b &= \bar{a} \leftrightarrow \bar{b} \\ a \leftrightarrow b &= \bar{a} \oplus b = a \oplus \bar{b} \end{aligned}

## NAND and NOR

\begin{aligned} \bar{a} &= a \barwedge a \\ \bar{a} &= a \veebar a \\ \overline{a \barwedge b} &= \bar{a} \veebar \bar{b} \\ \overline{a \veebar b} &= \bar{a} \barwedge \bar{b} \\ a \cdot b &= (a \barwedge b) \barwedge (a \barwedge b) \\ a \cdot b &= (a \veebar a) \veebar (b \veebar b) \\ a + b &= (a \barwedge a) \barwedge (b \barwedge b) \\ a + b &= (a \veebar b) \veebar (a \veebar b) \\ a \oplus b &= (a \barwedge (a \barwedge b))\barwedge ((a \barwedge b) \barwedge b) \\ a \oplus b &= (a \veebar b) \veebar ((a \veebar a) \veebar (b \veebar b)) \\ a \leftrightarrow b &= (a \barwedge b) \barwedge ((a \barwedge a) \barwedge (b \barwedge b)) \\ a \leftrightarrow b &= (a \veebar (a \veebar b)) \veebar ((a \veebar b) \veebar b) \end{aligned}

## Linear clause forms

These minimum conjunctive normal forms are often used to construct a linear clause form of some formula. The CNF is then typically passed to a SAT-solver. \begin{aligned} x \leftrightarrow \bar{a} &= (\bar{x} + \bar{a})(x + a) \\ x \leftrightarrow a \cdot b &= (\bar{x} + a)(\bar{x} + b)(x + \bar{a} + \bar{b}) \\ x \leftrightarrow a + b &= (x + \bar{a})(x + \bar{b})(\bar{x} + a + b) \\ x \leftrightarrow a \oplus b &= (x + a + \bar{b})(x + \bar{a} + b)(\bar{x} + a + b)(\bar{x} + \bar{a} + \bar{b}) \\ x \leftrightarrow a \rightarrow b &= (x + a)(x + \bar{b})(\bar{x} + \bar{a} + b) \\ x \leftrightarrow a \leftrightarrow b &= (\bar{x} + \bar{a} + b)(\bar{x} + a + \bar{b})(x + \bar{a} + \bar{b})(x + a + b) \end{aligned}