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..94fa7e788 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 + } + + /// 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) + } } 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/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/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 new file mode 100644 index 000000000..061ac0e81 --- /dev/null +++ b/src/rules/hamiltoniancircuit_bottlenecktravelingsalesman.rs @@ -0,0 +1,75 @@ +//! 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 { + crate::rules::graph_helpers::edges_to_cycle_order(self.target.graph(), target_solution) + } +} + +#[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..a3b20d080 --- /dev/null +++ b/src/rules/hamiltoniancircuit_hamiltonianpath.rs @@ -0,0 +1,157 @@ +//! 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![]; + } + + if target_solution.len() != n + 3 { + 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 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], + }; + + if oriented.get(1) != Some(&0) || oriented.get(n + 1) != Some(&v_prime) { + return vec![0; n]; + } + + oriented[1..=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(); + + // HC is unsatisfiable for n < 3; return a trivially unsatisfiable HP instance. + if n < 3 { + let target_graph = SimpleGraph::empty(n + 3); + let target = HamiltonianPath::new(target_graph); + return ReductionHamiltonianCircuitToHamiltonianPath { + target, + num_original_vertices: n, + }; + } + + 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/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/hamiltonianpath_isomorphicspanningtree.rs b/src/rules/hamiltonianpath_isomorphicspanningtree.rs new file mode 100644 index 000000000..481b24541 --- /dev/null +++ b/src/rules/hamiltonianpath_isomorphicspanningtree.rs @@ -0,0 +1,82 @@ +//! 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(); + + let tree = SimpleGraph::path(n); + + 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::path(5)); + 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..0dcd3c4ca --- /dev/null +++ b/src/rules/kclique_conjunctivebooleanquery.rs @@ -0,0 +1,107 @@ +//! 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 { + KClique::::config_from_vertices(self.num_vertices, target_solution) + } +} + +#[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.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::with_capacity(self.num_edges() * 2); + for (u, v) in self.graph().edges() { + 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::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)])); + } + } + + 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..e351a2cfa --- /dev/null +++ b/src/rules/kclique_subgraphisomorphism.rs @@ -0,0 +1,94 @@ +//! 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::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 { + KClique::::config_from_vertices(self.num_source_vertices, target_solution) + } +} + +#[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.num_vertices(); + let k = self.k(); + + let pattern = SimpleGraph::complete(k); + let host = self.graph().clone(); + + 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..002775c1f 100644 --- a/src/rules/mod.rs +++ b/src/rules/mod.rs @@ -9,9 +9,16 @@ 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 graph_helpers; +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 +38,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 +241,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 +261,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..b17a292b0 --- /dev/null +++ b/src/rules/satisfiability_naesatisfiability.rs @@ -0,0 +1,114 @@ +//! 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; + 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 { + // 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| { + 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(); + + 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/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/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..e9b9ca02a --- /dev/null +++ b/src/unit_tests/rules/hamiltoniancircuit_hamiltonianpath.rs @@ -0,0 +1,128 @@ +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", + ); +} + +#[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/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..b72884a81 --- /dev/null +++ b/src/unit_tests/rules/partition_multiprocessorscheduling.rs @@ -0,0 +1,129 @@ +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; + +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, reduction) = reduce_partition(&[1, 2, 3, 4]); + + assert_satisfaction_round_trip_from_satisfaction_target( + &source, + &reduction, + "Partition -> MultiprocessorScheduling closed loop", + ); +} + +#[test] +fn test_partition_to_multiprocessorscheduling_structure() { + let (source, reduction) = reduce_partition(&[1, 2, 3, 4]); + 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, 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); + + assert_satisfiability_matches(&source, target, false); +} + +#[test] +fn test_partition_to_multiprocessorscheduling_equal_elements() { + // [3, 3, 3, 3], sum=12, target=6 + let (source, reduction) = reduce_partition(&[3, 3, 3, 3]); + let target = reduction.target_problem(); + + assert_eq!(target.deadline(), 6); + assert_satisfiability_matches(&source, target, true); + + // 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, reduction) = reduce_partition(&[1, 2, 3, 4]); + 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, 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]); + + assert_satisfiability_matches(&source, target, false); +} + +#[test] +fn test_partition_to_multiprocessorscheduling_two_elements() { + // [5, 5], sum=10, target=5 + let (source, reduction) = reduce_partition(&[5, 5]); + let target = reduction.target_problem(); + + assert_eq!(target.deadline(), 5); + assert_satisfiability_matches(&source, target, true); + + 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..fbe452648 --- /dev/null +++ b/src/unit_tests/rules/satisfiability_naesatisfiability.rs @@ -0,0 +1,198 @@ +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 4, 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 + ); + } +} + +#[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()); +}