Satisfiability and Validity

Introduction

Satisfiability and validity are central concepts in formal logic that determine whether formulas are true, false, or contingent. Understanding these concepts is essential for:

• Logic programming and constraint solving
• Automated reasoning and theorem proving
• Formal verification
• Database query optimization
• Artificial intelligence

In this article, we’ll explore satisfiability and validity in depth.

Satisfiability

Definition

A formula is satisfiable if there exists at least one interpretation (model) that makes it true.

Formal Definition:

φ is satisfiable iff there exists a model M such that M ⊨ φ

Examples of Satisfiable Formulas

Simple Satisfiable Formula:

φ = P(x)
Satisfiable: Set P(x) = true

Complex Satisfiable Formula:

φ = (P ∨ Q) ∧ (¬P ∨ R)
Satisfiable: Set P = true, Q = false, R = true

Quantified Satisfiable Formula:

φ = ∃x P(x)
Satisfiable: Set P(a) = true for some element a

Satisfying Assignment

An assignment that makes a formula true is called a satisfying assignment.

Example:

Formula: (P ∨ Q) ∧ (¬P ∨ R)
Satisfying assignment: P = true, Q = false, R = true
Verification: (true ∨ false) ∧ (false ∨ true) = true ∧ true = true

Validity (Tautology)

Definition

A formula is valid (or a tautology) if it is true in all interpretations.

Formal Definition:

φ is valid (⊨ φ) iff for all models M: M ⊨ φ

Examples of Valid Formulas

Law of Excluded Middle:

φ = P ∨ ¬P
Valid: True regardless of P's value

Tautology:

φ = (P → Q) ∨ (Q → P)
Valid: True in all interpretations

Quantified Tautology:

φ = ∀x (P(x) ∨ ¬P(x))
Valid: True in all models

Verification of Validity

Truth Table Method:

For P ∨ ¬P:
P | ¬P | P ∨ ¬P
T | F  | T
F | T  | T
All rows true → Valid

Logical Reasoning:

For (P → Q) ∨ (Q → P):
Case 1: P is true
  If Q is true: P → Q is true, so disjunction is true
  If Q is false: Q → P is false, but P → Q is false, so... wait
  Actually: If P is true and Q is false, then P → Q is false
  But Q → P is true (false → true = true)
  So disjunction is true
Case 2: P is false
  P → Q is true (false → anything = true)
  So disjunction is true
All cases true → Valid

Unsatisfiability (Contradiction)

Definition

A formula is unsatisfiable (or a contradiction) if it is false in all interpretations.

Formal Definition:

φ is unsatisfiable iff for all models M: M ⊭ φ

Examples of Unsatisfiable Formulas

Simple Contradiction:

φ = P ∧ ¬P
Unsatisfiable: No assignment makes this true

Complex Contradiction:

φ = (P ∨ Q) ∧ ¬P ∧ ¬Q
Unsatisfiable: If P and Q are both false, then P ∨ Q is false

Quantified Contradiction:

φ = ∃x (P(x) ∧ ¬P(x))
Unsatisfiable: No element can satisfy both P and ¬P

Contingency

Definition

A formula is contingent if it is neither valid nor unsatisfiable (true in some models, false in others).

Formal Definition:

φ is contingent iff there exist models M₁, M₂ such that:
M₁ ⊨ φ and M₂ ⊭ φ

Examples of Contingent Formulas

Simple Contingent Formula:

φ = P
Contingent: True when P = true, false when P = false

Complex Contingent Formula:

φ = P ∧ Q
Contingent: True when both P and Q are true, false otherwise

Quantified Contingent Formula:

φ = ∃x P(x)
Contingent: True in models where P holds for some element,
           false in models where P holds for no element

Relationships Between Concepts

Satisfiability and Validity

Relationship:

Valid → Satisfiable (all valid formulas are satisfiable)
Satisfiable ↛ Valid (satisfiable formulas may not be valid)

Examples:

P ∨ ¬P: Valid and satisfiable
P: Satisfiable but not valid
P ∧ ¬P: Not satisfiable and not valid

Negation Relationships

Negation of Valid Formula:

If φ is valid, then ¬φ is unsatisfiable
⊨ φ ⟺ ⊭ ¬φ

Negation of Unsatisfiable Formula:

If φ is unsatisfiable, then ¬φ is valid
⊭ φ (for all models) ⟺ ⊨ ¬φ

Negation of Contingent Formula:

If φ is contingent, then ¬φ is also contingent

Logical Consequence and Validity

Definition

ψ is a logical consequence of φ (φ ⊨ ψ) if every model satisfying φ also satisfies ψ.

Formal Definition:

φ ⊨ ψ iff for all models M: if M ⊨ φ then M ⊨ ψ

