Logical equivalence, normal forms and satisfiability

Two formulas can look different and still say the same thing. Recognizing when that happens lets you simplify conditions in programs, design smaller circuits and transform problems into forms that algorithms can solve. This lesson defines tautologies, contradictions and logical equivalence, lists the standard equivalence laws, shows how to put any formula into a normal form, and introduces the satisfiability problem, one of the most important problems in computing.

Tautologies, contradictions and contingencies

A tautology is a formula that is true in every row of its truth table, whatever the values of its variables. The formula \(p \vee \neg p\) is the simplest example: every proposition is either true or false. A contradiction is false in every row, like \(p \wedge \neg p\). A formula that is true in some rows and false in others is a contingency. A formula is satisfiable if at least one row makes it true, so every tautology and every contingency is satisfiable, and only contradictions are not.

Logical equivalence

Two formulas \(A\) and \(B\) are logically equivalent, written \(A \equiv B\), if they have the same truth value in every row, that is, if \(A \longleftrightarrow B\) is a tautology. Equivalence is the logical version of equality in algebra: you can replace a formula by an equivalent one anywhere without changing the meaning of the whole.

The most direct way to prove an equivalence is to compare truth tables. That works well for two or three variables. A program can do the same check for any number of variables, as long as \(2^n\) rows is manageable.

from itertools import product

def equivalent(f, g, n):
    """True if functions f and g of n Booleans agree on every input."""
    return all(f(*v) == g(*v) for v in product([True, False], repeat=n))

imp = lambda a, b: (not a) or b
print("De Morgan 1:", equivalent(lambda p, q: not (p and q), lambda p, q: (not p) or (not q), 2))
print("De Morgan 2:", equivalent(lambda p, q: not (p or q), lambda p, q: (not p) and (not q), 2))
print("p->q vs ~p v q:", equivalent(imp, lambda p, q: (not p) or q, 2))
print("p->q vs q->p:", equivalent(imp, lambda p, q: imp(q, p), 2))
print("distribution:", equivalent(lambda p, q, r: p and (q or r),
                                  lambda p, q, r: (p and q) or (p and r), 3))

De Morgan 1: True
De Morgan 2: True
p->q vs ~p v q: True
p->q vs q->p: False
distribution: True

The standard equivalence laws

A small set of laws, each checkable by truth table, lets you transform formulas by algebra instead of tables. They mirror the laws of set operations you will meet in lesson 7, and the laws of Boolean algebra used in circuit design.

De Morgan's laws deserve special practice because they appear constantly in programming. The negation of a conjunction is the disjunction of the negations, and vice versa. In code, not (a and b) becomes (not a) or (not b). A loop that should continue while neither the end of the file has been reached nor an error has occurred can be written as while not (eof or error), or equivalently while not eof and not error.

A chain of equivalences like this is a proof. Each step must be justified by a law, and the laws themselves were proved by truth tables. For formulas with many variables, algebraic reasoning is far shorter than a truth table: a formula in 20 variables has over a million rows, but an equivalence proof might take five lines.

Normal forms

A normal form is a standard shape for formulas. Two are central. A literal is a variable or its negation, such as \(p\) or \(\neg q\). A clause is a disjunction of literals, such as \(p \vee \neg q \vee r\). A formula is in conjunctive normal form (CNF) if it is a conjunction of clauses: an AND of ORs. It is in disjunctive normal form (DNF) if it is a disjunction of conjunctions of literals: an OR of ANDs.

Every formula has an equivalent CNF and an equivalent DNF. DNF can be read straight off a truth table: for each row where the formula is true, write the conjunction of literals that describes that row, then join those conjunctions with OR. CNF comes from the false rows: for each false row, write the clause that rules out exactly that row, then join with AND.

from itertools import product

def dnf_from_table(f, names):
    terms = []
    for vals in product([True, False], repeat=len(names)):
        if f(*vals):
            lits = [n if v else "~" + n for n, v in zip(names, vals)]
            terms.append("(" + " & ".join(lits) + ")")
    return " | ".join(terms) if terms else "F"

