diff --git a/docs/paper/reductions.typ b/docs/paper/reductions.typ index 0e76be6..cfae33f 100644 --- a/docs/paper/reductions.typ +++ b/docs/paper/reductions.typ @@ -45,6 +45,10 @@ "Factoring": [Factoring], "KingsSubgraph": [King's Subgraph MIS], "TriangularSubgraph": [Triangular Subgraph MIS], + "MaximalIS": [Maximal Independent Set], + "BMF": [Boolean Matrix Factorization], + "PaintShop": [Paint Shop], + "BicliqueCover": [Biclique Cover], ) // Definition label: "def:" — each definition block must have a matching label @@ -335,6 +339,10 @@ In all graph problems below, $G = (V, E)$ denotes an undirected graph with $|V| Given $G = (V, E)$, find $K subset.eq V$ maximizing $|K|$ such that all pairs in $K$ are adjacent: $forall u, v in K: (u, v) in E$. Equivalent to MIS on the complement graph $overline(G)$. ] +#problem-def("MaximalIS")[ + Given $G = (V, E)$ with vertex weights $w: V -> RR$, find $S subset.eq V$ maximizing $sum_(v in S) w(v)$ such that $S$ is independent ($forall u, v in S: (u, v) in.not E$) and maximal (no vertex $u in V backslash S$ can be added to $S$ while maintaining independence). +] + == Set Problems @@ -378,6 +386,20 @@ In all graph problems below, $G = (V, E)$ denotes an undirected graph with $|V| Given a composite integer $N$ and bit sizes $m, n$, find integers $p in [2, 2^m - 1]$ and $q in [2, 2^n - 1]$ such that $p times q = N$. Here $p$ has $m$ bits and $q$ has $n$ bits. ] +== Specialized Problems + +#problem-def("BMF")[ + Given an $m times n$ boolean matrix $A$ and rank $k$, find boolean matrices $B in {0,1}^(m times k)$ and $C in {0,1}^(k times n)$ minimizing the Hamming distance $d_H (A, B circle.tiny C)$, where the boolean product $(B circle.tiny C)_(i j) = or.big_ell (B_(i ell) and C_(ell j))$. +] + +#problem-def("PaintShop")[ + Given a sequence of $2n$ positions where each of $n$ cars appears exactly twice, assign a binary color to each car (each car's two occurrences receive opposite colors) to minimize the number of color changes between consecutive positions. +] + +#problem-def("BicliqueCover")[ + Given a bipartite graph $G = (L, R, E)$ and integer $k$, find $k$ bicliques $(L_1, R_1), dots, (L_k, R_k)$ that cover all edges ($E subset.eq union.big_i L_i times R_i$) while minimizing the total size $sum_i (|L_i| + |R_i|)$. +] + // Completeness check: warn about problem types in JSON but missing from paper #{ let json-models = { @@ -756,6 +778,15 @@ where $P$ is a penalty weight large enough that any constraint violation costs m _Correctness._ Original clause true $arrow.l.r$ auxiliary chain can propagate truth through new clauses. ] +#reduction-rule("Satisfiability", "CircuitSAT", + example: true, + example-caption: [3-variable SAT formula to boolean circuit], +)[ + Each CNF clause $C_i = (ell_(i 1) or dots or ell_(i m_i))$ becomes an OR gate $g_i$, and a final AND gate computes $g_1 and dots and g_k$, constrained to output _true_. +][ + The circuit is satisfiable iff the CNF formula is satisfiable, since the AND-of-ORs structure is preserved exactly. Variable mapping: SAT variable $x_j$ maps to circuit input $x_j$; ancilla variables are the clause gate outputs and the final AND output. +] + #let cs_sg = load-example("circuitsat_to_spinglass") #let cs_sg_r = load-results("circuitsat_to_spinglass") #reduction-rule("CircuitSAT", "SpinGlass", diff --git a/examples/reduction_ksatisfiability_to_satisfiability.rs b/examples/reduction_ksatisfiability_to_satisfiability.rs new file mode 100644 index 0000000..c8cd7cc --- /dev/null +++ b/examples/reduction_ksatisfiability_to_satisfiability.rs @@ -0,0 +1,140 @@ +// # K-Satisfiability (3-SAT) to Satisfiability Reduction (Trivial Embedding) +// +// ## Mathematical Equivalence +// K-SAT is a special case of SAT where every clause has exactly k literals. +// The reduction is a trivial embedding: the K-SAT clauses are directly used +// as SAT clauses with no transformation needed. +// +// ## This Example +// - Instance: 3-SAT with 4 variables and 3 clauses (each with exactly 3 literals) +// - C1: x1 OR NOT x2 OR x3 +// - C2: NOT x1 OR x3 OR x4 +// - C3: x2 OR NOT x3 OR NOT x4 +// - Source K-SAT: satisfiable +// - Target: SAT with identical clauses (same variables, same clauses) +// +// ## Output +// Exports `docs/paper/examples/ksatisfiability_to_satisfiability.json` and +// `ksatisfiability_to_satisfiability.result.json`. + +use problemreductions::export::*; +use problemreductions::prelude::*; +use problemreductions::variant::K3; + +pub fn run() { + println!("=== K-Satisfiability (3-SAT) -> Satisfiability Reduction ===\n"); + + // 1. Create a small 3-SAT instance: 4 variables, 3 clauses (each with exactly 3 literals) + let clauses = vec![ + CNFClause::new(vec![1, -2, 3]), // x1 OR NOT x2 OR x3 + CNFClause::new(vec![-1, 3, 4]), // NOT x1 OR x3 OR x4 + CNFClause::new(vec![2, -3, -4]), // x2 OR NOT x3 OR NOT x4 + ]; + let clause_strings = [ + "x1 OR NOT x2 OR x3", + "NOT x1 OR x3 OR x4", + "x2 OR NOT x3 OR NOT x4", + ]; + + let ksat = KSatisfiability::::new(4, clauses); + + println!("Source: KSatisfiability with {} variables, {} clauses", ksat.num_vars(), ksat.num_clauses()); + for (i, c) in clause_strings.iter().enumerate() { + println!(" C{}: {}", i + 1, c); + } + + // 2. Reduce to Satisfiability (trivial embedding) + let reduction = ReduceTo::::reduce_to(&ksat); + let sat = reduction.target_problem(); + + println!("\n=== Problem Transformation ==="); + println!( + "Target: Satisfiability with {} variables, {} clauses", + sat.num_vars(), + sat.num_clauses() + ); + println!(" (Trivial embedding: K-SAT is a special case of SAT, no transformation needed)"); + + // Print target clauses + println!("\n Target SAT clauses:"); + for (i, clause) in sat.clauses().iter().enumerate() { + println!(" Clause {}: {:?}", i, clause.literals); + } + + // 3. Solve the target SAT problem (satisfaction problem) + let solver = BruteForce::new(); + let sat_solutions = solver.find_all_satisfying(sat); + println!("\n=== Solution ==="); + println!("Target SAT solutions found: {}", sat_solutions.len()); + + // 4. Extract and verify all solutions + let mut solutions = Vec::new(); + for sat_sol in &sat_solutions { + let ksat_sol = reduction.extract_solution(sat_sol); + let valid = ksat.evaluate(&ksat_sol); + let assignment: Vec = ksat_sol + .iter() + .enumerate() + .map(|(i, &v)| { + format!( + "x{}={}", + i + 1, + if v == 1 { "T" } else { "F" } + ) + }) + .collect(); + println!(" [{}] -> valid: {}", assignment.join(", "), valid); + assert!(valid, "Extracted K-SAT solution must be valid"); + + solutions.push(SolutionPair { + source_config: ksat_sol, + target_config: sat_sol.to_vec(), + }); + } + + println!( + "\nAll {} SAT solutions map to valid K-SAT assignments", + sat_solutions.len() + ); + println!("Reduction verified successfully"); + + // 5. Export JSON + let source_variant = variant_to_map(KSatisfiability::::variant()); + let target_variant = variant_to_map(Satisfiability::variant()); + let overhead = lookup_overhead( + "KSatisfiability", + &source_variant, + "Satisfiability", + &target_variant, + ) + .expect("KSatisfiability -> Satisfiability overhead not found"); + + let data = ReductionData { + source: ProblemSide { + problem: KSatisfiability::::NAME.to_string(), + variant: source_variant, + instance: serde_json::json!({ + "num_vars": ksat.num_vars(), + "num_clauses": ksat.num_clauses(), + "k": 3, + }), + }, + target: ProblemSide { + problem: Satisfiability::NAME.to_string(), + variant: target_variant, + instance: serde_json::json!({ + "num_vars": sat.num_vars(), + "num_clauses": sat.num_clauses(), + }), + }, + overhead: overhead_to_json(&overhead), + }; + + let results = ResultData { solutions }; + let name = "ksatisfiability_to_satisfiability"; + write_example(name, &data, &results); +} + +fn main() { + run() +} diff --git a/examples/reduction_maximumsetpacking_to_maximumindependentset.rs b/examples/reduction_maximumsetpacking_to_maximumindependentset.rs new file mode 100644 index 0000000..3f924df --- /dev/null +++ b/examples/reduction_maximumsetpacking_to_maximumindependentset.rs @@ -0,0 +1,145 @@ +// # Set Packing to Independent Set Reduction +// +// ## Mathematical Equivalence +// Each set becomes a vertex; two vertices are adjacent if their sets overlap. +// Selecting a collection of non-overlapping sets is equivalent to selecting +// an independent set in the conflict graph. The optimal packing size equals +// the maximum independent set size. +// +// ## This Example +// - Instance: 5 sets over universe {0,...,7}, with varying sizes (2 and 3) +// - S0 = {0, 1, 2}, S1 = {2, 3}, S2 = {4, 5, 6}, S3 = {1, 5, 7}, S4 = {3, 6} +// - Conflict edges: (0,1) share 2, (0,3) share 1, (1,4) share 3, (2,3) share 5, (2,4) share 6 +// - Source MaximumSetPacking: max packing size 2 (e.g., S0+S2, S1+S3, S3+S4, ...) +// - Target MaximumIndependentSet: 5 vertices, 5 edges, max IS size 2 +// +// ## Output +// Exports `docs/paper/examples/maximumsetpacking_to_maximumindependentset.json` and +// `maximumsetpacking_to_maximumindependentset.result.json`. +// +// See docs/paper/reductions.typ for the full reduction specification. + +use problemreductions::export::*; +use problemreductions::prelude::*; +use problemreductions::topology::{Graph, SimpleGraph}; + +pub fn run() { + println!("\n=== Set Packing -> Independent Set Reduction ===\n"); + + // 1. Create MaximumSetPacking instance: 5 sets over universe {0,...,7} + let sets = vec![ + vec![0, 1, 2], // S0 (size 3) + vec![2, 3], // S1 (size 2, overlaps S0 at 2) + vec![4, 5, 6], // S2 (size 3, disjoint from S0, S1) + vec![1, 5, 7], // S3 (size 3, overlaps S0 at 1, S2 at 5) + vec![3, 6], // S4 (size 2, overlaps S1 at 3, S2 at 6) + ]; + let num_sets = sets.len(); + let sp = MaximumSetPacking::with_weights(sets.clone(), vec![1i32; num_sets]); + + println!("Source: MaximumSetPacking with {} sets", num_sets); + for (i, s) in sets.iter().enumerate() { + println!(" S{} = {:?}", i, s); + } + + // 2. Reduce to MaximumIndependentSet + let reduction = ReduceTo::>::reduce_to(&sp); + let target = reduction.target_problem(); + + println!("\nTarget: MaximumIndependentSet"); + println!(" Vertices: {}", target.graph().num_vertices()); + println!(" Edges: {} {:?}", target.graph().num_edges(), target.graph().edges()); + + // 3. Solve the target problem + let solver = BruteForce::new(); + let target_solutions = solver.find_all_best(target); + + println!("\nBest target solutions: {}", target_solutions.len()); + + // 4. Extract and verify each solution + let mut solutions = Vec::new(); + for (i, target_sol) in target_solutions.iter().enumerate() { + let source_sol = reduction.extract_solution(target_sol); + let source_size = sp.evaluate(&source_sol); + let target_size = target.evaluate(target_sol); + + println!( + " Solution {}: target={:?} (size={:?}), source={:?} (size={:?}, valid={})", + i, + target_sol, + target_size, + source_sol, + source_size, + source_size.is_valid() + ); + + assert!( + source_size.is_valid(), + "Extracted source solution must be valid" + ); + + solutions.push(SolutionPair { + source_config: source_sol, + target_config: target_sol.clone(), + }); + } + + // 5. Verify the optimal value + let target_sol = &target_solutions[0]; + let source_sol = reduction.extract_solution(target_sol); + let source_size = sp.evaluate(&source_sol); + let target_size = target.evaluate(target_sol); + + assert_eq!( + source_size, + problemreductions::types::SolutionSize::Valid(2), + "MaximumSetPacking optimal packing size is 2" + ); + assert_eq!( + target_size, + problemreductions::types::SolutionSize::Valid(2), + "MaximumIndependentSet should also have size 2" + ); + + // 6. Export JSON + let source_variant = variant_to_map(MaximumSetPacking::::variant()); + let target_variant = variant_to_map(MaximumIndependentSet::::variant()); + let overhead = lookup_overhead( + "MaximumSetPacking", + &source_variant, + "MaximumIndependentSet", + &target_variant, + ) + .expect("MaximumSetPacking -> MaximumIndependentSet overhead not found"); + + let data = ReductionData { + source: ProblemSide { + problem: MaximumSetPacking::::NAME.to_string(), + variant: source_variant, + instance: serde_json::json!({ + "num_sets": sp.num_sets(), + "sets": sp.sets(), + }), + }, + target: ProblemSide { + problem: MaximumIndependentSet::::NAME.to_string(), + variant: target_variant, + instance: serde_json::json!({ + "num_vertices": target.graph().num_vertices(), + "num_edges": target.graph().num_edges(), + "edges": target.graph().edges(), + }), + }, + overhead: overhead_to_json(&overhead), + }; + + let results = ResultData { solutions }; + let name = "maximumsetpacking_to_maximumindependentset"; + write_example(name, &data, &results); + + println!("\nDone: SetPacking(5 sets) optimal=2 maps to IS(5 vertices, 5 edges) optimal=2"); +} + +fn main() { + run() +} diff --git a/examples/reduction_satisfiability_to_circuitsat.rs b/examples/reduction_satisfiability_to_circuitsat.rs new file mode 100644 index 0000000..f217649 --- /dev/null +++ b/examples/reduction_satisfiability_to_circuitsat.rs @@ -0,0 +1,160 @@ +// # SAT to CircuitSAT Reduction +// +// ## Mathematical Equivalence +// A CNF formula is converted into a boolean circuit by creating an OR gate for +// each clause and a final AND gate that requires all clause outputs to be true. +// The circuit is satisfiable iff the original CNF formula is satisfiable. +// +// ## This Example +// - Instance: 3-variable, 3-clause SAT formula +// - (x1 v ~x2 v x3) & (~x1 v x2) & (x2 v x3) +// - Source SAT: satisfiable +// - Target: CircuitSAT with OR gates per clause + AND gate +// +// ## Output +// Exports `docs/paper/examples/satisfiability_to_circuitsat.json` and `satisfiability_to_circuitsat.result.json`. + +use problemreductions::export::*; +use problemreductions::prelude::*; + +pub fn run() { + // 1. Create SAT instance: 3 variables, 3 clauses + // (x1 v ~x2 v x3) & (~x1 v x2) & (x2 v x3) + let sat = Satisfiability::new( + 3, + vec![ + CNFClause::new(vec![1, -2, 3]), // x1 v ~x2 v x3 + CNFClause::new(vec![-1, 2]), // ~x1 v x2 + CNFClause::new(vec![2, 3]), // x2 v x3 + ], + ); + + println!("=== SAT to CircuitSAT Reduction ===\n"); + println!("Source SAT formula: 3-variable, 3-clause"); + println!(" (x1 v ~x2 v x3) & (~x1 v x2) & (x2 v x3)"); + println!( + " {} variables, {} clauses", + sat.num_vars(), + sat.num_clauses() + ); + + // 2. Reduce to CircuitSAT + let reduction = ReduceTo::::reduce_to(&sat); + let circuit_sat = reduction.target_problem(); + + println!("\n=== Problem Transformation ==="); + println!( + "Source: Satisfiability with {} variables, {} clauses", + sat.num_vars(), + sat.num_clauses() + ); + println!( + "Target: CircuitSAT with {} variables, {} assignments (gates)", + circuit_sat.num_variables(), + circuit_sat.circuit().num_assignments() + ); + println!( + " Variables: {:?}", + circuit_sat.variable_names() + ); + println!(" Each clause becomes an OR gate; a final AND gate combines them."); + + // 3. Solve the target CircuitSAT problem (satisfaction problem) + let solver = BruteForce::new(); + let circuit_solutions = solver.find_all_satisfying(circuit_sat); + println!("\n=== Solution ==="); + println!( + "CircuitSAT satisfying assignments found: {}", + circuit_solutions.len() + ); + + // 4. Extract and verify source solutions + let sat_solution = reduction.extract_solution(&circuit_solutions[0]); + println!("First extracted SAT solution: {:?}", sat_solution); + println!( + " Interpretation: x1={}, x2={}, x3={}", + sat_solution[0], sat_solution[1], sat_solution[2] + ); + + let satisfied = sat.evaluate(&sat_solution); + println!("SAT solution valid: {}", satisfied); + assert!(satisfied, "Extracted SAT solution must be valid"); + + // Verify all CircuitSAT solutions map to valid SAT assignments + let mut valid_count = 0; + let mut solutions = Vec::new(); + for cs_sol in &circuit_solutions { + let sat_sol = reduction.extract_solution(cs_sol); + let s = sat.evaluate(&sat_sol); + if s { + valid_count += 1; + } + solutions.push(SolutionPair { + source_config: sat_sol, + target_config: cs_sol.to_vec(), + }); + } + println!( + "All {} CircuitSAT solutions map to valid SAT assignments: {}", + circuit_solutions.len(), + valid_count == circuit_solutions.len() + ); + assert_eq!(valid_count, circuit_solutions.len()); + + // Also verify that the extracted solutions cover all SAT solutions + let sat_all = solver.find_all_satisfying(&sat); + let extracted_set: std::collections::HashSet> = circuit_solutions + .iter() + .map(|cs| reduction.extract_solution(cs)) + .collect(); + let sat_set: std::collections::HashSet> = sat_all.into_iter().collect(); + assert_eq!( + extracted_set, sat_set, + "Extracted solutions must match all SAT solutions" + ); + println!( + "Unique SAT solutions extracted: {} (matches direct SAT solve)", + extracted_set.len() + ); + + println!("\nReduction verified successfully"); + + // 5. Export JSON + let source_variant = variant_to_map(Satisfiability::variant()); + let target_variant = variant_to_map(CircuitSAT::variant()); + let overhead = lookup_overhead( + "Satisfiability", + &source_variant, + "CircuitSAT", + &target_variant, + ) + .expect("Satisfiability -> CircuitSAT overhead not found"); + + let data = ReductionData { + source: ProblemSide { + problem: Satisfiability::NAME.to_string(), + variant: source_variant, + instance: serde_json::json!({ + "num_vars": sat.num_vars(), + "num_clauses": sat.num_clauses(), + }), + }, + target: ProblemSide { + problem: CircuitSAT::NAME.to_string(), + variant: target_variant, + instance: serde_json::json!({ + "num_variables": circuit_sat.num_variables(), + "num_gates": circuit_sat.circuit().num_assignments(), + }), + }, + overhead: overhead_to_json(&overhead), + }; + + let results = ResultData { solutions }; + let name = "satisfiability_to_circuitsat"; + write_example(name, &data, &results); +} + +fn main() { + run() +} diff --git a/problemreductions-cli/src/dispatch.rs b/problemreductions-cli/src/dispatch.rs index e1431be..285050b 100644 --- a/problemreductions-cli/src/dispatch.rs +++ b/problemreductions-cli/src/dispatch.rs @@ -218,6 +218,7 @@ pub fn load_problem( "MaximumMatching" => deser_opt::>(data), "MinimumDominatingSet" => deser_opt::>(data), "MaxCut" => deser_opt::>(data), + "MaximalIS" => deser_opt::>(data), "TravelingSalesman" => deser_opt::>(data), "KColoring" => match variant.get("k").map(|s| s.as_str()) { Some("K3") => deser_sat::>(data), @@ -265,6 +266,7 @@ pub fn serialize_any_problem( "MaximumMatching" => try_ser::>(any), "MinimumDominatingSet" => try_ser::>(any), "MaxCut" => try_ser::>(any), + "MaximalIS" => try_ser::>(any), "TravelingSalesman" => try_ser::>(any), "KColoring" => match variant.get("k").map(|s| s.as_str()) { Some("K3") => try_ser::>(any), diff --git a/src/models/mod.rs b/src/models/mod.rs index 06991b0..2b1bb93 100644 --- a/src/models/mod.rs +++ b/src/models/mod.rs @@ -10,10 +10,10 @@ pub mod specialized; // Re-export commonly used types pub use graph::{ - KColoring, MaxCut, MaximalIS, MaximumIndependentSet, MaximumMatching, MinimumDominatingSet, - MinimumVertexCover, TravelingSalesman, + KColoring, MaxCut, MaximalIS, MaximumClique, MaximumIndependentSet, MaximumMatching, + MinimumDominatingSet, MinimumVertexCover, TravelingSalesman, }; -pub use optimization::{SpinGlass, QUBO}; -pub use satisfiability::{CNFClause, Satisfiability}; +pub use optimization::{SpinGlass, ILP, QUBO}; +pub use satisfiability::{CNFClause, KSatisfiability, Satisfiability}; pub use set::{MaximumSetPacking, MinimumSetCovering}; pub use specialized::{BicliqueCover, CircuitSAT, Factoring, PaintShop, BMF}; diff --git a/src/unit_tests/rules/circuit_spinglass.rs b/src/unit_tests/rules/circuit_spinglass.rs index 249ad38..6342a12 100644 --- a/src/unit_tests/rules/circuit_spinglass.rs +++ b/src/unit_tests/rules/circuit_spinglass.rs @@ -46,7 +46,7 @@ where } #[test] -fn test_and_gadget() { +fn test_circuit_to_spinglass_closed_loop() { let gadget: LogicGadget = and_gadget(); assert_eq!(gadget.num_spins(), 3); assert_eq!(gadget.inputs, vec![0, 1]); diff --git a/src/unit_tests/rules/coloring_ilp.rs b/src/unit_tests/rules/coloring_ilp.rs index b1033c8..a8678c6 100644 --- a/src/unit_tests/rules/coloring_ilp.rs +++ b/src/unit_tests/rules/coloring_ilp.rs @@ -49,7 +49,7 @@ fn test_reduction_path_graph() { } #[test] -fn test_ilp_solution_equals_brute_force_triangle() { +fn test_coloring_to_ilp_closed_loop() { // Triangle needs 3 colors let problem = KColoring::::new(SimpleGraph::new(3, vec![(0, 1), (1, 2), (0, 2)])); let reduction = ReduceTo::::reduce_to(&problem); diff --git a/src/unit_tests/rules/factoring_circuit.rs b/src/unit_tests/rules/factoring_circuit.rs index c55726d..16019ab 100644 --- a/src/unit_tests/rules/factoring_circuit.rs +++ b/src/unit_tests/rules/factoring_circuit.rs @@ -129,7 +129,7 @@ fn test_factorization_6_satisfies_circuit() { } #[test] -fn test_factorization_15_satisfies_circuit() { +fn test_factoring_to_circuit_closed_loop() { let factoring = Factoring::new(4, 4, 15); let reduction = ReduceTo::::reduce_to(&factoring); diff --git a/src/unit_tests/rules/factoring_ilp.rs b/src/unit_tests/rules/factoring_ilp.rs index e8db96f..157157d 100644 --- a/src/unit_tests/rules/factoring_ilp.rs +++ b/src/unit_tests/rules/factoring_ilp.rs @@ -165,7 +165,7 @@ fn test_infeasible_target_too_large() { } #[test] -fn test_ilp_matches_brute_force() { +fn test_factoring_to_ilp_closed_loop() { let problem = Factoring::new(2, 2, 6); let reduction: ReductionFactoringToILP = ReduceTo::::reduce_to(&problem); let ilp = reduction.target_problem(); diff --git a/src/unit_tests/rules/maximumclique_ilp.rs b/src/unit_tests/rules/maximumclique_ilp.rs index 0ab9419..1bfc5f3 100644 --- a/src/unit_tests/rules/maximumclique_ilp.rs +++ b/src/unit_tests/rules/maximumclique_ilp.rs @@ -109,7 +109,7 @@ fn test_reduction_weighted() { } #[test] -fn test_ilp_solution_equals_brute_force_triangle() { +fn test_maximumclique_to_ilp_closed_loop() { // Triangle graph (K3): max clique = 3 vertices let problem: MaximumClique = MaximumClique::new( SimpleGraph::new(3, vec![(0, 1), (1, 2), (0, 2)]), diff --git a/src/unit_tests/rules/maximumindependentset_ilp.rs b/src/unit_tests/rules/maximumindependentset_ilp.rs index 168e25e..b85681c 100644 --- a/src/unit_tests/rules/maximumindependentset_ilp.rs +++ b/src/unit_tests/rules/maximumindependentset_ilp.rs @@ -51,7 +51,7 @@ fn test_reduction_weighted() { } #[test] -fn test_ilp_solution_equals_brute_force_triangle() { +fn test_maximumindependentset_to_ilp_closed_loop() { // Triangle graph: max IS = 1 vertex let problem = MaximumIndependentSet::new( SimpleGraph::new(3, vec![(0, 1), (1, 2), (0, 2)]), diff --git a/src/unit_tests/rules/maximumindependentset_maximumsetpacking.rs b/src/unit_tests/rules/maximumindependentset_maximumsetpacking.rs index 9cd6baa..693c2cb 100644 --- a/src/unit_tests/rules/maximumindependentset_maximumsetpacking.rs +++ b/src/unit_tests/rules/maximumindependentset_maximumsetpacking.rs @@ -3,7 +3,7 @@ use crate::solvers::BruteForce; include!("../jl_helpers.rs"); #[test] -fn test_weighted_reduction() { +fn test_maximumindependentset_to_maximumsetpacking_closed_loop() { let is_problem = MaximumIndependentSet::new(SimpleGraph::new(3, vec![(0, 1), (1, 2)]), vec![10, 20, 30]); let reduction = ReduceTo::>::reduce_to(&is_problem); diff --git a/src/unit_tests/rules/maximummatching_ilp.rs b/src/unit_tests/rules/maximummatching_ilp.rs index 987cc8d..65d6955 100644 --- a/src/unit_tests/rules/maximummatching_ilp.rs +++ b/src/unit_tests/rules/maximummatching_ilp.rs @@ -49,7 +49,7 @@ fn test_reduction_weighted() { } #[test] -fn test_ilp_solution_equals_brute_force_triangle() { +fn test_maximummatching_to_ilp_closed_loop() { // Triangle graph: max matching = 1 edge let problem = MaximumMatching::<_, i32>::unit_weights(SimpleGraph::new(3, vec![(0, 1), (1, 2), (0, 2)])); diff --git a/src/unit_tests/rules/maximummatching_maximumsetpacking.rs b/src/unit_tests/rules/maximummatching_maximumsetpacking.rs index 3504e79..9b38e7b 100644 --- a/src/unit_tests/rules/maximummatching_maximumsetpacking.rs +++ b/src/unit_tests/rules/maximummatching_maximumsetpacking.rs @@ -6,7 +6,7 @@ use crate::types::SolutionSize; include!("../jl_helpers.rs"); #[test] -fn test_matching_to_setpacking_structure() { +fn test_maximummatching_to_maximumsetpacking_closed_loop() { // Path graph 0-1-2 let matching = MaximumMatching::<_, i32>::unit_weights(SimpleGraph::new(3, vec![(0, 1), (1, 2)])); diff --git a/src/unit_tests/rules/maximumsetpacking_ilp.rs b/src/unit_tests/rules/maximumsetpacking_ilp.rs index a190e03..d547ca6 100644 --- a/src/unit_tests/rules/maximumsetpacking_ilp.rs +++ b/src/unit_tests/rules/maximumsetpacking_ilp.rs @@ -47,7 +47,7 @@ fn test_reduction_weighted() { } #[test] -fn test_ilp_solution_equals_brute_force_chain() { +fn test_maximumsetpacking_to_ilp_closed_loop() { // Chain: {0,1}, {1,2}, {2,3} - can select at most 2 non-adjacent sets let problem = MaximumSetPacking::::new(vec![vec![0, 1], vec![1, 2], vec![2, 3]]); let reduction: ReductionSPToILP = ReduceTo::::reduce_to(&problem); diff --git a/src/unit_tests/rules/minimumdominatingset_ilp.rs b/src/unit_tests/rules/minimumdominatingset_ilp.rs index 97eab1e..cc91b26 100644 --- a/src/unit_tests/rules/minimumdominatingset_ilp.rs +++ b/src/unit_tests/rules/minimumdominatingset_ilp.rs @@ -51,7 +51,7 @@ fn test_reduction_weighted() { } #[test] -fn test_ilp_solution_equals_brute_force_star() { +fn test_minimumdominatingset_to_ilp_closed_loop() { // Star graph: center vertex 0 connected to all others // Minimum dominating set is just the center (weight 1) let problem = MinimumDominatingSet::new( diff --git a/src/unit_tests/rules/minimumsetcovering_ilp.rs b/src/unit_tests/rules/minimumsetcovering_ilp.rs index f586c8c..e3b2139 100644 --- a/src/unit_tests/rules/minimumsetcovering_ilp.rs +++ b/src/unit_tests/rules/minimumsetcovering_ilp.rs @@ -46,7 +46,7 @@ fn test_reduction_weighted() { } #[test] -fn test_ilp_solution_equals_brute_force_simple() { +fn test_minimumsetcovering_to_ilp_closed_loop() { // Universe: {0, 1, 2}, Sets: S0={0,1}, S1={1,2}, S2={0,2} // Minimum cover: any 2 sets work let problem = MinimumSetCovering::::new(3, vec![vec![0, 1], vec![1, 2], vec![0, 2]]); diff --git a/src/unit_tests/rules/minimumvertexcover_ilp.rs b/src/unit_tests/rules/minimumvertexcover_ilp.rs index 6b5fe5a..d6a7674 100644 --- a/src/unit_tests/rules/minimumvertexcover_ilp.rs +++ b/src/unit_tests/rules/minimumvertexcover_ilp.rs @@ -51,7 +51,7 @@ fn test_reduction_weighted() { } #[test] -fn test_ilp_solution_equals_brute_force_triangle() { +fn test_minimumvertexcover_to_ilp_closed_loop() { // Triangle graph: min VC = 2 vertices let problem = MinimumVertexCover::new( SimpleGraph::new(3, vec![(0, 1), (1, 2), (0, 2)]), diff --git a/src/unit_tests/rules/minimumvertexcover_maximumindependentset.rs b/src/unit_tests/rules/minimumvertexcover_maximumindependentset.rs index b580f5c..1664b85 100644 --- a/src/unit_tests/rules/minimumvertexcover_maximumindependentset.rs +++ b/src/unit_tests/rules/minimumvertexcover_maximumindependentset.rs @@ -3,7 +3,7 @@ use crate::solvers::BruteForce; include!("../jl_helpers.rs"); #[test] -fn test_weighted_reduction() { +fn test_minimumvertexcover_to_maximumindependentset_closed_loop() { // Test with weighted problems let is_problem = MaximumIndependentSet::new(SimpleGraph::new(3, vec![(0, 1), (1, 2)]), vec![10, 20, 30]); diff --git a/src/unit_tests/rules/minimumvertexcover_minimumsetcovering.rs b/src/unit_tests/rules/minimumvertexcover_minimumsetcovering.rs index 2a67e8e..6a9b561 100644 --- a/src/unit_tests/rules/minimumvertexcover_minimumsetcovering.rs +++ b/src/unit_tests/rules/minimumvertexcover_minimumsetcovering.rs @@ -3,7 +3,7 @@ use crate::solvers::BruteForce; include!("../jl_helpers.rs"); #[test] -fn test_vc_to_sc_basic() { +fn test_minimumvertexcover_to_minimumsetcovering_closed_loop() { // Path graph 0-1-2 with edges (0,1) and (1,2) // Vertex 0 covers edge 0 // Vertex 1 covers edges 0 and 1 diff --git a/src/unit_tests/rules/sat_coloring.rs b/src/unit_tests/rules/sat_coloring.rs index c2e655d..456b3c8 100644 --- a/src/unit_tests/rules/sat_coloring.rs +++ b/src/unit_tests/rules/sat_coloring.rs @@ -32,7 +32,7 @@ fn test_special_vertex_accessors() { } #[test] -fn test_simple_sat_to_coloring() { +fn test_sat_to_coloring_closed_loop() { // Simple SAT: (x1) - one clause with one literal let sat = Satisfiability::new(1, vec![CNFClause::new(vec![1])]); let reduction = ReduceTo::>::reduce_to(&sat); diff --git a/src/unit_tests/rules/sat_ksat.rs b/src/unit_tests/rules/sat_ksat.rs index ea8b5c7..c0bc63c 100644 --- a/src/unit_tests/rules/sat_ksat.rs +++ b/src/unit_tests/rules/sat_ksat.rs @@ -102,7 +102,7 @@ fn test_sat_to_3sat_single_literal() { } #[test] -fn test_sat_to_3sat_preserves_satisfiability() { +fn test_sat_to_ksat_closed_loop() { // Create a SAT formula and verify the 3-SAT version is equisatisfiable let sat = Satisfiability::new( 3, diff --git a/src/unit_tests/rules/sat_maximumindependentset.rs b/src/unit_tests/rules/sat_maximumindependentset.rs index 5fded92..c34a467 100644 --- a/src/unit_tests/rules/sat_maximumindependentset.rs +++ b/src/unit_tests/rules/sat_maximumindependentset.rs @@ -42,7 +42,7 @@ fn test_boolvar_complement() { } #[test] -fn test_simple_sat_to_is() { +fn test_sat_to_maximumindependentset_closed_loop() { // Simple SAT: (x1) - one clause with one literal let sat = Satisfiability::new(1, vec![CNFClause::new(vec![1])]); let reduction = ReduceTo::>::reduce_to(&sat); diff --git a/src/unit_tests/rules/sat_minimumdominatingset.rs b/src/unit_tests/rules/sat_minimumdominatingset.rs index 1e56439..e6ae240 100644 --- a/src/unit_tests/rules/sat_minimumdominatingset.rs +++ b/src/unit_tests/rules/sat_minimumdominatingset.rs @@ -6,7 +6,7 @@ use crate::traits::Problem; include!("../jl_helpers.rs"); #[test] -fn test_simple_sat_to_ds() { +fn test_sat_to_minimumdominatingset_closed_loop() { // Simple SAT: (x1) - one variable, one clause let sat = Satisfiability::new(1, vec![CNFClause::new(vec![1])]); let reduction = ReduceTo::>::reduce_to(&sat); diff --git a/src/unit_tests/rules/spinglass_maxcut.rs b/src/unit_tests/rules/spinglass_maxcut.rs index c0d9a38..e24e17c 100644 --- a/src/unit_tests/rules/spinglass_maxcut.rs +++ b/src/unit_tests/rules/spinglass_maxcut.rs @@ -3,7 +3,7 @@ use crate::solvers::BruteForce; include!("../jl_helpers.rs"); #[test] -fn test_spinglass_to_maxcut_no_onsite() { +fn test_spinglass_to_maxcut_closed_loop() { // SpinGlass without onsite terms let sg = SpinGlass::::new(3, vec![((0, 1), 1), ((1, 2), 1)], vec![0, 0, 0]); let reduction = ReduceTo::>::reduce_to(&sg); diff --git a/src/unit_tests/rules/spinglass_qubo.rs b/src/unit_tests/rules/spinglass_qubo.rs index 7ffe80c..5dd7139 100644 --- a/src/unit_tests/rules/spinglass_qubo.rs +++ b/src/unit_tests/rules/spinglass_qubo.rs @@ -4,7 +4,7 @@ use crate::traits::Problem; include!("../jl_helpers.rs"); #[test] -fn test_antiferromagnetic() { +fn test_spinglass_to_qubo_closed_loop() { // Antiferromagnetic: J > 0, prefers anti-aligned spins let sg = SpinGlass::::new(2, vec![((0, 1), 1.0)], vec![0.0, 0.0]); let reduction = ReduceTo::>::reduce_to(&sg); diff --git a/tests/suites/examples.rs b/tests/suites/examples.rs index 721c1ed..3c9ad80 100644 --- a/tests/suites/examples.rs +++ b/tests/suites/examples.rs @@ -20,6 +20,7 @@ example_test!(reduction_ilp_to_qubo); example_test!(reduction_kcoloring_to_ilp); example_test!(reduction_kcoloring_to_qubo); example_test!(reduction_ksatisfiability_to_qubo); +example_test!(reduction_ksatisfiability_to_satisfiability); example_test!(reduction_maxcut_to_spinglass); example_test!(reduction_maximumclique_to_ilp); example_test!(reduction_maximumindependentset_to_ilp); @@ -29,6 +30,7 @@ example_test!(reduction_maximumindependentset_to_qubo); example_test!(reduction_maximummatching_to_ilp); example_test!(reduction_maximummatching_to_maximumsetpacking); example_test!(reduction_maximumsetpacking_to_ilp); +example_test!(reduction_maximumsetpacking_to_maximumindependentset); example_test!(reduction_maximumsetpacking_to_qubo); example_test!(reduction_minimumdominatingset_to_ilp); example_test!(reduction_minimumsetcovering_to_ilp); @@ -39,6 +41,7 @@ example_test!(reduction_minimumvertexcover_to_qubo); example_test!(reduction_qubo_to_ilp); example_test!(reduction_qubo_to_spinglass); example_test!(reduction_satisfiability_to_kcoloring); +example_test!(reduction_satisfiability_to_circuitsat); example_test!(reduction_satisfiability_to_ksatisfiability); example_test!(reduction_satisfiability_to_maximumindependentset); example_test!(reduction_satisfiability_to_minimumdominatingset); @@ -80,6 +83,10 @@ example_fn!( test_ksatisfiability_to_qubo, reduction_ksatisfiability_to_qubo ); +example_fn!( + test_ksatisfiability_to_satisfiability, + reduction_ksatisfiability_to_satisfiability +); example_fn!(test_maxcut_to_spinglass, reduction_maxcut_to_spinglass); example_fn!(test_maximumclique_to_ilp, reduction_maximumclique_to_ilp); example_fn!( @@ -110,6 +117,10 @@ example_fn!( test_maximumsetpacking_to_ilp, reduction_maximumsetpacking_to_ilp ); +example_fn!( + test_maximumsetpacking_to_maximumindependentset, + reduction_maximumsetpacking_to_maximumindependentset +); example_fn!( test_maximumsetpacking_to_qubo, reduction_maximumsetpacking_to_qubo @@ -140,6 +151,10 @@ example_fn!( ); example_fn!(test_qubo_to_ilp, reduction_qubo_to_ilp); example_fn!(test_qubo_to_spinglass, reduction_qubo_to_spinglass); +example_fn!( + test_satisfiability_to_circuitsat, + reduction_satisfiability_to_circuitsat +); example_fn!( test_satisfiability_to_kcoloring, reduction_satisfiability_to_kcoloring