CNF, DNF, logic gates, and Karnaugh maps
Any formula can be rewritten into a standard shape, wired up as a circuit, or simplified on a grid. Here you do all three.
Pick a formula and press Next Step to watch it become CNF and DNF side by side, one named rule at a time.
Watch the step-by-step conversion to Conjunctive Normal Form (CNF) and Disjunctive Normal Form (DNF).
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.
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.
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.
Choose a circuit and click the input switches to toggle them. Watch the signals flow through the gates to the output.
Click the input circles on the canvas to toggle 0/1. Blue wires carry signal 1, gray carry 0.
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.
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.
Click cells to set them to 1 and watch the minimal expression update. Neighboring cells differ in one variable, so each group of 1s collapses into a shorter term.
Click cells to toggle 0/1. Adjacent groups of 1s are detected automatically and the simplified Sum of Products is shown below.
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.
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.
Spot a mistake or have an idea?