diff --git a/docs/paper/reductions.typ b/docs/paper/reductions.typ
index c60593ad..b6dc7732 100644
--- a/docs/paper/reductions.typ
+++ b/docs/paper/reductions.typ
@@ -9335,6 +9335,23 @@ where $P$ is a penalty weight large enough that any constraint violation costs m
   _Solution extraction._ Return the values of the circuit input variables $x_1, dots, x_n$.
 ]
 
+#reduction-rule("CircuitSAT", "Satisfiability")[
+  The Tseitin transformation converts a boolean circuit into an equisatisfiable CNF formula. Each gate $g$ with output $v$ is replaced by a small set of definitional clauses encoding $v arrow.l.r.double f(a,b)$, where $f$ is the gate function. The conjunction of all definitional clauses is satisfiable iff the original circuit is satisfiable.
+][
+  _Construction._ Assign SAT variable indices $1, dots, n$ to circuit variables. Walk each assignment's expression tree recursively, introducing a fresh variable for each gate:
+  - *AND($a, b$):* fresh $v$; clauses $(overline(v) or a)$, $(overline(v) or b)$, $(v or overline(a) or overline(b))$.
+  - *OR($a, b$):* fresh $v$; clauses $(v or overline(a))$, $(v or overline(b))$, $(overline(v) or a or b)$.
+  - *NOT($a$):* fresh $v$; clauses $(overline(v) or overline(a))$, $(v or a)$.
+  - *XOR($a, b$):* fresh $v$; four clauses enforcing $v arrow.l.r.double a xor b$.
+  - *Const(true/false):* fresh $v$; unit clause $[v]$ or $[overline(v)]$.
+
+  For each assignment with root variable $r$ and output $o$: add $(overline(o) or r)$ and $(o or overline(r))$.
+
+  Multi-input gates are folded as binary trees.
+
+  _Correctness._ ($arrow.r.double$) A satisfying circuit assignment, extended with correct gate outputs, satisfies all definitional clauses. ($arrow.l.double$) Any SAT solution restricted to circuit variables satisfies the circuit. _Solution extraction._ Return the first $n$ SAT variables corresponding to circuit variables.
+]
+
 #let cs_sg = load-example("CircuitSAT", "SpinGlass")
 #let cs_sg_sol = cs_sg.solutions.at(0)
 #reduction-rule("CircuitSAT", "SpinGlass",
