CNF, DNF, logic gates, and Karnaugh maps
Every propositional formula can be rewritten into a standard shape. Conjunctive Normal Form (CNF) is a conjunction of disjunctions -- an AND of ORs. Disjunctive Normal Form (DNF) is the dual: an OR of ANDs. These normal forms are essential for SAT solving, circuit design, and automated reasoning.
In this lesson, you will convert formulas to CNF and DNF step by step, simulate logic gate circuits, and use Karnaugh maps to simplify boolean expressions.
Converting to normal form is a mechanical process: first eliminate implications and biconditionals, then push negations inward using De Morgan's laws, and finally distribute to reach the target form. Watch each transformation step.
Watch the step-by-step conversion to Conjunctive Normal Form (CNF) and Disjunctive Normal Form (DNF).
Key insight: CNF is the input format for SAT solvers, making it central to computational logic. DNF makes satisfiability obvious (any true conjunction works) but can be exponentially larger than CNF.
Boolean formulas have a direct physical realization as logic circuits. AND, OR, and NOT gates are the building blocks of every digital computer. Toggle the input switches and watch signals propagate through the circuit. Every circuit computes a boolean function.
Click the input circles on the canvas to toggle 0/1. Blue wires carry signal 1, gray carry 0.
Key insight: NAND gates alone are functionally complete -- any boolean function can be built using only NAND gates. This is why NAND flash memory and NAND-based circuits dominate hardware design.
A Karnaugh map is a visual method for simplifying boolean expressions with 2-4 variables. The grid uses Gray code ordering so that adjacent cells differ in exactly one variable. Groups of adjacent 1s correspond to simplified product terms. Click cells to set values and watch the minimal expression emerge.
Click cells to toggle 0/1. Adjacent groups of 1s are detected automatically and the simplified Sum of Products is shown below.
Key insight: Karnaugh maps exploit the geometry of the Boolean hypercube. Each group of 2ᵏ adjacent cells eliminates k variables from the corresponding product term, producing a minimal formula.