#atoms#assignments#truthtable#sat-unsat#entailment#countmodels
Models & Satisfiability
Ready
Rules at a glance
Gates
¬ flips. ∧ needs both. ∨ needs at least one. → is only false for “true → false”. ↔ is true when both sides agree. Binding strength: ¬, ∧, ∨, →, ↔ (strongest first).
Four questions
Can the lamp be on? satisfiable. Always on? valid. Can it be off? refutable. Never on? unsatisfiable. φ ⊨ ψ: whenever φ is on, ψ is on too.
Counting a checklist
A clause with k of the n atoms switches the lamp off in exactly 2n−k settings. Add these up, then subtract the settings that two clauses switch off together (none if they need opposite values).