From 309697b4e9bf9ca94594b6c3feb5e1a4294421e3 Mon Sep 17 00:00:00 2001 From: zazabap Date: Thu, 26 Mar 2026 12:12:57 +0000 Subject: [PATCH 1/5] feat: add 8 Tier 1a reduction rules (#770) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Implement 8 simple, verified reduction rules from Garey & Johnson: - HamiltonianCircuit → HamiltonianPath (#199): vertex duplication + pendants - KClique → SubgraphIsomorphism (#201): pattern = K_k - Partition → MultiprocessorScheduling (#203): m=2, D=S/2 - HamiltonianPath → IsomorphicSpanningTree (#234): T = P_n - HamiltonianCircuit → BottleneckTravelingSalesman (#259): {1,2}-distances - KClique → ConjunctiveBooleanQuery (#464): k-clique as Boolean CQ - ExactCoverBy3Sets → StaffScheduling (#487): subset-to-schedule encoding - Satisfiability → NAESatisfiability (#753): sentinel variable construction Each rule includes full test coverage (closed-loop, edge cases, extraction). Fixes #199, Fixes #201, Fixes #203, Fixes #234, Fixes #259, Fixes #464, Fixes #487, Fixes #753 Co-Authored-By: Claude Opus 4.6 (1M context) --- .../exactcoverby3sets_staffscheduling.rs | 110 +++++++++++ ...niancircuit_bottlenecktravelingsalesman.rs | 129 +++++++++++++ .../hamiltoniancircuit_hamiltonianpath.rs | 173 +++++++++++++++++ .../hamiltonianpath_isomorphicspanningtree.rs | 86 +++++++++ src/rules/kclique_conjunctivebooleanquery.rs | 115 +++++++++++ src/rules/kclique_subgraphisomorphism.rs | 108 +++++++++++ src/rules/mod.rs | 16 ++ .../partition_multiprocessorscheduling.rs | 78 ++++++++ src/rules/satisfiability_naesatisfiability.rs | 105 ++++++++++ .../exactcoverby3sets_staffscheduling.rs | 111 +++++++++++ ...niancircuit_bottlenecktravelingsalesman.rs | 82 ++++++++ .../hamiltoniancircuit_hamiltonianpath.rs | 112 +++++++++++ .../hamiltonianpath_isomorphicspanningtree.rs | 110 +++++++++++ .../rules/kclique_conjunctivebooleanquery.rs | 95 +++++++++ .../rules/kclique_subgraphisomorphism.rs | 116 +++++++++++ .../partition_multiprocessorscheduling.rs | 149 ++++++++++++++ .../rules/satisfiability_naesatisfiability.rs | 182 ++++++++++++++++++ 17 files changed, 1877 insertions(+) create mode 100644 src/rules/exactcoverby3sets_staffscheduling.rs create mode 100644 src/rules/hamiltoniancircuit_bottlenecktravelingsalesman.rs create mode 100644 src/rules/hamiltoniancircuit_hamiltonianpath.rs create mode 100644 src/rules/hamiltonianpath_isomorphicspanningtree.rs create mode 100644 src/rules/kclique_conjunctivebooleanquery.rs create mode 100644 src/rules/kclique_subgraphisomorphism.rs create mode 100644 src/rules/partition_multiprocessorscheduling.rs create mode 100644 src/rules/satisfiability_naesatisfiability.rs create mode 100644 src/unit_tests/rules/exactcoverby3sets_staffscheduling.rs create mode 100644 src/unit_tests/rules/hamiltoniancircuit_bottlenecktravelingsalesman.rs create mode 100644 src/unit_tests/rules/hamiltoniancircuit_hamiltonianpath.rs create mode 100644 src/unit_tests/rules/hamiltonianpath_isomorphicspanningtree.rs create mode 100644 src/unit_tests/rules/kclique_conjunctivebooleanquery.rs create mode 100644 src/unit_tests/rules/kclique_subgraphisomorphism.rs create mode 100644 src/unit_tests/rules/partition_multiprocessorscheduling.rs create mode 100644 src/unit_tests/rules/satisfiability_naesatisfiability.rs diff --git a/src/rules/exactcoverby3sets_staffscheduling.rs b/src/rules/exactcoverby3sets_staffscheduling.rs new file mode 100644 index 000000000..68684bc5e --- /dev/null +++ b/src/rules/exactcoverby3sets_staffscheduling.rs @@ -0,0 +1,110 @@ +//! Reduction from ExactCoverBy3Sets to StaffScheduling. +//! +//! Given an X3C instance with universe X (|X| = 3q) and collection C of +//! 3-element subsets, construct a StaffScheduling instance where: +//! - Each universe element becomes a period (m = 3q periods) +//! - Each subset S_j = {a, b, c} becomes a schedule with shifts at positions a, b, c +//! - All requirements are 1 (each period needs exactly 1 worker) +//! - The worker budget is q (an exact cover uses exactly q subsets) +//! - shifts_per_schedule = 3 (each schedule has exactly 3 active periods) +//! +//! An exact cover in X3C corresponds to a feasible staff assignment. + +use crate::models::misc::StaffScheduling; +use crate::models::set::ExactCoverBy3Sets; +use crate::reduction; +use crate::rules::traits::{ReduceTo, ReductionResult}; + +/// Result of reducing ExactCoverBy3Sets to StaffScheduling. +#[derive(Debug, Clone)] +pub struct ReductionXC3SToStaffScheduling { + target: StaffScheduling, +} + +impl ReductionResult for ReductionXC3SToStaffScheduling { + type Source = ExactCoverBy3Sets; + type Target = StaffScheduling; + + fn target_problem(&self) -> &StaffScheduling { + &self.target + } + + /// Extract XC3S solution from StaffScheduling solution. + /// + /// StaffScheduling config[j] = number of workers assigned to schedule j. + /// XC3S config[j] = 1 if subset j is selected, 0 otherwise. + fn extract_solution(&self, target_solution: &[usize]) -> Vec { + target_solution + .iter() + .map(|&count| if count > 0 { 1 } else { 0 }) + .collect() + } +} + +#[reduction( + overhead = { + num_periods = "universe_size", + num_schedules = "num_subsets", + num_workers = "universe_size / 3", + } +)] +impl ReduceTo for ExactCoverBy3Sets { + type Result = ReductionXC3SToStaffScheduling; + + fn reduce_to(&self) -> Self::Result { + let universe_size = self.universe_size(); + let q = universe_size / 3; + + // Build schedule patterns: one per subset + let schedules: Vec> = self + .subsets() + .iter() + .map(|subset| { + let mut schedule = vec![false; universe_size]; + for &elem in subset { + schedule[elem] = true; + } + schedule + }) + .collect(); + + // Each period requires exactly 1 worker + let requirements = vec![1u64; universe_size]; + + let target = StaffScheduling::new( + 3, // shifts_per_schedule + schedules, + requirements, + q as u64, // num_workers = q + ); + + ReductionXC3SToStaffScheduling { target } + } +} + +#[cfg(feature = "example-db")] +pub(crate) fn canonical_rule_example_specs() -> Vec { + use crate::export::SolutionPair; + + vec![crate::example_db::specs::RuleExampleSpec { + id: "exactcoverby3sets_to_staffscheduling", + build: || { + // Universe {0,1,2,3,4,5}, subsets [{0,1,2}, {3,4,5}, {0,3,4}, {1,2,5}] + // Exact cover: S0 + S1 + let source = + ExactCoverBy3Sets::new(6, vec![[0, 1, 2], [3, 4, 5], [0, 3, 4], [1, 2, 5]]); + // In StaffScheduling, assigning 1 worker to schedule 0 and 1 worker to schedule 1 + crate::example_db::specs::rule_example_with_witness::<_, StaffScheduling>( + source, + SolutionPair { + source_config: vec![1, 1, 0, 0], + target_config: vec![1, 1, 0, 0], + }, + ) + }, + }] +} + +#[cfg(test)] +#[path = "../unit_tests/rules/exactcoverby3sets_staffscheduling.rs"] +mod tests; diff --git a/src/rules/hamiltoniancircuit_bottlenecktravelingsalesman.rs b/src/rules/hamiltoniancircuit_bottlenecktravelingsalesman.rs new file mode 100644 index 000000000..9bc353d70 --- /dev/null +++ b/src/rules/hamiltoniancircuit_bottlenecktravelingsalesman.rs @@ -0,0 +1,129 @@ +//! Reduction from HamiltonianCircuit to BottleneckTravelingSalesman. +//! +//! The standard construction embeds the source graph into the complete graph on the +//! same vertex set, assigning weight 1 to source edges and weight 2 to non-edges. +//! The optimal bottleneck tour equals 1 iff the source graph contains a Hamiltonian circuit. + +use crate::models::graph::{BottleneckTravelingSalesman, HamiltonianCircuit}; +use crate::reduction; +use crate::rules::traits::{ReduceTo, ReductionResult}; +use crate::topology::{Graph, SimpleGraph}; + +/// Result of reducing HamiltonianCircuit to BottleneckTravelingSalesman. +#[derive(Debug, Clone)] +pub struct ReductionHamiltonianCircuitToBottleneckTravelingSalesman { + target: BottleneckTravelingSalesman, +} + +impl ReductionResult for ReductionHamiltonianCircuitToBottleneckTravelingSalesman { + type Source = HamiltonianCircuit; + type Target = BottleneckTravelingSalesman; + + fn target_problem(&self) -> &Self::Target { + &self.target + } + + fn extract_solution(&self, target_solution: &[usize]) -> Vec { + let graph = self.target.graph(); + let n = graph.num_vertices(); + if n == 0 { + return vec![]; + } + + let edges = graph.edges(); + if target_solution.len() != edges.len() { + return vec![0; n]; + } + + // Build adjacency from selected edges + let mut adjacency = vec![Vec::new(); n]; + let mut selected_count = 0usize; + for (idx, &selected) in target_solution.iter().enumerate() { + if selected != 1 { + continue; + } + let (u, v) = edges[idx]; + adjacency[u].push(v); + adjacency[v].push(u); + selected_count += 1; + } + + if selected_count != n || adjacency.iter().any(|neighbors| neighbors.len() != 2) { + return vec![0; n]; + } + + for neighbors in &mut adjacency { + neighbors.sort_unstable(); + } + + // Walk the cycle to produce a permutation + let mut order = Vec::with_capacity(n); + let mut prev = None; + let mut current = 0usize; + + for _ in 0..n { + order.push(current); + let neighbors = &adjacency[current]; + let next = match prev { + Some(previous) => { + if neighbors[0] == previous { + neighbors[1] + } else { + neighbors[0] + } + } + None => neighbors[0], + }; + prev = Some(current); + current = next; + } + + order + } +} + +#[reduction( + overhead = { + num_vertices = "num_vertices", + num_edges = "num_vertices * (num_vertices - 1) / 2", + } +)] +impl ReduceTo for HamiltonianCircuit { + type Result = ReductionHamiltonianCircuitToBottleneckTravelingSalesman; + + fn reduce_to(&self) -> Self::Result { + let num_vertices = self.num_vertices(); + let target_graph = SimpleGraph::complete(num_vertices); + let weights = target_graph + .edges() + .into_iter() + .map(|(u, v)| if self.graph().has_edge(u, v) { 1 } else { 2 }) + .collect(); + let target = BottleneckTravelingSalesman::new(target_graph, weights); + + ReductionHamiltonianCircuitToBottleneckTravelingSalesman { target } + } +} + +#[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_bottlenecktravelingsalesman", + build: || { + let source = HamiltonianCircuit::new(SimpleGraph::cycle(4)); + crate::example_db::specs::rule_example_with_witness::<_, BottleneckTravelingSalesman>( + source, + SolutionPair { + source_config: vec![0, 1, 2, 3], + target_config: vec![1, 0, 1, 1, 0, 1], + }, + ) + }, + }] +} + +#[cfg(test)] +#[path = "../unit_tests/rules/hamiltoniancircuit_bottlenecktravelingsalesman.rs"] +mod tests; diff --git a/src/rules/hamiltoniancircuit_hamiltonianpath.rs b/src/rules/hamiltoniancircuit_hamiltonianpath.rs new file mode 100644 index 000000000..ecab0800d --- /dev/null +++ b/src/rules/hamiltoniancircuit_hamiltonianpath.rs @@ -0,0 +1,173 @@ +//! Reduction from HamiltonianCircuit to HamiltonianPath. +//! +//! Given a Hamiltonian Circuit instance G = (V, E) with n vertices, we construct +//! a Hamiltonian Path instance G' with n + 3 vertices as follows: +//! +//! 1. Pick an arbitrary vertex v = 0. +//! 2. Create a duplicate vertex v' (index n) connected to all neighbors of v. +//! 3. Add a pendant vertex s (index n+1) with the single edge {s, v}. +//! 4. Add a pendant vertex t (index n+2) with the single edge {t, v'}. +//! +//! G has a Hamiltonian circuit iff G' has a Hamiltonian path (from s to t). +//! +//! The target graph G' has n + 3 vertices and m + deg(v) + 2 edges. + +use crate::models::graph::{HamiltonianCircuit, HamiltonianPath}; +use crate::reduction; +use crate::rules::traits::{ReduceTo, ReductionResult}; +use crate::topology::{Graph, SimpleGraph}; + +/// Result of reducing HamiltonianCircuit to HamiltonianPath. +/// +/// Stores the target HamiltonianPath instance and the number of original vertices +/// to enable solution extraction. +#[derive(Debug, Clone)] +pub struct ReductionHamiltonianCircuitToHamiltonianPath { + target: HamiltonianPath, + /// Number of vertices in the original graph. + num_original_vertices: usize, +} + +impl ReductionResult for ReductionHamiltonianCircuitToHamiltonianPath { + type Source = HamiltonianCircuit; + type Target = HamiltonianPath; + + fn target_problem(&self) -> &Self::Target { + &self.target + } + + fn extract_solution(&self, target_solution: &[usize]) -> Vec { + let n = self.num_original_vertices; + if n == 0 { + return vec![]; + } + + let n_prime = n + 3; // total vertices in target graph + if target_solution.len() != n_prime { + return vec![0; n]; + } + + let v_prime = n; // index of duplicated vertex v' + let s = n + 1; // pendant attached to v=0 + let t = n + 2; // pendant attached to v' + + // The HP path must start at s or t (pendants with degree 1). + // Determine path orientation: we want s at the start. + // target_solution[i] = vertex visited at position i. + + // Find position of s and t in the path + let s_pos = target_solution.iter().position(|&v| v == s); + let t_pos = target_solution.iter().position(|&v| v == t); + + let (s_pos, t_pos) = match (s_pos, t_pos) { + (Some(sp), Some(tp)) => (sp, tp), + _ => return vec![0; n], // invalid solution + }; + + // Build the path in order from s to t + let path: Vec = if s_pos == 0 && t_pos == n_prime - 1 { + // Already oriented s -> ... -> t + target_solution.to_vec() + } else if t_pos == 0 && s_pos == n_prime - 1 { + // Reverse: t -> ... -> s, flip to s -> ... -> t + target_solution.iter().copied().rev().collect() + } else { + // s or t not at endpoints -- invalid HP for our construction + return vec![0; n]; + }; + + // path = [s, v=0, ..., v'=n, t] + // Strip s (first) and t (last) to get inner path of length n+1 + let inner = &path[1..n_prime - 1]; // length n+1 + + // The inner path should start with v=0 and end with v'=n, or vice versa. + // Orient so it starts with v=0. + let oriented: Vec = if inner[0] == 0 && inner[n] == v_prime { + inner.to_vec() + } else if inner[0] == v_prime && inner[n] == 0 { + inner.iter().copied().rev().collect() + } else { + return vec![0; n]; + }; + + // oriented = [0, perm of 1..n-1, v'=n] + // The HC config is the first n entries (dropping v' at the end). + oriented[..n].to_vec() + } +} + +#[reduction( + overhead = { + num_vertices = "num_vertices + 3", + num_edges = "num_edges + num_vertices + 1", + } +)] +impl ReduceTo> for HamiltonianCircuit { + type Result = ReductionHamiltonianCircuitToHamiltonianPath; + + fn reduce_to(&self) -> Self::Result { + let n = self.num_vertices(); + let source_graph = self.graph(); + + // New vertex indices: + // 0..n-1: original vertices + // n: v' (duplicate of vertex 0) + // n+1: s (pendant of vertex 0) + // n+2: t (pendant of v') + let v_prime = n; + let s = n + 1; + let t = n + 2; + + let mut edges: Vec<(usize, usize)> = Vec::new(); + + // 1. Copy all original edges + for (u, v) in source_graph.edges() { + edges.push((u, v)); + } + + // 2. Connect v' to all neighbors of vertex 0 + for neighbor in source_graph.neighbors(0) { + edges.push((v_prime, neighbor)); + } + + // 3. Add pendant edge {s, 0} + edges.push((s, 0)); + + // 4. Add pendant edge {t, v'} + edges.push((t, v_prime)); + + let target_graph = SimpleGraph::new(n + 3, edges); + let target = HamiltonianPath::new(target_graph); + + ReductionHamiltonianCircuitToHamiltonianPath { + target, + num_original_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_hamiltonianpath", + build: || { + // Square graph (4-cycle): 0-1-2-3-0 + let source = HamiltonianCircuit::new(SimpleGraph::cycle(4)); + crate::example_db::specs::rule_example_with_witness::<_, HamiltonianPath>( + source, + SolutionPair { + // HC solution: visit vertices in order 0, 1, 2, 3 + source_config: vec![0, 1, 2, 3], + // HP solution on G' (7 vertices): s=5, 0, 1, 2, 3, v'=4, t=6 + target_config: vec![5, 0, 1, 2, 3, 4, 6], + }, + ) + }, + }] +} + +#[cfg(test)] +#[path = "../unit_tests/rules/hamiltoniancircuit_hamiltonianpath.rs"] +mod tests; diff --git a/src/rules/hamiltonianpath_isomorphicspanningtree.rs b/src/rules/hamiltonianpath_isomorphicspanningtree.rs new file mode 100644 index 000000000..b11dea000 --- /dev/null +++ b/src/rules/hamiltonianpath_isomorphicspanningtree.rs @@ -0,0 +1,86 @@ +//! Reduction from HamiltonianPath to IsomorphicSpanningTree. +//! +//! A Hamiltonian path in G exists iff G has a spanning tree isomorphic to the +//! path graph P_n. The reduction keeps G unchanged as the host graph and +//! constructs T = P_n (the path on n vertices: edges {0,1},{1,2},...,{n-2,n-1}). + +use crate::models::graph::{HamiltonianPath, IsomorphicSpanningTree}; +use crate::reduction; +use crate::rules::traits::{ReduceTo, ReductionResult}; +use crate::topology::SimpleGraph; + +/// Result of reducing HamiltonianPath to IsomorphicSpanningTree. +#[derive(Debug, Clone)] +pub struct ReductionHPToIST { + target: IsomorphicSpanningTree, +} + +impl ReductionResult for ReductionHPToIST { + type Source = HamiltonianPath; + type Target = IsomorphicSpanningTree; + + fn target_problem(&self) -> &Self::Target { + &self.target + } + + /// Solution extraction: identity mapping. + /// + /// The IST config maps tree vertex i to graph vertex config[i]. Since the + /// tree is P_n (path 0-1-2-...-n-1), this mapping directly gives the + /// vertex ordering of the Hamiltonian path. + fn extract_solution(&self, target_solution: &[usize]) -> Vec { + target_solution.to_vec() + } +} + +#[reduction( + overhead = { + num_vertices = "num_vertices", + num_graph_edges = "num_edges", + num_tree_edges = "num_vertices - 1", + } +)] +impl ReduceTo for HamiltonianPath { + type Result = ReductionHPToIST; + + fn reduce_to(&self) -> Self::Result { + let n = self.num_vertices(); + + // Host graph: keep G unchanged + let graph = self.graph().clone(); + + // Target tree: path graph P_n with edges {0,1},{1,2},...,{n-2,n-1} + let path_edges: Vec<(usize, usize)> = + (0..n.saturating_sub(1)).map(|i| (i, i + 1)).collect(); + let tree = SimpleGraph::new(n, path_edges); + + ReductionHPToIST { + target: IsomorphicSpanningTree::new(graph, tree), + } + } +} + +#[cfg(feature = "example-db")] +pub(crate) fn canonical_rule_example_specs() -> Vec { + use crate::export::SolutionPair; + + vec![crate::example_db::specs::RuleExampleSpec { + id: "hamiltonianpath_to_isomorphicspanningtree", + build: || { + // Path graph 0-1-2-3-4 has a trivial Hamiltonian path + let source = + HamiltonianPath::new(SimpleGraph::new(5, vec![(0, 1), (1, 2), (2, 3), (3, 4)])); + crate::example_db::specs::rule_example_with_witness::<_, IsomorphicSpanningTree>( + source, + SolutionPair { + source_config: vec![0, 1, 2, 3, 4], + target_config: vec![0, 1, 2, 3, 4], + }, + ) + }, + }] +} + +#[cfg(test)] +#[path = "../unit_tests/rules/hamiltonianpath_isomorphicspanningtree.rs"] +mod tests; diff --git a/src/rules/kclique_conjunctivebooleanquery.rs b/src/rules/kclique_conjunctivebooleanquery.rs new file mode 100644 index 000000000..c9ee18d4c --- /dev/null +++ b/src/rules/kclique_conjunctivebooleanquery.rs @@ -0,0 +1,115 @@ +//! Reduction from KClique to ConjunctiveBooleanQuery. +//! +//! Given a KClique instance (G=(V,E), k): +//! 1. Domain D = V (n elements, indexed 0..n-1). +//! 2. Single binary relation R with tuples: for each edge {u,v}∈E, include both +//! (u,v) and (v,u). So 2|E| tuples, each of arity 2. +//! 3. Query: k existential variables, with conjuncts R(y_i, y_j) for all 0≤i; + type Target = ConjunctiveBooleanQuery; + + fn target_problem(&self) -> &ConjunctiveBooleanQuery { + &self.target + } + + /// Extract solution from CBQ back to KClique. + /// + /// CBQ config: vec of length k, each value is a domain element (vertex index). + /// KClique config: binary vec of length n; set config[v]=1 for each v in + /// the CBQ assignment. + fn extract_solution(&self, target_solution: &[usize]) -> Vec { + let mut config = vec![0; self.num_vertices]; + for &v in target_solution { + config[v] = 1; + } + config + } +} + +#[reduction( + overhead = { + domain_size = "num_vertices", + num_relations = "1", + num_variables = "k", + num_conjuncts = "k * (k - 1) / 2", + } +)] +impl ReduceTo for KClique { + type Result = ReductionKCliqueToCBQ; + + fn reduce_to(&self) -> Self::Result { + let n = self.graph().num_vertices(); + let k = self.k(); + + // Build the single binary relation: for each edge {u,v}, include (u,v) and (v,u). + let mut tuples = Vec::new(); + for u in 0..n { + for v in (u + 1)..n { + if self.graph().has_edge(u, v) { + tuples.push(vec![u, v]); + tuples.push(vec![v, u]); + } + } + } + let relation = CbqRelation { arity: 2, tuples }; + + // Build conjuncts: R(y_i, y_j) for all 0 <= i < j < k. + let mut conjuncts = Vec::new(); + for i in 0..k { + for j in (i + 1)..k { + conjuncts.push((0, vec![QueryArg::Variable(i), QueryArg::Variable(j)])); + } + } + + let target = ConjunctiveBooleanQuery::new(n, vec![relation], k, conjuncts); + + ReductionKCliqueToCBQ { + target, + 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: "kclique_to_conjunctivebooleanquery", + build: || { + // Triangle (0,1,2) in a 5-vertex graph, k=3 → has 3-clique + let source = KClique::new( + SimpleGraph::new(5, vec![(0, 1), (0, 2), (1, 2), (2, 3), (3, 4)]), + 3, + ); + crate::example_db::specs::rule_example_with_witness::<_, ConjunctiveBooleanQuery>( + source, + SolutionPair { + source_config: vec![1, 1, 1, 0, 0], + target_config: vec![0, 1, 2], + }, + ) + }, + }] +} + +#[cfg(test)] +#[path = "../unit_tests/rules/kclique_conjunctivebooleanquery.rs"] +mod tests; diff --git a/src/rules/kclique_subgraphisomorphism.rs b/src/rules/kclique_subgraphisomorphism.rs new file mode 100644 index 000000000..1fd29c7db --- /dev/null +++ b/src/rules/kclique_subgraphisomorphism.rs @@ -0,0 +1,108 @@ +//! Reduction from KClique to SubgraphIsomorphism. +//! +//! Given a KClique instance (G, k), we construct a SubgraphIsomorphism instance +//! where the host graph is G and the pattern graph is K_k (the complete graph on +//! k vertices). G contains a k-clique if and only if G contains a subgraph +//! isomorphic to K_k. + +use crate::models::graph::{KClique, SubgraphIsomorphism}; +use crate::reduction; +use crate::rules::traits::{ReduceTo, ReductionResult}; +use crate::topology::{Graph, SimpleGraph}; + +/// Result of reducing KClique to SubgraphIsomorphism. +/// +/// The host graph is the original graph G and the pattern graph is K_k. +/// A subgraph isomorphism mapping f: V(K_k) -> V(G) identifies the k vertices +/// that form a clique in G. +#[derive(Debug, Clone)] +pub struct ReductionKCliqueToSubIso { + target: SubgraphIsomorphism, + num_source_vertices: usize, +} + +impl ReductionResult for ReductionKCliqueToSubIso { + type Source = KClique; + type Target = SubgraphIsomorphism; + + fn target_problem(&self) -> &SubgraphIsomorphism { + &self.target + } + + /// Extract KClique solution from SubgraphIsomorphism solution. + /// + /// The SubgraphIsomorphism config maps each pattern vertex (0..k-1) to a + /// host vertex. We create a binary vector of length n and set positions + /// f(0), f(1), ..., f(k-1) to 1. + fn extract_solution(&self, target_solution: &[usize]) -> Vec { + let mut config = vec![0; self.num_source_vertices]; + for &host_vertex in target_solution { + config[host_vertex] = 1; + } + config + } +} + +#[reduction( + overhead = { + num_host_vertices = "num_vertices", + num_host_edges = "num_edges", + num_pattern_vertices = "k", + num_pattern_edges = "k * (k - 1) / 2", + } +)] +impl ReduceTo for KClique { + type Result = ReductionKCliqueToSubIso; + + fn reduce_to(&self) -> Self::Result { + let n = self.graph().num_vertices(); + let k = self.k(); + + // Build the complete graph K_k as the pattern + let mut pattern_edges = Vec::new(); + for i in 0..k { + for j in (i + 1)..k { + pattern_edges.push((i, j)); + } + } + let pattern = SimpleGraph::new(k, pattern_edges); + + // Host graph is the original graph, cloned into a SimpleGraph + let host_edges = self.graph().edges(); + let host = SimpleGraph::new(n, host_edges); + + let target = SubgraphIsomorphism::new(host, pattern); + + ReductionKCliqueToSubIso { + target, + num_source_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: "kclique_to_subgraphisomorphism", + build: || { + // 5-vertex graph with a known 3-clique on vertices {2, 3, 4} + let source = KClique::new( + SimpleGraph::new(5, vec![(0, 1), (0, 2), (1, 3), (2, 3), (2, 4), (3, 4)]), + 3, + ); + crate::example_db::specs::rule_example_with_witness::<_, SubgraphIsomorphism>( + source, + SolutionPair { + source_config: vec![0, 0, 1, 1, 1], + target_config: vec![2, 3, 4], + }, + ) + }, + }] +} + +#[cfg(test)] +#[path = "../unit_tests/rules/kclique_subgraphisomorphism.rs"] +mod tests; diff --git a/src/rules/mod.rs b/src/rules/mod.rs index 1d9c5e77b..e2b67adea 100644 --- a/src/rules/mod.rs +++ b/src/rules/mod.rs @@ -9,9 +9,15 @@ pub use registry::{EdgeCapabilities, ReductionEntry, ReductionOverhead}; pub(crate) mod circuit_spinglass; mod closestvectorproblem_qubo; pub(crate) mod coloring_qubo; +pub(crate) mod exactcoverby3sets_staffscheduling; pub(crate) mod factoring_circuit; mod graph; +pub(crate) mod hamiltoniancircuit_bottlenecktravelingsalesman; +pub(crate) mod hamiltoniancircuit_hamiltonianpath; pub(crate) mod hamiltoniancircuit_travelingsalesman; +pub(crate) mod hamiltonianpath_isomorphicspanningtree; +pub(crate) mod kclique_conjunctivebooleanquery; +pub(crate) mod kclique_subgraphisomorphism; mod kcoloring_casts; mod knapsack_qubo; mod ksatisfiability_casts; @@ -31,11 +37,13 @@ pub(crate) mod minimumvertexcover_maximumindependentset; pub(crate) mod minimumvertexcover_minimumfeedbackvertexset; pub(crate) mod minimumvertexcover_minimumsetcovering; pub(crate) mod partition_knapsack; +pub(crate) mod partition_multiprocessorscheduling; pub(crate) mod sat_circuitsat; pub(crate) mod sat_coloring; pub(crate) mod sat_ksat; pub(crate) mod sat_maximumindependentset; pub(crate) mod sat_minimumdominatingset; +pub(crate) mod satisfiability_naesatisfiability; mod spinglass_casts; pub(crate) mod spinglass_maxcut; pub(crate) mod spinglass_qubo; @@ -232,10 +240,16 @@ pub use traits::{ pub(crate) fn canonical_rule_example_specs() -> Vec { let mut specs = Vec::new(); specs.extend(circuit_spinglass::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()); specs.extend(factoring_circuit::canonical_rule_example_specs()); + specs.extend(hamiltoniancircuit_bottlenecktravelingsalesman::canonical_rule_example_specs()); + specs.extend(hamiltoniancircuit_hamiltonianpath::canonical_rule_example_specs()); specs.extend(hamiltoniancircuit_travelingsalesman::canonical_rule_example_specs()); + specs.extend(hamiltonianpath_isomorphicspanningtree::canonical_rule_example_specs()); + specs.extend(kclique_conjunctivebooleanquery::canonical_rule_example_specs()); + specs.extend(kclique_subgraphisomorphism::canonical_rule_example_specs()); specs.extend(knapsack_qubo::canonical_rule_example_specs()); specs.extend(ksatisfiability_qubo::canonical_rule_example_specs()); specs.extend(ksatisfiability_subsetsum::canonical_rule_example_specs()); @@ -246,9 +260,11 @@ pub(crate) fn canonical_rule_example_specs() -> Vec &Self::Target { + &self.target + } + + /// Solution extraction: identity mapping. + /// Partition config (0/1 for subset) maps directly to processor assignment (0/1). + fn extract_solution(&self, target_solution: &[usize]) -> Vec { + target_solution.to_vec() + } +} + +#[reduction(overhead = { + num_tasks = "num_elements", +})] +impl ReduceTo for Partition { + type Result = ReductionPartitionToMPS; + + fn reduce_to(&self) -> Self::Result { + let lengths: Vec = self.sizes().to_vec(); + let deadline = self.total_sum() / 2; + + ReductionPartitionToMPS { + target: MultiprocessorScheduling::new(lengths, 2, deadline), + } + } +} + +#[cfg(feature = "example-db")] +pub(crate) fn canonical_rule_example_specs() -> Vec { + use crate::export::SolutionPair; + + vec![crate::example_db::specs::RuleExampleSpec { + id: "partition_to_multiprocessorscheduling", + build: || { + // sizes [1, 2, 3, 4], sum=10, target=5 + // partition: {1,4} on proc 0 and {2,3} on proc 1 + crate::example_db::specs::rule_example_with_witness::<_, MultiprocessorScheduling>( + Partition::new(vec![1, 2, 3, 4]), + SolutionPair { + source_config: vec![0, 1, 1, 0], + target_config: vec![0, 1, 1, 0], + }, + ) + }, + }] +} + +#[cfg(test)] +#[path = "../unit_tests/rules/partition_multiprocessorscheduling.rs"] +mod tests; diff --git a/src/rules/satisfiability_naesatisfiability.rs b/src/rules/satisfiability_naesatisfiability.rs new file mode 100644 index 000000000..8d9206eb8 --- /dev/null +++ b/src/rules/satisfiability_naesatisfiability.rs @@ -0,0 +1,105 @@ +//! Reduction from Satisfiability to NAE-Satisfiability. +//! +//! Given a SAT instance with n variables and m clauses, we construct an +//! equisatisfiable NAE-SAT instance by adding a fresh sentinel variable s. +//! Each SAT clause C_j = (l_1 ∨ ... ∨ l_k) becomes NAE clause +//! C'_j = (l_1, ..., l_k, s). The sentinel ensures that each NAE clause +//! has at least one false literal (the sentinel itself when s=false, or +//! the complement of the original satisfied literal when s=true). + +use crate::models::formula::{CNFClause, NAESatisfiability, Satisfiability}; +use crate::reduction; +use crate::rules::traits::{ReduceTo, ReductionResult}; + +/// Result of reducing Satisfiability to NAE-Satisfiability. +#[derive(Debug, Clone)] +pub struct ReductionSATToNAESAT { + /// Number of original variables in the source problem. + source_num_vars: usize, + /// The target NAE-SAT problem. + target: NAESatisfiability, +} + +impl ReductionResult for ReductionSATToNAESAT { + type Source = Satisfiability; + type Target = NAESatisfiability; + + fn target_problem(&self) -> &Self::Target { + &self.target + } + + fn extract_solution(&self, target_solution: &[usize]) -> Vec { + let n = self.source_num_vars; + // The sentinel variable is the last variable (index n). + let sentinel_value = target_solution[n]; + if sentinel_value == 0 { + // Sentinel is false: return first n variables as-is. + target_solution[..n].to_vec() + } else { + // Sentinel is true: return complement of first n variables. + target_solution[..n].iter().map(|&v| 1 - v).collect() + } + } +} + +#[reduction(overhead = { + num_vars = "num_vars + 1", + num_clauses = "num_clauses", + num_literals = "num_literals + num_clauses", +})] +impl ReduceTo for Satisfiability { + type Result = ReductionSATToNAESAT; + + fn reduce_to(&self) -> Self::Result { + let n = self.num_vars(); + // Sentinel variable has 0-indexed position n, so its 1-indexed literal is n+1. + let sentinel_lit = (n + 1) as i32; + + let nae_clauses: Vec = self + .clauses() + .iter() + .map(|clause| { + let mut lits = clause.literals.clone(); + lits.push(sentinel_lit); + CNFClause::new(lits) + }) + .collect(); + + let target = NAESatisfiability::new(n + 1, nae_clauses); + + ReductionSATToNAESAT { + source_num_vars: n, + target, + } + } +} + +#[cfg(feature = "example-db")] +pub(crate) fn canonical_rule_example_specs() -> Vec { + use crate::export::SolutionPair; + + vec![crate::example_db::specs::RuleExampleSpec { + id: "satisfiability_to_naesatisfiability", + build: || { + let source = Satisfiability::new( + 3, + vec![ + CNFClause::new(vec![1, 2]), + CNFClause::new(vec![-1, 3]), + CNFClause::new(vec![-2, -3]), + ], + ); + crate::example_db::specs::rule_example_with_witness::<_, NAESatisfiability>( + source, + SolutionPair { + source_config: vec![0, 1, 0], + target_config: vec![0, 1, 0, 0], + }, + ) + }, + }] +} + +#[cfg(test)] +#[path = "../unit_tests/rules/satisfiability_naesatisfiability.rs"] +mod tests; diff --git a/src/unit_tests/rules/exactcoverby3sets_staffscheduling.rs b/src/unit_tests/rules/exactcoverby3sets_staffscheduling.rs new file mode 100644 index 000000000..a8e7ed6e3 --- /dev/null +++ b/src/unit_tests/rules/exactcoverby3sets_staffscheduling.rs @@ -0,0 +1,111 @@ +use super::*; +use crate::models::misc::StaffScheduling; +use crate::models::set::ExactCoverBy3Sets; +use crate::rules::test_helpers::assert_satisfaction_round_trip_from_satisfaction_target; +use crate::rules::ReduceTo; +use crate::solvers::BruteForce; +use crate::traits::Problem; + +#[test] +fn test_exactcoverby3sets_to_staffscheduling_closed_loop() { + // Universe {0,1,2,3,4,5}, subsets [{0,1,2}, {3,4,5}, {0,3,4}, {1,2,5}] + // Exact cover: S0={0,1,2} + S1={3,4,5} + let source = ExactCoverBy3Sets::new(6, vec![[0, 1, 2], [3, 4, 5], [0, 3, 4], [1, 2, 5]]); + let result = ReduceTo::::reduce_to(&source); + let target = result.target_problem(); + + // Check target dimensions + assert_eq!(target.num_periods(), 6); + assert_eq!(target.shifts_per_schedule(), 3); + assert_eq!(target.num_schedules(), 4); + assert_eq!(target.num_workers(), 2); // q = 6/3 = 2 + + assert_satisfaction_round_trip_from_satisfaction_target( + &source, + &result, + "ExactCoverBy3Sets->StaffScheduling closed loop", + ); +} + +#[test] +fn test_exactcoverby3sets_to_staffscheduling_no_solution() { + // Universe {0,1,2,3,4,5} with overlapping subsets that cannot form exact cover + // All subsets share element 0 + let source = ExactCoverBy3Sets::new(6, vec![[0, 1, 2], [0, 3, 4], [0, 4, 5]]); + let result = ReduceTo::::reduce_to(&source); + let solver = BruteForce::new(); + let solutions = solver.find_all_witnesses(result.target_problem()); + assert!( + solutions.is_empty(), + "No exact cover exists, so StaffScheduling should have no solution" + ); +} + +#[test] +fn test_exactcoverby3sets_to_staffscheduling_unique_cover() { + // Universe {0,1,2,3,4,5,6,7,8} (q=3) + // Only one exact cover: S0 + S1 + S2 + let source = ExactCoverBy3Sets::new(9, vec![[0, 1, 2], [3, 4, 5], [6, 7, 8]]); + let result = ReduceTo::::reduce_to(&source); + let target = result.target_problem(); + + assert_eq!(target.num_periods(), 9); + assert_eq!(target.num_workers(), 3); // q = 9/3 = 3 + + let solver = BruteForce::new(); + let solutions = solver.find_all_witnesses(target); + // Each satisfying target config should extract to selecting all 3 subsets + for sol in &solutions { + let extracted = result.extract_solution(sol); + assert!( + source.evaluate(&extracted).0, + "Extracted solution must be valid" + ); + } + // There should be exactly one satisfying assignment (up to extraction) + let extracted_solutions: Vec> = solutions + .iter() + .map(|s| result.extract_solution(s)) + .collect(); + assert!( + extracted_solutions.iter().all(|s| *s == vec![1, 1, 1]), + "Only exact cover is all three subsets" + ); +} + +#[test] +fn test_exactcoverby3sets_to_staffscheduling_extract_solution() { + // Verify extract_solution maps correctly + let source = ExactCoverBy3Sets::new(6, vec![[0, 1, 2], [3, 4, 5], [0, 3, 4], [1, 2, 5]]); + let result = ReduceTo::::reduce_to(&source); + + // StaffScheduling config: [1, 1, 0, 0] means 1 worker on schedule 0 and 1 on schedule 1 + let target_config = vec![1, 1, 0, 0]; + let extracted = result.extract_solution(&target_config); + assert_eq!(extracted, vec![1, 1, 0, 0]); + + // Verify the extracted solution is valid in the source + assert!(source.evaluate(&extracted).0); + + // Config with 0 workers everywhere should extract to all-zero (no subsets selected) + let empty_config = vec![0, 0, 0, 0]; + let extracted_empty = result.extract_solution(&empty_config); + assert_eq!(extracted_empty, vec![0, 0, 0, 0]); +} + +#[test] +fn test_exactcoverby3sets_to_staffscheduling_schedule_structure() { + // Verify the schedule patterns are correctly constructed + let source = ExactCoverBy3Sets::new(6, vec![[0, 1, 2], [3, 4, 5]]); + let result = ReduceTo::::reduce_to(&source); + let target = result.target_problem(); + + let schedules = target.schedules(); + // Schedule 0 should have shifts at positions 0, 1, 2 + assert_eq!(schedules[0], vec![true, true, true, false, false, false]); + // Schedule 1 should have shifts at positions 3, 4, 5 + assert_eq!(schedules[1], vec![false, false, false, true, true, true]); + + // Requirements should all be 1 + assert!(target.requirements().iter().all(|&r| r == 1)); +} diff --git a/src/unit_tests/rules/hamiltoniancircuit_bottlenecktravelingsalesman.rs b/src/unit_tests/rules/hamiltoniancircuit_bottlenecktravelingsalesman.rs new file mode 100644 index 000000000..be81f53d8 --- /dev/null +++ b/src/unit_tests/rules/hamiltoniancircuit_bottlenecktravelingsalesman.rs @@ -0,0 +1,82 @@ +use crate::models::graph::{BottleneckTravelingSalesman, HamiltonianCircuit}; +use crate::rules::test_helpers::assert_satisfaction_round_trip_from_optimization_target; +use crate::rules::ReduceTo; +use crate::rules::ReductionResult; +use crate::solvers::BruteForce; +use crate::topology::{Graph, SimpleGraph}; +use crate::types::Min; +use crate::Problem; + +fn cycle5_hc() -> HamiltonianCircuit { + HamiltonianCircuit::new(SimpleGraph::cycle(5)) +} + +#[test] +fn test_hamiltoniancircuit_to_bottlenecktravelingsalesman_closed_loop() { + let source = cycle5_hc(); + let reduction = ReduceTo::::reduce_to(&source); + + assert_satisfaction_round_trip_from_optimization_target( + &source, + &reduction, + "HamiltonianCircuit -> BottleneckTravelingSalesman", + ); +} + +#[test] +fn test_hamiltoniancircuit_to_bottlenecktravelingsalesman_structure() { + let source = cycle5_hc(); + let reduction = ReduceTo::::reduce_to(&source); + let target = reduction.target_problem(); + + // Complete graph on 5 vertices: C(5,2) = 10 edges + assert_eq!(target.graph().num_vertices(), 5); + assert_eq!(target.graph().num_edges(), 10); + + // Edge weights: 1 for cycle edges, 2 for non-cycle edges + for ((u, v), weight) in target.graph().edges().into_iter().zip(target.weights()) { + let expected = if source.graph().has_edge(u, v) { 1 } else { 2 }; + assert_eq!(weight, expected, "unexpected weight on edge ({u}, {v})"); + } +} + +#[test] +fn test_hamiltoniancircuit_to_bottlenecktravelingsalesman_nonhamiltonian_bottleneck_gap() { + // Star graph has no Hamiltonian circuit, so optimal bottleneck must exceed 1 + let source = HamiltonianCircuit::new(SimpleGraph::star(5)); + let reduction = ReduceTo::::reduce_to(&source); + let target = reduction.target_problem(); + let best = BruteForce::new() + .find_witness(target) + .expect("complete weighted graph should always admit a tour"); + + let metric = target.evaluate(&best); + assert!(metric.is_valid(), "best BTSP solution evaluated as invalid"); + assert!( + metric.unwrap() > 1, + "expected bottleneck > 1 for non-Hamiltonian source" + ); +} + +#[test] +fn test_hamiltoniancircuit_to_bottlenecktravelingsalesman_extract_solution_cycle() { + let source = cycle5_hc(); + let reduction = ReduceTo::::reduce_to(&source); + let target = reduction.target_problem(); + + // Manually select the cycle edges in the complete graph + let cycle_edges = [(0usize, 1usize), (1, 2), (2, 3), (3, 4), (0, 4)]; + let target_solution: Vec = target + .graph() + .edges() + .into_iter() + .map(|(u, v)| usize::from(cycle_edges.contains(&(u, v)) || cycle_edges.contains(&(v, u)))) + .collect(); + + let extracted = reduction.extract_solution(&target_solution); + + // Bottleneck should be 1 (all selected edges are original cycle edges) + assert_eq!(target.evaluate(&target_solution), Min(Some(1))); + assert_eq!(extracted.len(), 5); + assert!(source.evaluate(&extracted).is_valid()); +} diff --git a/src/unit_tests/rules/hamiltoniancircuit_hamiltonianpath.rs b/src/unit_tests/rules/hamiltoniancircuit_hamiltonianpath.rs new file mode 100644 index 000000000..cd1a15502 --- /dev/null +++ b/src/unit_tests/rules/hamiltoniancircuit_hamiltonianpath.rs @@ -0,0 +1,112 @@ +use crate::models::graph::{HamiltonianCircuit, HamiltonianPath}; +use crate::rules::test_helpers::assert_satisfaction_round_trip_from_satisfaction_target; +use crate::rules::ReduceTo; +use crate::rules::ReductionResult; +use crate::solvers::BruteForce; +use crate::topology::{Graph, SimpleGraph}; +use crate::Problem; + +fn cycle4_hc() -> HamiltonianCircuit { + HamiltonianCircuit::new(SimpleGraph::cycle(4)) +} + +#[test] +fn test_hamiltoniancircuit_to_hamiltonianpath_closed_loop() { + let source = cycle4_hc(); + let reduction = ReduceTo::>::reduce_to(&source); + + assert_satisfaction_round_trip_from_satisfaction_target( + &source, + &reduction, + "HamiltonianCircuit -> HamiltonianPath", + ); +} + +#[test] +fn test_hamiltoniancircuit_to_hamiltonianpath_structure() { + let source = cycle4_hc(); + let reduction = ReduceTo::>::reduce_to(&source); + let target = reduction.target_problem(); + + // Original: 4 vertices, 4 edges (cycle) + // Target: 4 + 3 = 7 vertices + assert_eq!(target.graph().num_vertices(), 7); + + // deg(0) in cycle4 = 2, so target edges = 4 + 2 + 2 = 8 + assert_eq!(target.graph().num_edges(), 8); + + // s (=5) should only be connected to vertex 0 + let s_neighbors = target.graph().neighbors(5); + assert_eq!(s_neighbors, vec![0]); + + // t (=6) should only be connected to v' (=4) + let t_neighbors = target.graph().neighbors(6); + assert_eq!(t_neighbors, vec![4]); + + // v' (=4) should be connected to neighbors of 0 in original graph plus t + let v_prime_neighbors = target.graph().neighbors(4); + assert!(v_prime_neighbors.contains(&1)); // neighbor of 0 + assert!(v_prime_neighbors.contains(&3)); // neighbor of 0 + assert!(v_prime_neighbors.contains(&6)); // t +} + +#[test] +fn test_hamiltoniancircuit_to_hamiltonianpath_extract_solution() { + let source = cycle4_hc(); + let reduction = ReduceTo::>::reduce_to(&source); + + // HP solution: s=5, 0, 1, 2, 3, v'=4, t=6 + let hp_config = vec![5, 0, 1, 2, 3, 4, 6]; + let extracted = reduction.extract_solution(&hp_config); + + assert_eq!(extracted.len(), 4); + assert!( + source.evaluate(&extracted).0, + "extracted solution must be a valid HC" + ); +} + +#[test] +fn test_hamiltoniancircuit_to_hamiltonianpath_extract_reversed() { + let source = cycle4_hc(); + let reduction = ReduceTo::>::reduce_to(&source); + + // HP solution reversed: t=6, v'=4, 3, 2, 1, 0, s=5 + let hp_config = vec![6, 4, 3, 2, 1, 0, 5]; + let extracted = reduction.extract_solution(&hp_config); + + assert_eq!(extracted.len(), 4); + assert!( + source.evaluate(&extracted).0, + "extracted reversed solution must be a valid HC" + ); +} + +#[test] +fn test_hamiltoniancircuit_to_hamiltonianpath_no_circuit() { + // Path graph 0-1-2-3: no Hamiltonian circuit (vertices 0 and 3 have degree 1) + let source = HamiltonianCircuit::new(SimpleGraph::new(4, vec![(0, 1), (1, 2), (2, 3)])); + let reduction = ReduceTo::>::reduce_to(&source); + let target = reduction.target_problem(); + + // The target should have no Hamiltonian path (since source has no HC) + let solver = BruteForce::new(); + let witness = solver.find_witness(target); + assert!( + witness.is_none(), + "target should have no HP when source has no HC" + ); +} + +#[test] +fn test_hamiltoniancircuit_to_hamiltonianpath_triangle() { + // Triangle graph: 3 vertices, 3 edges, has HC + let source = HamiltonianCircuit::new(SimpleGraph::cycle(3)); + let reduction = ReduceTo::>::reduce_to(&source); + + assert_satisfaction_round_trip_from_satisfaction_target( + &source, + &reduction, + "HamiltonianCircuit(triangle) -> HamiltonianPath", + ); +} diff --git a/src/unit_tests/rules/hamiltonianpath_isomorphicspanningtree.rs b/src/unit_tests/rules/hamiltonianpath_isomorphicspanningtree.rs new file mode 100644 index 000000000..65483d472 --- /dev/null +++ b/src/unit_tests/rules/hamiltonianpath_isomorphicspanningtree.rs @@ -0,0 +1,110 @@ +use super::*; +use crate::models::graph::{HamiltonianPath, IsomorphicSpanningTree}; +use crate::rules::test_helpers::{ + assert_satisfaction_round_trip_from_satisfaction_target, solve_satisfaction_problem, +}; +use crate::rules::ReduceTo; +use crate::solvers::BruteForce; +use crate::topology::SimpleGraph; +use crate::traits::Problem; + +#[test] +fn test_hamiltonianpath_to_isomorphicspanningtree_closed_loop() { + // Graph with a known Hamiltonian path: 0-1-2-3-4 plus extra edges + let source = HamiltonianPath::new(SimpleGraph::new( + 5, + vec![(0, 1), (1, 2), (2, 3), (3, 4), (0, 3), (1, 4)], + )); + let result = ReduceTo::::reduce_to(&source); + let target = result.target_problem(); + + // Target should have same number of vertices and edges as source graph + assert_eq!(target.num_vertices(), 5); + assert_eq!(target.num_graph_edges(), 6); + // Tree is P_5: 4 edges + assert_eq!(target.num_tree_edges(), 4); + + assert_satisfaction_round_trip_from_satisfaction_target( + &source, + &result, + "HamiltonianPath->IsomorphicSpanningTree closed loop", + ); +} + +#[test] +fn test_hamiltonianpath_to_isomorphicspanningtree_path_graph() { + // Simple path graph: 0-1-2-3 (trivially has a Hamiltonian path) + let source = HamiltonianPath::new(SimpleGraph::new(4, vec![(0, 1), (1, 2), (2, 3)])); + let result = ReduceTo::::reduce_to(&source); + + assert_satisfaction_round_trip_from_satisfaction_target( + &source, + &result, + "HamiltonianPath->IsomorphicSpanningTree path graph", + ); +} + +#[test] +fn test_hamiltonianpath_to_isomorphicspanningtree_no_hamiltonian_path() { + // Star graph K_{1,4}: vertex 0 connected to 1,2,3,4 with no other edges. + // This has no Hamiltonian path because vertex 0 must appear in the middle + // but has only degree 4 neighbors that are pairwise non-adjacent. + // Actually for n=5 star, vertex 0 has degree 4, so it can be internal, + // but the leaves have degree 1, so at most 2 can be endpoints. + // A path visits 5 vertices needing 4 edges, but all edges go through 0. + // So the path must be leaf-0-leaf-..., but after visiting 0 we can only + // go to unvisited leaves, and from a leaf we can only go back to 0 (already visited). + // Path: leaf-0-leaf is length 2, can't extend. No HP exists. + let source = HamiltonianPath::new(SimpleGraph::new(5, vec![(0, 1), (0, 2), (0, 3), (0, 4)])); + let result = ReduceTo::::reduce_to(&source); + let solver = BruteForce::new(); + let target_solutions = solver.find_all_witnesses(result.target_problem()); + assert!( + target_solutions.is_empty(), + "Star graph K_{{1,4}} should have no Hamiltonian path" + ); + + // Also verify source has no solution + let source_solutions = solver.find_all_witnesses(&source); + assert!( + source_solutions.is_empty(), + "Star graph K_{{1,4}} should have no Hamiltonian path (direct check)" + ); +} + +#[test] +fn test_hamiltonianpath_to_isomorphicspanningtree_complete_graph() { + // Complete graph K4: every permutation is a valid Hamiltonian path + let source = HamiltonianPath::new(SimpleGraph::new( + 4, + vec![(0, 1), (0, 2), (0, 3), (1, 2), (1, 3), (2, 3)], + )); + let result = ReduceTo::::reduce_to(&source); + + let target_solution = solve_satisfaction_problem(result.target_problem()) + .expect("K4 should have an IST solution"); + let extracted = result.extract_solution(&target_solution); + // Extracted solution should be a valid Hamiltonian path + assert!( + source.evaluate(&extracted).0, + "Extracted solution should be a valid Hamiltonian path" + ); +} + +#[test] +fn test_hamiltonianpath_to_isomorphicspanningtree_small_triangle() { + // Triangle: 0-1-2-0 (has Hamiltonian path, e.g. 0-1-2) + let source = HamiltonianPath::new(SimpleGraph::new(3, vec![(0, 1), (1, 2), (0, 2)])); + let result = ReduceTo::::reduce_to(&source); + let target = result.target_problem(); + + assert_eq!(target.num_vertices(), 3); + assert_eq!(target.num_graph_edges(), 3); + assert_eq!(target.num_tree_edges(), 2); + + assert_satisfaction_round_trip_from_satisfaction_target( + &source, + &result, + "HamiltonianPath->IsomorphicSpanningTree triangle", + ); +} diff --git a/src/unit_tests/rules/kclique_conjunctivebooleanquery.rs b/src/unit_tests/rules/kclique_conjunctivebooleanquery.rs new file mode 100644 index 000000000..ddfcbb7a6 --- /dev/null +++ b/src/unit_tests/rules/kclique_conjunctivebooleanquery.rs @@ -0,0 +1,95 @@ +use crate::models::graph::KClique; +use crate::models::misc::ConjunctiveBooleanQuery; +use crate::rules::kclique_conjunctivebooleanquery::ReductionKCliqueToCBQ; +use crate::rules::test_helpers::assert_satisfaction_round_trip_from_satisfaction_target; +use crate::rules::traits::{ReduceTo, ReductionResult}; +use crate::solvers::BruteForce; +use crate::topology::SimpleGraph; +use crate::traits::Problem; +use crate::types::Or; + +#[test] +fn test_kclique_to_conjunctivebooleanquery_closed_loop() { + // Triangle graph (0,1,2) plus extra edges, k=3 + let graph = SimpleGraph::new(5, vec![(0, 1), (0, 2), (1, 2), (2, 3), (3, 4)]); + let problem = KClique::new(graph, 3); + let reduction: ReductionKCliqueToCBQ = ReduceTo::::reduce_to(&problem); + + assert_satisfaction_round_trip_from_satisfaction_target( + &problem, + &reduction, + "KClique -> CBQ triangle", + ); +} + +#[test] +fn test_reduction_structure() { + // Complete graph K4, k=3 + let graph = SimpleGraph::new(4, vec![(0, 1), (0, 2), (0, 3), (1, 2), (1, 3), (2, 3)]); + let problem = KClique::new(graph, 3); + let reduction: ReductionKCliqueToCBQ = ReduceTo::::reduce_to(&problem); + let cbq = reduction.target_problem(); + + // domain_size = num_vertices = 4 + assert_eq!(cbq.domain_size(), 4); + // 1 relation + assert_eq!(cbq.num_relations(), 1); + // k=3 variables + assert_eq!(cbq.num_variables(), 3); + // k*(k-1)/2 = 3 conjuncts + assert_eq!(cbq.num_conjuncts(), 3); + // K4 has 6 edges, so relation has 12 tuples + assert_eq!(cbq.relations()[0].tuples.len(), 12); + assert_eq!(cbq.relations()[0].arity, 2); +} + +#[test] +fn test_no_clique_infeasible() { + // Path graph 0-1-2, k=3 → no triangle + let graph = SimpleGraph::new(3, vec![(0, 1), (1, 2)]); + let problem = KClique::new(graph, 3); + let reduction: ReductionKCliqueToCBQ = ReduceTo::::reduce_to(&problem); + + let bf = BruteForce::new(); + // Source has no 3-clique + assert_eq!(bf.find_witness(&problem), None); + // Target CBQ should also be unsatisfiable + assert_eq!(bf.find_witness(reduction.target_problem()), None); +} + +#[test] +fn test_solution_extraction() { + // Triangle graph, k=3 + let graph = SimpleGraph::new(3, vec![(0, 1), (0, 2), (1, 2)]); + let problem = KClique::new(graph, 3); + let reduction: ReductionKCliqueToCBQ = ReduceTo::::reduce_to(&problem); + + let bf = BruteForce::new(); + let cbq_witness = bf + .find_witness(reduction.target_problem()) + .expect("CBQ should be satisfiable"); + let extracted = reduction.extract_solution(&cbq_witness); + assert_eq!(problem.evaluate(&extracted), Or(true)); + // All 3 vertices should be selected + assert_eq!(extracted.iter().sum::(), 3); +} + +#[test] +fn test_trivial_k1() { + // Any graph with at least 1 vertex, k=1 → always feasible + let graph = SimpleGraph::new(3, vec![(0, 1)]); + let problem = KClique::new(graph, 1); + let reduction: ReductionKCliqueToCBQ = ReduceTo::::reduce_to(&problem); + let cbq = reduction.target_problem(); + + // k=1: 0 conjuncts, 1 variable + assert_eq!(cbq.num_variables(), 1); + assert_eq!(cbq.num_conjuncts(), 0); + + let bf = BruteForce::new(); + let witness = bf + .find_witness(reduction.target_problem()) + .expect("k=1 should be feasible"); + let extracted = reduction.extract_solution(&witness); + assert_eq!(problem.evaluate(&extracted), Or(true)); +} diff --git a/src/unit_tests/rules/kclique_subgraphisomorphism.rs b/src/unit_tests/rules/kclique_subgraphisomorphism.rs new file mode 100644 index 000000000..d2abaf38c --- /dev/null +++ b/src/unit_tests/rules/kclique_subgraphisomorphism.rs @@ -0,0 +1,116 @@ +use super::*; +use crate::rules::test_helpers::assert_satisfaction_round_trip_from_satisfaction_target; +use crate::solvers::BruteForce; +use crate::traits::Problem; +use crate::types::Or; + +#[test] +fn test_kclique_to_subgraphisomorphism_closed_loop() { + // 5-vertex graph with a known 3-clique on vertices {2, 3, 4} + // Edges: 0-1, 0-2, 1-3, 2-3, 2-4, 3-4 + let source = KClique::new( + SimpleGraph::new(5, vec![(0, 1), (0, 2), (1, 3), (2, 3), (2, 4), (3, 4)]), + 3, + ); + let reduction = ReduceTo::::reduce_to(&source); + let target = reduction.target_problem(); + + // Host graph should match the source graph + assert_eq!(target.num_host_vertices(), 5); + assert_eq!(target.num_host_edges(), 6); + // Pattern is K_3: 3 vertices, 3 edges + assert_eq!(target.num_pattern_vertices(), 3); + assert_eq!(target.num_pattern_edges(), 3); + + assert_satisfaction_round_trip_from_satisfaction_target( + &source, + &reduction, + "KClique->SubgraphIsomorphism closed loop", + ); +} + +#[test] +fn test_kclique_to_subgraphisomorphism_complete_graph() { + // K4 graph, k=3 -> should find a 3-clique + let source = KClique::new( + SimpleGraph::new(4, vec![(0, 1), (0, 2), (0, 3), (1, 2), (1, 3), (2, 3)]), + 3, + ); + let reduction = ReduceTo::::reduce_to(&source); + let target = reduction.target_problem(); + + assert_eq!(target.num_host_vertices(), 4); + assert_eq!(target.num_host_edges(), 6); + assert_eq!(target.num_pattern_vertices(), 3); + assert_eq!(target.num_pattern_edges(), 3); + + // Solve the target and extract back to source + let bf = BruteForce::new(); + let witness = bf.find_witness(target).expect("K4 should contain K3"); + let extracted = reduction.extract_solution(&witness); + assert_eq!(source.evaluate(&extracted), Or(true)); + // Exactly 3 vertices should be selected + assert_eq!(extracted.iter().sum::(), 3); +} + +#[test] +fn test_kclique_to_subgraphisomorphism_no_clique() { + // Path graph: 0-1-2-3, k=3 -> no 3-clique exists + let source = KClique::new(SimpleGraph::new(4, vec![(0, 1), (1, 2), (2, 3)]), 3); + let reduction = ReduceTo::::reduce_to(&source); + let target = reduction.target_problem(); + + assert_eq!(target.num_host_vertices(), 4); + assert_eq!(target.num_host_edges(), 3); + assert_eq!(target.num_pattern_vertices(), 3); + assert_eq!(target.num_pattern_edges(), 3); + + // No subgraph isomorphism should exist + let bf = BruteForce::new(); + let witness = bf.find_witness(target); + assert!(witness.is_none(), "path graph should not contain K3"); + + // Also verify brute force on source agrees + let source_witness = bf.find_witness(&source); + assert!(source_witness.is_none()); +} + +#[test] +fn test_kclique_to_subgraphisomorphism_k_equals_1() { + // Any non-empty graph has a 1-clique (single vertex) + let source = KClique::new(SimpleGraph::new(3, vec![(0, 1)]), 1); + let reduction = ReduceTo::::reduce_to(&source); + let target = reduction.target_problem(); + + // Pattern is K_1: 1 vertex, 0 edges + assert_eq!(target.num_pattern_vertices(), 1); + assert_eq!(target.num_pattern_edges(), 0); + + let bf = BruteForce::new(); + let witness = bf + .find_witness(target) + .expect("should find a single vertex"); + let extracted = reduction.extract_solution(&witness); + assert_eq!(source.evaluate(&extracted), Or(true)); + assert_eq!(extracted.iter().sum::(), 1); +} + +#[test] +fn test_kclique_to_subgraphisomorphism_k_equals_2() { + // k=2 means we need an edge + let source = KClique::new(SimpleGraph::new(4, vec![(0, 1), (2, 3)]), 2); + let reduction = ReduceTo::::reduce_to(&source); + let target = reduction.target_problem(); + + // Pattern is K_2: 2 vertices, 1 edge + assert_eq!(target.num_pattern_vertices(), 2); + assert_eq!(target.num_pattern_edges(), 1); + + let bf = BruteForce::new(); + let witness = bf + .find_witness(target) + .expect("graph has edges, so K2 exists"); + let extracted = reduction.extract_solution(&witness); + assert_eq!(source.evaluate(&extracted), Or(true)); + assert_eq!(extracted.iter().sum::(), 2); +} diff --git a/src/unit_tests/rules/partition_multiprocessorscheduling.rs b/src/unit_tests/rules/partition_multiprocessorscheduling.rs new file mode 100644 index 000000000..66a0dbf73 --- /dev/null +++ b/src/unit_tests/rules/partition_multiprocessorscheduling.rs @@ -0,0 +1,149 @@ +use super::*; +use crate::models::misc::Partition; +use crate::rules::test_helpers::assert_satisfaction_round_trip_from_satisfaction_target; +use crate::solvers::BruteForce; +use crate::traits::Problem; + +#[test] +fn test_partition_to_multiprocessorscheduling_closed_loop() { + // sizes [1, 2, 3, 4], sum=10, target=5 + // partition: {1,4} and {2,3} + let source = Partition::new(vec![1, 2, 3, 4]); + let reduction = ReduceTo::::reduce_to(&source); + + assert_satisfaction_round_trip_from_satisfaction_target( + &source, + &reduction, + "Partition -> MultiprocessorScheduling closed loop", + ); +} + +#[test] +fn test_partition_to_multiprocessorscheduling_structure() { + let source = Partition::new(vec![1, 2, 3, 4]); + let reduction = ReduceTo::::reduce_to(&source); + let target = reduction.target_problem(); + + assert_eq!(target.lengths(), &[1, 2, 3, 4]); + assert_eq!(target.num_processors(), 2); + assert_eq!(target.deadline(), 5); // sum=10, 10/2=5 + assert_eq!(target.num_tasks(), source.num_elements()); +} + +#[test] +fn test_partition_to_multiprocessorscheduling_odd_sum() { + // sum = 2+4+5 = 11 (odd), no valid partition exists + let source = Partition::new(vec![2, 4, 5]); + let reduction = ReduceTo::::reduce_to(&source); + let target = reduction.target_problem(); + + // deadline = floor(11/2) = 5 + assert_eq!(target.deadline(), 5); + assert_eq!(target.num_processors(), 2); + + // Source is not satisfiable (odd sum) + let solver = BruteForce::new(); + let source_solutions = solver.find_all_witnesses(&source); + assert!(source_solutions.is_empty()); + + // Target should also be infeasible: total=11, floor(11/2)=5, + // so one processor must get at least ceil(11/2)=6 > 5 + let target_solutions = solver.find_all_witnesses(target); + assert!(target_solutions.is_empty()); +} + +#[test] +fn test_partition_to_multiprocessorscheduling_equal_elements() { + // [3, 3, 3, 3], sum=12, target=6 + let source = Partition::new(vec![3, 3, 3, 3]); + let reduction = ReduceTo::::reduce_to(&source); + let target = reduction.target_problem(); + + assert_eq!(target.deadline(), 6); + + // Both should be satisfiable (e.g., {3,3} and {3,3}) + let solver = BruteForce::new(); + let source_solutions = solver.find_all_witnesses(&source); + let target_solutions = solver.find_all_witnesses(target); + + assert!(!source_solutions.is_empty()); + assert!(!target_solutions.is_empty()); + + // Round trip should work + assert_satisfaction_round_trip_from_satisfaction_target( + &source, + &reduction, + "Partition -> MPS equal elements", + ); +} + +#[test] +fn test_partition_to_multiprocessorscheduling_solution_extraction() { + let source = Partition::new(vec![1, 2, 3, 4]); + let reduction = ReduceTo::::reduce_to(&source); + let target = reduction.target_problem(); + + let solver = BruteForce::new(); + let target_solutions = solver.find_all_witnesses(target); + + for sol in &target_solutions { + let extracted = reduction.extract_solution(sol); + // Solution length should match number of elements + assert_eq!(extracted.len(), source.num_elements()); + // Extracted solution should satisfy source if target is satisfied + let target_valid = target.evaluate(sol); + let source_valid = source.evaluate(&extracted); + if target_valid.0 { + assert!( + source_valid.0, + "Valid MPS solution should yield valid Partition" + ); + } + } +} + +#[test] +fn test_partition_to_multiprocessorscheduling_single_element() { + // Single element: [4], sum=4, target=2 + // Not partitionable since we need 2 subsets summing to 2 each but only have one element of size 4 + let source = Partition::new(vec![4]); + let reduction = ReduceTo::::reduce_to(&source); + let target = reduction.target_problem(); + + assert_eq!(target.deadline(), 2); + assert_eq!(target.num_tasks(), 1); + assert_eq!(target.lengths(), &[4]); + + // Source: not satisfiable (single element, total_sum=4, need 2 per subset but only have 4) + let solver = BruteForce::new(); + let source_solutions = solver.find_all_witnesses(&source); + assert!(source_solutions.is_empty()); + + // Target: task of length 4 > deadline 2, so infeasible + let target_solutions = solver.find_all_witnesses(target); + assert!(target_solutions.is_empty()); +} + +#[test] +fn test_partition_to_multiprocessorscheduling_two_elements() { + // [5, 5], sum=10, target=5 + let source = Partition::new(vec![5, 5]); + let reduction = ReduceTo::::reduce_to(&source); + let target = reduction.target_problem(); + + assert_eq!(target.deadline(), 5); + + let solver = BruteForce::new(); + let source_solutions = solver.find_all_witnesses(&source); + let target_solutions = solver.find_all_witnesses(target); + + // Both should be satisfiable: one element per subset/processor + assert!(!source_solutions.is_empty()); + assert!(!target_solutions.is_empty()); + + assert_satisfaction_round_trip_from_satisfaction_target( + &source, + &reduction, + "Partition -> MPS two elements", + ); +} diff --git a/src/unit_tests/rules/satisfiability_naesatisfiability.rs b/src/unit_tests/rules/satisfiability_naesatisfiability.rs new file mode 100644 index 000000000..09cf5b2fd --- /dev/null +++ b/src/unit_tests/rules/satisfiability_naesatisfiability.rs @@ -0,0 +1,182 @@ +use super::*; +use crate::rules::test_helpers::assert_satisfaction_round_trip_from_satisfaction_target; +use crate::solvers::BruteForce; +use crate::traits::Problem; + +#[test] +fn test_satisfiability_to_naesatisfiability_closed_loop() { + // Formula: (x1 ∨ x2) ∧ (¬x1 ∨ x3) ∧ (¬x2 ∨ ¬x3) + let sat = Satisfiability::new( + 3, + vec![ + CNFClause::new(vec![1, 2]), + CNFClause::new(vec![-1, 3]), + CNFClause::new(vec![-2, -3]), + ], + ); + + let reduction = ReduceTo::::reduce_to(&sat); + + assert_satisfaction_round_trip_from_satisfaction_target( + &sat, + &reduction, + "SAT->NAE-SAT closed loop", + ); +} + +#[test] +fn test_reduction_structure() { + let sat = Satisfiability::new( + 3, + vec![ + CNFClause::new(vec![1, 2]), + CNFClause::new(vec![-1, 3]), + CNFClause::new(vec![-2, -3]), + ], + ); + + let reduction = ReduceTo::::reduce_to(&sat); + let naesat = reduction.target_problem(); + + // Should have n+1 variables (3 original + 1 sentinel) + assert_eq!(naesat.num_vars(), 4); + // Same number of clauses + assert_eq!(naesat.num_clauses(), 3); + + // Each clause should have one extra literal (the sentinel) + for (i, clause) in naesat.clauses().iter().enumerate() { + assert_eq!( + clause.len(), + sat.clauses()[i].len() + 1, + "clause {} should have one extra literal", + i + ); + // Last literal should be the sentinel (positive literal for variable 3, i.e., literal 4) + assert_eq!(*clause.literals.last().unwrap(), 4); + } +} + +#[test] +fn test_solution_extraction_sentinel_false() { + // When sentinel is false, return original variables as-is + let sat = Satisfiability::new(3, vec![CNFClause::new(vec![1, 2])]); + + let reduction = ReduceTo::::reduce_to(&sat); + + // target_solution: [1, 0, 1, 0] means x1=true, x2=false, x3=true, sentinel=false + let extracted = reduction.extract_solution(&[1, 0, 1, 0]); + assert_eq!(extracted, vec![1, 0, 1]); +} + +#[test] +fn test_solution_extraction_sentinel_true() { + // When sentinel is true, return complement of original variables + let sat = Satisfiability::new(3, vec![CNFClause::new(vec![1, 2])]); + + let reduction = ReduceTo::::reduce_to(&sat); + + // target_solution: [0, 1, 0, 1] means x1=false, x2=true, x3=false, sentinel=true + // Complement: x1=true, x2=false, x3=true + let extracted = reduction.extract_solution(&[0, 1, 0, 1]); + assert_eq!(extracted, vec![1, 0, 1]); +} + +#[test] +fn test_unsatisfiable_formula() { + // (x1) ∧ (¬x1) is unsatisfiable + let sat = Satisfiability::new(1, vec![CNFClause::new(vec![1]), CNFClause::new(vec![-1])]); + + let reduction = ReduceTo::::reduce_to(&sat); + let naesat = reduction.target_problem(); + + let solver = BruteForce::new(); + let sat_solutions = solver.find_all_witnesses(&sat); + let naesat_solutions = solver.find_all_witnesses(naesat); + + // Both should be unsatisfiable + assert!(sat_solutions.is_empty()); + assert!(naesat_solutions.is_empty()); +} + +#[test] +fn test_single_clause() { + let sat = Satisfiability::new(2, vec![CNFClause::new(vec![1, -2])]); + + let reduction = ReduceTo::::reduce_to(&sat); + + assert_satisfaction_round_trip_from_satisfaction_target( + &sat, + &reduction, + "SAT->NAE-SAT single clause", + ); +} + +#[test] +fn test_empty_formula() { + // Empty formula is trivially satisfiable + let sat = Satisfiability::new(2, vec![]); + + let reduction = ReduceTo::::reduce_to(&sat); + let naesat = reduction.target_problem(); + + assert_eq!(naesat.num_vars(), 3); + assert_eq!(naesat.num_clauses(), 0); + + // Both should be satisfiable (any assignment works) + let solver = BruteForce::new(); + assert!(!solver.find_all_witnesses(&sat).is_empty()); + assert!(!solver.find_all_witnesses(naesat).is_empty()); +} + +#[test] +fn test_larger_instance() { + // A larger SAT instance to stress the reduction + let sat = Satisfiability::new( + 5, + vec![ + CNFClause::new(vec![1, 2, 3]), + CNFClause::new(vec![-1, -2, 4]), + CNFClause::new(vec![2, -3, 5]), + CNFClause::new(vec![-4, -5]), + CNFClause::new(vec![1, 3, -5]), + ], + ); + + let reduction = ReduceTo::::reduce_to(&sat); + let naesat = reduction.target_problem(); + + assert_eq!(naesat.num_vars(), 6); + assert_eq!(naesat.num_clauses(), 5); + + assert_satisfaction_round_trip_from_satisfaction_target( + &sat, + &reduction, + "SAT->NAE-SAT larger instance", + ); +} + +#[test] +fn test_all_satisfying_assignments_map_back() { + // Small instance: verify every NAE-SAT solution maps to a valid SAT solution + let sat = Satisfiability::new( + 2, + vec![CNFClause::new(vec![1, 2]), CNFClause::new(vec![-1, -2])], + ); + + let reduction = ReduceTo::::reduce_to(&sat); + let naesat = reduction.target_problem(); + + let solver = BruteForce::new(); + let nae_solutions = solver.find_all_witnesses(naesat); + + for nae_sol in &nae_solutions { + let sat_sol = reduction.extract_solution(nae_sol); + assert_eq!(sat_sol.len(), 2); + assert!( + sat.evaluate(&sat_sol).0, + "Extracted solution {:?} from NAE solution {:?} does not satisfy SAT", + sat_sol, + nae_sol + ); + } +} From a3e212c32de6279e20fb0a521ea6c80c1e89fe6f Mon Sep 17 00:00:00 2001 From: zazabap Date: Thu, 26 Mar 2026 12:55:57 +0000 Subject: [PATCH 2/5] fix: address PR #777 review comments MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - HC→HP: special-case n < 3 to avoid panic on empty/tiny graphs - SAT→NAESAT: handle empty clauses (map to fixed unsatisfiable NAE clause) - SAT→NAESAT: guard extract_solution against short configs with assert - SAT→NAESAT test: fix comment (variable 3 → variable 4) Co-Authored-By: Claude Opus 4.6 (1M context) --- .../hamiltoniancircuit_hamiltonianpath.rs | 14 ++++++++++++++ src/rules/satisfiability_naesatisfiability.rs | 19 ++++++++++++++++--- .../rules/satisfiability_naesatisfiability.rs | 2 +- 3 files changed, 31 insertions(+), 4 deletions(-) diff --git a/src/rules/hamiltoniancircuit_hamiltonianpath.rs b/src/rules/hamiltoniancircuit_hamiltonianpath.rs index ecab0800d..ef6ff49c8 100644 --- a/src/rules/hamiltoniancircuit_hamiltonianpath.rs +++ b/src/rules/hamiltoniancircuit_hamiltonianpath.rs @@ -107,6 +107,20 @@ impl ReduceTo> for HamiltonianCircuit fn reduce_to(&self) -> Self::Result { let n = self.num_vertices(); + + // HC is unsatisfiable for n < 3; return a trivially unsatisfiable HP instance. + if n < 3 { + // A single isolated vertex has no Hamiltonian path of length > 0, + // so HP on 1 vertex is trivially satisfied but HC on < 3 is not. + // Use a disconnected 2-vertex graph (no edges) which has no HP. + let target_graph = SimpleGraph::new(n + 3, vec![]); + let target = HamiltonianPath::new(target_graph); + return ReductionHamiltonianCircuitToHamiltonianPath { + target, + num_original_vertices: n, + }; + } + let source_graph = self.graph(); // New vertex indices: diff --git a/src/rules/satisfiability_naesatisfiability.rs b/src/rules/satisfiability_naesatisfiability.rs index 8d9206eb8..2863e3216 100644 --- a/src/rules/satisfiability_naesatisfiability.rs +++ b/src/rules/satisfiability_naesatisfiability.rs @@ -30,6 +30,13 @@ impl ReductionResult for ReductionSATToNAESAT { fn extract_solution(&self, target_solution: &[usize]) -> Vec { let n = self.source_num_vars; + // Guard against malformed configs from external callers. + assert!( + target_solution.len() > n, + "target config too short: expected at least {} entries, got {}", + n + 1, + target_solution.len() + ); // The sentinel variable is the last variable (index n). let sentinel_value = target_solution[n]; if sentinel_value == 0 { @@ -59,9 +66,15 @@ impl ReduceTo for Satisfiability { .clauses() .iter() .map(|clause| { - let mut lits = clause.literals.clone(); - lits.push(sentinel_lit); - CNFClause::new(lits) + if clause.literals.is_empty() { + // SAT allows empty clauses, which make the instance unsatisfiable. + // Map to a fixed unsatisfiable NAE clause (s, s) of length 2. + CNFClause::new(vec![sentinel_lit, sentinel_lit]) + } else { + let mut lits = clause.literals.clone(); + lits.push(sentinel_lit); + CNFClause::new(lits) + } }) .collect(); diff --git a/src/unit_tests/rules/satisfiability_naesatisfiability.rs b/src/unit_tests/rules/satisfiability_naesatisfiability.rs index 09cf5b2fd..c8cd23dd7 100644 --- a/src/unit_tests/rules/satisfiability_naesatisfiability.rs +++ b/src/unit_tests/rules/satisfiability_naesatisfiability.rs @@ -51,7 +51,7 @@ fn test_reduction_structure() { "clause {} should have one extra literal", i ); - // Last literal should be the sentinel (positive literal for variable 3, i.e., literal 4) + // Last literal should be the sentinel (positive literal for variable 4, i.e., literal 4) assert_eq!(*clause.literals.last().unwrap(), 4); } } From 9409359f6247a94f4769d5fa5c6f24ea809e6705 Mon Sep 17 00:00:00 2001 From: Xiwei Pan Date: Thu, 26 Mar 2026 21:58:59 +0800 Subject: [PATCH 3/5] refactor: extract shared cycle-walking helper, simplify reductions MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - Extract duplicated edges_to_cycle_order logic from HC→TSP and HC→BTSP into graph_helpers module (-110 lines) - Use SimpleGraph::complete(k) in KClique→SubgraphIsomorphism - Use .edges() directly in KClique→CBQ instead of O(n²) has_edge loop - Replace assert! with graceful fallback in SAT→NAE-SAT extract_solution Co-Authored-By: Claude Opus 4.6 (1M context) --- src/rules/graph_helpers.rs | 59 +++++++++++++++++++ ...niancircuit_bottlenecktravelingsalesman.rs | 56 +----------------- .../hamiltoniancircuit_travelingsalesman.rs | 54 +---------------- src/rules/kclique_conjunctivebooleanquery.rs | 11 +--- src/rules/kclique_subgraphisomorphism.rs | 9 +-- src/rules/mod.rs | 1 + src/rules/satisfiability_naesatisfiability.rs | 10 +--- 7 files changed, 69 insertions(+), 131 deletions(-) create mode 100644 src/rules/graph_helpers.rs diff --git a/src/rules/graph_helpers.rs b/src/rules/graph_helpers.rs new file mode 100644 index 000000000..58c54a34e --- /dev/null +++ b/src/rules/graph_helpers.rs @@ -0,0 +1,59 @@ +//! Shared helpers for graph-based reductions. + +use crate::topology::Graph; + +/// Extract a Hamiltonian cycle vertex ordering from edge-selection configs on complete graphs. +/// +/// Given a graph and a binary `target_solution` over its edges (1 = selected), +/// walks the selected edges to produce a vertex permutation representing the cycle. +/// Returns `vec![0; n]` if the selection does not form a valid Hamiltonian cycle. +pub(crate) fn edges_to_cycle_order(graph: &G, target_solution: &[usize]) -> Vec { + let n = graph.num_vertices(); + if n == 0 { + return vec![]; + } + + let edges = graph.edges(); + if target_solution.len() != edges.len() { + return vec![0; n]; + } + + let mut adjacency = vec![Vec::new(); n]; + let mut selected_count = 0usize; + for (idx, &selected) in target_solution.iter().enumerate() { + if selected != 1 { + continue; + } + let (u, v) = edges[idx]; + adjacency[u].push(v); + adjacency[v].push(u); + selected_count += 1; + } + + if selected_count != n || adjacency.iter().any(|neighbors| neighbors.len() != 2) { + return vec![0; n]; + } + + let mut order = Vec::with_capacity(n); + let mut prev = None; + let mut current = 0usize; + + for _ in 0..n { + order.push(current); + let neighbors = &adjacency[current]; + let next = match prev { + Some(previous) => { + if neighbors[0] == previous { + neighbors[1] + } else { + neighbors[0] + } + } + None => neighbors[0], + }; + prev = Some(current); + current = next; + } + + order +} diff --git a/src/rules/hamiltoniancircuit_bottlenecktravelingsalesman.rs b/src/rules/hamiltoniancircuit_bottlenecktravelingsalesman.rs index 9bc353d70..061ac0e81 100644 --- a/src/rules/hamiltoniancircuit_bottlenecktravelingsalesman.rs +++ b/src/rules/hamiltoniancircuit_bottlenecktravelingsalesman.rs @@ -24,61 +24,7 @@ impl ReductionResult for ReductionHamiltonianCircuitToBottleneckTravelingSalesma } fn extract_solution(&self, target_solution: &[usize]) -> Vec { - let graph = self.target.graph(); - let n = graph.num_vertices(); - if n == 0 { - return vec![]; - } - - let edges = graph.edges(); - if target_solution.len() != edges.len() { - return vec![0; n]; - } - - // Build adjacency from selected edges - let mut adjacency = vec![Vec::new(); n]; - let mut selected_count = 0usize; - for (idx, &selected) in target_solution.iter().enumerate() { - if selected != 1 { - continue; - } - let (u, v) = edges[idx]; - adjacency[u].push(v); - adjacency[v].push(u); - selected_count += 1; - } - - if selected_count != n || adjacency.iter().any(|neighbors| neighbors.len() != 2) { - return vec![0; n]; - } - - for neighbors in &mut adjacency { - neighbors.sort_unstable(); - } - - // Walk the cycle to produce a permutation - let mut order = Vec::with_capacity(n); - let mut prev = None; - let mut current = 0usize; - - for _ in 0..n { - order.push(current); - let neighbors = &adjacency[current]; - let next = match prev { - Some(previous) => { - if neighbors[0] == previous { - neighbors[1] - } else { - neighbors[0] - } - } - None => neighbors[0], - }; - prev = Some(current); - current = next; - } - - order + crate::rules::graph_helpers::edges_to_cycle_order(self.target.graph(), target_solution) } } diff --git a/src/rules/hamiltoniancircuit_travelingsalesman.rs b/src/rules/hamiltoniancircuit_travelingsalesman.rs index f34703f7d..eebeb26af 100644 --- a/src/rules/hamiltoniancircuit_travelingsalesman.rs +++ b/src/rules/hamiltoniancircuit_travelingsalesman.rs @@ -24,59 +24,7 @@ impl ReductionResult for ReductionHamiltonianCircuitToTravelingSalesman { } fn extract_solution(&self, target_solution: &[usize]) -> Vec { - let graph = self.target.graph(); - let n = graph.num_vertices(); - if n == 0 { - return vec![]; - } - - let edges = graph.edges(); - if target_solution.len() != edges.len() { - return vec![0; n]; - } - - let mut adjacency = vec![Vec::new(); n]; - let mut selected_count = 0usize; - for (idx, &selected) in target_solution.iter().enumerate() { - if selected != 1 { - continue; - } - let (u, v) = edges[idx]; - adjacency[u].push(v); - adjacency[v].push(u); - selected_count += 1; - } - - if selected_count != n || adjacency.iter().any(|neighbors| neighbors.len() != 2) { - return vec![0; n]; - } - - for neighbors in &mut adjacency { - neighbors.sort_unstable(); - } - - let mut order = Vec::with_capacity(n); - let mut prev = None; - let mut current = 0usize; - - for _ in 0..n { - order.push(current); - let neighbors = &adjacency[current]; - let next = match prev { - Some(previous) => { - if neighbors[0] == previous { - neighbors[1] - } else { - neighbors[0] - } - } - None => neighbors[0], - }; - prev = Some(current); - current = next; - } - - order + crate::rules::graph_helpers::edges_to_cycle_order(self.target.graph(), target_solution) } } diff --git a/src/rules/kclique_conjunctivebooleanquery.rs b/src/rules/kclique_conjunctivebooleanquery.rs index c9ee18d4c..cfc659cac 100644 --- a/src/rules/kclique_conjunctivebooleanquery.rs +++ b/src/rules/kclique_conjunctivebooleanquery.rs @@ -58,15 +58,10 @@ impl ReduceTo for KClique { let n = self.graph().num_vertices(); let k = self.k(); - // Build the single binary relation: for each edge {u,v}, include (u,v) and (v,u). let mut tuples = Vec::new(); - for u in 0..n { - for v in (u + 1)..n { - if self.graph().has_edge(u, v) { - tuples.push(vec![u, v]); - tuples.push(vec![v, u]); - } - } + for (u, v) in self.graph().edges() { + tuples.push(vec![u, v]); + tuples.push(vec![v, u]); } let relation = CbqRelation { arity: 2, tuples }; diff --git a/src/rules/kclique_subgraphisomorphism.rs b/src/rules/kclique_subgraphisomorphism.rs index 1fd29c7db..23041cd66 100644 --- a/src/rules/kclique_subgraphisomorphism.rs +++ b/src/rules/kclique_subgraphisomorphism.rs @@ -58,14 +58,7 @@ impl ReduceTo for KClique { let n = self.graph().num_vertices(); let k = self.k(); - // Build the complete graph K_k as the pattern - let mut pattern_edges = Vec::new(); - for i in 0..k { - for j in (i + 1)..k { - pattern_edges.push((i, j)); - } - } - let pattern = SimpleGraph::new(k, pattern_edges); + let pattern = SimpleGraph::complete(k); // Host graph is the original graph, cloned into a SimpleGraph let host_edges = self.graph().edges(); diff --git a/src/rules/mod.rs b/src/rules/mod.rs index e2b67adea..002775c1f 100644 --- a/src/rules/mod.rs +++ b/src/rules/mod.rs @@ -12,6 +12,7 @@ pub(crate) mod coloring_qubo; pub(crate) mod exactcoverby3sets_staffscheduling; pub(crate) mod factoring_circuit; mod graph; +pub(crate) mod graph_helpers; pub(crate) mod hamiltoniancircuit_bottlenecktravelingsalesman; pub(crate) mod hamiltoniancircuit_hamiltonianpath; pub(crate) mod hamiltoniancircuit_travelingsalesman; diff --git a/src/rules/satisfiability_naesatisfiability.rs b/src/rules/satisfiability_naesatisfiability.rs index 2863e3216..b17a292b0 100644 --- a/src/rules/satisfiability_naesatisfiability.rs +++ b/src/rules/satisfiability_naesatisfiability.rs @@ -30,13 +30,9 @@ impl ReductionResult for ReductionSATToNAESAT { fn extract_solution(&self, target_solution: &[usize]) -> Vec { let n = self.source_num_vars; - // Guard against malformed configs from external callers. - assert!( - target_solution.len() > n, - "target config too short: expected at least {} entries, got {}", - n + 1, - target_solution.len() - ); + if target_solution.len() <= n { + return vec![0; n]; + } // The sentinel variable is the last variable (index n). let sentinel_value = target_solution[n]; if sentinel_value == 0 { From 7e01a05cbbce35f6f9484133b58faff8eabeaf08 Mon Sep 17 00:00:00 2001 From: GiggleLiu Date: Thu, 26 Mar 2026 21:59:36 +0800 Subject: [PATCH 4/5] Refine tier1a rule implementations - simplify new graph reductions by using shared graph constructors and a shared KClique selection helper - reduce control-flow and repeated setup in HamiltonianCircuit/Partition-related rule code and tests - add regression coverage for HamiltonianCircuit small-n and Satisfiability empty-clause edge cases - remove the unused example variable warning and align rustfmt config with the stable toolchain --- rustfmt.toml | 10 +-- src/models/graph/kclique.rs | 14 ++++ .../consecutiveonesmatrixaugmentation_ilp.rs | 1 - .../hamiltoniancircuit_hamiltonianpath.rs | 58 ++++----------- .../hamiltonianpath_isomorphicspanningtree.rs | 8 +- src/rules/kclique_conjunctivebooleanquery.rs | 13 ++-- src/rules/kclique_subgraphisomorphism.rs | 15 +--- src/unit_tests/models/graph/kclique.rs | 14 ++++ .../hamiltoniancircuit_hamiltonianpath.rs | 16 ++++ .../partition_multiprocessorscheduling.rs | 74 +++++++------------ .../rules/satisfiability_naesatisfiability.rs | 16 ++++ 11 files changed, 113 insertions(+), 126 deletions(-) diff --git a/rustfmt.toml b/rustfmt.toml index 2a5d5c263..2feefadfe 100644 --- a/rustfmt.toml +++ b/rustfmt.toml @@ -8,17 +8,9 @@ tab_spaces = 4 newline_style = "Unix" use_small_heuristics = "Default" -# Imports -imports_granularity = "Crate" -group_imports = "StdExternalCrate" +# Stable import options reorder_imports = true -# Comments and documentation -format_code_in_doc_comments = true -normalize_comments = true -wrap_comments = true -comment_width = 100 - # Formatting style use_field_init_shorthand = true use_try_shorthand = true diff --git a/src/models/graph/kclique.rs b/src/models/graph/kclique.rs index d0b84cbcf..a00d37750 100644 --- a/src/models/graph/kclique.rs +++ b/src/models/graph/kclique.rs @@ -66,6 +66,20 @@ impl KClique { pub fn is_valid_solution(&self, config: &[usize]) -> bool { is_kclique_config(&self.graph, config, self.k) } + + /// Build a binary selection config from the listed vertices. + pub fn config_from_vertices(num_vertices: usize, selected_vertices: &[usize]) -> Vec { + let mut config = vec![0; num_vertices]; + for &vertex in selected_vertices { + config[vertex] = 1; + } + config + } + + /// Build a binary selection config from the listed vertices. + pub fn config_from_selected_vertices(&self, selected_vertices: &[usize]) -> Vec { + Self::config_from_vertices(self.num_vertices(), selected_vertices) + } } impl Problem for KClique diff --git a/src/rules/consecutiveonesmatrixaugmentation_ilp.rs b/src/rules/consecutiveonesmatrixaugmentation_ilp.rs index e3ca84e25..41a475898 100644 --- a/src/rules/consecutiveonesmatrixaugmentation_ilp.rs +++ b/src/rules/consecutiveonesmatrixaugmentation_ilp.rs @@ -182,7 +182,6 @@ pub(crate) fn canonical_rule_example_specs() -> Vec>::reduce_to(&source); let ilp_solver = crate::solvers::ILPSolver::new(); let target_config = ilp_solver diff --git a/src/rules/hamiltoniancircuit_hamiltonianpath.rs b/src/rules/hamiltoniancircuit_hamiltonianpath.rs index ef6ff49c8..a3b20d080 100644 --- a/src/rules/hamiltoniancircuit_hamiltonianpath.rs +++ b/src/rules/hamiltoniancircuit_hamiltonianpath.rs @@ -42,8 +42,7 @@ impl ReductionResult for ReductionHamiltonianCircuitToHamiltonianPath { return vec![]; } - let n_prime = n + 3; // total vertices in target graph - if target_solution.len() != n_prime { + if target_solution.len() != n + 3 { return vec![0; n]; } @@ -51,48 +50,22 @@ impl ReductionResult for ReductionHamiltonianCircuitToHamiltonianPath { let s = n + 1; // pendant attached to v=0 let t = n + 2; // pendant attached to v' - // The HP path must start at s or t (pendants with degree 1). - // Determine path orientation: we want s at the start. - // target_solution[i] = vertex visited at position i. - - // Find position of s and t in the path - let s_pos = target_solution.iter().position(|&v| v == s); - let t_pos = target_solution.iter().position(|&v| v == t); - - let (s_pos, t_pos) = match (s_pos, t_pos) { - (Some(sp), Some(tp)) => (sp, tp), - _ => return vec![0; n], // invalid solution + // The two pendants force any valid witness to have endpoints s and t. + let reversed; + let oriented = match (target_solution.first(), target_solution.last()) { + (Some(&start), Some(&end)) if start == s && end == t => target_solution, + (Some(&start), Some(&end)) if start == t && end == s => { + reversed = target_solution.iter().copied().rev().collect::>(); + reversed.as_slice() + } + _ => return vec![0; n], }; - // Build the path in order from s to t - let path: Vec = if s_pos == 0 && t_pos == n_prime - 1 { - // Already oriented s -> ... -> t - target_solution.to_vec() - } else if t_pos == 0 && s_pos == n_prime - 1 { - // Reverse: t -> ... -> s, flip to s -> ... -> t - target_solution.iter().copied().rev().collect() - } else { - // s or t not at endpoints -- invalid HP for our construction + if oriented.get(1) != Some(&0) || oriented.get(n + 1) != Some(&v_prime) { return vec![0; n]; - }; - - // path = [s, v=0, ..., v'=n, t] - // Strip s (first) and t (last) to get inner path of length n+1 - let inner = &path[1..n_prime - 1]; // length n+1 - - // The inner path should start with v=0 and end with v'=n, or vice versa. - // Orient so it starts with v=0. - let oriented: Vec = if inner[0] == 0 && inner[n] == v_prime { - inner.to_vec() - } else if inner[0] == v_prime && inner[n] == 0 { - inner.iter().copied().rev().collect() - } else { - return vec![0; n]; - }; + } - // oriented = [0, perm of 1..n-1, v'=n] - // The HC config is the first n entries (dropping v' at the end). - oriented[..n].to_vec() + oriented[1..=n].to_vec() } } @@ -110,10 +83,7 @@ impl ReduceTo> for HamiltonianCircuit // HC is unsatisfiable for n < 3; return a trivially unsatisfiable HP instance. if n < 3 { - // A single isolated vertex has no Hamiltonian path of length > 0, - // so HP on 1 vertex is trivially satisfied but HC on < 3 is not. - // Use a disconnected 2-vertex graph (no edges) which has no HP. - let target_graph = SimpleGraph::new(n + 3, vec![]); + let target_graph = SimpleGraph::empty(n + 3); let target = HamiltonianPath::new(target_graph); return ReductionHamiltonianCircuitToHamiltonianPath { target, diff --git a/src/rules/hamiltonianpath_isomorphicspanningtree.rs b/src/rules/hamiltonianpath_isomorphicspanningtree.rs index b11dea000..481b24541 100644 --- a/src/rules/hamiltonianpath_isomorphicspanningtree.rs +++ b/src/rules/hamiltonianpath_isomorphicspanningtree.rs @@ -49,10 +49,7 @@ impl ReduceTo for HamiltonianPath { // Host graph: keep G unchanged let graph = self.graph().clone(); - // Target tree: path graph P_n with edges {0,1},{1,2},...,{n-2,n-1} - let path_edges: Vec<(usize, usize)> = - (0..n.saturating_sub(1)).map(|i| (i, i + 1)).collect(); - let tree = SimpleGraph::new(n, path_edges); + let tree = SimpleGraph::path(n); ReductionHPToIST { target: IsomorphicSpanningTree::new(graph, tree), @@ -68,8 +65,7 @@ pub(crate) fn canonical_rule_example_specs() -> Vec( source, SolutionPair { diff --git a/src/rules/kclique_conjunctivebooleanquery.rs b/src/rules/kclique_conjunctivebooleanquery.rs index cfc659cac..0dcd3c4ca 100644 --- a/src/rules/kclique_conjunctivebooleanquery.rs +++ b/src/rules/kclique_conjunctivebooleanquery.rs @@ -35,11 +35,7 @@ impl ReductionResult for ReductionKCliqueToCBQ { /// KClique config: binary vec of length n; set config[v]=1 for each v in /// the CBQ assignment. fn extract_solution(&self, target_solution: &[usize]) -> Vec { - let mut config = vec![0; self.num_vertices]; - for &v in target_solution { - config[v] = 1; - } - config + KClique::::config_from_vertices(self.num_vertices, target_solution) } } @@ -55,10 +51,11 @@ impl ReduceTo for KClique { type Result = ReductionKCliqueToCBQ; fn reduce_to(&self) -> Self::Result { - let n = self.graph().num_vertices(); + let n = self.num_vertices(); let k = self.k(); - let mut tuples = Vec::new(); + // Build the single binary relation: for each edge {u,v}, include (u,v) and (v,u). + let mut tuples = Vec::with_capacity(self.num_edges() * 2); for (u, v) in self.graph().edges() { tuples.push(vec![u, v]); tuples.push(vec![v, u]); @@ -66,7 +63,7 @@ impl ReduceTo for KClique { let relation = CbqRelation { arity: 2, tuples }; // Build conjuncts: R(y_i, y_j) for all 0 <= i < j < k. - let mut conjuncts = Vec::new(); + let mut conjuncts = Vec::with_capacity(k * k.saturating_sub(1) / 2); for i in 0..k { for j in (i + 1)..k { conjuncts.push((0, vec![QueryArg::Variable(i), QueryArg::Variable(j)])); diff --git a/src/rules/kclique_subgraphisomorphism.rs b/src/rules/kclique_subgraphisomorphism.rs index 23041cd66..e351a2cfa 100644 --- a/src/rules/kclique_subgraphisomorphism.rs +++ b/src/rules/kclique_subgraphisomorphism.rs @@ -8,7 +8,7 @@ use crate::models::graph::{KClique, SubgraphIsomorphism}; use crate::reduction; use crate::rules::traits::{ReduceTo, ReductionResult}; -use crate::topology::{Graph, SimpleGraph}; +use crate::topology::SimpleGraph; /// Result of reducing KClique to SubgraphIsomorphism. /// @@ -35,11 +35,7 @@ impl ReductionResult for ReductionKCliqueToSubIso { /// host vertex. We create a binary vector of length n and set positions /// f(0), f(1), ..., f(k-1) to 1. fn extract_solution(&self, target_solution: &[usize]) -> Vec { - let mut config = vec![0; self.num_source_vertices]; - for &host_vertex in target_solution { - config[host_vertex] = 1; - } - config + KClique::::config_from_vertices(self.num_source_vertices, target_solution) } } @@ -55,14 +51,11 @@ impl ReduceTo for KClique { type Result = ReductionKCliqueToSubIso; fn reduce_to(&self) -> Self::Result { - let n = self.graph().num_vertices(); + let n = self.num_vertices(); let k = self.k(); let pattern = SimpleGraph::complete(k); - - // Host graph is the original graph, cloned into a SimpleGraph - let host_edges = self.graph().edges(); - let host = SimpleGraph::new(n, host_edges); + let host = self.graph().clone(); let target = SubgraphIsomorphism::new(host, pattern); diff --git a/src/unit_tests/models/graph/kclique.rs b/src/unit_tests/models/graph/kclique.rs index fc42e1909..16aca9e99 100644 --- a/src/unit_tests/models/graph/kclique.rs +++ b/src/unit_tests/models/graph/kclique.rs @@ -75,3 +75,17 @@ fn test_kclique_paper_example() { assert!(problem.evaluate(&issue_witness())); assert_eq!(solver.find_all_witnesses(&problem), vec![issue_witness()]); } + +#[test] +fn test_kclique_config_from_selected_vertices() { + let problem = KClique::new(issue_graph(), 3); + + assert_eq!( + problem.config_from_selected_vertices(&[2, 3, 4]), + issue_witness() + ); + assert_eq!( + problem.config_from_selected_vertices(&[4, 2, 4]), + vec![0, 0, 1, 0, 1] + ); +} diff --git a/src/unit_tests/rules/hamiltoniancircuit_hamiltonianpath.rs b/src/unit_tests/rules/hamiltoniancircuit_hamiltonianpath.rs index cd1a15502..e9b9ca02a 100644 --- a/src/unit_tests/rules/hamiltoniancircuit_hamiltonianpath.rs +++ b/src/unit_tests/rules/hamiltoniancircuit_hamiltonianpath.rs @@ -110,3 +110,19 @@ fn test_hamiltoniancircuit_to_hamiltonianpath_triangle() { "HamiltonianCircuit(triangle) -> HamiltonianPath", ); } + +#[test] +fn test_hamiltoniancircuit_to_hamiltonianpath_two_vertex_special_case_is_unsatisfiable() { + let source = HamiltonianCircuit::new(SimpleGraph::new(2, vec![(0, 1)])); + let reduction = ReduceTo::>::reduce_to(&source); + let target = reduction.target_problem(); + + assert_eq!(target.graph().num_vertices(), 5); + assert_eq!(target.graph().num_edges(), 0); + + let solver = BruteForce::new(); + assert!( + solver.find_witness(target).is_none(), + "2-vertex source should reduce to an unsatisfiable HamiltonianPath instance" + ); +} diff --git a/src/unit_tests/rules/partition_multiprocessorscheduling.rs b/src/unit_tests/rules/partition_multiprocessorscheduling.rs index 66a0dbf73..b72884a81 100644 --- a/src/unit_tests/rules/partition_multiprocessorscheduling.rs +++ b/src/unit_tests/rules/partition_multiprocessorscheduling.rs @@ -4,12 +4,27 @@ use crate::rules::test_helpers::assert_satisfaction_round_trip_from_satisfaction use crate::solvers::BruteForce; use crate::traits::Problem; +fn reduce_partition(sizes: &[u64]) -> (Partition, ReductionPartitionToMPS) { + let source = Partition::new(sizes.to_vec()); + let reduction = ReduceTo::::reduce_to(&source); + (source, reduction) +} + +fn assert_satisfiability_matches( + source: &Partition, + target: &MultiprocessorScheduling, + expected: bool, +) { + let solver = BruteForce::new(); + assert_eq!(solver.find_witness(source).is_some(), expected); + assert_eq!(solver.find_witness(target).is_some(), expected); +} + #[test] fn test_partition_to_multiprocessorscheduling_closed_loop() { // sizes [1, 2, 3, 4], sum=10, target=5 // partition: {1,4} and {2,3} - let source = Partition::new(vec![1, 2, 3, 4]); - let reduction = ReduceTo::::reduce_to(&source); + let (source, reduction) = reduce_partition(&[1, 2, 3, 4]); assert_satisfaction_round_trip_from_satisfaction_target( &source, @@ -20,8 +35,7 @@ fn test_partition_to_multiprocessorscheduling_closed_loop() { #[test] fn test_partition_to_multiprocessorscheduling_structure() { - let source = Partition::new(vec![1, 2, 3, 4]); - let reduction = ReduceTo::::reduce_to(&source); + let (source, reduction) = reduce_partition(&[1, 2, 3, 4]); let target = reduction.target_problem(); assert_eq!(target.lengths(), &[1, 2, 3, 4]); @@ -33,41 +47,24 @@ fn test_partition_to_multiprocessorscheduling_structure() { #[test] fn test_partition_to_multiprocessorscheduling_odd_sum() { // sum = 2+4+5 = 11 (odd), no valid partition exists - let source = Partition::new(vec![2, 4, 5]); - let reduction = ReduceTo::::reduce_to(&source); + let (source, reduction) = reduce_partition(&[2, 4, 5]); let target = reduction.target_problem(); // deadline = floor(11/2) = 5 assert_eq!(target.deadline(), 5); assert_eq!(target.num_processors(), 2); - // Source is not satisfiable (odd sum) - let solver = BruteForce::new(); - let source_solutions = solver.find_all_witnesses(&source); - assert!(source_solutions.is_empty()); - - // Target should also be infeasible: total=11, floor(11/2)=5, - // so one processor must get at least ceil(11/2)=6 > 5 - let target_solutions = solver.find_all_witnesses(target); - assert!(target_solutions.is_empty()); + assert_satisfiability_matches(&source, target, false); } #[test] fn test_partition_to_multiprocessorscheduling_equal_elements() { // [3, 3, 3, 3], sum=12, target=6 - let source = Partition::new(vec![3, 3, 3, 3]); - let reduction = ReduceTo::::reduce_to(&source); + let (source, reduction) = reduce_partition(&[3, 3, 3, 3]); let target = reduction.target_problem(); assert_eq!(target.deadline(), 6); - - // Both should be satisfiable (e.g., {3,3} and {3,3}) - let solver = BruteForce::new(); - let source_solutions = solver.find_all_witnesses(&source); - let target_solutions = solver.find_all_witnesses(target); - - assert!(!source_solutions.is_empty()); - assert!(!target_solutions.is_empty()); + assert_satisfiability_matches(&source, target, true); // Round trip should work assert_satisfaction_round_trip_from_satisfaction_target( @@ -79,8 +76,7 @@ fn test_partition_to_multiprocessorscheduling_equal_elements() { #[test] fn test_partition_to_multiprocessorscheduling_solution_extraction() { - let source = Partition::new(vec![1, 2, 3, 4]); - let reduction = ReduceTo::::reduce_to(&source); + let (source, reduction) = reduce_partition(&[1, 2, 3, 4]); let target = reduction.target_problem(); let solver = BruteForce::new(); @@ -106,40 +102,24 @@ fn test_partition_to_multiprocessorscheduling_solution_extraction() { fn test_partition_to_multiprocessorscheduling_single_element() { // Single element: [4], sum=4, target=2 // Not partitionable since we need 2 subsets summing to 2 each but only have one element of size 4 - let source = Partition::new(vec![4]); - let reduction = ReduceTo::::reduce_to(&source); + let (source, reduction) = reduce_partition(&[4]); let target = reduction.target_problem(); assert_eq!(target.deadline(), 2); assert_eq!(target.num_tasks(), 1); assert_eq!(target.lengths(), &[4]); - // Source: not satisfiable (single element, total_sum=4, need 2 per subset but only have 4) - let solver = BruteForce::new(); - let source_solutions = solver.find_all_witnesses(&source); - assert!(source_solutions.is_empty()); - - // Target: task of length 4 > deadline 2, so infeasible - let target_solutions = solver.find_all_witnesses(target); - assert!(target_solutions.is_empty()); + assert_satisfiability_matches(&source, target, false); } #[test] fn test_partition_to_multiprocessorscheduling_two_elements() { // [5, 5], sum=10, target=5 - let source = Partition::new(vec![5, 5]); - let reduction = ReduceTo::::reduce_to(&source); + let (source, reduction) = reduce_partition(&[5, 5]); let target = reduction.target_problem(); assert_eq!(target.deadline(), 5); - - let solver = BruteForce::new(); - let source_solutions = solver.find_all_witnesses(&source); - let target_solutions = solver.find_all_witnesses(target); - - // Both should be satisfiable: one element per subset/processor - assert!(!source_solutions.is_empty()); - assert!(!target_solutions.is_empty()); + assert_satisfiability_matches(&source, target, true); assert_satisfaction_round_trip_from_satisfaction_target( &source, diff --git a/src/unit_tests/rules/satisfiability_naesatisfiability.rs b/src/unit_tests/rules/satisfiability_naesatisfiability.rs index c8cd23dd7..fbe452648 100644 --- a/src/unit_tests/rules/satisfiability_naesatisfiability.rs +++ b/src/unit_tests/rules/satisfiability_naesatisfiability.rs @@ -180,3 +180,19 @@ fn test_all_satisfying_assignments_map_back() { ); } } + +#[test] +fn test_empty_clause_maps_to_unsatisfiable_nae_clause() { + let sat = Satisfiability::new(1, vec![CNFClause::new(vec![])]); + let reduction = ReduceTo::::reduce_to(&sat); + let naesat = reduction.target_problem(); + + assert_eq!(naesat.num_vars(), 2); + assert_eq!(naesat.num_clauses(), 1); + assert_eq!(naesat.num_literals(), 2); + assert_eq!(naesat.clauses()[0].literals, vec![2, 2]); + + let solver = BruteForce::new(); + assert!(solver.find_witness(&sat).is_none()); + assert!(solver.find_witness(naesat).is_none()); +} From 0033e2ac299624cf58c883fe3f814522cca0e238 Mon Sep 17 00:00:00 2001 From: Xiwei Pan Date: Thu, 26 Mar 2026 22:40:48 +0800 Subject: [PATCH 5/5] Fix duplicate docstring on KClique::config_from_selected_vertices Co-Authored-By: Claude Opus 4.6 (1M context) --- src/models/graph/kclique.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/models/graph/kclique.rs b/src/models/graph/kclique.rs index a00d37750..94fa7e788 100644 --- a/src/models/graph/kclique.rs +++ b/src/models/graph/kclique.rs @@ -76,7 +76,7 @@ impl KClique { config } - /// Build a binary selection config from the listed vertices. + /// Convenience wrapper around [`Self::config_from_vertices`] using `self.num_vertices()`. pub fn config_from_selected_vertices(&self, selected_vertices: &[usize]) -> Vec { Self::config_from_vertices(self.num_vertices(), selected_vertices) }