Chris Collins

Tools · math

Boolean logic

Truth tables with a column for every sub-expression, push negations inward one named law at a time, brute-force SAT on CNF clauses, Quine–McCluskey minimisation with Karnaugh maps and gate diagrams, equivalence checks, and register bitfields.

Added · updated 14 October 2026

Works with

How to use it

Minimise

Type an expression or enter minterms. The tool accepts textbook, programming, and logic notation:

  • NOT: A', !A, ~A, ¬A, or NOT A.

  • AND: AB (juxtaposition), A·B, A*B, A & B, A && B, or AND.

  • OR: +, |, ||, or OR.

  • XOR: ^, ⊕, or XOR.

  • Also NAND, NOR, XNOR, → (implies), and <→.

Precedence runs NOT, then AND, then XOR, then OR, then →, then <→. With single-letter variables on, AB means A·B. Turn it off for names like en && ready.

  • Minimisation uses Quine–McCluskey. It merges implicants that differ in one bit until no more merges are possible, which leaves the prime implicants. Essential primes are taken first. The remaining minterms are covered exactly with Petrick’s method, choosing the fewest terms and then the fewest literals. Very large cyclic cores fall back to a greedy cover, and the tool says so.

  • The minimal POS form minimises the 0s (the complement) the same way, then applies De Morgan’s laws. Don’t-cares (X) can be used by either form.

  • The Karnaugh map (2–4 variables) is laid out in Gray code, so adjacent cells differ by one variable. It outlines each chosen group, including groups that wrap around the edges. Switch between grouping the 1s (SOP) and the 0s (POS).

  • Click any K-map cell or truth-table output to cycle it through 0, 1, and X. This switches to minterm mode, so you can design from a truth table.

  • The gate diagram draws the minimised SOP or the expression as written (as SVG, downloadable). NOT applied to AND, OR, or XOR becomes NAND, NOR, or XNOR.

  • Output notation can be algebra, C/JavaScript, Verilog, or LaTeX.

Truth table

The book’s procedure as a table: the atoms first (T first, as itertools.product([True, False]) lists them, or switch to 0/1 counting up), then one column for each sub-expression, innermost first, ending with the whole expression. Shared sub-expressions get one column. Add a second expression to compare: rows where the two final columns disagree are shaded, and the verdict says whether they are equivalent. Up to 8 variables.

These tabs (Truth table, Push ¬ inward, SAT) read whole-word names (p, admin, x1) and need an explicit operator between operands: !, ~, ¬ or not; &, &&, ∧ or and; |, ||, ∨, or or +; ^ or ⊕; → or →; <→ or ↔. Precedence, tightest first: ¬, ∧, ⊕, ∨, →, ↔ (and → groups to the right).

Push ¬ inward

Type a formula and watch it rewritten one law at a time, always at the outermost, leftmost place a law fits: conditional (p → q ≡ ¬p ∨ q), biconditional, exclusive or, De Morgan on ∧ and on ∨, double negation, negated conditional, and so on. Each step names its law and is checked against the original’s truth table (✓). It stops at negation normal form (every ¬ on a variable), or choose On to CNF to keep going with the distributive law until it is an AND of ORs; then Check satisfiability sends the clauses to the SAT tab. Next step, Show all and Start over step through it. The shortest sum of products (from the minimiser) is shown underneath, which finds simplifications such as absorption that pushing negations cannot.

SAT

Enter a formula in conjunctive normal form as DIMACS-style integers — 1 2, -1 3 means (x1 ∨ x2) ∧ (¬x1 ∨ x3); clauses can be separated by commas, semicolons, new lines or a trailing 0, and a p cnf header and c comments are allowed — or type any formula and it is converted to CNF by the laws. Name the variables (x,y,z) if you like. The tool tries every assignment in the book’s order (itertools.product([False, True], repeat=n)), shows for each row which clauses hold and which clause it breaks first, and stops at the first model, printed as the book’s Python prints it. Tick Every row to count all the models. Brute force stops at 24 variables (16 million rows); the table shows the first 1,024 rows.

Equivalence

Compare two expressions over all combinations of their variables (up to 16). Mismatching rows are listed as counterexamples. Use this to check a De Morgan rewrite or a refactored if condition.

Register bitfields

