From 46303b61edd8a90a1d33074f2ff1039b4ad173ad Mon Sep 17 00:00:00 2001 From: Xiwei Pan Date: Sun, 2 Aug 2026 09:36:49 +0800 Subject: [PATCH 1/3] Add plan for #1098: HamiltonianCircuit to Satisfiability --- ...02-hamiltoniancircuit-to-satisfiability.md | 45 +++++++++++++++++++ 1 file changed, 45 insertions(+) create mode 100644 docs/plans/2026-08-02-hamiltoniancircuit-to-satisfiability.md diff --git a/docs/plans/2026-08-02-hamiltoniancircuit-to-satisfiability.md b/docs/plans/2026-08-02-hamiltoniancircuit-to-satisfiability.md new file mode 100644 index 000000000..87626cb46 --- /dev/null +++ b/docs/plans/2026-08-02-hamiltoniancircuit-to-satisfiability.md @@ -0,0 +1,45 @@ +# HamiltonianCircuit to Satisfiability Implementation Plan + +Issue: #1098, `[Rule] HamiltonianCircuit to Satisfiability` + +Base commit: `a9067297c9b7759b4f1139692553a465de49fed3` + +The implementation follows the repository's `add-rule` Steps 1-7. Mathematical verification has established the vertex-position encoding against every simple graph through five vertices, including solution extraction, overhead bounds, the fixed contradiction for `n < 3`, and the issue's YES/NO examples. + +## Batch 1: Implement and test the reduction + +1. Add `src/rules/hamiltoniancircuit_satisfiability.rs`. + - Implement `ReduceTo` for `HamiltonianCircuit` and a witness-preserving `ReductionResult`. + - For `n < 3`, emit one SAT variable with clauses `(z)` and `(not z)`. + - For `n >= 3`, map `(vertex, position)` to the 1-indexed SAT literal `vertex * n + position + 1`. + - Emit exactly-one constraints for every position and every vertex, followed by cyclic forbidden-successor clauses for equal vertices and non-edges. + - Decode a satisfying assignment by reading the unique true vertex at each position. + - Register the safe overhead bounds from the issue: `num_vars = num_vertices * num_vertices + 1`, `num_clauses = 2 * num_vertices + num_vertices * num_vertices * (num_vertices - 1) + num_vertices^3 + 2`, and `num_literals = 4 * num_vertices^3 + 2`. + +2. Register the module and example provider in `src/rules/mod.rs`. + +3. Add focused tests in `src/unit_tests/rules/hamiltoniancircuit_satisfiability.rs`. + - Closed loop on a triangle through the SAT brute-force solver. + - Exact structure and representative successor clauses on the five-cycle-plus-chord example. + - Extraction for both orientations of a circuit. + - Unsatisfiability of the five-vertex path and of every `n < 3` source instance. + - Semantics for isolated vertices, self-loops, and parallel edges. + - Assert the registered overhead evaluates to bounds that cover the constructed target. + +4. Add `hamiltoniancircuit_to_satisfiability` to the canonical rule example database from the issue's five-cycle-plus-chord source and its 25-bit diagonal position assignment. Regenerate `src/example_db/fixtures/examples.json` and verify the stored source witness, SAT witness, extracted circuit, and target metrics. + +5. Run focused Rust tests, formatter, and the standard non-paper verification needed before documentation. + +## Batch 2: Paper entry and final verification + +1. With fresh context after Batch 1, add the Velev-Gao SARA 2009 reference to `docs/paper/references.bib` if it is not already present. + +2. Add the mandatory `reduction-rule("HamiltonianCircuit", "Satisfiability", ...)` entry to `docs/paper/reductions.typ`. + - Load the canonical example fixture and derive the `pred create --example`, reduce, solve, and evaluate commands from it. + - Explain the `n x n` position matrix, the two exactly-one families, cyclic forbidden-successor clauses, both directions of correctness, and witness extraction. + - Walk through the five-cycle-plus-chord example using fixture data, including a representative forbidden pair and the recovered circuit. + - State that the fixture contains one canonical SAT witness while rotated/reversed Hamiltonian circuits produce multiple satisfying assignments. + +3. Regenerate the reduction graph and schemas, regenerate fixtures, and run `make paper`. + +4. Run `make test clippy`, `make coverage`, and inspect the final diff/status. Commit only files required for issue #1098; remove this plan file before the final push. From 15f2aa3ef35fc94b5468e514a1de8aaab32661b6 Mon Sep 17 00:00:00 2001 From: Xiwei Pan Date: Sun, 2 Aug 2026 12:41:11 +0800 Subject: [PATCH 2/3] Implement #1098: HamiltonianCircuit to Satisfiability --- docs/paper/reductions.typ | 60 ++++++ docs/paper/references.bib | 8 + .../hamiltoniancircuit_satisfiability.rs | 152 ++++++++++++++ src/rules/mod.rs | 2 + .../hamiltoniancircuit_satisfiability.rs | 191 ++++++++++++++++++ 5 files changed, 413 insertions(+) create mode 100644 src/rules/hamiltoniancircuit_satisfiability.rs create mode 100644 src/unit_tests/rules/hamiltoniancircuit_satisfiability.rs 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; + type Target = Satisfiability; + + fn target_problem(&self) -> &Self::Target { + &self.target + } + + fn extract_solution(&self, target_solution: &[usize]) -> Vec { + 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 for HamiltonianCircuit { + 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 { + 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 HamiltonianCircuit { + HamiltonianCircuit::new(SimpleGraph::new( + 5, + vec![(0, 1), (1, 2), (2, 3), (3, 4), (4, 0), (0, 2)], + )) +} + +fn position_assignment(circuit: &[usize]) -> Vec { + 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::::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::::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::::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::::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::::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::::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::::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::::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:: + .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::::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 = + 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::::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); +} From b3e5c5e307947089710651440b1ae48acffdb733 Mon Sep 17 00:00:00 2001 From: Xiwei Pan Date: Sun, 2 Aug 2026 12:41:11 +0800 Subject: [PATCH 3/3] chore: remove plan file after implementation --- ...02-hamiltoniancircuit-to-satisfiability.md | 45 ------------------- 1 file changed, 45 deletions(-) delete mode 100644 docs/plans/2026-08-02-hamiltoniancircuit-to-satisfiability.md diff --git a/docs/plans/2026-08-02-hamiltoniancircuit-to-satisfiability.md b/docs/plans/2026-08-02-hamiltoniancircuit-to-satisfiability.md deleted file mode 100644 index 87626cb46..000000000 --- a/docs/plans/2026-08-02-hamiltoniancircuit-to-satisfiability.md +++ /dev/null @@ -1,45 +0,0 @@ -# HamiltonianCircuit to Satisfiability Implementation Plan - -Issue: #1098, `[Rule] HamiltonianCircuit to Satisfiability` - -Base commit: `a9067297c9b7759b4f1139692553a465de49fed3` - -The implementation follows the repository's `add-rule` Steps 1-7. Mathematical verification has established the vertex-position encoding against every simple graph through five vertices, including solution extraction, overhead bounds, the fixed contradiction for `n < 3`, and the issue's YES/NO examples. - -## Batch 1: Implement and test the reduction - -1. Add `src/rules/hamiltoniancircuit_satisfiability.rs`. - - Implement `ReduceTo` for `HamiltonianCircuit` and a witness-preserving `ReductionResult`. - - For `n < 3`, emit one SAT variable with clauses `(z)` and `(not z)`. - - For `n >= 3`, map `(vertex, position)` to the 1-indexed SAT literal `vertex * n + position + 1`. - - Emit exactly-one constraints for every position and every vertex, followed by cyclic forbidden-successor clauses for equal vertices and non-edges. - - Decode a satisfying assignment by reading the unique true vertex at each position. - - Register the safe overhead bounds from the issue: `num_vars = num_vertices * num_vertices + 1`, `num_clauses = 2 * num_vertices + num_vertices * num_vertices * (num_vertices - 1) + num_vertices^3 + 2`, and `num_literals = 4 * num_vertices^3 + 2`. - -2. Register the module and example provider in `src/rules/mod.rs`. - -3. Add focused tests in `src/unit_tests/rules/hamiltoniancircuit_satisfiability.rs`. - - Closed loop on a triangle through the SAT brute-force solver. - - Exact structure and representative successor clauses on the five-cycle-plus-chord example. - - Extraction for both orientations of a circuit. - - Unsatisfiability of the five-vertex path and of every `n < 3` source instance. - - Semantics for isolated vertices, self-loops, and parallel edges. - - Assert the registered overhead evaluates to bounds that cover the constructed target. - -4. Add `hamiltoniancircuit_to_satisfiability` to the canonical rule example database from the issue's five-cycle-plus-chord source and its 25-bit diagonal position assignment. Regenerate `src/example_db/fixtures/examples.json` and verify the stored source witness, SAT witness, extracted circuit, and target metrics. - -5. Run focused Rust tests, formatter, and the standard non-paper verification needed before documentation. - -## Batch 2: Paper entry and final verification - -1. With fresh context after Batch 1, add the Velev-Gao SARA 2009 reference to `docs/paper/references.bib` if it is not already present. - -2. Add the mandatory `reduction-rule("HamiltonianCircuit", "Satisfiability", ...)` entry to `docs/paper/reductions.typ`. - - Load the canonical example fixture and derive the `pred create --example`, reduce, solve, and evaluate commands from it. - - Explain the `n x n` position matrix, the two exactly-one families, cyclic forbidden-successor clauses, both directions of correctness, and witness extraction. - - Walk through the five-cycle-plus-chord example using fixture data, including a representative forbidden pair and the recovered circuit. - - State that the fixture contains one canonical SAT witness while rotated/reversed Hamiltonian circuits produce multiple satisfying assignments. - -3. Regenerate the reduction graph and schemas, regenerate fixtures, and run `make paper`. - -4. Run `make test clippy`, `make coverage`, and inspect the final diff/status. Commit only files required for issue #1098; remove this plan file before the final push.