diff --git a/docs/paper/reductions.typ b/docs/paper/reductions.typ
index 88cd07556..200184038 100644
--- a/docs/paper/reductions.typ
+++ b/docs/paper/reductions.typ
@@ -13922,6 +13922,66 @@ The following reductions to Integer Linear Programming are straightforward formu
   _Solution extraction._ Sort tasks by their completion times $C_j$ and encode that order back into the source schedule representation.
 ]
 
+#let hc_sat = load-example("HamiltonianCircuit", "Satisfiability")
+#let hc_sat_sol = hc_sat.solutions.at(0)
+#let hc_sat_n = graph-num-vertices(hc_sat.source.instance)
+#let hc_sat_edges = hc_sat.source.instance.graph.edges
+#let hc_sat_clauses = hc_sat.target.instance.clauses
+#let hc_sat_num_literals = hc_sat_clauses.map(c => c.literals.len()).sum()
+#let hc_sat_var(vertex, position) = vertex * hc_sat_n + position + 1
+#let hc_sat_nonedge_u = hc_sat_sol.source_config.at(0)
+#let hc_sat_nonedge_v = hc_sat_sol.source_config.at(3)
+#let hc_sat_forbidden = (
+  -hc_sat_var(hc_sat_nonedge_u, 0),
+  -hc_sat_var(hc_sat_nonedge_v, 1),
+)
+#reduction-rule("HamiltonianCircuit", "Satisfiability",
+  example: true,
+  example-caption: [Five-cycle plus one chord ($n = #hc_sat_n$, $|E| = #hc_sat_edges.len()$)],
+  extra: [
+    #pred-commands(
+      "pred create --example " + problem-spec(hc_sat.source) + " -o hc.json",
+      "pred reduce hc.json --to " + target-spec(hc_sat) + " -o bundle.json",
+      "pred solve bundle.json",
+      "pred evaluate hc.json --config " + hc_sat_sol.source_config.map(str).join(","),
+    )
+
+    *Step 1 -- Read the source circuit instance.* The canonical fixture has $#hc_sat_n$ vertices and edges #hc_sat_edges.map(e => $(#e.at(0), #e.at(1))$).join(", "). Its stored circuit is $[#hc_sat_sol.source_config.map(str).join(", ")]$, with the closing edge from $#hc_sat_sol.source_config.last()$ back to $#hc_sat_sol.source_config.first()$.
+
+    *Step 2 -- Build the position matrix.* Introduce one variable per vertex-position pair, using the 1-based SAT literal $x_(v,p) arrow.r v n + p + 1$. Thus the fixture's $#hc_sat_n times #hc_sat_n$ matrix contains $#hc_sat.target.instance.num_vars$ variables. The target configuration
+    $ (#hc_sat_sol.target_config.map(str).join(", ")) $
+    is the diagonal permutation matrix: $x_(v,v) = 1$ for every fixture vertex $v$.
+
+    *Step 3 -- Force a permutation.* Each of the $#hc_sat_n$ positions gets one at-least-one clause and #(hc_sat_n * (hc_sat_n - 1) / 2) pairwise at-most-one clauses. The same clauses are added for each of the $#hc_sat_n$ vertices across all positions. These two exactly-one families therefore contribute #(2 * hc_sat_n) long clauses and #(hc_sat_n * hc_sat_n * (hc_sat_n - 1)) binary clauses.
+
+    *Step 4 -- Forbid impossible cyclic successors.* For each position $p$, let $q = (p + 1) mod n$. Whenever $u = v$ or ${u,v} in.not E$, add $not x_(u,p) or not x_(v,q)$. In the fixture, vertices $#hc_sat_nonedge_u$ and $#hc_sat_nonedge_v$ are not adjacent, so positions 0 and 1 give the target clause $(#hc_sat_forbidden.map(str).join(", "))$, namely $not x_(#hc_sat_nonedge_u,0) or not x_(#hc_sat_nonedge_v,1)$. The target has $#hc_sat_clauses.len()$ clauses and $#hc_sat_num_literals$ literal occurrences in total.
+
+    *Step 5 -- Verify and extract the circuit.* The diagonal assignment selects consecutive pairs $(0,1), (1,2), (2,3), (3,4)$ and the cyclic pair $(4,0)$ from the fixture edge list, so it satisfies every forbidden-successor clause. Reading the unique true vertex in positions $0, dots, #(hc_sat_n - 1)$ recovers $[#hc_sat_sol.source_config.map(str).join(", ")]$, and the final edge closes the Hamiltonian circuit.
+
+    *Multiplicity:* The fixture stores one canonical SAT witness. Its five-cycle has five choices of starting position and two traversal directions, producing $5 times 2 = 10$ satisfying position matrices. The extra chord does not create another Hamiltonian cycle: using it would trap vertex 1 in the triangle on vertices 0, 1, and 2, leaving vertices 3 and 4 outside the circuit.
+  ],
+)[
+  @VelevGao2009 This $O(n^3)$ reduction uses the absolute vertex-position encoding for Hamiltonian cycles. It constructs an $n times n$ Boolean matrix $x_(v,p)$ and CNF clauses that make the matrix a permutation and allow only graph edges between cyclically consecutive positions. For $n < 3$, it instead emits the fixed contradiction $(z) and (not z)$.
+][
+  _Construction._ Let $G = (V,E)$ be a simple undirected graph with $V = {0, dots, n - 1}$. If $n < 3$, output the two unit clauses $(z)$ and $(not z)$. Otherwise, for every vertex $v in V$ and position $p in {0, dots, n - 1}$ introduce a Boolean variable $x_(v,p)$, where $x_(v,p) = 1$ means that vertex $v$ occupies position $p$ of the cyclic ordering. The implementation assigns it the 1-based SAT literal $v n + p + 1$.
+
+  For each position $p$, require exactly one vertex:
+  $ (or.big_(v in V) x_(v,p)) quad and quad (not x_(u,p) or not x_(v,p)) quad "for all " u < v. $
+  For each vertex $v$, require exactly one position:
+  $ (or.big_(p=0)^(n-1) x_(v,p)) quad and quad (not x_(v,p) or not x_(v,q)) quad "for all " p < q. $
+  Finally, for each $p$, set $q = (p + 1) mod n$. For every ordered pair $(u,v)$ with $u = v$ or ${u,v} in.not E$, add
+  $ not x_(u,p) or not x_(v,q). $
+  Because the successor position wraps modulo $n$, this family enforces the closing edge as well as the $n - 1$ internal successor edges.
+
+  _Correctness._ ($arrow.r.double$) Suppose $G$ has a Hamiltonian circuit $v_0, v_1, dots, v_(n-1), v_0$. Set $x_(v_p,p) = 1$ and every other variable to 0. Each position contains exactly one vertex and every vertex occurs exactly once. Every consecutive pair $v_p,v_q$, including $p=n-1$ and $q=0$, consists of distinct adjacent vertices, so no forbidden-successor clause has both literals false. Hence the CNF formula is satisfiable.
+
+  ($arrow.l.double$) Conversely, suppose the CNF formula is satisfiable. The position clauses select a unique vertex $v_p$ at every position, and the vertex clauses ensure that the selected sequence contains every vertex exactly once. If any consecutive pair $v_p,v_q$ were equal or were not an edge of $G$, the construction would contain $not x_(v_p,p) or not x_(v_q,q)$; both literals would be false, contradicting satisfiability. Thus all cyclically consecutive vertices are distinct and adjacent, so $v_0,v_1,dots,v_(n-1),v_0$ is a Hamiltonian circuit. For $n < 3$, both the source model and the fixed contradictory target are infeasible.
+
+  _Variable mapping._ Source vertex $v$ at circuit position $p$ maps to target variable index $v n + p$ in the zero-based assignment vector, represented by signed SAT literal $v n + p + 1$ in clauses.
+
+  _Solution extraction._ For each position $p$, find the unique vertex $v$ for which $x_(v,p) = 1$, and return the sequence $(v_0, dots, v_(n-1))$.
+]
+
 #let hc_tsp = load-example("HamiltonianCircuit", "TravelingSalesman")
 #let hc_tsp_sol = hc_tsp.solutions.at(0)
 #let hc_tsp_n = graph-num-vertices(hc_tsp.source.instance)
diff --git a/docs/paper/references.bib b/docs/paper/references.bib
index 186f70de2..d3636decf 100644
--- a/docs/paper/references.bib
+++ b/docs/paper/references.bib
@@ -2143,3 +2143,11 @@ @article{berlekampMcElieceTilborg1978
   doi     = {10.1109/TIT.1978.1055873}
 }
 
+@inproceedings{VelevGao2009,
+  author    = {Velev, Miroslav N. and Gao, Ping},
+  title     = {Efficient {SAT} Techniques for Absolute Encoding of Permutation Problems: Application to {H}amiltonian Cycles},
+  booktitle = {Proceedings of the Eighth Symposium on Abstraction, Reformulation and Approximation},
+  pages     = {159--166},
+  publisher = {AAAI Press},
+  year      = {2009}
+}
diff --git a/src/rules/hamiltoniancircuit_satisfiability.rs b/src/rules/hamiltoniancircuit_satisfiability.rs
new file mode 100644
index 000000000..9a43cb8bc
--- /dev/null
+++ b/src/rules/hamiltoniancircuit_satisfiability.rs
@@ -0,0 +1,152 @@
+//! Reduction from HamiltonianCircuit to Satisfiability.
+//!
+//! The construction uses one Boolean variable for each `(vertex, position)` pair.
+//! Exactly-one constraints make satisfying assignments permutation matrices, and
+//! forbidden-successor clauses require consecutive vertices, including the last
+//! and first positions, to be adjacent in the source graph.
+
+use crate::models::formula::{CNFClause, Satisfiability};
+use crate::models::graph::HamiltonianCircuit;
+use crate::reduction;
+use crate::rules::traits::{ReduceTo, ReductionResult};
+use crate::topology::{Graph, SimpleGraph};
+
+/// Result of reducing HamiltonianCircuit to Satisfiability.
+#[derive(Debug, Clone)]
+pub struct ReductionHamiltonianCircuitToSatisfiability {
+    target: Satisfiability,
+    num_vertices: usize,
+}
+
+impl ReductionResult for ReductionHamiltonianCircuitToSatisfiability {
+    type Source = HamiltonianCircuit<SimpleGraph>;
+    type Target = Satisfiability;
+
+    fn target_problem(&self) -> &Self::Target {
+        &self.target
+    }
+
+    fn extract_solution(&self, target_solution: &[usize]) -> Vec<usize> {
+        let n = self.num_vertices;
+        (0..n)
+            .map(|position| {
+                (0..n)
+                    .find(|&vertex| target_solution[vertex * n + position] == 1)
+                    .expect("satisfying assignment has one vertex at every position")
+            })
+            .collect()
+    }
+}
+
+fn variable(vertex: usize, position: usize, n: usize) -> i32 {
+    (vertex * n + position + 1) as i32
+}
+
+#[reduction(overhead = {
+    num_vars = "num_vertices * num_vertices + 1",
+    num_clauses = "2 * num_vertices + num_vertices * num_vertices * (num_vertices - 1) + num_vertices^3 + 2",
+    num_literals = "4 * num_vertices^3 + 2",
+})]
+impl ReduceTo<Satisfiability> for HamiltonianCircuit<SimpleGraph> {
+    type Result = ReductionHamiltonianCircuitToSatisfiability;
+
+    fn reduce_to(&self) -> Self::Result {
+        let n = self.num_vertices();
+        if n < 3 {
+            return ReductionHamiltonianCircuitToSatisfiability {
+                target: Satisfiability::new(
+                    1,
+                    vec![CNFClause::new(vec![1]), CNFClause::new(vec![-1])],
+                ),
+                num_vertices: n,
+            };
+        }
+
+        let mut clauses = Vec::new();
+
+        // Every position contains exactly one vertex.
+        for position in 0..n {
+            clauses.push(CNFClause::new(
+                (0..n).map(|vertex| variable(vertex, position, n)).collect(),
+            ));
+            for first_vertex in 0..n {
+                for second_vertex in first_vertex + 1..n {
+                    clauses.push(CNFClause::new(vec![
+                        -variable(first_vertex, position, n),
+                        -variable(second_vertex, position, n),
+                    ]));
+                }
+            }
+        }
+
+        // Every vertex occurs at exactly one position.
+        for vertex in 0..n {
+            clauses.push(CNFClause::new(
+                (0..n)
+                    .map(|position| variable(vertex, position, n))
+                    .collect(),
+            ));
+            for first_position in 0..n {
+                for second_position in first_position + 1..n {
+                    clauses.push(CNFClause::new(vec![
+                        -variable(vertex, first_position, n),
+                        -variable(vertex, second_position, n),
+                    ]));
+                }
+            }
+        }
+
+        // Consecutive positions contain distinct adjacent vertices. The successor
+        // position is cyclic, so this also enforces the closing edge.
+        for position in 0..n {
+            let successor = (position + 1) % n;
+            for vertex in 0..n {
+                for next_vertex in 0..n {
+                    if vertex == next_vertex || !self.graph().has_edge(vertex, next_vertex) {
+                        clauses.push(CNFClause::new(vec![
+                            -variable(vertex, position, n),
+                            -variable(next_vertex, successor, n),
+                        ]));
+                    }
+                }
+            }
+        }
+
+        ReductionHamiltonianCircuitToSatisfiability {
+            target: Satisfiability::new(n * n, clauses),
+            num_vertices: n,
+        }
+    }
+}
+
+#[cfg(feature = "example-db")]
+pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
+    use crate::export::SolutionPair;
+
+    vec![crate::example_db::specs::RuleExampleSpec {
+        id: "hamiltoniancircuit_to_satisfiability",
+        build: || {
+            let source = HamiltonianCircuit::new(SimpleGraph::new(
+                5,
+                vec![(0, 1), (1, 2), (2, 3), (3, 4), (4, 0), (0, 2)],
+            ));
+            crate::example_db::specs::rule_example_with_witness::<_, Satisfiability>(
+                source,
+                SolutionPair {
+                    source_config: vec![0, 1, 2, 3, 4],
+                    target_config: vec![
+                        1, 0, 0, 0, 0, // vertex 0 is at position 0
+                        0, 1, 0, 0, 0, // vertex 1 is at position 1
+                        0, 0, 1, 0, 0, // vertex 2 is at position 2
+                        0, 0, 0, 1, 0, // vertex 3 is at position 3
+                        0, 0, 0, 0, 1, // vertex 4 is at position 4
+                    ],
+                },
+            )
+        },
+    }]
+}
+
+#[cfg(test)]
+#[path = "../unit_tests/rules/hamiltoniancircuit_satisfiability.rs"]
+mod tests;
diff --git a/src/rules/mod.rs b/src/rules/mod.rs
index 95eb5f477..50d56bbb5 100644
--- a/src/rules/mod.rs
+++ b/src/rules/mod.rs
@@ -37,6 +37,7 @@ pub(crate) mod hamiltoniancircuit_hamiltonianpath;
 pub(crate) mod hamiltoniancircuit_longestcircuit;
 pub(crate) mod hamiltoniancircuit_quadraticassignment;
 pub(crate) mod hamiltoniancircuit_ruralpostman;
