Boolean satisfiability problem Created 2026-09-24 Updated 2026-10-18
The Boolean satisfiability problem asks whether a Boolean formula has an assignment making it true. A complete assignment is a Boolean valuation: it gives every Boolean variable a truth value, consistently at all occurrences. A satisfying assignment, also called a model of a Boolean formula, makes the entire Boolean formula true. A solver's answer SAT asserts that at least one satisfying assignment exists; UNSAT asserts that the input is an unsatisfiable Boolean formula. These are statements about existence, rather than the truth value under one particular Boolean valuation.
For conjunctive normal form, or CNF, write
Each Boolean literal is a Boolean variable or its logical negation. Each Boolean clause uses inclusive logical disjunction: one true Boolean literal suffices. The outer logical conjunction requires every Boolean clause to succeed under the same Boolean valuation. Choosing a different Boolean valuation for each Boolean clause would answer a different question.
Consider the original three-Boolean variable example
At the Boolean valuation , the Boolean literals in have values , those in have values , and those in have values . Every Boolean clause therefore has truth value one, so has truth value one: this is a satisfying assignment.
The complete truth table has Boolean valuations. Exactly two are satisfying assignments: and . In particular, satisfies the first two Boolean clauses but falsifies the third, so satisfying most Boolean clauses does not suffice for SAT. That different objective belongs to maximum satisfiability.
Figure 2.
All eight Boolean valuations of the original CNF example, with its two satisfying assignments highlighted
. Details.
A short proof of completeness avoids listing all eight rows. If , the Boolean clause forces , after which forces ; is already true. If , forces , after which forces ; is already true. These two cases exhaust the truth values of and produce precisely the two satisfying assignments above.
Verifying a satisfying assignment and finding a satisfying assignment are different tasks. Given a candidate, evaluate the Boolean formula once; finding a candidate requires choosing compatible truth values across all its Boolean clauses. The Cook-Levin theorem says that general SAT is NP-complete, even though a proposed satisfying assignment is efficiently checkable. Its proof encodes a bounded nondeterministic computation as a Boolean formula whose satisfying assignments describe accepting computations. Stephen A. Cook's 1971 paper established this connection between computational complexity theory and propositional logic.[ref]
A concrete use is checking finite configuration rules. Let mean that an optional feature is enabled, that a fallback is selected, and that the feature's required component is installed. Require a feature or fallback, require the component whenever the feature is enabled, and forbid using the fallback with that component. Logical implication rewrites the second rule as ; De Morgan's laws rewrite the third rule as . Their logical conjunction is exactly , so its two satisfying assignments give the two allowed configurations. The usefulness of SAT lies in expressing local rules uniformly while demanding one globally consistent Boolean valuation. The conclusion concerns exactly these encoded rules.
Complement of a set Created 2026-10-05 Updated 2026-10-14
The complement of a subset within a specified universal set contains exactly the set elements of excluded from :
Here depends on the chosen universal set. Within , taking a complement performs logical negation (NOT) on membership. Writing keeps the ambient set visible when there could be ambiguity.
For , , and :
If the universal set grows to , the same sets have different complements: and . In a database illustration, “records that fail this condition” therefore requires deciding which records are eligible to begin with; those eligible records form .
For subsets , De Morgan's laws exchange union and intersection when taking complements:
For the same example, failing both conditions leaves . Failing at least one condition leaves . This is useful for rewriting exclusion rules into separate membership tests. The symmetry is also pleasing: exchanging union with intersection turns one rule into its partner.
Figure 1.
De Morgan's laws: excluding a union means failing both tests, while excluding an intersection means failing at least one
. Details.
A brief membership proof works in classical propositional logic. For any , let mean and mean . The truth table below checks all four possibilities, with meaning true and false:
Each paired column agrees. Translating logical disjunction (OR), logical conjunction (AND), and logical negation (NOT) back into membership proves the two set equalities. For the general method of reducing set equalities to equivalences in propositional logic, see Lehman, Leighton and Meyer, Mathematics for Computer Science (2015), §4.1.5 and Problem 4.5.
A historical perspective appears in Augustus De Morgan's [ref]: he describes treating each name together with its contradictory name. In the membership viewpoint here, a set and its complement likewise pair a condition with its logical negation.
Countable intersection 2026-10-14
The countable intersection of a sequence of sets contains exactly the elements belonging to every set. De Morgan's laws identify its relative complement with the union of their complements.
For a Boolean function of input bits, define its De Morgan dual by complementing every input, applying , and complementing the output:
De Morgan's laws say that the De Morgan dual of logical conjunction is logical disjunction, and conversely. The constant zero Boolean function becomes constant one. This is different from merely negating the output: for AND, output logical negation gives one at , whereas the De Morgan dual gives zero there.
Taking the De Morgan dual twice restores the original Boolean function:
Here each input is complemented twice as well. For a Boolean formula built from AND, OR, NOT and constants, its De Morgan dual can therefore be obtained by exchanging AND with OR and zero with one throughout, leaving input names and NOT in place. A structural induction proves the rule: it holds for an input and each constant, De Morgan's laws handle the two binary logical connectives, and double logical negation handles NOT. This symmetry lets one translate a complex test systematically instead of guessing where its failures occur.
De Morgan's laws Created 2026-09-28 Updated 2026-10-14
De Morgan's laws exchange logical conjunction and logical disjunction when a logical negation moves across them:
Here denotes logical equivalence: the two propositional formulas agree under every Boolean valuation.[ref]
A complete verification uses the four rows of a truth table. In input order , both sides of the first logical equivalence have output sequence ; both sides of the second have . A proof in words is equally short: failure of “both” means at least one failure, whereas failure of “at least one” means both fail. The differing middle rows explain why simply pushing logical negation inward without changing AND to OR is wrong.
For the events in Boolean operations on events, the corresponding set identities are
One can prove these identities by checking an arbitrary set element : its two membership truth values obey De Morgan's laws. The same reasoning works for any two subsets of a common universal set.
Figure 1.
De Morgan's laws shade the same set whether a compound event is complemented first or its component events are complemented first
. Details.
For a nested program test, let mean “backup recent”, mean “backup verified”, and mean “manual override authorized”. Rejecting when neither an acceptable backup nor an override is present gives
The transformed condition reads “backup stale or unverified, and no override”. Apply the second of De Morgan's laws at the outside, then the first at the inner logical conjunction. For it rejects; changing only to one makes it accept. With Boolean operands in Python, not ((recent and verified) or override) and ((not recent) or (not verified)) and (not override) have the same result and inspect the operands in the same order, with the same skipped operands.
Dual Boolean function Created 2026-09-28 Updated 2026-10-03
The dual of a Boolean function is . Swapping AND with OR and zero with one in a monotone circuit for produces a circuit for by De Morgan's laws.
A failure-probability budget assigns nonnegative numbers to a finite or countable family of failure events in a common probability space, with verified bounds . The union bound guarantees that the probability of any failure is at most . By De Morgan's laws and the complement rule of probability, the probability that every requirement succeeds obeys
Thus guarantees simultaneous success with probability at least , even when all failure events depend on the same observations. The numbers are upper allowances; adding them is not a calculation of the exact failure probability.
For three requirements, give each a failure-probability budget . The total budget is , so simultaneous success has probability at least . On a sample space of twenty equally likely outcomes, let , , and . These disjoint events attain the budget and the success bound. If instead all three failure events equal , their individual probabilities are unchanged, but exact failure has probability and simultaneous success has probability . This second model shows how overlap can leave the guarantee conservative.
Figure 1.
A shared failure-probability budget covers both separate failures and one common failure
. The two panels each have twenty equally likely numbered outcomes. The blue, orange, and purple marks identify membership in , , and , respectively. Their individual probabilities are in both panels. The union has three outcomes on the left and one on the right, while the union bound is in both. The event of simultaneous success is the complement of an event of any failure and contains seventeen or nineteen outcomes. These are illustrative probability models, not measured failure rates. Details.
For requirements, an equal allocation is convenient; unequal allocations also work when some requirements are harder to satisfy. For infinitely many requirements indexed by , the allocation uses total budget by the geometric series. A fixed positive allowance for every requirement instead gives an infinite sum and no positive simultaneous-success guarantee from the union bound. The individual probability bounds must cover all the failure events being combined: omitting possible failure modes leaves the resulting guarantee about the listed requirements only. The same addition of error allowances underlies the Bonferroni correction in simultaneous hypothesis tests.
Logical equivalence 2026-10-14
Two propositional formulas are logically equivalent in classical propositional logic when they have the same truth value under every Boolean valuation. Identical output columns in a truth table prove logical equivalence; one differing row refutes it. De Morgan's laws give useful examples.
Negation Created 2026-09-24 Updated 2026-10-14
Logical negation exchanges zero and one: and . For a numerical bit , this is ; applying logical negation twice restores . It acts on the entire propositional formula in its scope. Parentheses therefore matter: says that neither condition holds, while also accepts every case where holds. At their values are zero and one.
On a set, logical negation becomes taking a complement in a fixed universal set. In Boolean operations on events, “not even” selects . “Not both even and at least four” selects ; it does not require both qualifications to fail. De Morgan's laws make the scope of these compound negations precise.
The AND-NOT circuit value problem belongs to P: validate the Boolean circuit and evaluate its gates in a topological ordering. Evaluation takes polynomial time even if its description is not already in a topological ordering.
For P-completeness we use logspace many-one reductions. Start from the supplied circuit value problem over the usual AND (logical conjunction), OR (logical disjunction) and NOT (negation) basis. Retain AND and NOT gates, and replace every OR gate by the De Morgan's laws gadget
This adds only a constant number of gates per old gate, preserves its truth value for all inputs and keeps the Boolean circuit acyclic. If the format includes constant source nodes, replace them by additional input nodes assigned fixed bits zero and one; these are inputs, not disallowed gates. Larger fan-in gates can first be replaced by binary trees of their inputs.
To output the new description, keep the old gate index and a constant-size gadget position, rescan old references when necessary, and assign consistent new indices to each gadget's terminal output. These counters and references occupy bits; the input assignment is copied with any constant-source bits appended. Thus the construction is a logspace many-one reduction preserving acceptance. Since Boolean circuit Value is P-complete under such reductions,
Context-free languages are closed under union: use a new start symbol with alternatives for two renamed context-free grammars. If they were closed under complement in , De Morgan's laws would give
contradicting the preceding intersection example. Therefore some CFL has a non-context-free complement. This is an existence argument; it does not assert that both complements of the particular are non-context-free.
A concrete choice is . Words outside form a regular language. Among words inside it, membership in means the first two counts or the last two counts differ. Each unequal-count comparison has a context-free grammar: for with , use , ; for , replace by . Append any number of 's, or prefix any number of 's for the analogous comparison. Taking these unions gives a context-free language whose complement is the non-context-free equal-three-count language. These productions are definitions of the example, not a restriction to strict Chomsky normal form.
As Boolean functions on edge indicators,
Thus is the dual Boolean function of the clique function. Given a monotone circuit for , swap every AND gate with an OR gate and swap the constants zero and one. De Morgan's laws show that the resulting circuit has the same size and computes . The lower bound from part (v), with the same choice of , therefore applies to .