Skip to main content
⚡ Calmops
🤖 AI 🏗️ Architecture 🌐 Web 🗃️ Database ⚙️ DevOps 🌍 Network 💻 Programming 🧮 Algorithms 📐 Software Eng. ☁️ Cloud 🔒 Security 📈 Finance More →

What is a SAT Problem? A Complete Guide to Boolean Satisfiability

Created: January 23, 2026 AI/LLMs 10 min read

Introduction

SAT (short for Boolean Satisfiability Problem) is one of the most famous and fundamental problems in computer science, logic, and theoretical computing. Despite its simple definition, SAT has profound implications for computational complexity theory and practical applications ranging from circuit verification to artificial intelligence.

In this comprehensive guide, we’ll explore what SAT is, why it matters, how it’s solved in practice, and how it connects to real-world problems.

What is SAT? The Core Question

SAT asks a deceptively simple question:

Given a Boolean (true/false) formula made of variables and logical operators (AND, OR, NOT), is there any way to assign TRUE or FALSE to each variable so that the whole formula becomes TRUE?

The answer is binary:

  • If yes → the formula is satisfiable (SAT returns “yes” + typically one example assignment)
  • If no → the formula is unsatisfiable (no possible assignment makes it true)

This simplicity masks incredible depth. SAT is the canonical NP-complete problem, meaning it’s believed to be computationally hard in the worst case, yet modern SAT solvers can handle millions of variables in practice.

Simple Examples: Building Intuition

Let’s start with basic examples to build intuition:

Example 1: Tautology (Always True)

Formula: x ∨ ¬x (x OR NOT x)

This formula is always true regardless of x’s value:

  • If x = true: true ∨ false = true
  • If x = false: false ∨ true = true

Result: Satisfiable (trivially — any assignment works)

Example 2: Contradiction (Always False)

Formula: x ∧ ¬x (x AND NOT x)

This formula is always false:

  • If x = true: true ∧ false = false
  • If x = false: false ∧ true = false

Result: Unsatisfiable (no assignment works)

Example 3: Constrained Formula

Formula: (a ∨ b) ∧ (¬a ∨ ¬b)

This says: “at least one of a or b is true” AND “at least one of a or b is false”

This forces exactly one of a or b to be true:

  • a = true, b = false: (true ∨ false) ∧ (false ∨ true) = true ∧ true = true ✓
  • a = false, b = true: (false ∨ true) ∧ (true ∨ false) = true ∧ true = true ✓
  • a = true, b = true: (true ∨ true) ∧ (false ∨ false) = true ∧ false = false ✗
  • a = false, b = false: (false ∨ false) ∧ (true ∨ true) = false ∧ true = false ✗

Result: Satisfiable (with constraints on valid assignments)

Example 4: Three-Variable Formula

Formula: (a ∨ b ∨ ¬c) ∧ (¬a ∨ c) ∧ (b ∨ ¬c)

Let’s test a = true, b = false, c = true:

  • (true ∨ false ∨ false) = true ✓
  • (false ∨ true) = true ✓
  • (false ∨ false) = false ✗

Let’s test a = false, b = true, c = false:

  • (false ∨ true ∨ true) = true ✓
  • (true ∨ false) = true ✓
  • (true ∨ true) = true ✓

Result: Satisfiable (a = false, b = true, c = false works)

Conjunctive Normal Form (CNF): The Standard Representation

Modern SAT solvers almost exclusively work with formulas in Conjunctive Normal Form (CNF):

CNF = AND of many clauses, where each clause is OR of literals

A literal is either a variable or its negation. A clause is a disjunction (OR) of literals.

CNF Structure

(literal₁ ∨ literal₂ ∨ ... ∨ literalₙ) ∧
(literal₁ ∨ literal₂ ∨ ... ∨ literalₘ) ∧
...
(literal₁ ∨ literal₂ ∨ ... ∨ literalₚ)

Why CNF?

  1. Universality: Any Boolean formula can be converted to CNF
  2. Efficiency: SAT solvers are optimized for CNF structure
  3. Simplicity: Uniform representation makes algorithm design easier

CNF Example: 3-SAT

A 3-SAT instance has exactly 3 literals per clause:

(a ∨ ¬b ∨ c) ∧
(¬a ∨ b) ∧
(¬c ∨ ¬b)

Wait — the second clause has only 2 literals. That’s fine; 3-SAT means “at most 3 literals per clause.”

Can we satisfy all three clauses simultaneously?

Let’s try a = false, b = true, c = true:

  • (false ∨ false ∨ true) = true ✓
  • (true ∨ true) = true ✓
  • (false ∨ false) = false ✗

Let’s try a = true, b = false, c = true:

  • (true ∨ true ∨ true) = true ✓
  • (false ∨ false) = false ✗

Let’s try a = false, b = false, c = false:

  • (false ∨ true ∨ false) = true ✓
  • (true ∨ false) = true ✓
  • (true ∨ true) = true ✓