+pub(crate) mod hamiltoniancircuit_satisfiability;
 pub(crate) mod hamiltoniancircuit_stackercrane;
 pub(crate) mod hamiltoniancircuit_strongconnectivityaugmentation;
 pub(crate) mod hamiltoniancircuit_travelingsalesman;
@@ -448,6 +449,7 @@ pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::Ru
     specs.extend(hamiltoniancircuit_longestcircuit::canonical_rule_example_specs());
     specs.extend(hamiltoniancircuit_quadraticassignment::canonical_rule_example_specs());
     specs.extend(hamiltoniancircuit_ruralpostman::canonical_rule_example_specs());
+    specs.extend(hamiltoniancircuit_satisfiability::canonical_rule_example_specs());
     specs.extend(hamiltoniancircuit_stackercrane::canonical_rule_example_specs());
     specs.extend(hamiltoniancircuit_strongconnectivityaugmentation::canonical_rule_example_specs());
     specs.extend(hamiltoniancircuit_travelingsalesman::canonical_rule_example_specs());
diff --git a/src/unit_tests/rules/hamiltoniancircuit_satisfiability.rs b/src/unit_tests/rules/hamiltoniancircuit_satisfiability.rs
new file mode 100644
index 000000000..42f61c7ed
--- /dev/null
+++ b/src/unit_tests/rules/hamiltoniancircuit_satisfiability.rs
@@ -0,0 +1,191 @@
+use super::*;
+use crate::rules::ReductionEntry;
+use crate::solvers::BruteForce;
+use crate::traits::Problem;
+
+fn five_cycle_with_chord() -> HamiltonianCircuit<SimpleGraph> {
+    HamiltonianCircuit::new(SimpleGraph::new(
+        5,
+        vec![(0, 1), (1, 2), (2, 3), (3, 4), (4, 0), (0, 2)],
+    ))
+}
+
+fn position_assignment(circuit: &[usize]) -> Vec<usize> {
+    let n = circuit.len();
+    let mut assignment = vec![0; n * n];
+    for (position, &vertex) in circuit.iter().enumerate() {
+        assignment[vertex * n + position] = 1;
+    }
+    assignment
+}
+
+fn permutations(values: &mut [usize], start: usize, visit: &mut impl FnMut(&[usize])) {
+    if start == values.len() {
+        visit(values);
+        return;
+    }
+    for index in start..values.len() {
+        values.swap(start, index);
+        permutations(values, start + 1, visit);
+        values.swap(start, index);
+    }
+}
+
+#[test]
+fn test_hamiltoniancircuit_to_satisfiability_closed_loop() {
+    let source = HamiltonianCircuit::new(SimpleGraph::cycle(3));
+    let reduction = ReduceTo::<Satisfiability>::reduce_to(&source);
+    let target_solution = BruteForce::new()
+        .find_witness(reduction.target_problem())
+        .expect("the triangle encoding must be satisfiable");
+    let source_solution = reduction.extract_solution(&target_solution);
+
+    assert!(source.evaluate(&source_solution));
+}
+
+#[test]
+fn test_five_cycle_with_chord_structure() {
+    let reduction = ReduceTo::<Satisfiability>::reduce_to(&five_cycle_with_chord());
+    let target = reduction.target_problem();
+
+    assert_eq!(target.num_vars(), 25);
+    assert_eq!(target.num_clauses(), 175);
+    assert_eq!(target.num_literals(), 380);
+    assert_eq!(target.clauses()[0], CNFClause::new(vec![1, 6, 11, 16, 21]));
+    assert_eq!(target.clauses()[1], CNFClause::new(vec![-1, -6]));
+    assert_eq!(target.clauses()[55], CNFClause::new(vec![1, 2, 3, 4, 5]));
+
+    let clauses = target.clauses();
+    assert!(clauses.contains(&CNFClause::new(vec![-1, -2])));
+    assert!(clauses.contains(&CNFClause::new(vec![-1, -17])));
+    assert!(clauses.contains(&CNFClause::new(vec![-10, -16])));
+}
+
+#[test]
+fn test_extracts_both_circuit_orientations() {
+    let reduction = ReduceTo::<Satisfiability>::reduce_to(&five_cycle_with_chord());
+
+    for circuit in [vec![0, 1, 2, 3, 4], vec![0, 4, 3, 2, 1]] {
+        let assignment = position_assignment(&circuit);
+        assert!(reduction.target_problem().evaluate(&assignment));
+        assert_eq!(reduction.extract_solution(&assignment), circuit);
+    }
+}
+
+#[test]
+fn test_five_vertex_path_encoding_is_unsatisfiable() {
+    let source = HamiltonianCircuit::new(SimpleGraph::path(5));
+    let reduction = ReduceTo::<Satisfiability>::reduce_to(&source);
+    let mut circuit = vec![0, 1, 2, 3, 4];
+    permutations(&mut circuit, 0, &mut |candidate| {
+        assert!(!reduction
+            .target_problem()
+            .evaluate(&position_assignment(candidate)));
+    });
+}
+
+#[test]
+fn test_instances_with_fewer_than_three_vertices_are_unsatisfiable() {
+    for n in 0..3 {
+        let source = HamiltonianCircuit::new(SimpleGraph::empty(n));
+        let reduction = ReduceTo::<Satisfiability>::reduce_to(&source);
+        let target = reduction.target_problem();
+
+        assert_eq!(target.num_vars(), 1);
+        assert_eq!(
+            target.clauses(),
+            &[CNFClause::new(vec![1]), CNFClause::new(vec![-1])]
+        );
+        assert!(BruteForce::new().find_witness(target).is_none());
+    }
+}
+
+#[test]
+fn test_isolated_vertex_blocks_satisfiability() {
+    let source = HamiltonianCircuit::new(SimpleGraph::new(4, vec![(0, 1), (1, 2), (2, 0)]));
+    let reduction = ReduceTo::<Satisfiability>::reduce_to(&source);
+    let mut circuit = vec![0, 1, 2, 3];
+    permutations(&mut circuit, 0, &mut |candidate| {
+        assert!(!reduction
+            .target_problem()
+            .evaluate(&position_assignment(candidate)));
+    });
+}
+
+#[test]
+fn test_self_loops_do_not_allow_repeated_vertices() {
+    let source = HamiltonianCircuit::new(SimpleGraph::new(3, vec![(0, 0), (0, 1), (1, 2), (2, 0)]));
+    let reduction = ReduceTo::<Satisfiability>::reduce_to(&source);
+
+    assert!(reduction
+        .target_problem()
+        .clauses()
+        .contains(&CNFClause::new(vec![-1, -2])));
+    assert!(reduction
+        .target_problem()
+        .evaluate(&position_assignment(&[0, 1, 2])));
+}
+
+#[test]
+fn test_parallel_edges_have_simple_adjacency_semantics() {
+    let source = HamiltonianCircuit::new(SimpleGraph::new(3, vec![(0, 1), (0, 1), (1, 2), (2, 0)]));
+    let reduction = ReduceTo::<Satisfiability>::reduce_to(&source);
+    let assignment = position_assignment(&[0, 1, 2]);
+
+    assert!(reduction.target_problem().evaluate(&assignment));
+    assert_eq!(reduction.extract_solution(&assignment), vec![0, 1, 2]);
+}
+
+#[test]
+fn test_registered_overhead_covers_constructed_target() {
+    let entry = inventory::iter::<ReductionEntry>
+        .into_iter()
+        .find(|entry| {
+            entry.source_name == "HamiltonianCircuit" && entry.target_name == "Satisfiability"
+        })
+        .expect("HamiltonianCircuit to Satisfiability must be registered");
+    let source = five_cycle_with_chord();
+    let overhead = (entry.overhead_eval_fn)(&source as &dyn std::any::Any);
+
+    assert_eq!(overhead.get("num_vars"), Some(26));
+    assert_eq!(overhead.get("num_clauses"), Some(237));
+    assert_eq!(overhead.get("num_literals"), Some(502));
+
+    for source in (0..3)
+        .map(|n| HamiltonianCircuit::new(SimpleGraph::empty(n)))
+        .chain(std::iter::once(source))
+    {
+        let reduction = ReduceTo::<Satisfiability>::reduce_to(&source);
+        let target = reduction.target_problem();
+        let overhead = (entry.overhead_eval_fn)(&source as &dyn std::any::Any);
+        assert!(target.num_vars() <= overhead.get("num_vars").unwrap());
+        assert!(target.num_clauses() <= overhead.get("num_clauses").unwrap());
+        assert!(target.num_literals() <= overhead.get("num_literals").unwrap());
+    }
+}
+
+#[cfg(feature = "example-db")]
+#[test]
+fn test_canonical_example_witness_and_metrics() {
+    let example = (canonical_rule_example_specs()[0].build)();
+    let source: HamiltonianCircuit<SimpleGraph> =
+        serde_json::from_value(example.source.instance).unwrap();
+    let target: Satisfiability = serde_json::from_value(example.target.instance).unwrap();
+    let solution = &example.solutions[0];
+    let reduction = ReduceTo::<Satisfiability>::reduce_to(&source);
+
+    assert_eq!(solution.source_config, vec![0, 1, 2, 3, 4]);
+    assert_eq!(
+        solution.target_config,
+        position_assignment(&[0, 1, 2, 3, 4])
+    );
+    assert!(source.evaluate(&solution.source_config));
+    assert!(target.evaluate(&solution.target_config));
+    assert_eq!(
+        reduction.extract_solution(&solution.target_config),
+        solution.source_config
+    );
+    assert_eq!(target.num_vars(), 25);
+    assert_eq!(target.num_clauses(), 175);
+    assert_eq!(target.num_literals(), 380);
+}