def cnf_from_table(f, names):
    clauses = []
    for vals in product([True, False], repeat=len(names)):
        if not f(*vals):
            lits = ["~" + n if v else n for n, v in zip(names, vals)]
            clauses.append("(" + " | ".join(lits) + ")")
    return " & ".join(clauses) if clauses else "T"

majority = lambda p, q, r: (p + q + r) >= 2
print("DNF:", dnf_from_table(majority, "pqr"))
print("CNF:", cnf_from_table(majority, "pqr"))

DNF: (p & q & r) | (p & q & ~r) | (p & ~q & r) | (~p & q & r)
CNF: (~p | q | r) & (p | ~q | r) & (p | q | ~r) & (p | q | r)

Normal forms read straight from a table can be long, because they have one term per row. Simplification can shorten them: the majority function above is also \((p \wedge q) \vee (p \wedge r) \vee (q \wedge r)\). Finding the smallest equivalent formula is a hard problem in general; circuit designers use tools such as Karnaugh maps for small cases and specialized software for large ones.

You can also convert to CNF by algebra: replace \(\to\) and \(\longleftrightarrow\) using their definitions, push negations inward with De Morgan's laws and double negation until they sit only on variables, and then distribute \(\vee\) over \(\wedge\). The last step can make the formula grow exponentially, which is why practical tools use a cleverer method, the Tseitin transformation, that adds new variables and keeps the size linear.

Satisfiability

The satisfiability problem, called SAT, asks: given a formula, is there an assignment of truth values that makes it true? For a formula in \(n\) variables, the obvious method tries all \(2^n\) assignments. That is fine for 20 variables (about a million assignments) and impossible for 300, since \(2^{300}\) exceeds the number of atoms in the observable universe.

from itertools import product

# Clauses in CNF: each literal is +i for variable i, -i for its negation
clauses = [[1, 2], [-1, 3], [-2, -3], [-1, -2, 3], [2, 3]]
n = 3

def satisfies(assign, clauses):
    return all(any(assign[abs(l)] == (l > 0) for l in c) for c in clauses)

solutions = []
for vals in product([False, True], repeat=n):
    assign = {i + 1: v for i, v in enumerate(vals)}
    if satisfies(assign, clauses):
        solutions.append(vals)
print("assignments tried:", 2 ** n)
print("satisfying assignments (x1, x2, x3):", solutions)

assignments tried: 8
satisfying assignments (x1, x2, x3): [(False, True, False), (True, False, True)]

SAT matters far beyond logic puzzles. Scheduling exams so that no student has two at once, checking that a hardware design never reaches a bad state, finding a configuration of software packages whose version constraints are compatible, and solving Sudoku can all be written as SAT problems. Modern SAT solvers use clever search with conflict-driven clause learning and routinely solve industrial instances with millions of variables, even though no algorithm is known that solves every instance quickly.

In 1971, Stephen Cook of the University of Toronto proved that SAT is NP-complete: every problem whose solutions can be checked quickly can be translated into SAT. Leonid Levin proved a similar result independently in the Soviet Union. Whether SAT can always be solved in polynomial time is the famous P versus NP question, one of the Millennium Prize Problems. You will study NP-completeness in CMPUT-304 and CMPUT-474; for now, the key idea is that checking a proposed solution is easy (just evaluate the formula) while finding one may be hard.

Valid arguments

Equivalence also clarifies what makes an argument valid. An argument with premises \(P_1, \ldots, P_k\) and conclusion \(C\) is valid if \((P_1 \wedge \cdots \wedge P_k) \to C\) is a tautology: whenever all premises are true, the conclusion must be true. Validity is about form, not content. The argument if it is raining the ground is wet; it is raining; so the ground is wet has the valid form called modus ponens. The argument if it is raining the ground is wet; the ground is wet; so it is raining is invalid, because the ground could be wet for another reason. That error is called affirming the consequent.