Result: Satisfiable (a = false, b = false, c = false works)

Converting Formulas to CNF

Any Boolean formula can be converted to CNF using logical equivalences:

De Morgan’s Laws

¬(A ∧ B) ≡ ¬A ∨ ¬B
¬(A ∨ B) ≡ ¬A ∧ ¬B

Distributivity

A ∨ (B ∧ C) ≡ (A ∨ B) ∧ (A ∨ C)
A ∧ (B ∨ C) ≡ (A ∧ B) ∨ (A ∧ C)

Example Conversion

Original: (a ∨ b) → c (implication)

Step 1: Eliminate implication (A → B ≡ ¬A ∨ B)

¬(a ∨ b) ∨ c

Step 2: Apply De Morgan’s law

(¬a ∧ ¬b) ∨ c

Step 3: Distribute OR over AND

(¬a ∨ c) ∧ (¬b ∨ c)

Result: CNF form with two clauses

Why SAT Matters: NP-Completeness

The Cook-Levin Theorem (1971)

SAT was the first problem proven to be NP-complete by Stephen Cook. This means:

  1. SAT is in NP: Given a proposed solution (assignment), we can verify it in polynomial time
  2. SAT is NP-hard: Every problem in NP can be reduced to SAT in polynomial time

What This Means

  • If we find a polynomial-time algorithm for SAT, we solve P vs NP (and win a $1 million Millennium Prize)
  • Most computer scientists believe P ≠ NP, meaning SAT is fundamentally hard
  • Yet modern SAT solvers are remarkably efficient on practical instances

The Complexity Hierarchy

P (polynomial time)
  ↓
NP (nondeterministic polynomial)
  ├─ NP-Complete (hardest in NP)
  │   ├─ SAT
  │   ├─ 3-SAT
  │   ├─ Clique
  │   ├─ Vertex Cover
  │   └─ Hamiltonian Cycle
  └─ NP-Hard (at least as hard as NP-Complete)

Real-World Applications of SAT

SAT’s theoretical importance is matched by practical utility:

1. Circuit Verification

Verify that a digital circuit behaves correctly:

  • Variables represent circuit inputs and internal signals
  • Clauses encode circuit logic gates
  • SAT solver checks if incorrect behavior is possible

2. Software Testing

Generate test cases that exercise specific code paths:

  • Variables represent input values
  • Clauses encode program constraints
  • SAT solver finds inputs that trigger bugs

3. Scheduling and Planning

Solve scheduling problems (job scheduling, timetabling):

  • Variables represent task assignments
  • Clauses encode constraints (no conflicts, deadlines, resources)
  • SAT solver finds valid schedules

4. Cryptography

Analyze cryptographic algorithms:

  • Variables represent key bits
  • Clauses encode encryption equations
  • SAT solver attempts to break encryption

5. Sudoku and Puzzles

Solve constraint satisfaction puzzles:

  • Variables represent cell values
  • Clauses encode Sudoku rules
  • SAT solver finds valid solutions

6. Graph Problems

Solve NP-complete graph problems:

  • Graph Coloring: Can we color a graph with k colors?
  • Clique: Does the graph contain a clique of size k?
  • Vertex Cover: Can we cover all edges with k vertices?

7. AI Reasoning and Planning

Automated reasoning in AI systems:

  • Variables represent propositions
  • Clauses encode knowledge and constraints
  • SAT solver performs logical inference

Modern SAT Solvers: From Theory to Practice

Despite SAT being NP-complete, modern SAT solvers are remarkably efficient:

Key Algorithms and Techniques

DPLL Algorithm (1962)

  • Systematic search with backtracking
  • Unit propagation: if a clause has one unassigned literal, set it to satisfy the clause
  • Pure literal elimination: if a variable appears only positive or only negative, set it accordingly

CDCL (Conflict-Driven Clause Learning) (1996)

  • Learns from conflicts to avoid redundant search
  • Analyzes conflicts and adds learned clauses
  • Dramatically improves performance

Local Search Heuristics

  • Random restarts to escape local plateaus
  • Variable selection heuristics (VSIDS: Variable State Independent Decaying Sum)
  • Clause weighting strategies
Solver Year Notable Features
MiniSat 2003 Influential, clean implementation
Glucose 2009 Improved clause learning
Kissat 2019 Modern, competitive
CaDiCaL 2019 Incremental solving
Lingeling 2010 Highly optimized

Performance in Practice

Modern SAT solvers can handle:

  • Millions of variables
  • Millions of clauses
  • Industrial instances in seconds to minutes

This is remarkable given the worst-case exponential complexity.

SAT Solver Example: Simple DPLL Implementation

Here’s a simplified SAT solver using the DPLL algorithm:

def dpll(clauses, assignment=None):
    """
    Simple DPLL SAT solver.
    Returns (satisfiable, assignment) tuple.
    """
    if assignment is None:
        assignment = {}
    
    # Simplify clauses with current assignment
    simplified = simplify_clauses(clauses, assignment)
    
    # Check for empty clause (unsatisfiable)
    if [] in simplified:
        return False, None
    
    # Check for empty clause list (satisfiable)
    if not simplified:
        return True, assignment
    
    # Unit propagation: find unit clauses
    unit_clause = find_unit_clause(simplified)
    if unit_clause:
        var = list(unit_clause)[0]
        new_assignment = assignment.copy()
        new_assignment[var] = True
        return dpll(clauses, new_assignment)
    
    # Pure literal elimination
    pure_var = find_pure_literal(simplified)
    if pure_var:
        new_assignment = assignment.copy()
        new_assignment[pure_var] = True
        return dpll(clauses, new_assignment)
    
    # Choose a variable and try both values
    var = choose_variable(simplified)
    
    # Try var = True
    new_assignment = assignment.copy()
    new_assignment[var] = True
    sat, result = dpll(clauses, new_assignment)
    if sat:
        return True, result
    
    # Try var = False
    new_assignment = assignment.copy()
    new_assignment[var] = False
    return dpll(clauses, new_assignment)

def simplify_clauses(clauses, assignment):
    """Remove satisfied clauses and false literals."""
    simplified = []
    for clause in clauses:
        new_clause = set()
        satisfied = False
        
        for literal in clause:
            var = abs(literal)
            if var in assignment:
                if (literal > 0 and assignment[var]) or \
                   (literal < 0 and not assignment[var]):
                    satisfied = True
                    break
            else:
                new_clause.add(literal)
        
        if not satisfied:
            simplified.append(new_clause)
    
    return simplified

def find_unit_clause(clauses):
    """Find a clause with exactly one literal."""
    for clause in clauses:
        if len(clause) == 1:
            return clause
    return None

def find_pure_literal(clauses):
    """Find a variable that appears only positive or only negative."""
    positive = set()
    negative = set()
    
    for clause in clauses:
        for literal in clause:
            if literal > 0:
                positive.add(literal)
            else:
                negative.add(-literal)
    
    pure_positive = positive - negative
    if pure_positive:
        return list(pure_positive)[0]
    
    pure_negative = negative - positive
    if pure_negative:
        return list(pure_negative)[0]
    
    return None

def choose_variable(clauses):
    """Choose a variable from remaining clauses."""
    for clause in clauses:
        if clause:
            return abs(list(clause)[0])
    return None

Practical SAT Solving: Using a Real Solver

In practice, you’d use an existing SAT solver. Here’s how to use PySAT:

from pysat.solvers import Glucose3

# Create solver instance
solver = Glucose3()

# Add clauses (CNF format: positive/negative integers)
# Clause: (a ∨ ¬b ∨ c) represented as [1, -2, 3]
solver.add_clause([1, -2, 3])
solver.add_clause([-1, 2])
solver.add_clause([-3, -2])

# Check satisfiability
if solver.solve():
    print("Satisfiable")
    model = solver.get_model()
    print(f"Assignment: {model}")
else:
    print("Unsatisfiable")

solver.delete()

Common SAT Problem Variants

MAX-SAT (Maximum Satisfiability)

Find an assignment that satisfies the maximum number of clauses (some clauses may be unsatisfiable).

Weighted MAX-SAT

Each clause has a weight; maximize total weight of satisfied clauses.

Partial MAX-SAT

Some clauses are hard (must be satisfied); others are soft (maximize satisfaction).

QBF (Quantified Boolean Formula)

Extends SAT with quantifiers (∀, ∃), making it PSPACE-complete.

Best Practices for SAT Solving

1. Problem Formulation

  • Encode your problem clearly in CNF
  • Minimize the number of variables and clauses
  • Use auxiliary variables to simplify complex constraints

2. Solver Selection

  • Use modern solvers (Kissat, CaDiCaL, Glucose)
  • Consider incremental solving if solving related instances
  • Profile solver performance on your instances

3. Preprocessing

  • Remove redundant clauses
  • Simplify unit clauses
  • Eliminate pure literals before solving

4. Debugging Unsatisfiable Instances

  • Use UNSAT cores to identify conflicting constraints
  • Relax constraints incrementally to find the source
  • Verify problem encoding

5. Performance Optimization

  • Use appropriate variable ordering heuristics
  • Enable clause learning
  • Consider parallel SAT solving for large instances

Conclusion

SAT is a deceptively simple yet profoundly important problem. It’s the canonical NP-complete problem, yet modern SAT solvers handle millions of variables efficiently. From circuit verification to AI reasoning, SAT’s applications span computer science.

Understanding SAT provides insight into computational complexity, algorithm design, and the practical limits of computation. Whether you’re solving puzzles, verifying systems, or exploring theoretical computer science, SAT is a fundamental tool worth mastering.

External Resources

Comments