Describe a hardware register’s fields, one per line: NAME bit, NAME hi:lo, or NAME[hi:lo], with an optional # description. Enter a value (hex, binary, or decimal) to decode every field. Click bits to toggle them, or edit a field’s value to pack it back into the register. Overlapping fields and fields beyond the register width are flagged. Export the layout as C _Pos/_Msk macros (CMSIS style), a C bitfield union, Rust constants, or Python. The sample is an STM32-style USART control register.

Sharing

Share link (under the title) copies a URL that reopens this tool exactly as you have it — every tab’s inputs, with the current tab selected. Opening such a link replaces the inputs this browser had saved for the tool.

Linking to an example

Links can be written by hand. Put the tab after #: min, truth, eq, nnf, sat or bits (an example= link without one opens the example’s own tab).

Parameter Meaning Example

expr

Minimise tab expression (single-letter variables)

?expr=A’B%20%2B%20AB'#min

f

Truth table: the expression

?f=(m%20%7C%20s)%20%26%20l#truth

g

Truth table: a second expression to compare (optional)

&g=m%20%7C%20s%20%26%20l

order

Truth table row order: tf (T first, the book) or 01

&order=01

a, b

Equivalence tab: the two expressions

?a=!(p%26q)&b=!p%7C!q#eq

nnf

Push ¬ inward: the expression

?nnf=!(a%7C(o%26!l))#nnf

to

Stop at nnf or go on to cnf

&to=cnf

cnf

SAT: clauses (1 2, -1 3) or a formula

?cnf=1%202,-1%203,-2%20-3,-3%201#sat

names

SAT: names for variables 1, 2, 3 …

&names=x,y,z

all

SAT: try every row and count the models (true/false)

&all=true

example

A preset from the list below; parameters given alongside it win

?example=ch21-sat

*A ` in a link means a space*, so `?f=p+q` does not mean p OR q. Write OR as `|` (`%7C`), `or`, or `%2B`. The truth-table, ¬ and SAT tabs reject two operands with nothing between them, so a decoded ` shows up as an error ("Missing operator") rather than a silent AND. & must be written %26.

Presets (?example=…), from Mathematics, Reconnected, chapter 21:

  • ch21-connectives — p → q beside ¬p ∨ q: the conditional’s surprising rows.

  • ch21-banner — the banner ticket: (m ∨ s) ∧ ℓ against the buggy m ∨ s ∧ ℓ; rows 2 and 4 differ.

  • ch21-conditional — the truth_table procedure’s output for p → q.

  • ch21-demorgan — ¬(p ∧ q) and ¬p ∨ ¬q agree on every row.

  • ch21-contrapositive — p → q against ¬q → ¬p (equivalent).

  • ch21-converse — p → q against q → p (not equivalent).

  • ch21-distributive — p ∧ (q ∨ r) against (p ∧ q) ∨ (p ∧ r).

  • ch21-absorption — (p ∧ q) ∨ (p ∧ ¬q) is just p.

  • ch21-playground — the truth-table playground lab: the permission check and its rewrite side by side.

  • ch21-weekend — the exercise’s wrong rewrite of not (is_weekend or is_holiday).

  • ch21-venn — (A ∖ B) ∪ C̄ as rows of a three-variable truth table (the Venn lab’s second panel).

  • ch21-permission — ¬(a ∨ (o ∧ ¬ℓ)) pushed inward: De Morgan on ∨, De Morgan on ∧, double negation.

  • ch21-negated-conditional — the exercise ¬(p → q) ∨ q: negated conditional, distribution, and the minimal form p ∨ q.

  • ch21-cnf — (p → q) → r all the way to CNF.

  • ch21-sat — the coda’s formula; first model x = F, y = T, z = F after 3 rows.

  • ch21-sat-all — the same, every row: 2 of 8 assignments satisfy it.

  • ch21-sat-deps — package dependencies as SAT: install app, libA v2 and libB.

  • ch21-unsat — x ∧ ¬x: both rows break a clause.

For example ?example=ch21-permission#nnf, ?example=ch21-sat#sat, or the original style ?expr=A’B + AB' + AB.

Related: symbolic algebra, number theory, probability.

Companion to chapter 21, Logic and sets of Mathematics, Reconnected: the laws of logic and satisfiability.

Runs entirely in your browser; nothing you type leaves this page.