diff --git a/src/rules/circuitsat_satisfiability.rs b/src/rules/circuitsat_satisfiability.rs
new file mode 100644
index 00000000..946e46e4
--- /dev/null
+++ b/src/rules/circuitsat_satisfiability.rs
@@ -0,0 +1,252 @@
+//! Reduction from CircuitSAT to Satisfiability via the Tseitin transformation.
+//!
+//! Each gate in the boolean circuit is converted to definitional CNF clauses
+//! that preserve satisfiability. The resulting SAT instance has one variable
+//! per circuit variable plus auxiliary variables for intermediate gate outputs.
+
+use crate::models::formula::{Assignment, BooleanExpr, BooleanOp, CNFClause, CircuitSAT, Satisfiability};
+use crate::reduction;
+use crate::rules::traits::{ReduceTo, ReductionResult};
+use std::collections::HashMap;
+
+/// Result of reducing CircuitSAT to Satisfiability.
+#[derive(Debug, Clone)]
+pub struct ReductionCircuitSATToSatisfiability {
+    target: Satisfiability,
+    /// Maps circuit variable name -> SAT variable index (1-indexed).
+    var_map: HashMap<String, i32>,
+    /// Sorted circuit variable names (defines the circuit config ordering).
+    circuit_var_names: Vec<String>,
+}
+
+impl ReductionResult for ReductionCircuitSATToSatisfiability {
+    type Source = CircuitSAT;
+    type Target = Satisfiability;
+
+    fn target_problem(&self) -> &Satisfiability {
+        &self.target
+    }
+
+    fn extract_solution(&self, target_solution: &[usize]) -> Vec<usize> {
+        // The circuit variable names define the config ordering.
+        // For each circuit variable, look up its SAT index and read the value.
+        self.circuit_var_names
+            .iter()
+            .map(|name| {
+                let sat_idx = self.var_map[name]; // 1-indexed
+                target_solution[(sat_idx as usize) - 1]
+            })
+            .collect()
+    }
+}
+
+/// State for the Tseitin transformation.
+struct TseitinBuilder {
+    var_map: HashMap<String, i32>,
+    next_var: i32,
+    clauses: Vec<CNFClause>,
+}
+
+impl TseitinBuilder {
+    fn new(circuit_var_names: &[String]) -> Self {
+        let mut var_map = HashMap::new();
+        let mut next_var = 1i32;
+        // Assign indices to circuit variables first, preserving sorted order.
+        for name in circuit_var_names {
+            var_map.insert(name.clone(), next_var);
+            next_var += 1;
+        }
+        Self {
+            var_map,
+            next_var,
+            clauses: Vec::new(),
+        }
+    }
+
+    fn get_var(&mut self, name: &str) -> i32 {
+        if let Some(&v) = self.var_map.get(name) {
+            v
+        } else {
+            let v = self.next_var;
+            self.var_map.insert(name.to_string(), v);
+            self.next_var += 1;
+            v
+        }
+    }
+
+    fn fresh_var(&mut self) -> i32 {
+        let v = self.next_var;
+        self.next_var += 1;
+        v
+    }
+
+    /// Walk the expression tree, creating definitional clauses.
+    /// Returns the SAT variable index representing this subexpression.
+    fn tseitin(&mut self, expr: &BooleanExpr) -> i32 {
+        match &expr.op {
+            BooleanOp::Var(name) => self.get_var(name),
+            BooleanOp::Const(value) => {
+                let v = self.fresh_var();
+                if *value {
+                    self.clauses.push(CNFClause::new(vec![v]));
+                } else {
+                    self.clauses.push(CNFClause::new(vec![-v]));
+                }
+                v
+            }
+            BooleanOp::Not(inner) => {
+                let a = self.tseitin(inner);
+                let v = self.fresh_var();
+                // v <=> NOT a
+                self.clauses.push(CNFClause::new(vec![-v, -a]));
+                self.clauses.push(CNFClause::new(vec![v, a]));
+                v
+            }
+            BooleanOp::And(children) => {
+                let child_vars: Vec<i32> = children.iter().map(|c| self.tseitin(c)).collect();
+                if child_vars.len() == 1 {
+                    return child_vars[0];
+                }
+                // Build binary tree of AND gates
+                let mut result = child_vars[0];
+                for &b in &child_vars[1..] {
+                    let a = result;
+                    let v = self.fresh_var();
+                    // v <=> a AND b
+                    self.clauses.push(CNFClause::new(vec![-v, a]));
+                    self.clauses.push(CNFClause::new(vec![-v, b]));
+                    self.clauses.push(CNFClause::new(vec![v, -a, -b]));
+                    result = v;
+                }
+                result
+            }
+            BooleanOp::Or(children) => {
+                let child_vars: Vec<i32> = children.iter().map(|c| self.tseitin(c)).collect();
+                if child_vars.len() == 1 {
+                    return child_vars[0];
+                }
+                // Build binary tree of OR gates
+                let mut result = child_vars[0];
+                for &b in &child_vars[1..] {
+                    let a = result;
+                    let v = self.fresh_var();
+                    // v <=> a OR b
+                    self.clauses.push(CNFClause::new(vec![v, -a]));
+                    self.clauses.push(CNFClause::new(vec![v, -b]));
+                    self.clauses.push(CNFClause::new(vec![-v, a, b]));
+                    result = v;
+                }
+                result
+            }
+            BooleanOp::Xor(children) => {
+                let child_vars: Vec<i32> = children.iter().map(|c| self.tseitin(c)).collect();
+                if child_vars.len() == 1 {
+                    return child_vars[0];
+                }
+                // Build binary tree of XOR gates
+                let mut result = child_vars[0];
+                for &b in &child_vars[1..] {
+                    let a = result;
+                    let v = self.fresh_var();
+                    // v <=> a XOR b
+                    self.clauses.push(CNFClause::new(vec![-v, -a, -b]));
+                    self.clauses.push(CNFClause::new(vec![-v, a, b]));
+                    self.clauses.push(CNFClause::new(vec![v, -a, b]));
+                    self.clauses.push(CNFClause::new(vec![v, a, -b]));
+                    result = v;
+                }
+                result
+            }
+        }
+    }
+
+    fn process_assignment(&mut self, assign: &Assignment) {
+        let root_var = self.tseitin(&assign.expr);
+        // Each output must equal the expression result
+        for out_name in &assign.outputs {
+            let out_var = self.get_var(out_name);
+            // out_var <=> root_var
+            self.clauses.push(CNFClause::new(vec![-out_var, root_var]));
+            self.clauses.push(CNFClause::new(vec![out_var, -root_var]));
+        }
+    }
+
+    fn num_vars(&self) -> usize {
+        (self.next_var - 1) as usize
+    }
+}
+
+#[reduction(
+    overhead = {
+        num_vars = "num_variables + num_assignments",
+        num_clauses = "3 * num_assignments + num_variables",
+    }
+)]
+impl ReduceTo<Satisfiability> for CircuitSAT {
+    type Result = ReductionCircuitSATToSatisfiability;
+
+    fn reduce_to(&self) -> Self::Result {
+        let circuit_var_names: Vec<String> = self.variable_names().to_vec();
+
+        let mut builder = TseitinBuilder::new(&circuit_var_names);
+
+        for assign in &self.circuit().assignments {
+            builder.process_assignment(assign);
+        }
+
+        let num_vars = builder.num_vars();
+        let target = Satisfiability::new(num_vars, builder.clauses.clone());
+
+        ReductionCircuitSATToSatisfiability {
+            target,
+            var_map: builder.var_map,
+            circuit_var_names,
+        }
+    }
+}
+
+#[cfg(feature = "example-db")]
+pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
+    use crate::export::SolutionPair;
+    use crate::models::formula::{BooleanExpr, Circuit};
+
+    vec![crate::example_db::specs::RuleExampleSpec {
+        id: "circuitsat_to_satisfiability",
+        build: || {
+            // c = x AND y, d = c OR z
+            let circuit = Circuit::new(vec![
+                Assignment::new(
+                    vec!["c".to_string()],
+                    BooleanExpr::and(vec![BooleanExpr::var("x"), BooleanExpr::var("y")]),
+                ),
+                Assignment::new(
+                    vec!["d".to_string()],
+                    BooleanExpr::or(vec![BooleanExpr::var("c"), BooleanExpr::var("z")]),
+                ),
+            ]);
+            let source = CircuitSAT::new(circuit);
+
+            // Find a valid solution pair by brute force
+            let reduction = <CircuitSAT as ReduceTo<Satisfiability>>::reduce_to(&source);
+            let solver = crate::solvers::BruteForce::new();
+            let target_solutions = solver.find_all_witnesses(reduction.target_problem());
+            let target_config = target_solutions
+                .into_iter()
+                .next()
+                .expect("YES instance must have a solution");
+            let source_config = reduction.extract_solution(&target_config);
+
+            crate::example_db::specs::rule_example_with_witness::<_, Satisfiability>(
+                source,
+                SolutionPair {
+                    source_config,
+                    target_config,
+                },
+            )
+        },
+    }]
+}
+
+#[cfg(test)]
+#[path = "../unit_tests/rules/circuitsat_satisfiability.rs"]
+mod tests;
diff --git a/src/rules/mod.rs b/src/rules/mod.rs
index fabfa8c2..33054685 100644
--- a/src/rules/mod.rs
+++ b/src/rules/mod.rs
@@ -9,6 +9,7 @@ pub use cost::{
 pub use registry::{EdgeCapabilities, ReductionEntry, ReductionOverhead};
 
 pub(crate) mod circuit_spinglass;
+pub(crate) mod circuitsat_satisfiability;
 mod closestvectorproblem_qubo;
 pub(crate) mod coloring_qubo;
 pub(crate) mod exactcoverby3sets_maximumsetpacking;
@@ -297,6 +298,7 @@ pub use traits::{
 pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
     let mut specs = Vec::new();
     specs.extend(circuit_spinglass::canonical_rule_example_specs());
+    specs.extend(circuitsat_satisfiability::canonical_rule_example_specs());
     specs.extend(exactcoverby3sets_staffscheduling::canonical_rule_example_specs());
     specs.extend(closestvectorproblem_qubo::canonical_rule_example_specs());
     specs.extend(coloring_qubo::canonical_rule_example_specs());
diff --git a/src/unit_tests/example_db.rs b/src/unit_tests/example_db.rs
index 157a9649..6850eaa4 100644
--- a/src/unit_tests/example_db.rs
+++ b/src/unit_tests/example_db.rs
@@ -282,6 +282,30 @@ fn test_build_rule_db_has_unique_structural_keys() {
     }
 }
 
+#[test]
+fn test_find_rule_example_circuitsat_to_satisfiability() {
+    let source = ProblemRef {
+        name: "CircuitSAT".to_string(),
+        variant: BTreeMap::new(),
+    };
+    let target = ProblemRef {
+        name: "Satisfiability".to_string(),
+        variant: BTreeMap::new(),
+    };
+
+    let example = find_rule_example(&source, &target).expect("CircuitSAT -> SAT example exists");
+    assert_eq!(example.source.problem, "CircuitSAT");
+    assert_eq!(example.target.problem, "Satisfiability");
+    assert!(
+        example.source.instance.get("circuit").is_some(),
+        "CircuitSAT source should have circuit field"
+    );
+    assert!(
+        example.target.instance.get("clauses").is_some(),
+        "Satisfiability target should have clauses field"
+    );
+}
+
 #[test]
 fn test_find_rule_example_rejects_composed_path_pairs() {
     let source = ProblemRef {
diff --git a/src/unit_tests/rules/analysis.rs b/src/unit_tests/rules/analysis.rs
index a12dd4a2..f29c732f 100644
--- a/src/unit_tests/rules/analysis.rs
+++ b/src/unit_tests/rules/analysis.rs
@@ -261,6 +261,8 @@ fn test_find_dominated_rules_returns_known_set() {
         ),
         // ExactCoverBy3Sets → MaxSetPacking → ILP is better than direct ExactCoverBy3Sets → ILP
         ("ExactCoverBy3Sets", "ILP {variable: \"bool\"}"),
+        // CircuitSAT → SAT → NAESAT → ILP is better than direct CircuitSAT → ILP
+        ("CircuitSAT", "ILP {variable: \"bool\"}"),
     ]
     .into_iter()
     .collect();
diff --git a/src/unit_tests/rules/circuitsat_satisfiability.rs b/src/unit_tests/rules/circuitsat_satisfiability.rs
new file mode 100644
index 00000000..0af54c66
--- /dev/null
+++ b/src/unit_tests/rules/circuitsat_satisfiability.rs
@@ -0,0 +1,153 @@
+use super::*;
+use crate::models::formula::{
+    Assignment, BooleanExpr, Circuit, CircuitSAT, Satisfiability,
+};
+use crate::rules::test_helpers::assert_satisfaction_round_trip_from_satisfaction_target;
+use crate::rules::ReduceTo;
+use crate::solvers::BruteForce;
+use crate::traits::Problem;
+
+/// YES instance: c = x AND y, d = c OR z (5 circuit vars, satisfiable)
+fn make_yes_instance() -> CircuitSAT {
+    let circuit = Circuit::new(vec![
+        Assignment::new(
+            vec!["c".to_string()],
+            BooleanExpr::and(vec![BooleanExpr::var("x"), BooleanExpr::var("y")]),
+        ),
+        Assignment::new(
+            vec!["d".to_string()],
+            BooleanExpr::or(vec![BooleanExpr::var("c"), BooleanExpr::var("z")]),
+        ),
+    ]);
+    CircuitSAT::new(circuit)
+}
+
+/// NO instance: c = x AND y, d = NOT(c), force c = d (contradictory)
+fn make_no_instance() -> CircuitSAT {
+    let circuit = Circuit::new(vec![
+        Assignment::new(
+            vec!["c".to_string()],
+            BooleanExpr::and(vec![BooleanExpr::var("x"), BooleanExpr::var("y")]),
+        ),
+        Assignment::new(
+            vec!["d".to_string()],
+            BooleanExpr::not(BooleanExpr::var("c")),
+        ),
+        // Force c = d (contradicts d = NOT(c))
+        Assignment::new(
+            vec!["c".to_string()],
+            BooleanExpr::var("d"),
+        ),
+    ]);
+    CircuitSAT::new(circuit)
+}
+
+#[test]
+fn test_circuitsat_to_satisfiability_closed_loop() {
+    let source = make_yes_instance();
+    let result = ReduceTo::<Satisfiability>::reduce_to(&source);
+    assert_satisfaction_round_trip_from_satisfaction_target(
+        &source,
+        &result,
+        "CircuitSAT->Satisfiability closed loop",
+    );
+}
+
+#[test]
+fn test_circuitsat_to_satisfiability_infeasible() {
+    let source = make_no_instance();
+    let result = ReduceTo::<Satisfiability>::reduce_to(&source);
+    let solver = BruteForce::new();
+    let target_solutions = solver.find_all_witnesses(result.target_problem());
+    assert!(
+        target_solutions.is_empty(),
+        "Infeasible CircuitSAT -> Satisfiability should have no solutions"
+    );
+}
+
+#[test]
+fn test_circuitsat_to_satisfiability_structure() {
+    let source = make_yes_instance();
+    let result = ReduceTo::<Satisfiability>::reduce_to(&source);
+    let target = result.target_problem();
+
+    // Circuit has 5 variables: c, d, x, y, z
+    assert_eq!(source.num_variables(), 5);
+
+    // Target should have at least as many variables as circuit
+    assert!(
+        target.num_vars() >= source.num_variables(),
+        "SAT should have at least as many vars as CircuitSAT: {} >= {}",
+        target.num_vars(),
+        source.num_variables()
+    );
+
+    // Target should have clauses
+    assert!(
+        target.num_clauses() > 0,
+        "SAT should have at least one clause"
+    );
+}
+
+#[test]
+fn test_circuitsat_to_satisfiability_solution_extraction() {
+    let source = make_yes_instance();
+    let result = ReduceTo::<Satisfiability>::reduce_to(&source);
+    let solver = BruteForce::new();
+    let target_solutions = solver.find_all_witnesses(result.target_problem());
+
+    assert!(
+        !target_solutions.is_empty(),
+        "YES instance should have solutions"
+    );
+
+    // Every extracted solution must be a valid circuit assignment
+    for target_sol in &target_solutions {
+        let source_sol = result.extract_solution(target_sol);
+        assert_eq!(
+            source_sol.len(),
+            source.num_variables(),
+            "Extracted solution should have one value per circuit variable"
+        );
+        let source_val = source.evaluate(&source_sol);
+        assert!(
+            source_val.0,
+            "Extracted solution should satisfy the circuit"
+        );
+    }
+}
+
+#[test]
+fn test_circuitsat_to_satisfiability_xor_gate() {
+    // Test XOR gate: c = x XOR y
+    let circuit = Circuit::new(vec![Assignment::new(
+        vec!["c".to_string()],
+        BooleanExpr::xor(vec![BooleanExpr::var("x"), BooleanExpr::var("y")]),
+    )]);
+    let source = CircuitSAT::new(circuit);
+    let result = ReduceTo::<Satisfiability>::reduce_to(&source);
+    assert_satisfaction_round_trip_from_satisfaction_target(
+        &source,
+        &result,
+        "CircuitSAT->Satisfiability XOR gate",
+    );
+}
+
+#[test]
+fn test_circuitsat_to_satisfiability_constant_gates() {
+    // Test with constants: c = true, d = c AND x
+    let circuit = Circuit::new(vec![
+        Assignment::new(vec!["c".to_string()], BooleanExpr::constant(true)),
+        Assignment::new(
+            vec!["d".to_string()],
+            BooleanExpr::and(vec![BooleanExpr::var("c"), BooleanExpr::var("x")]),
+        ),
+    ]);
+    let source = CircuitSAT::new(circuit);
+    let result = ReduceTo::<Satisfiability>::reduce_to(&source);
+    assert_satisfaction_round_trip_from_satisfaction_target(
+        &source,
+        &result,
+        "CircuitSAT->Satisfiability constant gates",
+    );
+}