Relationship to Validity

Theorem:

φ ⊨ ψ iff ⊨ (φ → ψ)
(ψ is consequence of φ iff φ → ψ is valid)

Examples

Example 1:

φ = ∀x P(x)
ψ = P(a)
φ ⊨ ψ (if all x satisfy P, then a satisfies P)

Example 2:

φ = P ∧ Q
ψ = P
φ ⊨ ψ (if both P and Q, then P)

SAT Problem

Definition

The Boolean Satisfiability Problem (SAT) asks: Given a Boolean formula, is it satisfiable?

Formal Definition:

SAT = {φ | φ is a satisfiable Boolean formula}

Significance

• NP-Complete: SAT is the first proven NP-complete problem
• Practical Importance: Many problems reduce to SAT
• Active Research: SAT solvers are highly optimized

SAT Solver Techniques

DPLL Algorithm:

1. Unit propagation: Assign variables in unit clauses
2. Pure literal elimination: Assign pure literals
3. Branching: Try both values for unassigned variable
4. Backtracking: Undo assignments if contradiction found

Modern Techniques:

- Conflict-driven clause learning (CDCL)
- Non-chronological backtracking
- Variable ordering heuristics
- Preprocessing and simplification

Glossary

• Satisfiable: True in at least one model
• Valid: True in all models
• Unsatisfiable: False in all models
• Contingent: True in some models, false in others
• Tautology: Valid formula
• Contradiction: Unsatisfiable formula
• Satisfying assignment: Assignment making formula true
• Logical consequence: Formula follows from another
• SAT problem: Satisfiability of Boolean formulas
• SAT solver: Algorithm solving SAT instances

Practice Problems

Problem 1: Satisfiability

Is the formula (P ∨ Q) ∧ (¬P ∨ ¬Q) satisfiable?

Solution:

Try P = true, Q = false:
(true ∨ false) ∧ (false ∨ true) = true ∧ true = true
Yes, satisfiable with assignment P = true, Q = false

Problem 2: Validity

Is the formula (P → Q) ∨ (Q → P) valid?

Solution:

Truth table:
P | Q | P→Q | Q→P | (P→Q)∨(Q→P)
T | T | T   | T   | T
T | F | F   | T   | T
F | T | T   | F   | T
F | F | T   | T   | T
All rows true → Valid

Problem 3: Unsatisfiability

Is the formula (P ∧ Q) ∧ (¬P ∨ ¬Q) unsatisfiable?

Solution:

For the formula to be true:
- P ∧ Q must be true: P = true, Q = true
- ¬P ∨ ¬Q must be true: At least one of P, Q is false
Contradiction: Can't have both P and Q true and at least one false
Unsatisfiable

Problem 4: Logical Consequence

Does P ∧ Q logically imply P ∨ Q?

Solution:

Check if (P ∧ Q) → (P ∨ Q) is valid:
If P ∧ Q is true, then both P and Q are true
Then P ∨ Q is true
So implication is valid
Yes, P ∧ Q ⊨ P ∨ Q

Related Resources

Online Platforms

• Stanford Encyclopedia of Philosophy - Logic articles
• Khan Academy Logic
• Coursera Logic Courses
• MIT OpenCourseWare
• Brilliant.org Logic

Interactive Tools

• Truth Table Generator - Generate truth tables
• SAT Solver - Solve SAT instances
• Formula Evaluator - Evaluate formulas
• Satisfiability Checker - Check satisfiability
• Validity Checker - Check validity

Recommended Books

• “Introduction to Logic” by Hurley - Comprehensive coverage
• “Language, Proof, and Logic” by Barwise & Etchemendy - Interactive approach
• “Symbolic Logic” by Lewis & Langford - Classic text
• “Logic: The Basics” by Priest - Accessible introduction
• “Handbook of Satisfiability” - Comprehensive SAT reference

Academic Journals

• Journal of Symbolic Logic
• Studia Logica
• Archive for Mathematical Logic
• Annals of Pure and Applied Logic
• Journal of Automated Reasoning

Software Tools

• SAT Solvers - Solve SAT problems
• Prolog - Logic programming
• Coq - Theorem prover
• Z3 - SMT solver
• Datalog - Logic database

Conclusion

Satisfiability and validity are fundamental concepts:

• Satisfiable formulas have at least one true interpretation
• Valid formulas are true in all interpretations
• Unsatisfiable formulas are false in all interpretations
• Contingent formulas are true in some, false in others
• SAT problem is NP-complete and practically important

Understanding these concepts is essential for logic, formal verification, and automated reasoning.

In the next article, we’ll explore completeness and soundness, which relate proof theory to model theory.

---

Next Article: Completeness and Soundness

Previous Article: Model Theory Basics