CaDiCaL SAT Solver

A Modern SAT Solver Built for Speed and Simplicity

Course: Formal Methods (CS-320)

Introduction to CaDiCaL

• What: An open-source SAT solver that checks if a logical formula can be made true.
• Who: Created by Armin Biere and his team at the Johannes Kepler University Linz.
• Why: Designed to be easy to read and modify while still being one of the fastest solvers in the world.
• Language: Written in C++, MIT license, version 2.0.

What is SAT?

SAT (Boolean Satisfiability): Given a formula made of AND, OR, and NOT over true/false variables, can we find values that make the whole thing true?

Simple Example

c Two variables (x₁, x₂), two rules:
 Rule 1:  x₁ OR x₂      (at least one must be true)
 Rule 2:  NOT x₁         (x₁ must be false)

 Solution: x₁ = false, x₂ = true  ✓

Where is SAT Used?

• Hardware verification – checking if circuits work correctly
• Software testing – finding bugs automatically
• Scheduling – solving timetabling and planning problems

How SAT Solvers Work

SAT solvers have evolved from a simple approach to a much smarter one.

The Old Way: DPLL (1962)

• Pick a variable, guess true or false.
• If something goes wrong, undo the last guess and try the other value.
• Problem: It keeps making the same mistakes because it has no memory.

The Modern Way: CDCL (1996+)

• When a conflict happens, the solver analyzes why it went wrong.
• It learns a new rule (clause) so the same mistake never happens again.
• It jumps back directly to the real cause instead of undoing one step at a time.

CaDiCaL’s Core Loop

CaDiCaL repeats these four steps until it finds a solution or proves there is none.

Smart Search Strategies

CaDiCaL uses several tricks to search faster and avoid wasting time.

• Activity Scoring (EVSIDS): Variables that appear in recent conflicts get higher priority — the solver focuses on the “trouble spots” first.
• Phase Saving: When a variable is re-visited, it reuses its last assigned value instead of guessing fresh. This avoids redoing work.
• Restarts: Periodically wipe the current search and start again from scratch (keeping learned clauses). This prevents getting stuck.
• Inprocessing: Between restarts, CaDiCaL simplifies the formula — removing unnecessary variables and clauses to make future search faster.

Interactive CDCL Demonstration

Watch CDCL solve a small formula step-by-step. Click Step to advance or Auto to animate.

Interactive CDCL: An UNSAT Example

Now watch CDCL prove a formula has no solution — learning a clause, backjumping, and hitting a dead end.

Strengths & Weaknesses

Comparing CaDiCaL with PicoSAT across key aspects.

CaDiCaL Solves It Efficiently

CaDiCaL solved the problem significantly faster and more efficiently than PicoSAT.

CaDiCaL

PicoSAT

Summary & Reflections

Key takeaways from studying CaDiCaL and SAT solving.

• Clause learning is powerful: Instead of blindly guessing, CDCL learns from mistakes and never repeats the same conflict.
• Simplification matters: CaDiCaL’s inprocessing, simplifying the formula during the search, gives it a big edge over simpler solvers.
• Code quality counts: CaDiCaL shows that clean, readable code and top-tier performance are not mutually exclusive.
• Real-world impact: SAT solvers like CaDiCaL are used inside hardware verifiers, SMT solvers, and proof checkers worldwide.

Thank You & Questions

CaDiCaL is easy to understand and fast enough to win SAT competitions.