A logician wants to prove that from premises P₁ and P₂, conclusion C necessarily follows. She assumes ¬C alongside P₁ and P₂ and derives a contradiction. This refutation approach works because:
ADeriving a contradiction from ¬C proves that C is a tautology independently of any premises
BThe contradiction shows P₁ ∧ P₂ ∧ ¬C is unsatisfiable, which is equivalent to P₁ ∧ P₂ ⊨ C
CRefutation proofs are valid only in propositional logic and do not extend to first-order logic
DDeriving a contradiction from any set of assumptions proves that those assumptions are all true
Logical consequence (φ ⊨ ψ) holds if and only if φ ∧ ¬ψ is unsatisfiable — there is no interpretation making the premises true and the conclusion false. Refutation proofs exploit this equivalence directly: assume the negation of the conclusion, add it to the premises, and derive ⊥. If you succeed, you have shown the negated conclusion is incompatible with the premises, proving the original consequence.
Question 2 Multiple Choice
A propositional formula contains 20 distinct atomic variables. Checking its satisfiability by brute-force truth table requires how many rows?
A20 × 2 = 40 rows
B20² = 400 rows
C2²⁰ = 1,048,576 rows
D20! rows (factorial of 20)
Each atomic variable can independently be assigned true or false, giving 2 options per variable. For n independent variables, the number of distinct truth assignments is 2ⁿ. With 20 variables, that is 2²⁰ = 1,048,576 rows. This exponential blowup is precisely why SAT is computationally difficult in general — truth table enumeration is not a scalable algorithm.
Question 3 True / False
A formula is unsatisfiable if and only if its negation is a tautology.
TTrue
FFalse
Answer: True
If φ is unsatisfiable, it is false under every interpretation. Therefore ¬φ is true under every interpretation — a tautology. Conversely, if ¬φ is a tautology (true everywhere), then φ must be false everywhere — unsatisfiable. The duality between satisfiability and tautology mirrors the duality between ∃ and ∀: satisfiability says ∃ an interpretation making φ true; being a tautology says ∀ interpretations make φ true.
Question 4 True / False
Because SAT is NP-complete, modern SAT solvers cannot efficiently handle any practical satisfiability problem.
TTrue
FFalse
Answer: False
NP-completeness characterizes worst-case behavior, not typical behavior. Modern SAT solvers based on CDCL (conflict-driven clause learning) exploit the structure of practical problem instances — learned clauses, propagation, heuristic branching — to solve formulas with millions of variables in seconds. Industrial applications in hardware verification, planning, and cryptanalysis rely on this practical efficiency. Worst-case hardness and practical hardness are not the same thing.
Question 5 Short Answer
Explain the duality between satisfiability and logical consequence: how does proving that a formula is unsatisfiable allow you to establish that a consequence relationship holds?
Think about your answer, then reveal below.
Model answer: φ ⊨ ψ holds if and only if φ ∧ ¬ψ is unsatisfiable. If there is no interpretation making φ true while ψ is false, then every interpretation making φ true must also make ψ true — the definition of consequence. So to prove φ ⊨ ψ, it suffices to show φ ∧ ¬ψ has no model. This is why refutation-complete proof systems (like resolution) work by negating the conclusion and deriving a contradiction.
The duality runs deep: semantic consequence (a model-theoretic concept) and syntactic provability (a proof-theoretic concept) are connected through satisfiability. The completeness theorem for first-order logic says these two notions coincide: φ ⊨ ψ iff φ ⊢ ψ. Both sides can be reduced to unsatisfiability checks, which is why automated theorem provers almost universally work via refutation.