Propositional Logic

Propositional logic is the part of formal logic that studies whole statements, called propositions, each of which is simply true or false, and the ways of combining them with connectives such as and, or, not, implies and if-and-only-if. It has no machinery for looking inside a statement: "it is raining" is an indivisible atom, and the only question the logic asks is how the truth of a compound formula depends on the truth of its atoms. Its algebraic form goes back to George Boole's 1854 book on the laws of thought, and its first formal systems were part of the logical revival that began with Frege's 1879 Begriffsschrift.

The vocabulary is small: atomic propositions (p, q, r), the connectives (negation, conjunction, disjunction, implication, biconditional), and parentheses that fix how they nest. A formula such as (p ∧ q) → r is built from these pieces and gets its meaning from a valuation, an assignment of true or false to each atom. The meaning of every connective is fixed by a truth table, a device made standard in the early twentieth century by Emil Post's 1921 work and Wittgenstein's Tractatus. A formula with n atoms has 2^n possible valuations, so its full truth table has 2^n rows, and that exponential growth is the root of almost everything interesting about the subject. A formula true under every valuation is a tautology, one true under none is a contradiction, and one true under at least one is satisfiable.

Satisfiability, the question of whether any valuation makes a formula true, became the founding problem of computational complexity when Stephen Cook proved in 1971 that it is NP-complete. His paper "The Complexity of Theorem-Proving Procedures," presented at the ACM Symposium on Theory of Computing in 1971, showed that any problem solvable by a nondeterministic polynomial-time machine can be translated into a propositional formula that is satisfiable exactly when the machine accepts. Leonid Levin reached an equivalent result independently in the Soviet Union, which is why the result is called the Cook-Levin theorem. Richard Karp's 1972 paper then showed twenty-one other familiar problems to be equally hard. The practical lesson is that SAT is easy to verify and apparently hard to solve: checking a proposed valuation takes one pass through the formula, but no known algorithm avoids exponential worst-case time, and whether one exists is the P versus NP question.

Worst-case hardness did not stop people from building solvers, and the history of SAT solving is one of the great engineering surprises of computer science. The Davis-Putnam procedure of 1960, refined by Davis, Logemann and Loveland in 1962 into the DPLL algorithm, searches by assigning a variable, simplifying the formula by unit propagation, and backtracking on conflict. The next leap, conflict-driven clause learning, appeared in the GRASP solver of Marques-Silva and Sakallah in 1996 and was pushed to industrial strength by the Chaff solver in 2001, with its efficient watched-literal data structure and activity-based variable selection. Modern solvers routinely handle formulas with millions of variables and clauses, even though a handful of random-looking formulas of a few hundred variables can still defeat them.

The most commercially important use of SAT is in hardware design, where a chip's logic is itself a propositional formula. Equivalence checking asks whether two circuits compute the same function by asking whether a formula stating that they differ is unsatisfiable; bounded model checking, introduced by Biere, Cimatti, Clarke and Zhu in 1999, unrolls a design for k steps and asks a solver whether a property violation is reachable within that many steps. A satisfying valuation is then a concrete counterexample trace, which is far more useful to an engineer than a bare "no." The same encoding trick drives software verification, AI planning, scheduling, package dependency resolution and parts of cryptanalysis, and the solvers inside satisfiability modulo theories tools extend it with arithmetic and data structures.

Propositional logic is also the clean contrast case for richer logics: it is decidable, complete and cheap to reason about, precisely because it cannot say anything about objects. The statement "every man is mortal and Socrates is a man, so Socrates is mortal" cannot be captured, because the argument depends on quantifying over individuals, which is the territory of predicate logic. A common misconception is that NP-complete means unsolvable in practice; the reality is that structured instances arising from circuits and software often fall to modern solvers in seconds, while the worst case remains exponential. A second pitfall is confusing the connective "implies" with causation: p → q is false only when p is true and q is false, so a false premise implies anything.

Read propositional logic as the logic of true-or-false statements stripped to their connective skeleton: a system small enough to be decided by a truth table, yet rich enough that asking whether one formula can be satisfied turned out to be the hardest-looking problem in a vast family, and the engine of modern automated verification.