How to convert an expression to CNF

1. Type or paste your expression. Use whichever notation you know: A'B + C, !A & B | C or ¬A ∧ B ∨ C all work, and the symbol buttons help on a phone.
2. Press Convert to CNF. Results also update as you type.
3. Read the minimal CNF at the top, follow the step-by-step working, or open the truth table. Use Show results as to switch notation and Copy to take any answer.

What is conjunctive normal form?

A formula is in conjunctive normal form when it is an AND of clauses and every clause is an OR of literals (a variable or its negation), for example (A ∨ ¬B) ∧ (B ∨ C). In digital electronics the same shape is called a product of sums (POS). Every Boolean function has a CNF.

Three CNFs, and when to use each

• Minimal CNF: the fewest clauses, then the fewest literals. It is found exactly by grouping the rows where the function is 0 (Quine–McCluskey with a complete search of the prime implicant chart, as in Petrick's method), and checked against your input on every row.
• Canonical CNF: one clause (maxterm) for every row where the function is 0. It is unique and easy to check, but long.
• Step-by-step CNF: what you get by hand with the laws of Boolean algebra: remove ↔ and ⊕, remove →, push NOT inward with De Morgan's laws, distribute ∨ over ∧ and simplify. It is equivalent to the input but not always minimal.

Tseitin encoding for SAT solvers

Distributing ∨ over ∧ can make a CNF exponentially long. SAT solvers avoid this with the Tseitin transformation, which adds one new variable per gate and needs only a few clauses per gate. The result is not equivalent to your formula, but it is satisfiable exactly when your formula is. Open For SAT solvers to copy or download it in the standard DIMACS format used by MiniSat, Glucose, CaDiCaL and Kissat.

Frequently asked questions

Which operators can I use?

NOT: ' after a variable or bracket, or ! ¬ ~ before it. AND: writing variables next to each other, or · * & ∧ .. OR: + | ∨. XOR: ^ ⊕; XNOR ⊙. Implication: -> →. If and only if: <-> ↔ ==. NAND ↑ and NOR ↓. Note that ^ means XOR, as in programming; use ∧ or & for AND.

What order do the operators bind in?

From tightest to loosest: NOT, AND (and NAND), XOR (and XNOR), OR (and NOR), implication, if-and-only-if. Implication groups to the right, so A → B → C means A → (B → C). Use brackets when in doubt.

How are variable names read?

A variable is one letter, optionally followed by digits, so AB means A AND B and x1x2 means x1 AND x2. Upper and lower case are different variables. Up to 10 variables are supported, because the truth table doubles with each one (1,024 rows at 10).

Can I enter a truth table instead?

Yes, as a minterm list: Σm(1, 3, 5) + d(7) lists the rows where the function is 1 and the don't-care rows. Name the variables with a header such as F(A, B, C) = Σm(1, 3, 5). A maxterm list ΠM(0, 2, 4) works too.

Is my expression uploaded?

No. Everything is calculated in your browser. The Copy link button puts the expression in the part of the link after #, which browsers do not send to our server.

References

• W. V. Quine, “The problem of simplifying truth functions”, American Mathematical Monthly 59 (1952) 521–531.
• E. J. McCluskey, “Minimization of Boolean functions”, Bell System Technical Journal 35 (1956) 1417–1444.
• S. R. Petrick, “A direct determination of the irredundant forms of a Boolean function from the set of prime implicants”, AFCRC report TR-56-110 (1956).
• G. S. Tseitin, “On the complexity of derivation in propositional calculus”, Studies in Constructive Mathematics and Mathematical Logic 2 (1968) 115–125.