From dbbbbbd723e5a5029c47a2ea3add30e73a7d980a Mon Sep 17 00:00:00 2001 From: GiggleLiu Date: Tue, 7 Apr 2026 16:35:53 +0800 Subject: [PATCH 01/13] Add CircuitSAT to Satisfiability reduction (#970) --- docs/paper/reductions.typ | 41 +++ src/rules/circuit_sat.rs | 370 ++++++++++++++++++++++++++++ src/rules/mod.rs | 2 + src/unit_tests/rules/circuit_sat.rs | 88 +++++++ src/unit_tests/rules/graph.rs | 24 +- 5 files changed, 524 insertions(+), 1 deletion(-) create mode 100644 src/rules/circuit_sat.rs create mode 100644 src/unit_tests/rules/circuit_sat.rs diff --git a/docs/paper/reductions.typ b/docs/paper/reductions.typ index 0d4572ef..bfe70228 100644 --- a/docs/paper/reductions.typ +++ b/docs/paper/reductions.typ @@ -10247,6 +10247,46 @@ where $P$ is a penalty weight large enough that any constraint violation costs m _Solution extraction._ Return the values of the circuit input variables $x_1, dots, x_n$. ] +#let cs_sat = load-example("CircuitSAT", "Satisfiability") +#let cs_sat_sol = cs_sat.solutions.at(0) +#reduction-rule("CircuitSAT", "Satisfiability", + example: true, + example-caption: [Tseitin encoding of a circuit equation], + extra: [ + #pred-commands( + "pred create --example " + problem-spec(cs_sat.source) + " -o circuitsat.json", + "pred reduce circuitsat.json --to " + target-spec(cs_sat) + " -o bundle.json", + "pred solve bundle.json", + "pred evaluate circuitsat.json --config " + cs_sat_sol.source_config.map(str).join(","), + ) + Circuit: #circuit-num-gates(cs_sat.source.instance) assignment, #circuit-num-variables(cs_sat.source.instance) named variables \ + Target: #cs_sat.target.instance.num_vars SAT variables, #cs_sat.target.instance.clauses.len() clauses \ + + *Step 1 -- Flatten the expression.* The canonical example is the circuit equation $r = (x_1 and x_2) or (not x_3 and x_4)$. Introduce auxiliary variables $a = x_1 and x_2$, $b = not x_3$, $c = b and x_4$, and $d = a or c$. This yields #cs_sat.target.instance.num_vars SAT variables: the five named circuit variables $(r, x_1, x_2, x_3, x_4)$ plus four Tseitin variables $(a, b, c, d)$. + + *Step 2 -- Emit clauses.* Add three clauses for $a = x_1 and x_2$, two for $b = not x_3$, three for $c = b and x_4$, three for $d = a or c$, and two clauses for the output identity $r equiv d$. The CNF therefore has #cs_sat.target.instance.clauses.len() clauses. + + *Step 3 -- Verify a witness.* The fixture stores source config #cs_sat_sol.source_config.map(str).join(", "), meaning $(r, x_1, x_2, x_3, x_4) = (1, 1, 1, 0, 1)$. Extending with $(a, b, c, d) = (1, 1, 1, 1)$ gives the SAT witness #cs_sat_sol.target_config.map(str).join(", "), which satisfies every gate-definition clause and the two clauses enforcing $r equiv d$. + + *Multiplicity:* The fixture stores one canonical consistent assignment. Other satisfying assignments may exist whenever the circuit equations leave some named variables unconstrained. + ], +)[ + This linear-time Tseitin reduction @cook1971 rewrites each circuit assignment into CNF by keeping every named circuit variable as a SAT variable and introducing one auxiliary variable for each non-leaf subexpression after constant folding and binary balancing. The target therefore has one SAT variable per circuit variable plus one per introduced gate. +][ + _Construction._ Consider one circuit assignment $o_1, dots, o_t = e$. First simplify constant subexpressions inside $e$ and rewrite every n-ary AND, OR, and XOR node as a balanced binary tree. For each non-leaf subexpression $alpha$, introduce a fresh SAT variable $v_alpha$; named circuit variables are reused directly. Add the standard Tseitin clauses + $ + v_(not a) " iff " not a, \ + v_(a and b) " iff " a and b, \ + v_(a or b) " iff " a or b, \ + v_(a xor b) " iff " a xor b + $ + using the 2-clause NOT gadget, the 3-clause AND/OR gadgets, and the 4-clause XOR gadget. If the simplified right-hand side becomes a variable or auxiliary variable $z_e$, add $(overline(o_i) or z_e)$ and $(o_i or overline(z_e))$ for every output $o_i$. If it simplifies to a constant, add the unit clause $o_i$ or $overline(o_i)$ accordingly. Repeat this independently for every assignment in the circuit. + + _Correctness._ ($arrow.r.double$) Let $sigma$ be a satisfying CircuitSAT assignment. Set every auxiliary variable $v_alpha$ to the truth value of the corresponding subexpression $alpha$ under $sigma$. Each Tseitin gadget is then satisfied because its output variable matches the gate semantics, and every output-equivalence or unit clause holds because $sigma$ already makes each circuit assignment $o_1, dots, o_t = e$ true. Hence the CNF is satisfiable. ($arrow.l.double$) Let $tau$ satisfy the constructed CNF. Every Tseitin gadget forces its auxiliary variable to equal the truth value of its subexpression, so the root variable $z_e$ equals the value of $e$. The output-equivalence clauses therefore force every output $o_i$ to equal $e$, and unit clauses force the required constants. Restricting $tau$ to the named circuit variables yields an assignment satisfying every original circuit equation. + + _Solution extraction._ Return the values of the named circuit variables and discard the auxiliary Tseitin variables. +] + #let cs_sg = load-example("CircuitSAT", "SpinGlass") #let cs_sg_sol = cs_sg.solutions.at(0) #reduction-rule("CircuitSAT", "SpinGlass", @@ -13148,6 +13188,7 @@ The following table shows concrete variable overhead for example instances, take (source: "Satisfiability", target: "KColoring"), (source: "Satisfiability", target: "MinimumDominatingSet"), (source: "Satisfiability", target: "KSatisfiability"), + (source: "CircuitSAT", target: "Satisfiability"), (source: "CircuitSAT", target: "SpinGlass"), (source: "Factoring", target: "CircuitSAT"), (source: "MaximumSetPacking", target: "ILP"), diff --git a/src/rules/circuit_sat.rs b/src/rules/circuit_sat.rs new file mode 100644 index 00000000..b0cbb676 --- /dev/null +++ b/src/rules/circuit_sat.rs @@ -0,0 +1,370 @@ +//! Reduction from CircuitSAT to Satisfiability via Tseitin encoding. + +use crate::models::formula::{ + Assignment, BooleanExpr, BooleanOp, CNFClause, CircuitSAT, Satisfiability, +}; +use crate::reduction; +use crate::rules::traits::{ReduceTo, ReductionResult}; +use std::collections::HashMap; + +#[derive(Debug, Clone, PartialEq, Eq)] +enum NormalizedExpr { + Var(String), + Const(bool), + Not(Box), + And(Box, Box), + Or(Box, Box), + Xor(Box, Box), +} + +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +enum EncodedTerm { + Const(bool), + Var(i32), +} + +#[derive(Debug, Clone)] +struct TseitinEncoding { + num_vars: usize, + clauses: Vec, +} + +#[derive(Debug)] +struct TseitinEncoder { + source_var_ids: HashMap, + clauses: Vec, + next_var: i32, +} + +impl TseitinEncoder { + fn new(source: &CircuitSAT) -> Self { + let source_var_ids = source + .variable_names() + .iter() + .enumerate() + .map(|(index, name)| (name.clone(), index as i32 + 1)) + .collect(); + Self { + source_var_ids, + clauses: Vec::new(), + next_var: source.num_variables() as i32 + 1, + } + } + + fn encode_problem(mut self, source: &CircuitSAT) -> TseitinEncoding { + for assignment in &source.circuit().assignments { + self.encode_assignment(assignment); + } + + TseitinEncoding { + num_vars: (self.next_var - 1) as usize, + clauses: self.clauses, + } + } + + fn encode_assignment(&mut self, assignment: &Assignment) { + if assignment.outputs.is_empty() { + return; + } + + let root = self.encode_expr(&normalize_expr(&assignment.expr)); + match root { + EncodedTerm::Const(value) => { + let literal_sign = if value { 1 } else { -1 }; + for output in &assignment.outputs { + let output_var = self.source_var(output); + self.push_clause(vec![literal_sign * output_var]); + } + } + EncodedTerm::Var(root_var) => { + for output in &assignment.outputs { + let output_var = self.source_var(output); + self.push_equivalence(output_var, root_var); + } + } + } + } + + fn encode_expr(&mut self, expr: &NormalizedExpr) -> EncodedTerm { + match expr { + NormalizedExpr::Var(name) => EncodedTerm::Var(self.source_var(name)), + NormalizedExpr::Const(value) => EncodedTerm::Const(*value), + NormalizedExpr::Not(inner) => match self.encode_expr(inner) { + EncodedTerm::Const(value) => EncodedTerm::Const(!value), + EncodedTerm::Var(child_var) => { + let gate_var = self.allocate_auxiliary_var(); + self.push_clause(vec![-gate_var, -child_var]); + self.push_clause(vec![gate_var, child_var]); + EncodedTerm::Var(gate_var) + } + }, + NormalizedExpr::And(left, right) => { + let left_term = self.encode_expr(left); + let right_term = self.encode_expr(right); + let left_var = self.expect_var(left_term, "AND left input"); + let right_var = self.expect_var(right_term, "AND right input"); + let gate_var = self.allocate_auxiliary_var(); + self.push_clause(vec![-gate_var, left_var]); + self.push_clause(vec![-gate_var, right_var]); + self.push_clause(vec![gate_var, -left_var, -right_var]); + EncodedTerm::Var(gate_var) + } + NormalizedExpr::Or(left, right) => { + let left_term = self.encode_expr(left); + let right_term = self.encode_expr(right); + let left_var = self.expect_var(left_term, "OR left input"); + let right_var = self.expect_var(right_term, "OR right input"); + let gate_var = self.allocate_auxiliary_var(); + self.push_clause(vec![gate_var, -left_var]); + self.push_clause(vec![gate_var, -right_var]); + self.push_clause(vec![-gate_var, left_var, right_var]); + EncodedTerm::Var(gate_var) + } + NormalizedExpr::Xor(left, right) => { + let left_term = self.encode_expr(left); + let right_term = self.encode_expr(right); + let left_var = self.expect_var(left_term, "XOR left input"); + let right_var = self.expect_var(right_term, "XOR right input"); + let gate_var = self.allocate_auxiliary_var(); + self.push_clause(vec![-left_var, -right_var, -gate_var]); + self.push_clause(vec![left_var, right_var, -gate_var]); + self.push_clause(vec![left_var, -right_var, gate_var]); + self.push_clause(vec![-left_var, right_var, gate_var]); + EncodedTerm::Var(gate_var) + } + } + } + + fn expect_var(&self, term: EncodedTerm, context: &str) -> i32 { + match term { + EncodedTerm::Var(var) => var, + EncodedTerm::Const(_) => { + panic!("normalized Tseitin encoding produced a constant for {context}") + } + } + } + + fn source_var(&self, name: &str) -> i32 { + *self + .source_var_ids + .get(name) + .unwrap_or_else(|| panic!("CircuitSAT variable {name:?} missing from source ordering")) + } + + fn allocate_auxiliary_var(&mut self) -> i32 { + let var = self.next_var; + self.next_var += 1; + var + } + + fn push_equivalence(&mut self, left: i32, right: i32) { + self.push_clause(vec![-left, right]); + self.push_clause(vec![left, -right]); + } + + fn push_clause(&mut self, literals: Vec) { + self.clauses.push(CNFClause::new(literals)); + } +} + +fn make_and(left: NormalizedExpr, right: NormalizedExpr) -> NormalizedExpr { + NormalizedExpr::And(Box::new(left), Box::new(right)) +} + +fn make_or(left: NormalizedExpr, right: NormalizedExpr) -> NormalizedExpr { + NormalizedExpr::Or(Box::new(left), Box::new(right)) +} + +fn make_xor(left: NormalizedExpr, right: NormalizedExpr) -> NormalizedExpr { + NormalizedExpr::Xor(Box::new(left), Box::new(right)) +} + +fn build_balanced_expr( + mut items: Vec, + combine: fn(NormalizedExpr, NormalizedExpr) -> NormalizedExpr, +) -> NormalizedExpr { + if items.len() == 1 { + return items.pop().expect("single item exists"); + } + + let right = items.split_off(items.len() / 2); + combine( + build_balanced_expr(items, combine), + build_balanced_expr(right, combine), + ) +} + +fn normalize_expr(expr: &BooleanExpr) -> NormalizedExpr { + match &expr.op { + BooleanOp::Var(name) => NormalizedExpr::Var(name.clone()), + BooleanOp::Const(value) => NormalizedExpr::Const(*value), + BooleanOp::Not(inner) => match normalize_expr(inner) { + NormalizedExpr::Const(value) => NormalizedExpr::Const(!value), + NormalizedExpr::Not(grandchild) => *grandchild, + normalized => NormalizedExpr::Not(Box::new(normalized)), + }, + BooleanOp::And(args) => normalize_nary_gate(args, false, true, make_and), + BooleanOp::Or(args) => normalize_nary_gate(args, true, false, make_or), + BooleanOp::Xor(args) => { + let mut parity = false; + let mut normalized_args = Vec::new(); + + for arg in args { + match normalize_expr(arg) { + NormalizedExpr::Const(value) => parity ^= value, + normalized => normalized_args.push(normalized), + } + } + + match normalized_args.len() { + 0 => NormalizedExpr::Const(parity), + 1 => { + let base = normalized_args.pop().expect("single item exists"); + if parity { + NormalizedExpr::Not(Box::new(base)) + } else { + base + } + } + _ => { + let base = build_balanced_expr(normalized_args, make_xor); + if parity { + NormalizedExpr::Not(Box::new(base)) + } else { + base + } + } + } + } + } +} + +fn normalize_nary_gate( + args: &[BooleanExpr], + absorbing_value: bool, + identity_value: bool, + combine: fn(NormalizedExpr, NormalizedExpr) -> NormalizedExpr, +) -> NormalizedExpr { + let mut normalized_args = Vec::new(); + + for arg in args { + match normalize_expr(arg) { + NormalizedExpr::Const(value) if value == absorbing_value => { + return NormalizedExpr::Const(absorbing_value) + } + NormalizedExpr::Const(value) if value == identity_value => {} + normalized => normalized_args.push(normalized), + } + } + + match normalized_args.len() { + 0 => NormalizedExpr::Const(identity_value), + 1 => normalized_args.pop().expect("single item exists"), + _ => build_balanced_expr(normalized_args, combine), + } +} + +fn build_tseitin_encoding(source: &CircuitSAT) -> TseitinEncoding { + TseitinEncoder::new(source).encode_problem(source) +} + +impl CircuitSAT { + pub fn tseitin_num_vars(&self) -> usize { + build_tseitin_encoding(self).num_vars + } + + pub fn tseitin_num_clauses(&self) -> usize { + build_tseitin_encoding(self).clauses.len() + } +} + +/// Result of reducing CircuitSAT to SAT. +#[derive(Debug, Clone)] +pub struct ReductionCircuitSATToSAT { + target: Satisfiability, + source_var_count: usize, +} + +impl ReductionResult for ReductionCircuitSATToSAT { + type Source = CircuitSAT; + type Target = Satisfiability; + + fn target_problem(&self) -> &Self::Target { + &self.target + } + + fn extract_solution(&self, target_solution: &[usize]) -> Vec { + target_solution + .iter() + .take(self.source_var_count) + .copied() + .collect() + } +} + +#[reduction( + overhead = { + num_vars = "tseitin_num_vars", + num_clauses = "tseitin_num_clauses", + } +)] +impl ReduceTo for CircuitSAT { + type Result = ReductionCircuitSATToSAT; + + fn reduce_to(&self) -> Self::Result { + let encoding = build_tseitin_encoding(self); + ReductionCircuitSATToSAT { + target: Satisfiability::new(encoding.num_vars, encoding.clauses), + source_var_count: self.num_variables(), + } + } +} + +#[cfg(any(test, feature = "example-db"))] +fn issue_example_source() -> CircuitSAT { + use crate::models::formula::Circuit; + + CircuitSAT::new(Circuit::new(vec![Assignment::new( + vec!["r".to_string()], + BooleanExpr::or(vec![ + BooleanExpr::and(vec![BooleanExpr::var("x1"), BooleanExpr::var("x2")]), + BooleanExpr::and(vec![ + BooleanExpr::not(BooleanExpr::var("x3")), + BooleanExpr::var("x4"), + ]), + ]), + )])) +} + +#[cfg(feature = "example-db")] +pub(crate) fn canonical_rule_example_specs() -> Vec { + use crate::export::SolutionPair; + use crate::solvers::BruteForce; + + vec![crate::example_db::specs::RuleExampleSpec { + id: "circuitsat_to_satisfiability", + build: || { + let source = issue_example_source(); + let source_config = vec![1, 1, 1, 0, 1]; + let reduction = ReduceTo::::reduce_to(&source); + let target_config = BruteForce::new() + .find_all_witnesses(reduction.target_problem()) + .into_iter() + .find(|candidate| reduction.extract_solution(candidate) == source_config) + .expect("canonical CircuitSAT -> Satisfiability example must be satisfiable"); + + crate::example_db::specs::assemble_rule_example( + &source, + reduction.target_problem(), + vec![SolutionPair { + source_config, + target_config, + }], + ) + }, + }] +} + +#[cfg(test)] +#[path = "../unit_tests/rules/circuit_sat.rs"] +mod tests; diff --git a/src/rules/mod.rs b/src/rules/mod.rs index f0039b76..7c15977d 100644 --- a/src/rules/mod.rs +++ b/src/rules/mod.rs @@ -8,6 +8,7 @@ pub use cost::{ }; pub use registry::{EdgeCapabilities, ReductionEntry, ReductionOverhead}; +pub(crate) mod circuit_sat; pub(crate) mod circuit_spinglass; mod closestvectorproblem_qubo; pub(crate) mod coloring_qubo; @@ -352,6 +353,7 @@ pub use traits::{ #[cfg(feature = "example-db")] pub(crate) fn canonical_rule_example_specs() -> Vec { let mut specs = Vec::new(); + specs.extend(circuit_sat::canonical_rule_example_specs()); specs.extend(circuit_spinglass::canonical_rule_example_specs()); specs.extend(exactcoverby3sets_staffscheduling::canonical_rule_example_specs()); specs.extend(closestvectorproblem_qubo::canonical_rule_example_specs()); diff --git a/src/unit_tests/rules/circuit_sat.rs b/src/unit_tests/rules/circuit_sat.rs new file mode 100644 index 00000000..0f8cab80 --- /dev/null +++ b/src/unit_tests/rules/circuit_sat.rs @@ -0,0 +1,88 @@ +use super::*; +use crate::models::formula::{Assignment, BooleanExpr, Circuit, CircuitSAT, Satisfiability}; +use crate::rules::test_helpers::{ + assert_satisfaction_round_trip_from_satisfaction_target, solve_satisfaction_problem, +}; +use crate::rules::ReduceTo; +use crate::traits::Problem; + +fn contradiction_source() -> CircuitSAT { + CircuitSAT::new(Circuit::new(vec![Assignment::new( + vec!["x".to_string()], + BooleanExpr::not(BooleanExpr::var("x")), + )])) +} + +#[test] +fn test_circuitsat_to_satisfiability_closed_loop() { + let source = issue_example_source(); + let reduction = ReduceTo::::reduce_to(&source); + + assert_satisfaction_round_trip_from_satisfaction_target( + &source, + &reduction, + "CircuitSAT -> Satisfiability closed loop", + ); + + let target_solution = solve_satisfaction_problem(reduction.target_problem()) + .expect("issue example should yield a SAT witness"); + let extracted = reduction.extract_solution(&target_solution); + assert_eq!(extracted.len(), source.num_variables()); + assert!(source.evaluate(&extracted).0); +} + +#[test] +fn test_circuitsat_to_satisfiability_unsatisfiable() { + let source = contradiction_source(); + let reduction = ReduceTo::::reduce_to(&source); + + assert!( + solve_satisfaction_problem(reduction.target_problem()).is_none(), + "x = NOT x should stay unsatisfiable after Tseitin encoding" + ); +} + +#[test] +fn test_circuitsat_to_satisfiability_issue_example_counts() { + let source = issue_example_source(); + let reduction = ReduceTo::::reduce_to(&source); + + assert_eq!(source.tseitin_num_vars(), 9); + assert_eq!(source.tseitin_num_clauses(), 13); + assert_eq!(reduction.target_problem().num_vars(), 9); + assert_eq!(reduction.target_problem().num_clauses(), 13); +} + +#[test] +fn test_circuitsat_to_satisfiability_simplifies_constants() { + let source = CircuitSAT::new(Circuit::new(vec![Assignment::new( + vec!["r".to_string()], + BooleanExpr::and(vec![BooleanExpr::var("x"), BooleanExpr::constant(true)]), + )])); + let reduction = ReduceTo::::reduce_to(&source); + + assert_eq!(reduction.target_problem().num_vars(), 2); + assert_eq!(reduction.target_problem().num_clauses(), 2); + assert_satisfaction_round_trip_from_satisfaction_target( + &source, + &reduction, + "constant folding in CircuitSAT -> Satisfiability", + ); +} + +#[test] +fn test_circuitsat_to_satisfiability_handles_multiple_outputs() { + let source = CircuitSAT::new(Circuit::new(vec![Assignment::new( + vec!["a".to_string(), "b".to_string()], + BooleanExpr::xor(vec![BooleanExpr::var("x"), BooleanExpr::var("y")]), + )])); + let reduction = ReduceTo::::reduce_to(&source); + + assert_eq!(reduction.target_problem().num_vars(), 5); + assert_eq!(reduction.target_problem().num_clauses(), 8); + assert_satisfaction_round_trip_from_satisfaction_target( + &source, + &reduction, + "multiple outputs in CircuitSAT -> Satisfiability", + ); +} diff --git a/src/unit_tests/rules/graph.rs b/src/unit_tests/rules/graph.rs index b12d58a0..c82ddd48 100644 --- a/src/unit_tests/rules/graph.rs +++ b/src/unit_tests/rules/graph.rs @@ -1,6 +1,6 @@ use super::*; use crate::models::algebraic::{ILP, QUBO}; -use crate::models::formula::NAESatisfiability; +use crate::models::formula::{CircuitSAT, NAESatisfiability, Satisfiability}; use crate::models::graph::MaxCut; use crate::models::graph::{MaximumIndependentSet, MinimumVertexCover}; use crate::models::misc::Knapsack; @@ -1041,6 +1041,28 @@ fn test_directed_edge_pairs() { ); } +#[test] +fn test_circuitsat_to_satisfiability_direct_edge() { + let graph = ReductionGraph::new(); + let src = ReductionGraph::variant_to_map(&CircuitSAT::variant()); + let dst = ReductionGraph::variant_to_map(&Satisfiability::variant()); + + assert!(graph.has_direct_reduction_by_name("CircuitSAT", "Satisfiability")); + + let path = graph.find_cheapest_path( + "CircuitSAT", + &src, + "Satisfiability", + &dst, + &ProblemSize::new(vec![]), + &MinimizeSteps, + ); + assert!( + path.is_some(), + "CircuitSAT -> Satisfiability path should exist" + ); +} + #[test] fn test_variant_to_map() { let variant: &[(&str, &str)] = &[("graph", "SimpleGraph"), ("weight", "i32")]; From 63ffbb671955c69efb81aeb92029301d7604a2a1 Mon Sep 17 00:00:00 2001 From: GiggleLiu Date: Tue, 7 Apr 2026 17:00:40 +0800 Subject: [PATCH 02/13] Add Maximum2Satisfiability to MaxCut reduction --- docs/paper/reductions.typ | 51 +++++++ src/rules/maximum2satisfiability_maxcut.rs | 132 ++++++++++++++++++ src/rules/mod.rs | 2 + src/unit_tests/rules/graph.rs | 11 +- .../rules/maximum2satisfiability_maxcut.rs | 125 +++++++++++++++++ tests/suites/reductions.rs | 30 ++++ 6 files changed, 350 insertions(+), 1 deletion(-) create mode 100644 src/rules/maximum2satisfiability_maxcut.rs create mode 100644 src/unit_tests/rules/maximum2satisfiability_maxcut.rs diff --git a/docs/paper/reductions.typ b/docs/paper/reductions.typ index bfe70228..9e2643a9 100644 --- a/docs/paper/reductions.typ +++ b/docs/paper/reductions.typ @@ -4171,6 +4171,57 @@ A classical NP-complete problem from Garey and Johnson @garey1979[Ch.~3, p.~76], ] } +#let max2sat_mc = load-example("Maximum2Satisfiability", "MaxCut") +#let max2sat_mc_sol = max2sat_mc.solutions.at(0) +#reduction-rule("Maximum2Satisfiability", "MaxCut", + example: true, + example-caption: [$n = #max2sat_mc.source.instance.num_vars$ variables, $m = #max2sat_mc.source.instance.clauses.len()$ clauses, target has #max2sat_mc.target.instance.graph.num_vertices vertices and #max2sat_mc.target.instance.graph.edges.len() edges], + extra: [ + #pred-commands( + "pred create --example " + problem-spec(max2sat_mc.source) + " -o max2sat.json", + "pred reduce max2sat.json --to " + target-spec(max2sat_mc) + " -o bundle.json", + "pred solve bundle.json", + "pred evaluate max2sat.json --config " + max2sat_mc_sol.source_config.map(str).join(","), + ) + + *Step 1 -- Source instance.* The canonical source has $n = #max2sat_mc.source.instance.num_vars$ variables and #max2sat_mc.source.instance.clauses.len() two-literal clauses. The stored optimal assignment is $(#max2sat_mc_sol.source_config.map(str).join(", "))$, which satisfies all five clauses. + + *Step 2 -- Accumulate the cut weights.* Introduce the reference vertex $s = v_0$ and variable vertices $v_1, v_2, v_3$. After summing the per-clause contributions and deleting zero-weight edges, the target graph has the four signed edges $(s, v_2)$ with weight $-1$, $(s, v_3)$ with weight $-1$, $(v_1, v_2)$ with weight $2$, and $(v_2, v_3)$ with weight $-1$. + + *Step 3 -- Verify the witness.* The target witness $(#max2sat_mc_sol.target_config.map(str).join(", "))$ puts $v_2$ and $v_3$ on the same side as $s$ and $v_1$ on the opposite side, so extraction recovers $(#max2sat_mc_sol.source_config.map(str).join(", "))$. Only edge $(v_1, v_2)$ crosses, so the cut value is $2$ and the affine objective identity certifies optimality #sym.checkmark. + + *Multiplicity:* The fixture stores one canonical witness. Flipping every target bit yields the complementary cut partition but extracts the same source assignment because extraction compares each variable vertex to $s$. + ], +)[ + This $O(n + m)$ reduction @karp1972 @garey1979 builds a signed weighted graph with one reference vertex $s$ and one vertex per Boolean variable. Each 2-clause contributes two reference-variable terms and, when the clause uses two different variables, one variable-variable term. After doubling the affine clause identity to clear fractions, the target has $n + 1$ vertices and at most $n + m$ nonzero edges. +][ + _Construction._ Let $phi$ be a MAX-2-SAT instance on variables $x_1, dots, x_n$. Create one reference vertex $s = v_0$ and one vertex $v_i$ for each variable $x_i$. For a literal $ell$ over variable $x_i$, define $sigma(ell) = 1$ when $ell = x_i$ and $sigma(ell) = -1$ when $ell = not x_i$. For each clause $C = (ell_a or ell_b)$, add $-sigma(ell_a)$ to edge $(s, v_a)$ and $-sigma(ell_b)$ to edge $(s, v_b)$. If $a != b$, also add $sigma(ell_a) sigma(ell_b)$ to edge $(v_a, v_b)$. Repeated contributions accumulate; zero-weight edges are omitted. Interpret a cut by setting $x_i = 1$ exactly when $v_i$ lies on the same side of the cut as $s$. + + _Correctness._ Let $delta(u, v) in {0, 1}$ indicate whether vertices $u$ and $v$ lie on opposite sides of the cut. For each variable define $y_i = 1 - 2 delta(s, v_i)$, so $y_i = 1$ iff $x_i = 1$ and $y_i = -1$ iff $x_i = 0$. For clause $C = (ell_a or ell_b)$ with $sigma_a = sigma(ell_a)$ and $sigma_b = sigma(ell_b)$, its satisfaction indicator is + $ + S_C = (3 + sigma_a y_a + sigma_b y_b - sigma_a sigma_b y_a y_b) / 4. + $ + Since $y_i = 1 - 2 delta(s, v_i)$ and $y_a y_b = 1 - 2 delta(v_a, v_b)$, multiplying by $2$ yields + $ + 2 S_C + = K_C + - sigma_a delta(s, v_a) + - sigma_b delta(s, v_b) + + sigma_a sigma_b delta(v_a, v_b), + $ + where $K_C = (3 + sigma_a + sigma_b - sigma_a sigma_b) / 2$ is independent of the chosen cut. Summing over all clauses gives + $ + 2 S(phi, bold(x)) = C_0 + w(delta) + $ + for the constant $C_0 = sum_C K_C$. + + ($arrow.r.double$) Any truth assignment $bold(x)$ induces a cut by placing $v_i$ with $s$ iff $x_i = 1$. The displayed identity shows that an assignment satisfying $k$ clauses yields cut value $2k - C_0$. + + ($arrow.l.double$) Any cut $delta$ extracts a truth assignment by comparing each $v_i$ with $s$. If another assignment satisfied more clauses, its induced cut would have strictly larger cut value by the same identity, contradicting maximality. Therefore every maximum cut extracts to an optimal MAX-2-SAT assignment. + + _Solution extraction._ Return the source bit $x_i = 1$ iff $v_i$ and $s$ lie on the same side of the cut. Because this depends only on equality with $s$, globally swapping the two cut sides leaves the extracted assignment unchanged. +] + #let max2sat_ilp = load-example("Maximum2Satisfiability", "ILP") #let max2sat_ilp_sol = max2sat_ilp.solutions.at(0) #reduction-rule("Maximum2Satisfiability", "ILP", diff --git a/src/rules/maximum2satisfiability_maxcut.rs b/src/rules/maximum2satisfiability_maxcut.rs new file mode 100644 index 00000000..8b0e8d6c --- /dev/null +++ b/src/rules/maximum2satisfiability_maxcut.rs @@ -0,0 +1,132 @@ +//! Reduction from Maximum 2-Satisfiability (MAX-2-SAT) to MaxCut. +//! +//! The reduction uses one reference vertex `s` plus one vertex per Boolean +//! variable. For a partition of the target graph, a variable is interpreted as +//! true exactly when its vertex lies on the same side of the cut as `s`. +//! +//! For each 2-literal clause `(l_1 \/ l_2)`, we add the doubled affine form of +//! its satisfaction indicator: +//! `2 * sat(C) = K_C + w(s,a) cut(s,a) + w(s,b) cut(s,b) + w(a,b) cut(a,b)`. +//! Summing over clauses yields +//! `2 * satisfied(phi, x) = C_0 + cut_value(G_phi, partition)`, so every +//! optimal cut extracts to an optimal MAX-2-SAT assignment. + +use crate::models::formula::Maximum2Satisfiability; +use crate::models::graph::MaxCut; +use crate::reduction; +use crate::rules::traits::{ReduceTo, ReductionResult}; +use crate::topology::SimpleGraph; +use std::collections::BTreeMap; + +/// Result of reducing Maximum2Satisfiability to MaxCut. +#[derive(Debug, Clone)] +pub struct ReductionMaximum2SatisfiabilityToMaxCut { + target: MaxCut, + source_num_vars: usize, +} + +impl ReductionResult for ReductionMaximum2SatisfiabilityToMaxCut { + type Source = Maximum2Satisfiability; + type Target = MaxCut; + + fn target_problem(&self) -> &Self::Target { + &self.target + } + + fn extract_solution(&self, target_solution: &[usize]) -> Vec { + let reference_side = target_solution[0]; + (0..self.source_num_vars) + .map(|i| usize::from(target_solution[i + 1] == reference_side)) + .collect() + } +} + +fn add_edge_weight(weights: &mut BTreeMap<(usize, usize), i32>, u: usize, v: usize, delta: i32) { + let edge = if u < v { (u, v) } else { (v, u) }; + *weights.entry(edge).or_insert(0) += delta; +} + +fn literal_polarity(lit: i32) -> i32 { + if lit > 0 { + 1 + } else { + -1 + } +} + +#[reduction( + overhead = { + num_vertices = "num_vars + 1", + num_edges = "num_vars + num_clauses", + } +)] +impl ReduceTo> for Maximum2Satisfiability { + type Result = ReductionMaximum2SatisfiabilityToMaxCut; + + fn reduce_to(&self) -> Self::Result { + let mut accumulated = BTreeMap::new(); + + for clause in self.clauses() { + let literals = &clause.literals; + let (lit_a, lit_b) = (literals[0], literals[1]); + let var_a = lit_a.unsigned_abs() as usize; + let var_b = lit_b.unsigned_abs() as usize; + let sigma_a = literal_polarity(lit_a); + let sigma_b = literal_polarity(lit_b); + + add_edge_weight(&mut accumulated, 0, var_a, -sigma_a); + add_edge_weight(&mut accumulated, 0, var_b, -sigma_b); + if var_a != var_b { + add_edge_weight(&mut accumulated, var_a, var_b, sigma_a * sigma_b); + } + } + + let (edges, weights): (Vec<_>, Vec<_>) = accumulated + .into_iter() + .filter(|(_, weight)| *weight != 0) + .unzip(); + + let target = MaxCut::new(SimpleGraph::new(self.num_vars() + 1, edges), weights); + + ReductionMaximum2SatisfiabilityToMaxCut { + target, + source_num_vars: self.num_vars(), + } + } +} + +#[cfg(feature = "example-db")] +pub(crate) fn canonical_rule_example_specs() -> Vec { + use crate::export::SolutionPair; + use crate::models::formula::CNFClause; + + vec![crate::example_db::specs::RuleExampleSpec { + id: "maximum2satisfiability_to_maxcut", + build: || { + let source = Maximum2Satisfiability::new( + 3, + vec![ + CNFClause::new(vec![1, 2]), + CNFClause::new(vec![-1, 3]), + CNFClause::new(vec![2, -3]), + CNFClause::new(vec![-1, -2]), + CNFClause::new(vec![1, 3]), + ], + ); + crate::example_db::specs::rule_example_with_witness::<_, MaxCut>( + source, + SolutionPair { + // x1=F, x2=T, x3=T satisfies all five clauses. + source_config: vec![0, 1, 1], + // Vertex 0 is the reference vertex s. Variables are true + // exactly when they share s's side of the cut. + target_config: vec![0, 1, 0, 0], + }, + ) + }, + }] +} + +#[cfg(test)] +#[path = "../unit_tests/rules/maximum2satisfiability_maxcut.rs"] +mod tests; diff --git a/src/rules/mod.rs b/src/rules/mod.rs index 7c15977d..68331978 100644 --- a/src/rules/mod.rs +++ b/src/rules/mod.rs @@ -58,6 +58,7 @@ pub(crate) mod ksatisfiability_subsetsum; pub(crate) mod ksatisfiability_timetabledesign; pub(crate) mod longestcommonsubsequence_maximumindependentset; pub(crate) mod maxcut_minimumcutintoboundedsets; +pub(crate) mod maximum2satisfiability_maxcut; pub(crate) mod maximumclique_maximumindependentset; mod maximumindependentset_casts; mod maximumindependentset_gridgraph; @@ -398,6 +399,7 @@ pub(crate) fn canonical_rule_example_specs() -> Vec>()); } +#[test] +fn test_maximum2satisfiability_to_maxcut_reduction_registered() { + let graph = ReductionGraph::new(); + + assert!(graph.has_direct_reduction::>()); +} + #[test] fn test_nae_sat_to_partition_into_perfect_matchings_reduction_registered() { use crate::models::graph::PartitionIntoPerfectMatchings; diff --git a/src/unit_tests/rules/maximum2satisfiability_maxcut.rs b/src/unit_tests/rules/maximum2satisfiability_maxcut.rs new file mode 100644 index 00000000..7f7acee3 --- /dev/null +++ b/src/unit_tests/rules/maximum2satisfiability_maxcut.rs @@ -0,0 +1,125 @@ +use super::*; +use crate::models::formula::{CNFClause, Maximum2Satisfiability}; +use crate::models::graph::MaxCut; +use crate::rules::test_helpers::assert_optimization_round_trip_from_optimization_target; +use crate::topology::SimpleGraph; +use crate::traits::Problem; +use crate::types::Max; + +fn make_issue_instance() -> Maximum2Satisfiability { + Maximum2Satisfiability::new( + 3, + vec![ + CNFClause::new(vec![1, 2]), + CNFClause::new(vec![-1, 3]), + CNFClause::new(vec![2, -3]), + CNFClause::new(vec![-1, -2]), + CNFClause::new(vec![1, 3]), + ], + ) +} + +#[test] +fn test_maximum2satisfiability_to_maxcut_closed_loop() { + let source = make_issue_instance(); + let reduction = ReduceTo::>::reduce_to(&source); + + assert_optimization_round_trip_from_optimization_target( + &source, + &reduction, + "Maximum2Satisfiability -> MaxCut closed loop", + ); +} + +#[test] +fn test_maximum2satisfiability_to_maxcut_structure() { + let source = make_issue_instance(); + let reduction = ReduceTo::>::reduce_to(&source); + let target = reduction.target_problem(); + + assert_eq!(target.num_vertices(), 4); + assert_eq!(target.num_edges(), 4); + assert_eq!(target.edge_weight(0, 1), None); + assert_eq!(target.edge_weight(0, 2), Some(&-1)); + assert_eq!(target.edge_weight(0, 3), Some(&-1)); + assert_eq!(target.edge_weight(1, 2), Some(&2)); + assert_eq!(target.edge_weight(1, 3), None); + assert_eq!(target.edge_weight(2, 3), Some(&-1)); + + let source_solution = vec![0, 1, 1]; + let target_solution = vec![0, 1, 0, 0]; + assert_eq!(source.evaluate(&source_solution), Max(Some(5))); + assert_eq!(target.evaluate(&target_solution), Max(Some(2))); +} + +#[test] +fn test_maximum2satisfiability_to_maxcut_extract_solution_uses_reference_vertex() { + let source = make_issue_instance(); + let reduction = ReduceTo::>::reduce_to(&source); + + assert_eq!(reduction.extract_solution(&[0, 1, 0, 0]), vec![0, 1, 1]); + assert_eq!(reduction.extract_solution(&[1, 0, 1, 1]), vec![0, 1, 1]); + assert_eq!( + source.evaluate(&reduction.extract_solution(&[1, 0, 1, 1])), + Max(Some(5)) + ); +} + +#[test] +fn test_maximum2satisfiability_to_maxcut_handles_duplicate_and_tautological_clauses() { + let source = Maximum2Satisfiability::new( + 2, + vec![ + CNFClause::new(vec![1, 1]), + CNFClause::new(vec![1, -1]), + CNFClause::new(vec![-2, -2]), + ], + ); + let reduction = ReduceTo::>::reduce_to(&source); + let target = reduction.target_problem(); + + assert_eq!(target.num_vertices(), 3); + assert_eq!(target.num_edges(), 2); + assert_eq!(target.edge_weight(0, 1), Some(&-2)); + assert_eq!(target.edge_weight(0, 2), Some(&2)); + assert_eq!(target.edge_weight(1, 2), None); + + assert_optimization_round_trip_from_optimization_target( + &source, + &reduction, + "Maximum2Satisfiability -> MaxCut duplicate clauses", + ); +} + +#[cfg(feature = "example-db")] +#[test] +fn test_maximum2satisfiability_to_maxcut_canonical_example_spec() { + let spec = canonical_rule_example_specs() + .into_iter() + .find(|spec| spec.id == "maximum2satisfiability_to_maxcut") + .expect("missing canonical Maximum2Satisfiability -> MaxCut example spec"); + let example = (spec.build)(); + + assert_eq!(example.source.problem, "Maximum2Satisfiability"); + assert_eq!(example.target.problem, "MaxCut"); + assert_eq!(example.source.instance["num_vars"], 3); + assert_eq!(example.target.instance["graph"]["num_vertices"], 4); + assert_eq!( + example.target.instance["graph"]["edges"] + .as_array() + .unwrap() + .len(), + 4 + ); + assert_eq!( + example.target.instance["edge_weights"], + serde_json::json!([-1, -1, 2, -1]) + ); + assert_eq!( + example.solutions, + vec![crate::export::SolutionPair { + source_config: vec![0, 1, 1], + target_config: vec![0, 1, 0, 0], + }] + ); +} diff --git a/tests/suites/reductions.rs b/tests/suites/reductions.rs index 5ea6e9ec..453f7baf 100644 --- a/tests/suites/reductions.rs +++ b/tests/suites/reductions.rs @@ -295,6 +295,36 @@ mod sg_qubo_reductions { } } +/// Tests for Maximum2Satisfiability -> MaxCut reductions. +mod max2sat_maxcut_reductions { + use super::*; + + #[test] + fn test_maximum2satisfiability_to_maxcut_closed_loop() { + let source = Maximum2Satisfiability::new( + 3, + vec![ + CNFClause::new(vec![1, 2]), + CNFClause::new(vec![-1, 3]), + CNFClause::new(vec![2, -3]), + CNFClause::new(vec![-1, -2]), + CNFClause::new(vec![1, 3]), + ], + ); + + let reduction = ReduceTo::>::reduce_to(&source); + let target = reduction.target_problem(); + + assert_eq!(target.graph().num_vertices(), 4); + + let solver = BruteForce::new(); + let target_solutions = solver.find_all_witnesses(target); + let extracted = reduction.extract_solution(&target_solutions[0]); + + assert_eq!(source.evaluate(&extracted), Max(Some(5))); + } +} + /// Tests for SpinGlass <-> MaxCut reductions. mod sg_maxcut_reductions { use super::*; From cf219fcaa56c56ceee7a5a98b2ee61a1c6811abc Mon Sep 17 00:00:00 2001 From: GiggleLiu Date: Tue, 7 Apr 2026 17:22:46 +0800 Subject: [PATCH 03/13] feat: add satisfiability to maximum2satisfiability reduction --- docs/paper/reductions.typ | 66 ++++++++ src/rules/mod.rs | 2 + .../satisfiability_maximum2satisfiability.rs | 150 ++++++++++++++++++ .../satisfiability_maximum2satisfiability.rs | 72 +++++++++ 4 files changed, 290 insertions(+) create mode 100644 src/rules/satisfiability_maximum2satisfiability.rs create mode 100644 src/unit_tests/rules/satisfiability_maximum2satisfiability.rs diff --git a/docs/paper/reductions.typ b/docs/paper/reductions.typ index 9e2643a9..b6f4775d 100644 --- a/docs/paper/reductions.typ +++ b/docs/paper/reductions.typ @@ -10275,6 +10275,71 @@ where $P$ is a penalty weight large enough that any constraint violation costs m _Solution extraction._ Discard auxiliary variables; return original variable assignments. ] +#let sat_max2sat = load-example("Satisfiability", "Maximum2Satisfiability") +#let sat_max2sat_sol = sat_max2sat.solutions.at(0) +#reduction-rule("Satisfiability", "Maximum2Satisfiability", + example: true, + example-caption: [3-variable 2-clause SAT to MAX-2-SAT], + extra: [ + #pred-commands( + "pred create --example " + problem-spec(sat_max2sat.source) + " -o sat.json", + "pred reduce sat.json --to " + target-spec(sat_max2sat) + " -o bundle.json", + "pred solve bundle.json", + "pred evaluate sat.json --config " + sat_max2sat_sol.source_config.map(str).join(","), + ) + *Step 1 -- Source instance.* The canonical SAT formula has $n = #sat_max2sat.source.instance.num_vars$ variables and $m = #sat-num-clauses(sat_max2sat.source.instance)$ clauses: + $ + C_1 = (x_1 or overline(x_2) or x_3), quad + C_2 = (overline(x_1) or x_2). + $ + The stored satisfying assignment is $(x_1, x_2, x_3) = (#sat_max2sat_sol.source_config.map(str).join(", "))$. + + *Step 2 -- Normalize to 3-CNF.* Clause $C_1$ already has width $3$. Clause $C_2$ introduces one auxiliary variable $y_1$ and becomes + $ + (overline(x_1) or x_2 or y_1) and + (overline(x_1) or x_2 or overline(y_1)). + $ + The normalized formula therefore has $4$ variables and $3$ clauses. + + *Step 3 -- Build the MAX-2-SAT gadgets.* Introduce one gadget variable per normalized clause, so the target has $#sat_max2sat.target.instance.num_vars$ variables and #sat_max2sat.target.instance.clauses.len() clauses. The stored witness is $(x_1, x_2, x_3, y_1, w_1, w_2, w_3) = (#sat_max2sat_sol.target_config.map(str).join(", "))$. With $(y_1, w_1, w_2, w_3) = (0, 1, 0, 1)$, each of the three gadgets satisfies exactly $7$ clauses, so the target objective reaches $21 = 7 times 3$ #sym.checkmark. + + *Multiplicity:* The fixture stores one canonical optimum. Auxiliary variables such as $y_1$ can vary across optimal witnesses, but truncating any optimal target assignment to the first $3$ coordinates still yields a satisfying assignment of the original SAT formula. + ], +)[ + This reduction composes a satisfiability-preserving normalization to 3-CNF with the Garey--Johnson--Stockmeyer MAX-2-SAT gadget @garey1976 @garey1979. Each normalized 3-clause contributes a 10-clause MAX-2-SAT block with a one-clause gap between the satisfied and unsatisfied cases. For a SAT instance with $n$ variables, $m$ clauses, and total literal count $L = sum_j |C_j|$, the implementation produces at most $n + 2L + 4m$ target variables and $10 (L + 3m)$ target clauses. +][ + _Construction._ Let $phi = and.big_(j=1)^m C_j$ be a CNF formula on variables $x_1, dots, x_n$. + + _Step 1: normalize each clause to width 3._ Replace every clause independently: + - if $C = ()$, introduce a fresh variable $y$ and use $(y or y or y) and (overline(y) or overline(y) or overline(y))$; + - if $C = (ell_1)$, introduce fresh $y, z$ and use the four clauses $(ell_1 or y or z)$, $(ell_1 or y or overline(z))$, $(ell_1 or overline(y) or z)$, $(ell_1 or overline(y) or overline(z))$; + - if $C = (ell_1 or ell_2)$, introduce fresh $y$ and use $(ell_1 or ell_2 or y) and (ell_1 or ell_2 or overline(y))$; + - if $C$ already has width $3$, keep it unchanged; + - if $C = (ell_1 or dots or ell_k)$ with $k > 3$, introduce fresh $y_1, dots, y_(k-3)$ and replace $C$ by + $ + (ell_1 or ell_2 or y_1) and + (overline(y_1) or ell_3 or y_2) and dots and + (overline(y_(k-3)) or ell_(k-1) or ell_k). + $ + Let the resulting 3-CNF formula be $psi = and.big_(t=1)^(m') D_t$. + + _Step 2: convert each 3-clause to MAX-2-SAT._ For every normalized clause $D_t = (a_t or b_t or c_t)$, introduce a fresh variable $w_t$ and add the ten 2-clauses + $ + (a_t or a_t), (b_t or b_t), (c_t or c_t), (w_t or w_t), \ + (overline(a_t) or overline(b_t)), (overline(b_t) or overline(c_t)), (overline(a_t) or overline(c_t)), \ + (a_t or overline(w_t)), (b_t or overline(w_t)), (c_t or overline(w_t)). + $ + The repeated literals encode unit clauses inside the exact-2-literal MAX-2-SAT model. + + _Correctness._ For one gadget corresponding to $D_t$, exhaustive case analysis shows that the best choice of $w_t$ satisfies exactly $7$ of the ten clauses when $D_t$ is true and at most $6$ when $D_t$ is false. Therefore, for every assignment to the normalized variables, + $ + "MAX2SAT"("target") = 6 m' + \#\{t : D_t " is true"\}. + $ + ($arrow.r.double$) If $phi$ is satisfiable, then the normalized formula $psi$ is satisfiable by Step 1. Every normalized clause is true, so each gadget attains value $7$ and the target optimum is $7 m'$. ($arrow.l.double$) If the target optimum is $7 m'$, then every gadget must contribute $7$, so every normalized clause $D_t$ is true. Hence $psi$ is satisfiable, and the normalization in Step 1 implies that the restriction to the original variables satisfies $phi$. If $phi$ is unsatisfiable, then $psi$ is unsatisfiable, so every assignment leaves at least one normalized clause false and the target optimum is strictly less than $7 m'$. + + _Solution extraction._ Discard all auxiliary normalization variables and all gadget variables $w_t$; return only the first $n$ Boolean variables $(x_1, dots, x_n)$. +] + #let sat_cs = load-example("Satisfiability", "CircuitSAT") #let sat_cs_sol = sat_cs.solutions.at(0) #reduction-rule("Satisfiability", "CircuitSAT", @@ -13236,6 +13301,7 @@ The following table shows concrete variable overhead for example instances, take ), (source: "ILP", target: "QUBO"), (source: "Satisfiability", target: "MaximumIndependentSet"), + (source: "Satisfiability", target: "Maximum2Satisfiability"), (source: "Satisfiability", target: "KColoring"), (source: "Satisfiability", target: "MinimumDominatingSet"), (source: "Satisfiability", target: "KSatisfiability"), diff --git a/src/rules/mod.rs b/src/rules/mod.rs index 68331978..2230d2f7 100644 --- a/src/rules/mod.rs +++ b/src/rules/mod.rs @@ -99,6 +99,7 @@ pub(crate) mod sat_ksat; pub(crate) mod sat_maximumindependentset; pub(crate) mod sat_minimumdominatingset; pub(crate) mod satisfiability_integralflowhomologousarcs; +pub(crate) mod satisfiability_maximum2satisfiability; pub(crate) mod satisfiability_naesatisfiability; pub(crate) mod satisfiability_nontautology; pub(crate) mod setsplitting_betweenness; @@ -423,6 +424,7 @@ pub(crate) fn canonical_rule_example_specs() -> Vec &Self::Target { + &self.target + } + + fn extract_solution(&self, target_solution: &[usize]) -> Vec { + target_solution[..self.source_num_vars].to_vec() + } +} + +fn add_normalized_clause(clause: &CNFClause, next_var: &mut i32, normalized: &mut Vec) { + match clause.len() { + 0 => { + let y = *next_var; + *next_var += 1; + normalized.push(CNFClause::new(vec![y, y, y])); + normalized.push(CNFClause::new(vec![-y, -y, -y])); + } + 1 => { + let l1 = clause.literals[0]; + let y = *next_var; + let z = *next_var + 1; + *next_var += 2; + normalized.push(CNFClause::new(vec![l1, y, z])); + normalized.push(CNFClause::new(vec![l1, y, -z])); + normalized.push(CNFClause::new(vec![l1, -y, z])); + normalized.push(CNFClause::new(vec![l1, -y, -z])); + } + 2 => { + let l1 = clause.literals[0]; + let l2 = clause.literals[1]; + let y = *next_var; + *next_var += 1; + normalized.push(CNFClause::new(vec![l1, l2, y])); + normalized.push(CNFClause::new(vec![l1, l2, -y])); + } + 3 => normalized.push(clause.clone()), + k => { + let literals = &clause.literals; + let y_vars: Vec = (*next_var..*next_var + (k as i32 - 3)).collect(); + *next_var += k as i32 - 3; + + normalized.push(CNFClause::new(vec![literals[0], literals[1], y_vars[0]])); + for i in 1..k - 3 { + normalized.push(CNFClause::new(vec![ + -y_vars[i - 1], + literals[i + 1], + y_vars[i], + ])); + } + normalized.push(CNFClause::new(vec![ + -y_vars[y_vars.len() - 1], + literals[k - 2], + literals[k - 1], + ])); + } + } +} + +fn add_gjs_gadget(clause: &CNFClause, w: i32, target_clauses: &mut Vec) { + let a = clause.literals[0]; + let b = clause.literals[1]; + let c = clause.literals[2]; + + target_clauses.push(CNFClause::new(vec![a, a])); + target_clauses.push(CNFClause::new(vec![b, b])); + target_clauses.push(CNFClause::new(vec![c, c])); + target_clauses.push(CNFClause::new(vec![w, w])); + target_clauses.push(CNFClause::new(vec![-a, -b])); + target_clauses.push(CNFClause::new(vec![-b, -c])); + target_clauses.push(CNFClause::new(vec![-a, -c])); + target_clauses.push(CNFClause::new(vec![a, -w])); + target_clauses.push(CNFClause::new(vec![b, -w])); + target_clauses.push(CNFClause::new(vec![c, -w])); +} + +#[reduction( + overhead = { + num_vars = "num_vars + 2 * num_literals + 4 * num_clauses", + num_clauses = "10 * (num_literals + 3 * num_clauses)", + } +)] +impl ReduceTo for Satisfiability { + type Result = ReductionSatisfiabilityToMaximum2Satisfiability; + + fn reduce_to(&self) -> Self::Result { + let mut normalized = Vec::new(); + let mut next_var = self.num_vars() as i32 + 1; + + for clause in self.clauses() { + add_normalized_clause(clause, &mut next_var, &mut normalized); + } + + let mut target_clauses = Vec::with_capacity(normalized.len() * 10); + for clause in &normalized { + let w = next_var; + next_var += 1; + add_gjs_gadget(clause, w, &mut target_clauses); + } + + let target = Maximum2Satisfiability::new((next_var - 1) as usize, target_clauses); + + ReductionSatisfiabilityToMaximum2Satisfiability { + target, + source_num_vars: self.num_vars(), + } + } +} + +#[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_maximum2satisfiability", + build: || { + let source = Satisfiability::new( + 3, + vec![CNFClause::new(vec![1, -2, 3]), CNFClause::new(vec![-1, 2])], + ); + crate::example_db::specs::rule_example_with_witness::<_, Maximum2Satisfiability>( + source, + SolutionPair { + source_config: vec![1, 1, 1], + target_config: vec![1, 1, 1, 0, 1, 0, 1], + }, + ) + }, + }] +} + +#[cfg(test)] +#[path = "../unit_tests/rules/satisfiability_maximum2satisfiability.rs"] +mod tests; diff --git a/src/unit_tests/rules/satisfiability_maximum2satisfiability.rs b/src/unit_tests/rules/satisfiability_maximum2satisfiability.rs new file mode 100644 index 00000000..502874a6 --- /dev/null +++ b/src/unit_tests/rules/satisfiability_maximum2satisfiability.rs @@ -0,0 +1,72 @@ +use super::*; +use crate::models::formula::{CNFClause, Maximum2Satisfiability, Satisfiability}; +use crate::rules::test_helpers::{ + assert_satisfaction_round_trip_from_optimization_target, solve_optimization_problem, +}; +use crate::rules::traits::ReduceTo; +use crate::solvers::{BruteForce, Solver}; +use crate::traits::Problem; + +#[test] +fn test_satisfiability_to_maximum2satisfiability_structure() { + let source = Satisfiability::new( + 3, + vec![CNFClause::new(vec![1, -2, 3]), CNFClause::new(vec![-1, 2])], + ); + + let reduction = ReduceTo::::reduce_to(&source); + let target = reduction.target_problem(); + + assert_eq!(target.num_vars(), 7); + assert_eq!(target.num_clauses(), 30); + assert_eq!(target.clauses()[0].literals, vec![1, 1]); + assert_eq!(target.clauses()[4].literals, vec![-1, 2]); + assert_eq!(target.clauses()[10].literals, vec![-1, -1]); + assert_eq!(target.clauses()[20].literals, vec![-1, -1]); +} + +#[test] +fn test_satisfiability_to_maximum2satisfiability_closed_loop() { + let source = Satisfiability::new( + 3, + vec![CNFClause::new(vec![1, -2, 3]), CNFClause::new(vec![-1, 2])], + ); + + let reduction = ReduceTo::::reduce_to(&source); + let target = reduction.target_problem(); + + assert_satisfaction_round_trip_from_optimization_target( + &source, + &reduction, + "SAT -> Maximum2Satisfiability closed loop", + ); + + assert_eq!(BruteForce::new().solve(target).0, Some(21)); +} + +#[test] +fn test_satisfiability_to_maximum2satisfiability_unsatisfiable_gap() { + let source = Satisfiability::new(1, vec![CNFClause::new(vec![1]), CNFClause::new(vec![-1])]); + + let reduction = ReduceTo::::reduce_to(&source); + let target = reduction.target_problem(); + + assert_eq!(BruteForce::new().solve(target).0, Some(55)); + + let target_solution = + solve_optimization_problem(target).expect("MAX-2-SAT target should always have a witness"); + let extracted = reduction.extract_solution(&target_solution); + assert!(!source.evaluate(&extracted).0); +} + +#[test] +fn test_satisfiability_to_maximum2satisfiability_empty_clause() { + let source = Satisfiability::new(1, vec![CNFClause::new(vec![])]); + + let reduction = ReduceTo::::reduce_to(&source); + let target = reduction.target_problem(); + + assert_eq!(target.num_vars(), 4); + assert_eq!(target.num_clauses(), 20); + assert_eq!(BruteForce::new().solve(target).0, Some(13)); +} From efd6afec925270624513059796b1b3def8c53a4a Mon Sep 17 00:00:00 2001 From: GiggleLiu Date: Tue, 7 Apr 2026 17:44:32 +0800 Subject: [PATCH 04/13] feat: add KSAT to decision MVC reduction --- docs/paper/reductions.typ | 36 ++++++++ ...tisfiability_decisionminimumvertexcover.rs | 92 +++++++++++++++++++ src/rules/mod.rs | 2 + src/unit_tests/reduction_graph.rs | 19 ++++ ...tisfiability_decisionminimumvertexcover.rs | 79 ++++++++++++++++ 5 files changed, 228 insertions(+) create mode 100644 src/rules/ksatisfiability_decisionminimumvertexcover.rs create mode 100644 src/unit_tests/rules/ksatisfiability_decisionminimumvertexcover.rs diff --git a/docs/paper/reductions.typ b/docs/paper/reductions.typ index b6f4775d..db83a2d5 100644 --- a/docs/paper/reductions.typ +++ b/docs/paper/reductions.typ @@ -13674,6 +13674,42 @@ The following table shows concrete variable overhead for example instances, take ] +#let ksat_dmvc = load-example("KSatisfiability", "DecisionMinimumVertexCover") +#let ksat_dmvc_sol = ksat_dmvc.solutions.at(0) +#reduction-rule("KSatisfiability", "DecisionMinimumVertexCover", + example: true, + example-caption: [3-SAT with $n = #ksat_dmvc.source.instance.num_vars$ variables, $m = #sat-num-clauses(ksat_dmvc.source.instance)$ clauses reduced to Decision Minimum Vertex Cover with bound $k = #ksat_dmvc.target.instance.bound$], + extra: [ + #pred-commands( + "pred create --example " + problem-spec(ksat_dmvc.source) + " -o ksat.json", + "pred reduce ksat.json --to " + target-spec(ksat_dmvc) + " -o bundle.json", + "pred solve bundle.json", + "pred evaluate ksat.json --config " + ksat_dmvc_sol.source_config.map(str).join(","), + ) + + *Step 1 -- Source instance.* The 3-SAT formula has $n = #ksat_dmvc.source.instance.num_vars$ variables and $m = #sat-num-clauses(ksat_dmvc.source.instance)$ clauses: #{ksat_dmvc.source.instance.clauses.enumerate().map(((j, c)) => { + let lits = c.literals.map(l => if l > 0 { $x_#l$ } else { $overline(x)_#calc.abs(l)$ }) + [$c_#j = (#lits.join($or$))$] + }).join(", ")}. A satisfying assignment is $(#ksat_dmvc_sol.source_config.map(str).join(", "))$. + + *Step 2 -- Build the vertex-cover graph.* Create one truth-setting edge $(u_i, overline(u)_i)$ per variable and one clause triangle per clause. Each triangle vertex is connected to the literal vertex of its clause position by a communication edge. The resulting graph has $|V| = 2n + 3m = #graph-num-vertices(ksat_dmvc.target.instance)$ vertices and $|E| = n + 6m = #graph-num-edges(ksat_dmvc.target.instance)$ edges. + + *Step 3 -- Add the decision threshold.* Wrap the constructed Minimum Vertex Cover instance in the decision predicate with bound $k = n + 2m = #ksat_dmvc.target.instance.bound$. For this example, $k = 3 + 2 dot 2 = 7$. + + *Step 4 -- Verify a witness.* The target configuration $(#ksat_dmvc_sol.target_config.map(str).join(", "))$ selects #ksat_dmvc_sol.target_config.filter(x => x == 1).len() vertices, so it meets the bound exactly. Each truth-setting edge has one selected endpoint #sym.checkmark. Each clause triangle has two selected vertices #sym.checkmark. Each communication edge is covered either by its literal endpoint or by its triangle endpoint #sym.checkmark. Extracting the truth-setting choices returns $(#ksat_dmvc_sol.source_config.map(str).join(", "))$, which satisfies every clause #sym.checkmark + + *Multiplicity:* The fixture stores one canonical decision witness. Different satisfying assignments may yield different size-$k$ covers of the same graph. + ], +)[ + Use the classical 3-SAT to Vertex Cover gadget construction, then ask whether the resulting graph has a vertex cover of size at most $k = n + 2m$ @garey1979. +][ + _Construction._ Given 3-CNF $phi$ with $n$ variables and $m$ clauses, build the graph $G = (V, E)$ used in the classical 3-SAT $arrow.r$ Minimum Vertex Cover reduction: for each variable $x_i$, add literal vertices $u_i$ and $overline(u)_i$ with one truth-setting edge between them; for each clause $c_j$, add triangle vertices $t^j_0, t^j_1, t^j_2$; for each literal position $(j, r)$, add a communication edge from $t^j_r$ to the literal vertex representing that literal. Assign unit weight to every vertex and set the decision threshold to $k = n + 2m$. + + _Correctness._ ($arrow.r.double$) If $phi$ is satisfiable, choose one literal vertex per variable according to a satisfying assignment and choose two triangle vertices per clause, omitting a vertex whose literal is true. This gives a cover of size $n + 2m$, so the decision instance is yes. ($arrow.l.double$) If the decision instance is yes, any cover of size at most $n + 2m$ must use exactly one literal vertex per variable edge and exactly two vertices per clause triangle. The omitted triangle vertex in each clause has its communication edge covered only by a selected literal vertex, so the corresponding literal is true. These selected literal vertices define a satisfying assignment for $phi$. + + _Solution extraction._ For each variable $x_i$, inspect the truth-setting pair. Set $x_i = 1$ when the cover contains $u_i$, and set $x_i = 0$ otherwise. +] + #let ksat_mvc = load-example("KSatisfiability", "MinimumVertexCover") #let ksat_mvc_sol = ksat_mvc.solutions.at(0) #reduction-rule("KSatisfiability", "MinimumVertexCover", diff --git a/src/rules/ksatisfiability_decisionminimumvertexcover.rs b/src/rules/ksatisfiability_decisionminimumvertexcover.rs new file mode 100644 index 00000000..37d22483 --- /dev/null +++ b/src/rules/ksatisfiability_decisionminimumvertexcover.rs @@ -0,0 +1,92 @@ +//! Reduction from KSatisfiability (3-SAT) to Decision Minimum Vertex Cover. +//! +//! This wraps the classical Garey & Johnson Theorem 3.3 construction in the +//! `Decision>` wrapper, with threshold +//! `k = n + 2m` for `n` variables and `m` clauses. + +use crate::models::decision::Decision; +use crate::models::formula::KSatisfiability; +use crate::models::graph::MinimumVertexCover; +use crate::reduction; +use crate::rules::ksatisfiability_minimumvertexcover::Reduction3SATToMVC; +use crate::rules::traits::{ReduceTo, ReductionResult}; +use crate::topology::SimpleGraph; +use crate::variant::K3; + +/// Result of reducing KSatisfiability to Decision>. +#[derive(Debug, Clone)] +pub struct Reduction3SATToDecisionMVC { + target: Decision>, + base_reduction: Reduction3SATToMVC, +} + +impl ReductionResult for Reduction3SATToDecisionMVC { + type Source = KSatisfiability; + type Target = Decision>; + + fn target_problem(&self) -> &Self::Target { + &self.target + } + + fn extract_solution(&self, target_solution: &[usize]) -> Vec { + self.base_reduction.extract_solution(target_solution) + } +} + +#[reduction( + overhead = { + num_vertices = "2 * num_vars + 3 * num_clauses", + num_edges = "num_vars + 6 * num_clauses", + k = "num_vars + 2 * num_clauses", + } +)] +impl ReduceTo>> for KSatisfiability { + type Result = Reduction3SATToDecisionMVC; + + fn reduce_to(&self) -> Self::Result { + let base_reduction = as ReduceTo< + MinimumVertexCover, + >>::reduce_to(self); + let bound = i32::try_from(self.num_vars() + 2 * self.num_clauses()) + .expect("decision minimum vertex cover bound must fit in i32"); + let target = Decision::new(base_reduction.target_problem().clone(), bound); + + Reduction3SATToDecisionMVC { + target, + base_reduction, + } + } +} + +#[cfg(feature = "example-db")] +pub(crate) fn canonical_rule_example_specs() -> Vec { + use crate::export::SolutionPair; + use crate::models::formula::CNFClause; + + vec![crate::example_db::specs::RuleExampleSpec { + id: "ksatisfiability_to_decisionminimumvertexcover", + build: || { + let source = KSatisfiability::::new( + 3, + vec![ + CNFClause::new(vec![1, 2, 3]), + CNFClause::new(vec![-1, -2, 3]), + ], + ); + crate::example_db::specs::rule_example_with_witness::< + _, + Decision>, + >( + source, + SolutionPair { + source_config: vec![0, 0, 1], + target_config: vec![0, 1, 0, 1, 1, 0, 1, 1, 0, 1, 1, 0], + }, + ) + }, + }] +} + +#[cfg(test)] +#[path = "../unit_tests/rules/ksatisfiability_decisionminimumvertexcover.rs"] +mod tests; diff --git a/src/rules/mod.rs b/src/rules/mod.rs index 2230d2f7..473354ae 100644 --- a/src/rules/mod.rs +++ b/src/rules/mod.rs @@ -46,6 +46,7 @@ mod knapsack_qubo; pub(crate) mod ksatisfiability_acyclicpartition; mod ksatisfiability_casts; pub(crate) mod ksatisfiability_cyclicordering; +pub(crate) mod ksatisfiability_decisionminimumvertexcover; pub(crate) mod ksatisfiability_kclique; pub(crate) mod ksatisfiability_kernel; pub(crate) mod ksatisfiability_minimumvertexcover; @@ -390,6 +391,7 @@ pub(crate) fn canonical_rule_example_specs() -> Vec, + Decision>, + >(ReductionMode::Witness)); + assert!(!graph.has_direct_reduction_mode::< + KSatisfiability, + Decision>, + >(ReductionMode::Aggregate)); + assert!(!graph.has_direct_reduction_mode::< + KSatisfiability, + Decision>, + >(ReductionMode::Turing)); +} diff --git a/src/unit_tests/rules/ksatisfiability_decisionminimumvertexcover.rs b/src/unit_tests/rules/ksatisfiability_decisionminimumvertexcover.rs new file mode 100644 index 00000000..70a1e5b9 --- /dev/null +++ b/src/unit_tests/rules/ksatisfiability_decisionminimumvertexcover.rs @@ -0,0 +1,79 @@ +use super::*; +use crate::models::decision::Decision; +use crate::models::formula::CNFClause; +use crate::models::graph::MinimumVertexCover; +use crate::rules::test_helpers::assert_satisfaction_round_trip_from_satisfaction_target; +use crate::solvers::BruteForce; +use crate::topology::SimpleGraph; +use crate::traits::Problem; +use crate::variant::K3; + +#[test] +fn test_ksatisfiability_to_decisionminimumvertexcover_closed_loop() { + let source = KSatisfiability::::new( + 3, + vec![ + CNFClause::new(vec![1, 2, 3]), + CNFClause::new(vec![-1, -2, 3]), + ], + ); + let reduction = ReduceTo::>>::reduce_to(&source); + let target = reduction.target_problem(); + + assert_eq!(target.inner().num_vertices(), 12); + assert_eq!(target.inner().num_edges(), 15); + assert_eq!(target.bound(), &7); + + assert_satisfaction_round_trip_from_satisfaction_target( + &source, + &reduction, + "3SAT -> Decision MVC closed loop", + ); +} + +#[test] +fn test_ksatisfiability_to_decisionminimumvertexcover_unsatisfiable() { + let source = KSatisfiability::::new( + 1, + vec![ + CNFClause::new(vec![1, 1, 1]), + CNFClause::new(vec![-1, -1, -1]), + CNFClause::new(vec![1, 1, 1]), + ], + ); + let reduction = ReduceTo::>>::reduce_to(&source); + let target = reduction.target_problem(); + + assert_eq!(target.bound(), &7); + assert!(BruteForce::new().find_witness(target).is_none()); +} + +#[test] +fn test_ksatisfiability_to_decisionminimumvertexcover_structure_and_bound() { + let source = KSatisfiability::::new(2, vec![CNFClause::new(vec![1, -1, 2])]); + let reduction = ReduceTo::>>::reduce_to(&source); + let target = reduction.target_problem(); + + assert_eq!(target.inner().num_vertices(), 7); + assert_eq!(target.inner().num_edges(), 8); + assert_eq!(target.bound(), &4); +} + +#[test] +fn test_ksatisfiability_to_decisionminimumvertexcover_extract_solution() { + let source = KSatisfiability::::new( + 3, + vec![ + CNFClause::new(vec![1, 2, 3]), + CNFClause::new(vec![-1, -2, 3]), + ], + ); + let reduction = ReduceTo::>>::reduce_to(&source); + let cover = vec![0, 1, 0, 1, 1, 0, 1, 1, 0, 1, 1, 0]; + + assert_eq!( + reduction.target_problem().evaluate(&cover), + crate::types::Or(true) + ); + assert_eq!(reduction.extract_solution(&cover), vec![0, 0, 1]); +} From bfee0de1995cbf3b8f3fb0013fea497cc0143b83 Mon Sep 17 00:00:00 2001 From: GiggleLiu Date: Tue, 7 Apr 2026 18:27:26 +0800 Subject: [PATCH 05/13] feat: add 3sat to directed two-commodity flow --- docs/paper/reductions.typ | 35 +- .../directed_two_commodity_integral_flow.rs | 16 +- .../directedtwocommodityintegralflow_ilp.rs | 44 +-- ...bility_directedtwocommodityintegralflow.rs | 338 ++++++++++++++++++ src/rules/mod.rs | 4 + .../directed_two_commodity_integral_flow.rs | 11 + .../directedtwocommodityintegralflow_ilp.rs | 23 +- ...bility_directedtwocommodityintegralflow.rs | 158 ++++++++ 8 files changed, 599 insertions(+), 30 deletions(-) create mode 100644 src/rules/ksatisfiability_directedtwocommodityintegralflow.rs create mode 100644 src/unit_tests/rules/ksatisfiability_directedtwocommodityintegralflow.rs diff --git a/docs/paper/reductions.typ b/docs/paper/reductions.typ index db83a2d5..b50c4d74 100644 --- a/docs/paper/reductions.typ +++ b/docs/paper/reductions.typ @@ -8247,7 +8247,7 @@ A classical NP-complete problem from Garey and Johnson @garey1979[Ch.~3, p.~76], } #problem-def("DirectedTwoCommodityIntegralFlow")[ - Given a directed graph $G = (V, A)$ with arc capacities $c: A -> ZZ^+$, two source-sink pairs $(s_1, t_1)$ and $(s_2, t_2)$, and requirements $R_1, R_2 in ZZ^+$, determine whether there exist two integral flow functions $f_1, f_2: A -> ZZ_(>= 0)$ such that (1) $f_1(a) + f_2(a) <= c(a)$ for all $a in A$, (2) flow $f_i$ is conserved at every vertex except $s_1, s_2, t_1, t_2$, and (3) the net flow into $t_i$ under $f_i$ is at least $R_i$ for $i in {1, 2}$. + Given a directed graph $G = (V, A)$ with arc capacities $c: A -> ZZ^+$, two source-sink pairs $(s_1, t_1)$ and $(s_2, t_2)$, and requirements $R_1, R_2 in ZZ^+$, determine whether there exist two integral flow functions $f_1, f_2: A -> ZZ_(>= 0)$ such that (1) $f_1(a) + f_2(a) <= c(a)$ for all $a in A$, (2) for each commodity $i in {1, 2}$, flow $f_i$ is conserved at every vertex except $s_i$ and $t_i$, and (3) the net flow into $t_i$ under $f_i$ is at least $R_i$. ][ Directed Two-Commodity Integral Flow is a fundamental NP-complete problem in multicommodity flow theory, catalogued as ND38 in Garey & Johnson @garey1979. While single-commodity max-flow is solvable in polynomial time and fractional multicommodity flow reduces to linear programming, requiring integral flows with just two commodities makes the problem NP-complete. @@ -13803,6 +13803,39 @@ The following table shows concrete variable overhead for example instances, take _Solution extraction._ Return the first $n$ target coordinates unchanged, discarding $z_0$, $z_T$, and all clause auxiliaries. ] +#let ksat_d2cif = load-example("KSatisfiability", "DirectedTwoCommodityIntegralFlow") +#let ksat_d2cif_sol = ksat_d2cif.solutions.at(0) +#reduction-rule("KSatisfiability", "DirectedTwoCommodityIntegralFlow", + example: true, + example-caption: [Two-clause 3-SAT instance ($n = #ksat_d2cif.source.instance.num_vars$, $m = #sat-num-clauses(ksat_d2cif.source.instance)$) reduced to Directed Two-Commodity Integral Flow], + extra: [ + #pred-commands( + "pred create --example " + problem-spec(ksat_d2cif.source) + " -o ksat.json", + "pred reduce ksat.json --to " + target-spec(ksat_d2cif) + " -o bundle.json", + "pred solve bundle.json", + "pred evaluate ksat.json --config " + ksat_d2cif_sol.source_config.map(str).join(","), + ) + + *Step 1 -- Source instance.* The source formula has clauses $c_1 = (x_1 or overline(x)_2 or x_3)$ and $c_2 = (overline(x)_1 or x_2 or overline(x)_3)$. The canonical satisfying assignment is $(#ksat_d2cif_sol.source_config.map(str).join(", "))$, i.e.\ $x_1 = 1$, $x_2 = 1$, $x_3 = 0$. + + *Step 2 -- Build the lobes and clause sinks.* Each variable appears once positively and once negatively, so each lobe contains an entry vertex, an exit vertex, one dummy segment on each branch, and one literal-occurrence segment on each branch. That is $10$ vertices and $14$ arcs per variable. Adding the $4$ terminals and $2$ clause vertices gives $|V| = #ksat_d2cif.target.instance.graph.num_vertices = 36$; adding the $4$ commodity-1 chain arcs and $2$ clause-to-sink arcs gives $|A| = #ksat_d2cif.target.instance.graph.arcs.len() = 48$. + + *Step 3 -- Verify a witness.* Commodity 1 uses the lower branch in the lobes of $x_1$ and $x_2$ and the upper branch in the lobe of $x_3$, exactly matching the assignment $(1, 1, 0)$. Clause $c_1$ is satisfied by $x_1$, so commodity 2 routes one unit through the positive occurrence segment of $x_1$ into $d_1$. Clause $c_2$ is satisfied by $x_2$, so a second unit routes through the positive occurrence segment of $x_2$ into $d_2$. Both clause-to-sink arcs carry one unit, so the target meets $R_2 = #ksat_d2cif.target.instance.requirement_2 = 2$ #sym.checkmark. Reading back which lower-branch entry arcs commodity 1 used recovers $(#ksat_d2cif_sol.source_config.map(str).join(", "))$ #sym.checkmark + + *Multiplicity:* The fixture stores one canonical witness. This source formula has multiple satisfying assignments, and each satisfying clause can choose any satisfied literal occurrence when routing commodity 2. + ], +)[ + This $O(n + m)$ reduction @even1976 @garey1979[ND38] builds a unit-capacity directed network of variable lobes and clause sinks. Each literal occurrence contributes one clause-entry segment on the corresponding branch, and the repository pads every branch with one dummy segment so variables with missing polarity occurrences still have two realizable choices. For a 3-CNF formula with $n$ variables and $m$ clauses, the target has $6n + 7m + 4$ vertices and $7n + 13m + 1$ arcs. +][ + _Construction._ Let $phi = and_(j=1)^m C_j$ be a 3-CNF formula on variables $x_1, dots, x_n$. For each variable $x_i$, let $p_i$ be its number of positive occurrences and $q_i$ its number of negative occurrences. Create terminals $s_1, t_1, s_2, t_2$, one clause vertex $d_j$ for each clause, and for each variable a lobe with entry $a_i$ and exit $b_i$. The upper branch contains a dummy segment followed by one directed segment $u_(i,r)^+ -> w_(i,r)^+$ for each positive occurrence $r = 1, dots, p_i$; the lower branch contains a dummy segment followed by one directed segment $u_(i,r)^- -> w_(i,r)^-$ for each negative occurrence $r = 1, dots, q_i$. Chain the lobes with arcs $s_1 -> a_1$, $b_i -> a_(i+1)$, and $b_n -> t_1$. For every positive occurrence of $x_i$ in clause $C_j$, add $s_2 -> u_(i,r)^+$ and $w_(i,r)^+ -> d_j$; for every negative occurrence, add $s_2 -> u_(i,r)^-$ and $w_(i,r)^- -> d_j$. Finally add $d_j -> t_2$ for each clause. All arcs have capacity $1$, and the requirements are $R_1 = 1$ and $R_2 = m$. + + _Correctness._ ($arrow.r.double$) Suppose $phi$ is satisfiable. Route commodity 1 through the lower branch of lobe $i$ when $x_i = 1$, and through the upper branch when $x_i = 0$. Consider any clause $C_j$. Choose one satisfied literal occurrence in that clause. If the chosen literal is $x_i$, route one unit of commodity 2 along $s_2 -> u_(i,r)^+ -> w_(i,r)^+ -> d_j -> t_2$; if it is $overline(x)_i$, use the analogous lower-branch route. A true literal always lies on the branch opposite to commodity 1, so the shared occurrence segment is free. Because occurrence segments are distinct per clause position, the $m$ commodity-2 units respect all capacities. + + ($arrow.l.double$) Suppose the target instance is feasible. Because commodity 1 has requirement $R_1 = 1$ and conservation holds for commodity 1 away from $s_1$ and $t_1$, its unit flow traverses exactly one branch in each lobe. Define $x_i = 1$ iff commodity 1 uses the lower branch of lobe $i$. Now fix any clause vertex $d_j$. Since $d_j -> t_2$ is the only outgoing arc from $d_j$, meeting $R_2 = m$ forces one unit of commodity 2 through every clause vertex. That unit must arrive from some occurrence segment $u -> w -> d_j$. The shared arc $u -> w$ cannot lie on commodity 1's chosen branch, so the corresponding literal is true under the assignment above. Hence every clause contains a true literal and $phi$ is satisfiable. + + _Solution extraction._ For each variable lobe, inspect the first lower-branch arc leaving its entry. Output $x_i = 1$ exactly when commodity 1 uses that arc. +] + #let part_swi = load-example("Partition", "SequencingWithinIntervals") #let part_swi_sol = part_swi.solutions.at(0) #reduction-rule("Partition", "SequencingWithinIntervals", diff --git a/src/models/graph/directed_two_commodity_integral_flow.rs b/src/models/graph/directed_two_commodity_integral_flow.rs index 97b4dd49..f67445df 100644 --- a/src/models/graph/directed_two_commodity_integral_flow.rs +++ b/src/models/graph/directed_two_commodity_integral_flow.rs @@ -39,7 +39,7 @@ inventory::submit! { /// whether two integral flow functions f_1, f_2: A -> Z_0^+ exist such that: /// 1. Joint capacity: f_1(a) + f_2(a) <= c(a) for all a in A /// 2. Flow conservation: for each commodity i, flow is conserved at every -/// vertex except the four terminals +/// vertex except its own source and sink /// 3. Requirements: net flow into t_i under f_i is at least R_i /// /// # Variables @@ -191,8 +191,6 @@ impl DirectedTwoCommodityIntegralFlow { return false; } let arcs = self.graph.arcs(); - let terminals = [self.source_1, self.sink_1, self.source_2, self.sink_2]; - // (1) Joint capacity constraint for a in 0..m { let f1 = config[a] as u64; @@ -216,8 +214,18 @@ impl DirectedTwoCommodityIntegralFlow { } for (commodity, commodity_balances) in balances.iter().enumerate() { + let src = if commodity == 0 { + self.source_1 + } else { + self.source_2 + }; for (v, &balance) in commodity_balances.iter().enumerate() { - if !terminals.contains(&v) && balance != 0 { + let snk = if commodity == 0 { + self.sink_1 + } else { + self.sink_2 + }; + if v != src && v != snk && balance != 0 { return false; } } diff --git a/src/rules/directedtwocommodityintegralflow_ilp.rs b/src/rules/directedtwocommodityintegralflow_ilp.rs index f16c304c..86f62576 100644 --- a/src/rules/directedtwocommodityintegralflow_ilp.rs +++ b/src/rules/directedtwocommodityintegralflow_ilp.rs @@ -70,40 +70,44 @@ impl ReduceTo> for DirectedTwoCommodityIntegralFlow { )); } - // 2. Flow conservation at non-terminal vertices - let terminals = [ - self.source_1(), - self.sink_1(), - self.source_2(), - self.sink_2(), - ]; - + // 2. Flow conservation away from each commodity's own source and sink for vertex in 0..n { - if terminals.contains(&vertex) { - continue; - } - // Commodity 1: Σ_in f1 - Σ_out f1 = 0 - let mut terms_c1: Vec<(usize, f64)> = Vec::new(); + let mut terms_c1: Option> = None; // Commodity 2: Σ_in f2 - Σ_out f2 = 0 - let mut terms_c2: Vec<(usize, f64)> = Vec::new(); + let mut terms_c2: Option> = None; + + if vertex != self.source_1() && vertex != self.sink_1() { + terms_c1 = Some(Vec::new()); + } + if vertex != self.source_2() && vertex != self.sink_2() { + terms_c2 = Some(Vec::new()); + } for (a, &(u, v)) in arcs.iter().enumerate() { if vertex == u { // Arc leaves vertex: outgoing - terms_c1.push((f1(a), -1.0)); - terms_c2.push((f2(a), -1.0)); + if let Some(terms) = &mut terms_c1 { + terms.push((f1(a), -1.0)); + } + if let Some(terms) = &mut terms_c2 { + terms.push((f2(a), -1.0)); + } } else if vertex == v { // Arc enters vertex: incoming - terms_c1.push((f1(a), 1.0)); - terms_c2.push((f2(a), 1.0)); + if let Some(terms) = &mut terms_c1 { + terms.push((f1(a), 1.0)); + } + if let Some(terms) = &mut terms_c2 { + terms.push((f2(a), 1.0)); + } } } - if !terms_c1.is_empty() { + if let Some(terms_c1) = terms_c1.filter(|terms| !terms.is_empty()) { constraints.push(LinearConstraint::eq(terms_c1, 0.0)); } - if !terms_c2.is_empty() { + if let Some(terms_c2) = terms_c2.filter(|terms| !terms.is_empty()) { constraints.push(LinearConstraint::eq(terms_c2, 0.0)); } } diff --git a/src/rules/ksatisfiability_directedtwocommodityintegralflow.rs b/src/rules/ksatisfiability_directedtwocommodityintegralflow.rs new file mode 100644 index 00000000..bcf39b7a --- /dev/null +++ b/src/rules/ksatisfiability_directedtwocommodityintegralflow.rs @@ -0,0 +1,338 @@ +//! Reduction from KSatisfiability (3-SAT) to DirectedTwoCommodityIntegralFlow. +//! +//! This uses a padded occurrence-lobe variant of the Even-Itai-Shamir +//! construction: each variable branch begins with one dummy segment, then one +//! segment per literal occurrence of that polarity. Commodity 1 chooses exactly +//! one branch per variable. Commodity 2 must enter a literal-occurrence segment +//! from `s_2`, traverse that segment's internal arc, and then exit to a clause +//! vertex before reaching `t_2`. + +use crate::models::formula::KSatisfiability; +use crate::models::graph::DirectedTwoCommodityIntegralFlow; +use crate::reduction; +use crate::rules::traits::{ReduceTo, ReductionResult}; +use crate::topology::DirectedGraph; +use crate::variant::K3; + +#[derive(Debug, Clone, Copy)] +struct ClauseOccurrence { + clause_idx: usize, + variable: usize, + requires_true: bool, +} + +#[cfg_attr(not(any(test, feature = "example-db")), allow(dead_code))] +#[derive(Debug, Clone)] +struct VariablePaths { + upper_path: Vec, + lower_path: Vec, + lower_entry_arc: usize, +} + +#[cfg_attr(not(any(test, feature = "example-db")), allow(dead_code))] +#[derive(Debug, Clone)] +struct ClauseRoute { + variable: usize, + requires_true: bool, + source_arc: usize, + branch_arc: usize, + clause_arc: usize, +} + +#[derive(Debug, Clone)] +struct BranchBuild { + path_arcs: Vec, + entry_arc: usize, +} + +struct BranchContext<'a> { + source_2: usize, + clause_vertices: &'a [usize], + clause_routes: &'a mut [Vec], +} + +#[cfg_attr(not(any(test, feature = "example-db")), allow(dead_code))] +#[derive(Debug, Clone)] +pub struct Reduction3SATToDirectedTwoCommodityIntegralFlow { + target: DirectedTwoCommodityIntegralFlow, + commodity_1_chain_arcs: Vec, + variable_paths: Vec, + clause_routes: Vec>, + clause_sink_arcs: Vec, +} + +fn literal_var_index(literal: i32) -> usize { + literal.unsigned_abs() as usize - 1 +} + +#[cfg_attr(not(any(test, feature = "example-db")), allow(dead_code))] +fn literal_satisfied(requires_true: bool, assignment: &[usize], variable: usize) -> bool { + assignment.get(variable).copied().unwrap_or(0) == usize::from(requires_true) +} + +fn build_branch( + add_vertex: &mut FV, + add_arc: &mut FA, + entry: usize, + exit: usize, + occurrences: &[ClauseOccurrence], + branch_context: &mut BranchContext<'_>, +) -> BranchBuild +where + FV: FnMut() -> usize, + FA: FnMut(usize, usize) -> usize, +{ + let mut path_arcs = Vec::with_capacity(2 * occurrences.len() + 3); + + let dummy_odd = add_vertex(); + let dummy_even = add_vertex(); + let entry_arc = add_arc(entry, dummy_odd); + path_arcs.push(entry_arc); + path_arcs.push(add_arc(dummy_odd, dummy_even)); + + let mut previous_even = dummy_even; + + for occurrence in occurrences { + let odd = add_vertex(); + let even = add_vertex(); + path_arcs.push(add_arc(previous_even, odd)); + let branch_arc = add_arc(odd, even); + path_arcs.push(branch_arc); + + let source_arc = add_arc(branch_context.source_2, odd); + let clause_arc = add_arc(even, branch_context.clause_vertices[occurrence.clause_idx]); + branch_context.clause_routes[occurrence.clause_idx].push(ClauseRoute { + variable: occurrence.variable, + requires_true: occurrence.requires_true, + source_arc, + branch_arc, + clause_arc, + }); + + previous_even = even; + } + + path_arcs.push(add_arc(previous_even, exit)); + + BranchBuild { + path_arcs, + entry_arc, + } +} + +impl Reduction3SATToDirectedTwoCommodityIntegralFlow { + #[cfg(any(test, feature = "example-db"))] + pub(crate) fn encode_assignment(&self, assignment: &[usize]) -> Vec { + assert_eq!( + assignment.len(), + self.variable_paths.len(), + "assignment length must match num_vars", + ); + + let num_arcs = self.target.num_arcs(); + let mut flow = vec![0usize; 2 * num_arcs]; + + for &arc_idx in &self.commodity_1_chain_arcs { + flow[arc_idx] = 1; + } + + for (value, paths) in assignment.iter().zip(&self.variable_paths) { + let chosen_path = if *value == 1 { + &paths.lower_path + } else { + &paths.upper_path + }; + for &arc_idx in chosen_path { + flow[arc_idx] = 1; + } + } + + for (clause_idx, routes) in self.clause_routes.iter().enumerate() { + if let Some(route) = routes + .iter() + .find(|route| literal_satisfied(route.requires_true, assignment, route.variable)) + { + flow[num_arcs + route.source_arc] = 1; + flow[num_arcs + route.branch_arc] = 1; + flow[num_arcs + route.clause_arc] = 1; + flow[num_arcs + self.clause_sink_arcs[clause_idx]] = 1; + } + } + + flow + } +} + +impl ReductionResult for Reduction3SATToDirectedTwoCommodityIntegralFlow { + type Source = KSatisfiability; + type Target = DirectedTwoCommodityIntegralFlow; + + fn target_problem(&self) -> &Self::Target { + &self.target + } + + fn extract_solution(&self, target_solution: &[usize]) -> Vec { + self.variable_paths + .iter() + .map(|paths| usize::from(target_solution.get(paths.lower_entry_arc).copied().unwrap_or(0) > 0)) + .collect() + } +} + +#[reduction(overhead = { + num_vertices = "6 * num_vars + 2 * num_literals + num_clauses + 4", + num_arcs = "7 * num_vars + 4 * num_literals + num_clauses + 1", +})] +impl ReduceTo for KSatisfiability { + type Result = Reduction3SATToDirectedTwoCommodityIntegralFlow; + + fn reduce_to(&self) -> Self::Result { + let source_1 = 0usize; + let sink_1 = 1usize; + let source_2 = 2usize; + let sink_2 = 3usize; + + let mut positive_occurrences = vec![Vec::::new(); self.num_vars()]; + let mut negative_occurrences = vec![Vec::::new(); self.num_vars()]; + for (clause_idx, clause) in self.clauses().iter().enumerate() { + for &literal in &clause.literals { + let variable = literal_var_index(literal); + let occurrence = ClauseOccurrence { + clause_idx, + variable, + requires_true: literal > 0, + }; + if literal > 0 { + positive_occurrences[variable].push(occurrence); + } else { + negative_occurrences[variable].push(occurrence); + } + } + } + + let mut next_vertex = 4 + self.num_clauses(); + let clause_vertices: Vec = (0..self.num_clauses()).map(|idx| 4 + idx).collect(); + let mut add_vertex = || { + let id = next_vertex; + next_vertex += 1; + id + }; + + let mut arcs = Vec::<(usize, usize)>::new(); + let mut add_arc = |u: usize, v: usize| { + arcs.push((u, v)); + arcs.len() - 1 + }; + + let mut entries = Vec::with_capacity(self.num_vars()); + let mut exits = Vec::with_capacity(self.num_vars()); + let mut variable_paths = Vec::with_capacity(self.num_vars()); + let mut clause_routes = vec![Vec::::new(); self.num_clauses()]; + let mut branch_context = BranchContext { + source_2, + clause_vertices: &clause_vertices, + clause_routes: &mut clause_routes, + }; + + for variable in 0..self.num_vars() { + let entry = add_vertex(); + let exit = add_vertex(); + entries.push(entry); + exits.push(exit); + + let upper = build_branch( + &mut add_vertex, + &mut add_arc, + entry, + exit, + &positive_occurrences[variable], + &mut branch_context, + ); + let lower = build_branch( + &mut add_vertex, + &mut add_arc, + entry, + exit, + &negative_occurrences[variable], + &mut branch_context, + ); + + variable_paths.push(VariablePaths { + upper_path: upper.path_arcs, + lower_path: lower.path_arcs, + lower_entry_arc: lower.entry_arc, + }); + } + + let mut commodity_1_chain_arcs = Vec::with_capacity(self.num_vars() + 1); + if self.num_vars() == 0 { + commodity_1_chain_arcs.push(add_arc(source_1, sink_1)); + } else { + commodity_1_chain_arcs.push(add_arc(source_1, entries[0])); + for variable in 0..self.num_vars() - 1 { + commodity_1_chain_arcs.push(add_arc(exits[variable], entries[variable + 1])); + } + commodity_1_chain_arcs.push(add_arc(exits[self.num_vars() - 1], sink_1)); + } + + let clause_sink_arcs: Vec = clause_vertices + .iter() + .map(|&clause_vertex| add_arc(clause_vertex, sink_2)) + .collect(); + + let capacities = vec![1u64; arcs.len()]; + let target = DirectedTwoCommodityIntegralFlow::new( + DirectedGraph::new(next_vertex, arcs), + capacities, + source_1, + sink_1, + source_2, + sink_2, + 1, + self.num_clauses() as u64, + ); + + Reduction3SATToDirectedTwoCommodityIntegralFlow { + target, + commodity_1_chain_arcs, + variable_paths, + clause_routes, + clause_sink_arcs, + } + } +} + +#[cfg(feature = "example-db")] +pub(crate) fn canonical_rule_example_specs() -> Vec { + use crate::export::SolutionPair; + + vec![crate::example_db::specs::RuleExampleSpec { + id: "ksatisfiability_to_directedtwocommodityintegralflow", + build: || { + let source = KSatisfiability::::new( + 3, + vec![ + crate::models::formula::CNFClause::new(vec![1, -2, 3]), + crate::models::formula::CNFClause::new(vec![-1, 2, -3]), + ], + ); + let reduction = + crate::rules::ReduceTo::::reduce_to(&source); + let source_config = vec![1, 1, 0]; + let target_config = reduction.encode_assignment(&source_config); + + crate::example_db::specs::assemble_rule_example( + &source, + reduction.target_problem(), + vec![SolutionPair { + source_config, + target_config, + }], + ) + }, + }] +} + +#[cfg(test)] +#[path = "../unit_tests/rules/ksatisfiability_directedtwocommodityintegralflow.rs"] +mod tests; diff --git a/src/rules/mod.rs b/src/rules/mod.rs index 473354ae..15e84bab 100644 --- a/src/rules/mod.rs +++ b/src/rules/mod.rs @@ -47,6 +47,7 @@ pub(crate) mod ksatisfiability_acyclicpartition; mod ksatisfiability_casts; pub(crate) mod ksatisfiability_cyclicordering; pub(crate) mod ksatisfiability_decisionminimumvertexcover; +pub(crate) mod ksatisfiability_directedtwocommodityintegralflow; pub(crate) mod ksatisfiability_kclique; pub(crate) mod ksatisfiability_kernel; pub(crate) mod ksatisfiability_minimumvertexcover; @@ -457,6 +458,9 @@ pub(crate) fn canonical_rule_example_specs() -> Vec>::reduce_to(&problem); + assert!( + ILPSolver::new().solve(reduction.target_problem()).is_none(), + "commodity 1 must conserve flow at commodity 2's source in the ILP reduction" + ); +} + #[test] fn test_directedtwocommodityintegralflow_to_ilp_extract_solution() { let problem = feasible_instance(); diff --git a/src/unit_tests/rules/ksatisfiability_directedtwocommodityintegralflow.rs b/src/unit_tests/rules/ksatisfiability_directedtwocommodityintegralflow.rs new file mode 100644 index 00000000..00c62d4f --- /dev/null +++ b/src/unit_tests/rules/ksatisfiability_directedtwocommodityintegralflow.rs @@ -0,0 +1,158 @@ +#[cfg(feature = "example-db")] +use super::canonical_rule_example_specs; +use super::*; +#[cfg(feature = "ilp-solver")] +use crate::models::algebraic::ILP; +use crate::models::formula::CNFClause; +#[cfg(feature = "example-db")] +use crate::models::graph::DirectedTwoCommodityIntegralFlow; +use crate::rules::{ReduceTo, ReductionGraph, ReductionResult}; +#[cfg(feature = "ilp-solver")] +use crate::solvers::ILPSolver; +use crate::traits::Problem; +use crate::variant::K3; + +fn issue_example() -> KSatisfiability { + KSatisfiability::::new( + 3, + vec![ + CNFClause::new(vec![1, -2, 3]), + CNFClause::new(vec![-1, 2, -3]), + ], + ) +} + +fn unsatisfiable_instance() -> KSatisfiability { + KSatisfiability::::new( + 1, + vec![ + CNFClause::new(vec![1, 1, 1]), + CNFClause::new(vec![-1, -1, -1]), + ], + ) +} + +fn all_assignments(num_vars: usize) -> Vec> { + (0..(1usize << num_vars)) + .map(|mask| { + (0..num_vars) + .map(|bit| usize::from(((mask >> bit) & 1) == 1)) + .collect() + }) + .collect() +} + +#[cfg(feature = "ilp-solver")] +fn solve_target_via_ilp(problem: &crate::models::graph::DirectedTwoCommodityIntegralFlow) -> Option> { + let reduction = ReduceTo::>::reduce_to(problem); + let ilp_solution = ILPSolver::new().solve(reduction.target_problem())?; + let extracted = reduction.extract_solution(&ilp_solution); + problem.evaluate(&extracted).0.then_some(extracted) +} + +#[test] +fn test_ksatisfiability_to_directedtwocommodityintegralflow_structure() { + let source = issue_example(); + let reduction = ReduceTo::::reduce_to(&source); + let target = reduction.target_problem(); + + assert_eq!(target.num_vertices(), 36); + assert_eq!(target.num_arcs(), 48); + assert_eq!(target.requirement_1(), 1); + assert_eq!(target.requirement_2(), 2); + assert_eq!(target.max_capacity(), 1); +} + +#[test] +fn test_ksatisfiability_to_directedtwocommodityintegralflow_assignment_encoding_matches_truth_table() { + let source = issue_example(); + let reduction = ReduceTo::::reduce_to(&source); + let target = reduction.target_problem(); + + for assignment in all_assignments(source.num_vars()) { + let flow = reduction.encode_assignment(&assignment); + assert_eq!( + source.evaluate(&assignment).0, + target.evaluate(&flow).0, + "assignment {:?} should preserve satisfiability through the encoded flow", + assignment + ); + } +} + +#[test] +fn test_ksatisfiability_to_directedtwocommodityintegralflow_extract_solution_from_encoded_witness() { + let source = issue_example(); + let reduction = ReduceTo::::reduce_to(&source); + + let assignment = vec![1, 1, 0]; + let flow = reduction.encode_assignment(&assignment); + assert!(reduction.target_problem().evaluate(&flow).0); + assert_eq!(reduction.extract_solution(&flow), assignment); +} + +#[cfg(feature = "ilp-solver")] +#[test] +fn test_ksatisfiability_to_directedtwocommodityintegralflow_closed_loop() { + let source = issue_example(); + let reduction = ReduceTo::::reduce_to(&source); + + let target_solution = solve_target_via_ilp(reduction.target_problem()) + .expect("satisfiable source instance should produce a feasible two-commodity flow"); + + assert!(reduction.target_problem().evaluate(&target_solution).0); + + let extracted = reduction.extract_solution(&target_solution); + assert!(source.evaluate(&extracted).0); +} + +#[cfg(feature = "ilp-solver")] +#[test] +fn test_ksatisfiability_to_directedtwocommodityintegralflow_unsatisfiable() { + let source = unsatisfiable_instance(); + let reduction = ReduceTo::::reduce_to(&source); + let maybe_solution = solve_target_via_ilp(reduction.target_problem()); + assert!( + maybe_solution.is_none(), + "unsatisfiable 3SAT instance should produce an infeasible two-commodity flow" + ); +} + +#[test] +fn test_reduction_graph_registers_ksatisfiability_to_directedtwocommodityintegralflow() { + let graph = ReductionGraph::new(); + assert!(graph.has_direct_reduction_by_name( + "KSatisfiability", + "DirectedTwoCommodityIntegralFlow", + )); +} + +#[cfg(feature = "example-db")] +#[test] +fn test_ksatisfiability_to_directedtwocommodityintegralflow_canonical_example_spec() { + let example = (canonical_rule_example_specs() + .into_iter() + .find(|spec| spec.id == "ksatisfiability_to_directedtwocommodityintegralflow") + .expect("missing canonical 3SAT -> DirectedTwoCommodityIntegralFlow example spec") + .build)(); + + assert_eq!(example.source.problem, "KSatisfiability"); + assert_eq!(example.target.problem, "DirectedTwoCommodityIntegralFlow"); + assert_eq!(example.target.instance["requirement_1"], serde_json::json!(1)); + assert_eq!(example.target.instance["requirement_2"], serde_json::json!(2)); + assert_eq!(example.solutions.len(), 1); + assert_eq!(example.solutions[0].source_config, vec![1, 1, 0]); + + let source: KSatisfiability = serde_json::from_value(example.source.instance.clone()) + .expect("source example deserializes"); + let target: DirectedTwoCommodityIntegralFlow = + serde_json::from_value(example.target.instance.clone()) + .expect("target example deserializes"); + + assert!(source + .evaluate(&example.solutions[0].source_config) + .is_valid()); + assert!(target + .evaluate(&example.solutions[0].target_config) + .is_valid()); +} From 78405fbf91590705d29dea0709a534ac1978b668 Mon Sep 17 00:00:00 2001 From: GiggleLiu Date: Tue, 7 Apr 2026 20:35:27 +0800 Subject: [PATCH 06/13] Add MonochromaticTriangle reductions --- docs/paper/reductions.typ | 68 +++++++ src/models/graph/monochromatic_triangle.rs | 5 + .../ksatisfiability_monochromatictriangle.rs | 172 ++++++++++++++++++ src/rules/mod.rs | 9 +- src/rules/monochromatictriangle_ilp.rs | 79 ++++++++ .../ksatisfiability_monochromatictriangle.rs | 88 +++++++++ .../rules/monochromatictriangle_ilp.rs | 82 +++++++++ 7 files changed, 500 insertions(+), 3 deletions(-) create mode 100644 src/rules/ksatisfiability_monochromatictriangle.rs create mode 100644 src/rules/monochromatictriangle_ilp.rs create mode 100644 src/unit_tests/rules/ksatisfiability_monochromatictriangle.rs create mode 100644 src/unit_tests/rules/monochromatictriangle_ilp.rs diff --git a/docs/paper/reductions.typ b/docs/paper/reductions.typ index b50c4d74..61e5b9af 100644 --- a/docs/paper/reductions.typ +++ b/docs/paper/reductions.typ @@ -11270,6 +11270,43 @@ The following reductions to Integer Linear Programming are straightforward formu _Solution extraction._ $S_2 = {u_i : x_i = 1}$, $S_1 = U without S_2$. ] +#let mono_ilp = load-example("MonochromaticTriangle", "ILP") +#let mono_ilp_sol = mono_ilp.solutions.at(0) +#reduction-rule("MonochromaticTriangle", "ILP", + example: true, + example-caption: [$K_4$ with $n = #graph-num-vertices(mono_ilp.source.instance)$ vertices, $m = #graph-num-edges(mono_ilp.source.instance)$ edges, and $#mono_ilp.source.instance.triangles.len()$ triangles], + extra: [ + #pred-commands( + "pred create --example " + problem-spec(mono_ilp.source) + " -o monochromatic-triangle.json", + "pred reduce monochromatic-triangle.json --to " + target-spec(mono_ilp) + " -o bundle.json", + "pred solve bundle.json", + "pred evaluate monochromatic-triangle.json --config " + mono_ilp_sol.source_config.map(str).join(","), + ) + + *Step 1 -- Source instance.* The canonical Monochromatic Triangle fixture is $K_4$ on vertices $0, 1, 2, 3$ with edges #{mono_ilp.source.instance.graph.edges.map(((u, v)) => [${#u, #v}$]).join(", ")}. It has $#mono_ilp.source.instance.triangles.len()$ triangles, so the reduction creates one pair of inequalities for each of those four triangles. + + *Step 2 -- Build the ILP.* Introduce one binary variable per edge, so the target has $m = #mono_ilp.target.instance.num_vars$ variables. For each triangle, add the lower bound $x_a + x_b + x_c >= 1$ and the upper bound $x_a + x_b + x_c <= 2$, giving $#mono_ilp.target.instance.constraints.len()$ total constraints. + + *Step 3 -- Verify a witness.* The stored ILP witness is $(#mono_ilp_sol.target_config.map(str).join(", "))$. Because extraction is identity, it immediately yields the edge coloring $(#mono_ilp_sol.source_config.map(str).join(", "))$, and evaluating that coloring on the source returns `true` #sym.checkmark. Every triangle therefore uses both colors. + + *Multiplicity:* The fixture stores one canonical edge coloring. Any binary ILP solution satisfying all triangle pairs is a valid Monochromatic Triangle witness. + ], +)[ + This $O(m + t)$ reduction uses one binary variable per edge and two linear inequalities per triangle, where $m = |E|$ and $t$ is the number of triangles in the source graph. The target ILP is a pure feasibility problem with $m$ variables and $2t$ constraints. +][ + _Construction._ Let the source graph edges be indexed as $e_0, dots, e_(m-1)$. Introduce binary variables $x_0, dots, x_(m-1)$, where $x_i = 0$ or $1$ is the color assigned to edge $e_i$. For every triangle $T = {e_a, e_b, e_c}$ in the source graph, add the pair of inequalities + $ + x_a + x_b + x_c >= 1 + quad "and" quad + x_a + x_b + x_c <= 2. + $ + The objective is empty, so the ILP asks only for feasibility. + + _Correctness._ ($arrow.r.double$) Any triangle-free 2-edge-coloring assigns each triangle at least one edge of color 0 and at least one edge of color 1, so the corresponding sum is either $1$ or $2$ and both inequalities hold. ($arrow.l.double$) Any feasible ILP assignment gives a 0/1 color to every edge, and the triangle bounds forbid sums $0$ and $3$, so no triangle is monochromatic. + + _Solution extraction._ Return the ILP variables unchanged as the target edge-coloring vector. +] + #let ss_bt = load-example("SetSplitting", "Betweenness") #let ss_bt_sol = ss_bt.solutions.at(0) #reduction-rule("SetSplitting", "Betweenness", @@ -13751,6 +13788,37 @@ The following table shows concrete variable overhead for example instances, take _Solution extraction._ For variable $x_i$, set $x_i = 1$ if the cover indicator at position $2i$ is 1. ] +#let ksat_mono = load-example("KSatisfiability", "MonochromaticTriangle") +#let ksat_mono_sol = ksat_mono.solutions.at(0) +#reduction-rule("KSatisfiability", "MonochromaticTriangle", + example: true, + example-caption: [Single-clause 3-SAT instance ($n = #ksat_mono.source.instance.num_vars$, $m = #sat-num-clauses(ksat_mono.source.instance)$) reduced to a 4-triangle graph], + extra: [ + #pred-commands( + "pred create --example " + problem-spec(ksat_mono.source) + " -o ksat.json", + "pred reduce ksat.json --to " + target-spec(ksat_mono) + " -o bundle.json", + "pred solve bundle.json", + "pred evaluate ksat.json --config " + ksat_mono_sol.source_config.map(str).join(","), + ) + + *Step 1 -- Source instance.* The fixture uses the single clause $c_1 = (x_1 or x_2 or x_3)$. The extracted satisfying assignment is $(#ksat_mono_sol.source_config.map(str).join(", "))$. + + *Step 2 -- Build the clause gadget.* Create literal vertices $p_1, p_2, p_3, n_1, n_2, n_3$ together with negation edges $(p_1, n_1)$, $(p_2, n_2)$, and $(p_3, n_3)$. For the clause, add intermediates $m_12, m_13, m_23$ and the six fan edges $(p_1, m_12)$, $(p_2, m_12)$, $(p_1, m_13)$, $(p_3, m_13)$, $(p_2, m_23)$, $(p_3, m_23)$, plus the clause triangle on $(m_12, m_13, m_23)$. The target therefore has $|V| = #graph-num-vertices(ksat_mono.target.instance)$ vertices, $|E| = #graph-num-edges(ksat_mono.target.instance)$ edges, and $#ksat_mono.target.instance.triangles.len()$ triangles. + + *Step 3 -- Verify a witness.* The stored target coloring is $(#ksat_mono_sol.target_config.map(str).join(", "))$. Its first $n = #ksat_mono.source.instance.num_vars$ entries color the negation edges; reading those colors and applying the global color-swap symmetry fix yields the source assignment $(#ksat_mono_sol.source_config.map(str).join(", "))$, which satisfies $c_1$ #sym.checkmark. The same target coloring makes all four target triangles non-monochromatic #sym.checkmark. + + *Multiplicity:* The fixture stores one canonical target coloring. Swapping the two edge colors gives another valid witness and may flip the decoded assignment to its complement. + ], +)[ + This $O(n + m)$ reduction @garey1979[GT6] uses one positive/negative literal pair per variable and one three-vertex clause gadget per clause. The target graph has $2n + 3m$ vertices and $n + 9m$ edges. +][ + _Construction._ Let $phi = and_(j=1)^m (ell_1^j or ell_2^j or ell_3^j)$ be a 3-CNF formula on variables $x_1, dots, x_n$. For each variable $x_i$, create literal vertices $p_i$ and $n_i$ and add the negation edge $(p_i, n_i)$. For each clause $C_j$, map each literal $ell_r^j$ to its literal vertex $v_r^j$ ($x_i mapsto p_i$, $overline(x)_i mapsto n_i$). Introduce fresh intermediate vertices $m_12^j$, $m_13^j$, and $m_23^j$. Add fan edges $(v_1^j, m_12^j)$, $(v_2^j, m_12^j)$, $(v_1^j, m_13^j)$, $(v_3^j, m_13^j)$, $(v_2^j, m_23^j)$, and $(v_3^j, m_23^j)$, then connect the intermediates into the clause triangle $(m_12^j, m_13^j)$, $(m_12^j, m_23^j)$, $(m_13^j, m_23^j)$. Each clause gadget therefore contributes exactly four triangles: the clause triangle itself and the three fan triangles rooted at $v_1^j$, $v_2^j$, and $v_3^j$. + + _Correctness._ ($arrow.r.double$) Fix a satisfying assignment of $phi$. Color each negation edge $(p_i, n_i)$ by the truth value of $x_i$, using color $0$ for true and color $1$ for false. For any clause, at least one of its literals is satisfied, and the four-triangle gadget has a 2-edge-coloring extending those literal choices with no monochromatic triangle; the implementation follows the verified local construction from issue #884 and colors each clause independently because the intermediates are clause-local. ($arrow.l.double$) Given a triangle-free coloring of the target graph, inspect the negation-edge colors. Either those colors, or their global complement after swapping the two colors, yields a satisfying assignment of the source formula under the same verified gadget analysis. + + _Solution extraction._ Read the negation-edge colors in variable order, setting $x_i = 1$ when $(p_i, n_i)$ has color $0$ and $x_i = 0$ otherwise. If that assignment does not satisfy $phi$, complement all bits; this accounts for the global color-swap symmetry of the target witness. +] + #let ksat_1in3 = load-example("KSatisfiability", "OneInThreeSatisfiability") #let ksat_1in3_sol = ksat_1in3.solutions.at(0) #reduction-rule("KSatisfiability", "OneInThreeSatisfiability", diff --git a/src/models/graph/monochromatic_triangle.rs b/src/models/graph/monochromatic_triangle.rs index 728ed436..17366640 100644 --- a/src/models/graph/monochromatic_triangle.rs +++ b/src/models/graph/monochromatic_triangle.rs @@ -125,6 +125,11 @@ impl MonochromaticTriangle { &self.triangles } + /// Get the number of triangles in the graph. + pub fn num_triangles(&self) -> usize { + self.triangles.len() + } + /// Get the ordered edge list. pub fn edge_list(&self) -> &[(usize, usize)] { &self.edge_list diff --git a/src/rules/ksatisfiability_monochromatictriangle.rs b/src/rules/ksatisfiability_monochromatictriangle.rs new file mode 100644 index 00000000..d2a49e31 --- /dev/null +++ b/src/rules/ksatisfiability_monochromatictriangle.rs @@ -0,0 +1,172 @@ +//! Reduction from KSatisfiability (3-SAT) to MonochromaticTriangle. +//! +//! For each variable, create positive/negative literal vertices joined by a +//! negation edge. Each clause adds three fresh intermediates that form a clause +//! triangle, plus six fan edges from the clause literals to those intermediates. +//! The resulting graph has a triangle-free 2-edge-coloring iff the source +//! formula is satisfiable. + +use crate::models::formula::KSatisfiability; +use crate::models::graph::MonochromaticTriangle; +use crate::reduction; +use crate::rules::traits::{ReduceTo, ReductionResult}; +use crate::topology::SimpleGraph; +use crate::traits::Problem; +use crate::variant::K3; +use std::collections::HashMap; + +fn normalized_edge(u: usize, v: usize) -> (usize, usize) { + if u < v { + (u, v) + } else { + (v, u) + } +} + +fn literal_vertex(num_vars: usize, literal: i32) -> usize { + if literal > 0 { + literal as usize - 1 + } else { + num_vars + literal.unsigned_abs() as usize - 1 + } +} + +/// Result of reducing KSatisfiability to MonochromaticTriangle. +#[derive(Debug, Clone)] +pub struct Reduction3SATToMonochromaticTriangle { + target: MonochromaticTriangle, + source: KSatisfiability, + negation_edge_indices: Vec, +} + +impl ReductionResult for Reduction3SATToMonochromaticTriangle { + type Source = KSatisfiability; + type Target = MonochromaticTriangle; + + fn target_problem(&self) -> &Self::Target { + &self.target + } + + fn extract_solution(&self, target_solution: &[usize]) -> Vec { + let direct: Vec = self + .negation_edge_indices + .iter() + .map( + |&edge_idx| match target_solution.get(edge_idx).copied().unwrap_or(1) { + 0 => 1, + _ => 0, + }, + ) + .collect(); + if self.source.evaluate(&direct).0 { + return direct; + } + + let complement: Vec = direct.iter().map(|&value| 1 - value).collect(); + if self.source.evaluate(&complement).0 { + return complement; + } + + direct + } +} + +#[reduction( + overhead = { + num_vertices = "2 * num_vars + 3 * num_clauses", + num_edges = "num_vars + 9 * num_clauses", + } +)] +impl ReduceTo> for KSatisfiability { + type Result = Reduction3SATToMonochromaticTriangle; + + fn reduce_to(&self) -> Self::Result { + let num_vars = self.num_vars(); + let num_clauses = self.num_clauses(); + let mut edges = Vec::with_capacity(num_vars + 9 * num_clauses); + + for var in 0..num_vars { + edges.push((var, num_vars + var)); + } + + for (clause_idx, clause) in self.clauses().iter().enumerate() { + let clause_base = 2 * num_vars + 3 * clause_idx; + let m12 = clause_base; + let m13 = clause_base + 1; + let m23 = clause_base + 2; + let literal_vertices: Vec = clause + .literals + .iter() + .map(|&literal| literal_vertex(num_vars, literal)) + .collect(); + let v1 = literal_vertices[0]; + let v2 = literal_vertices[1]; + let v3 = literal_vertices[2]; + + edges.extend_from_slice(&[ + (v1, m12), + (v2, m12), + (v1, m13), + (v3, m13), + (v2, m23), + (v3, m23), + (m12, m13), + (m12, m23), + (m13, m23), + ]); + } + + let target = + MonochromaticTriangle::new(SimpleGraph::new(2 * num_vars + 3 * num_clauses, edges)); + let edge_indices: HashMap<(usize, usize), usize> = target + .edge_list() + .iter() + .copied() + .enumerate() + .map(|(idx, (u, v))| (normalized_edge(u, v), idx)) + .collect(); + let negation_edge_indices = (0..num_vars) + .map(|var| edge_indices[&normalized_edge(var, num_vars + var)]) + .collect(); + + Reduction3SATToMonochromaticTriangle { + target, + source: self.clone(), + negation_edge_indices, + } + } +} + +#[cfg(feature = "example-db")] +pub(crate) fn canonical_rule_example_specs() -> Vec { + use crate::export::SolutionPair; + use crate::models::formula::CNFClause; + use crate::solvers::BruteForce; + + vec![crate::example_db::specs::RuleExampleSpec { + id: "ksatisfiability_to_monochromatictriangle", + build: || { + let source = KSatisfiability::::new(3, vec![CNFClause::new(vec![1, 2, 3])]); + let reduction = + as ReduceTo>>::reduce_to( + &source, + ); + let target_config = BruteForce::new() + .find_witness(reduction.target_problem()) + .expect("canonical MonochromaticTriangle example must be feasible"); + let source_config = reduction.extract_solution(&target_config); + crate::example_db::specs::assemble_rule_example( + &source, + reduction.target_problem(), + vec![SolutionPair { + source_config, + target_config, + }], + ) + }, + }] +} + +#[cfg(test)] +#[path = "../unit_tests/rules/ksatisfiability_monochromatictriangle.rs"] +mod tests; diff --git a/src/rules/mod.rs b/src/rules/mod.rs index 15e84bab..0ac05ad6 100644 --- a/src/rules/mod.rs +++ b/src/rules/mod.rs @@ -51,6 +51,7 @@ pub(crate) mod ksatisfiability_directedtwocommodityintegralflow; pub(crate) mod ksatisfiability_kclique; pub(crate) mod ksatisfiability_kernel; pub(crate) mod ksatisfiability_minimumvertexcover; +pub(crate) mod ksatisfiability_monochromatictriangle; pub(crate) mod ksatisfiability_oneinthreesatisfiability; pub(crate) mod ksatisfiability_preemptivescheduling; pub(crate) mod ksatisfiability_quadraticcongruences; @@ -256,6 +257,8 @@ pub(crate) mod minmaxmulticenter_ilp; #[cfg(feature = "ilp-solver")] pub(crate) mod mixedchinesepostman_ilp; #[cfg(feature = "ilp-solver")] +pub(crate) mod monochromatictriangle_ilp; +#[cfg(feature = "ilp-solver")] pub(crate) mod multiplecopyfileallocation_ilp; #[cfg(feature = "ilp-solver")] pub(crate) mod multiprocessorscheduling_ilp; @@ -396,6 +399,7 @@ pub(crate) fn canonical_rule_example_specs() -> Vec Vec Vec, +} + +impl ReductionResult for ReductionMonochromaticTriangleToILP { + type Source = MonochromaticTriangle; + type Target = ILP; + + fn target_problem(&self) -> &Self::Target { + &self.target + } + + fn extract_solution(&self, target_solution: &[usize]) -> Vec { + target_solution.to_vec() + } +} + +#[reduction( + overhead = { + num_vars = "num_edges", + num_constraints = "2 * num_triangles", + } +)] +impl ReduceTo> for MonochromaticTriangle { + type Result = ReductionMonochromaticTriangleToILP; + + fn reduce_to(&self) -> Self::Result { + let mut constraints = Vec::with_capacity(2 * self.num_triangles()); + for triangle in self.triangles() { + let terms: Vec<(usize, f64)> = + triangle.iter().map(|&edge_idx| (edge_idx, 1.0)).collect(); + constraints.push(LinearConstraint::ge(terms.clone(), 1.0)); + constraints.push(LinearConstraint::le(terms, 2.0)); + } + + ReductionMonochromaticTriangleToILP { + target: ILP::new( + self.num_edges(), + constraints, + vec![], + ObjectiveSense::Minimize, + ), + } + } +} + +#[cfg(feature = "example-db")] +pub(crate) fn canonical_rule_example_specs() -> Vec { + use crate::topology::SimpleGraph; + + vec![crate::example_db::specs::RuleExampleSpec { + id: "monochromatictriangle_to_ilp", + build: || { + let source = MonochromaticTriangle::new(SimpleGraph::new( + 4, + vec![(0, 1), (0, 2), (0, 3), (1, 2), (1, 3), (2, 3)], + )); + crate::example_db::specs::rule_example_via_ilp::<_, bool>(source) + }, + }] +} + +#[cfg(test)] +#[path = "../unit_tests/rules/monochromatictriangle_ilp.rs"] +mod tests; diff --git a/src/unit_tests/rules/ksatisfiability_monochromatictriangle.rs b/src/unit_tests/rules/ksatisfiability_monochromatictriangle.rs new file mode 100644 index 00000000..6dfdfc69 --- /dev/null +++ b/src/unit_tests/rules/ksatisfiability_monochromatictriangle.rs @@ -0,0 +1,88 @@ +use crate::models::formula::{CNFClause, KSatisfiability}; +use crate::models::graph::MonochromaticTriangle; +use crate::rules::traits::{ReduceTo, ReductionResult}; +use crate::topology::{Graph, SimpleGraph}; +use crate::traits::Problem; +use crate::variant::K3; +use std::collections::BTreeSet; + +#[cfg(feature = "ilp-solver")] +use crate::models::algebraic::ILP; +#[cfg(feature = "ilp-solver")] +use crate::solvers::ILPSolver; + +#[test] +fn test_ksatisfiability_to_monochromatic_triangle_structure() { + let source = KSatisfiability::::new(3, vec![CNFClause::new(vec![1, 2, 3])]); + let reduction = ReduceTo::>::reduce_to(&source); + let target = reduction.target_problem(); + + assert_eq!(target.num_vertices(), 9); + assert_eq!(target.num_edges(), 12); + assert_eq!(target.triangles().len(), 4); + + let expected_edges = BTreeSet::from([ + (0, 3), + (0, 6), + (0, 7), + (1, 4), + (1, 6), + (1, 8), + (2, 5), + (2, 7), + (2, 8), + (6, 7), + (6, 8), + (7, 8), + ]); + let actual_edges: BTreeSet<_> = target + .graph() + .edges() + .into_iter() + .map(|(u, v)| if u < v { (u, v) } else { (v, u) }) + .collect(); + assert_eq!(actual_edges, expected_edges); +} + +#[test] +fn test_ksatisfiability_to_monochromatic_triangle_complement_extraction() { + let source = KSatisfiability::::new(3, vec![CNFClause::new(vec![1, 2, 3])]); + let reduction = ReduceTo::>::reduce_to(&source); + + // Negation edges all use color 1, so direct extraction gives (0,0,0), + // which does not satisfy (x1 v x2 v x3). The complement (1,1,1) does. + let target_coloring = vec![1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0]; + + assert!( + reduction.target_problem().evaluate(&target_coloring), + "the supplied target coloring must avoid monochromatic triangles" + ); + + let extracted = reduction.extract_solution(&target_coloring); + assert_eq!(extracted, vec![1, 1, 1]); + assert!(source.evaluate(&extracted)); +} + +#[cfg(feature = "ilp-solver")] +#[test] +fn test_ksatisfiability_to_monochromatic_triangle_closed_loop() { + let source = KSatisfiability::::new( + 4, + vec![ + CNFClause::new(vec![1, 2, 3]), + CNFClause::new(vec![-1, 3, 4]), + ], + ); + let reduction = ReduceTo::>::reduce_to(&source); + let mono_to_ilp = ReduceTo::>::reduce_to(reduction.target_problem()); + + let ilp_solution = ILPSolver::new() + .solve(mono_to_ilp.target_problem()) + .expect("reduced MonochromaticTriangle instance should be feasible"); + let mono_solution = mono_to_ilp.extract_solution(&ilp_solution); + + assert!(reduction.target_problem().evaluate(&mono_solution)); + + let extracted = reduction.extract_solution(&mono_solution); + assert!(source.evaluate(&extracted)); +} diff --git a/src/unit_tests/rules/monochromatictriangle_ilp.rs b/src/unit_tests/rules/monochromatictriangle_ilp.rs new file mode 100644 index 00000000..f55c96ee --- /dev/null +++ b/src/unit_tests/rules/monochromatictriangle_ilp.rs @@ -0,0 +1,82 @@ +use crate::models::algebraic::{ObjectiveSense, ILP}; +use crate::models::graph::MonochromaticTriangle; +use crate::rules::traits::{ReduceTo, ReductionResult}; +use crate::solvers::ILPSolver; +use crate::topology::SimpleGraph; +use crate::traits::Problem; + +fn k4_instance() -> MonochromaticTriangle { + MonochromaticTriangle::new(SimpleGraph::new( + 4, + vec![(0, 1), (0, 2), (0, 3), (1, 2), (1, 3), (2, 3)], + )) +} + +#[test] +fn test_monochromatic_triangle_to_ilp_structure() { + let problem = k4_instance(); + let reduction = ReduceTo::>::reduce_to(&problem); + let ilp = reduction.target_problem(); + + assert_eq!(ilp.num_vars, 6); + assert_eq!(ilp.constraints.len(), 8); + assert_eq!(ilp.objective, vec![]); + assert_eq!(ilp.sense, ObjectiveSense::Minimize); +} + +#[test] +fn test_monochromatic_triangle_to_ilp_constraint_pairs_on_single_triangle() { + let problem = MonochromaticTriangle::new(SimpleGraph::new(3, vec![(0, 1), (0, 2), (1, 2)])); + let reduction = ReduceTo::>::reduce_to(&problem); + let ilp = reduction.target_problem(); + + assert_eq!(ilp.num_vars, 3); + assert_eq!(ilp.constraints.len(), 2); + assert_eq!(ilp.constraints[0].rhs, 1.0); + assert_eq!(ilp.constraints[1].rhs, 2.0); + assert_eq!(ilp.constraints[0].terms.len(), 3); + assert_eq!(ilp.constraints[1].terms.len(), 3); +} + +#[test] +fn test_monochromatic_triangle_to_ilp_closed_loop() { + let problem = k4_instance(); + let reduction = ReduceTo::>::reduce_to(&problem); + + let ilp_solution = ILPSolver::new() + .solve(reduction.target_problem()) + .expect("K4 should admit a monochromatic-triangle-free 2-edge-coloring"); + let extracted = reduction.extract_solution(&ilp_solution); + + assert_eq!(extracted, ilp_solution); + assert!(problem.evaluate(&extracted)); +} + +#[test] +fn test_monochromatic_triangle_to_ilp_infeasible_k6() { + let mut edges = Vec::new(); + for u in 0..6 { + for v in (u + 1)..6 { + edges.push((u, v)); + } + } + let problem = MonochromaticTriangle::new(SimpleGraph::new(6, edges)); + let reduction = ReduceTo::>::reduce_to(&problem); + + assert!( + ILPSolver::new().solve(reduction.target_problem()).is_none(), + "K6 should be infeasible by R(3,3)=6" + ); +} + +#[test] +fn test_monochromatic_triangle_to_ilp_extract_solution_identity() { + let problem = k4_instance(); + let reduction = ReduceTo::>::reduce_to(&problem); + let coloring = vec![0, 0, 1, 1, 0, 1]; + + let extracted = reduction.extract_solution(&coloring); + + assert_eq!(extracted, coloring); + assert!(problem.evaluate(&extracted)); +} From 301fb488a3f9caee0691a086f79fad1f5b879e75 Mon Sep 17 00:00:00 2001 From: GiggleLiu Date: Tue, 7 Apr 2026 20:38:02 +0800 Subject: [PATCH 07/13] style: format ksatisfiability_directedtwocommodityintegralflow Co-Authored-By: Claude Opus 4.6 (1M context) --- ...bility_directedtwocommodityintegralflow.rs | 10 ++++- ...bility_directedtwocommodityintegralflow.rs | 42 ++++++++++++------- 2 files changed, 37 insertions(+), 15 deletions(-) diff --git a/src/rules/ksatisfiability_directedtwocommodityintegralflow.rs b/src/rules/ksatisfiability_directedtwocommodityintegralflow.rs index bcf39b7a..d0cde28e 100644 --- a/src/rules/ksatisfiability_directedtwocommodityintegralflow.rs +++ b/src/rules/ksatisfiability_directedtwocommodityintegralflow.rs @@ -174,7 +174,15 @@ impl ReductionResult for Reduction3SATToDirectedTwoCommodityIntegralFlow { fn extract_solution(&self, target_solution: &[usize]) -> Vec { self.variable_paths .iter() - .map(|paths| usize::from(target_solution.get(paths.lower_entry_arc).copied().unwrap_or(0) > 0)) + .map(|paths| { + usize::from( + target_solution + .get(paths.lower_entry_arc) + .copied() + .unwrap_or(0) + > 0, + ) + }) .collect() } } diff --git a/src/unit_tests/rules/ksatisfiability_directedtwocommodityintegralflow.rs b/src/unit_tests/rules/ksatisfiability_directedtwocommodityintegralflow.rs index 00c62d4f..6ed29abe 100644 --- a/src/unit_tests/rules/ksatisfiability_directedtwocommodityintegralflow.rs +++ b/src/unit_tests/rules/ksatisfiability_directedtwocommodityintegralflow.rs @@ -43,7 +43,9 @@ fn all_assignments(num_vars: usize) -> Vec> { } #[cfg(feature = "ilp-solver")] -fn solve_target_via_ilp(problem: &crate::models::graph::DirectedTwoCommodityIntegralFlow) -> Option> { +fn solve_target_via_ilp( + problem: &crate::models::graph::DirectedTwoCommodityIntegralFlow, +) -> Option> { let reduction = ReduceTo::>::reduce_to(problem); let ilp_solution = ILPSolver::new().solve(reduction.target_problem())?; let extracted = reduction.extract_solution(&ilp_solution); @@ -53,7 +55,8 @@ fn solve_target_via_ilp(problem: &crate::models::graph::DirectedTwoCommodityInte #[test] fn test_ksatisfiability_to_directedtwocommodityintegralflow_structure() { let source = issue_example(); - let reduction = ReduceTo::::reduce_to(&source); + let reduction = + ReduceTo::::reduce_to(&source); let target = reduction.target_problem(); assert_eq!(target.num_vertices(), 36); @@ -64,9 +67,11 @@ fn test_ksatisfiability_to_directedtwocommodityintegralflow_structure() { } #[test] -fn test_ksatisfiability_to_directedtwocommodityintegralflow_assignment_encoding_matches_truth_table() { +fn test_ksatisfiability_to_directedtwocommodityintegralflow_assignment_encoding_matches_truth_table( +) { let source = issue_example(); - let reduction = ReduceTo::::reduce_to(&source); + let reduction = + ReduceTo::::reduce_to(&source); let target = reduction.target_problem(); for assignment in all_assignments(source.num_vars()) { @@ -81,9 +86,11 @@ fn test_ksatisfiability_to_directedtwocommodityintegralflow_assignment_encoding_ } #[test] -fn test_ksatisfiability_to_directedtwocommodityintegralflow_extract_solution_from_encoded_witness() { +fn test_ksatisfiability_to_directedtwocommodityintegralflow_extract_solution_from_encoded_witness() +{ let source = issue_example(); - let reduction = ReduceTo::::reduce_to(&source); + let reduction = + ReduceTo::::reduce_to(&source); let assignment = vec![1, 1, 0]; let flow = reduction.encode_assignment(&assignment); @@ -95,7 +102,8 @@ fn test_ksatisfiability_to_directedtwocommodityintegralflow_extract_solution_fro #[test] fn test_ksatisfiability_to_directedtwocommodityintegralflow_closed_loop() { let source = issue_example(); - let reduction = ReduceTo::::reduce_to(&source); + let reduction = + ReduceTo::::reduce_to(&source); let target_solution = solve_target_via_ilp(reduction.target_problem()) .expect("satisfiable source instance should produce a feasible two-commodity flow"); @@ -110,7 +118,8 @@ fn test_ksatisfiability_to_directedtwocommodityintegralflow_closed_loop() { #[test] fn test_ksatisfiability_to_directedtwocommodityintegralflow_unsatisfiable() { let source = unsatisfiable_instance(); - let reduction = ReduceTo::::reduce_to(&source); + let reduction = + ReduceTo::::reduce_to(&source); let maybe_solution = solve_target_via_ilp(reduction.target_problem()); assert!( maybe_solution.is_none(), @@ -121,10 +130,9 @@ fn test_ksatisfiability_to_directedtwocommodityintegralflow_unsatisfiable() { #[test] fn test_reduction_graph_registers_ksatisfiability_to_directedtwocommodityintegralflow() { let graph = ReductionGraph::new(); - assert!(graph.has_direct_reduction_by_name( - "KSatisfiability", - "DirectedTwoCommodityIntegralFlow", - )); + assert!( + graph.has_direct_reduction_by_name("KSatisfiability", "DirectedTwoCommodityIntegralFlow",) + ); } #[cfg(feature = "example-db")] @@ -138,8 +146,14 @@ fn test_ksatisfiability_to_directedtwocommodityintegralflow_canonical_example_sp assert_eq!(example.source.problem, "KSatisfiability"); assert_eq!(example.target.problem, "DirectedTwoCommodityIntegralFlow"); - assert_eq!(example.target.instance["requirement_1"], serde_json::json!(1)); - assert_eq!(example.target.instance["requirement_2"], serde_json::json!(2)); + assert_eq!( + example.target.instance["requirement_1"], + serde_json::json!(1) + ); + assert_eq!( + example.target.instance["requirement_2"], + serde_json::json!(2) + ); assert_eq!(example.solutions.len(), 1); assert_eq!(example.solutions[0].source_config, vec![1, 1, 0]); From c6c20b7aab900d8f353d4240951cf19647fe6e47 Mon Sep 17 00:00:00 2001 From: GiggleLiu Date: Tue, 7 Apr 2026 23:01:22 +0800 Subject: [PATCH 08/13] feat: add proof-only mvc to mmm rule --- docs/paper/reductions.typ | 47 ++++++++++- ...nimumvertexcover_minimummaximalmatching.rs | 68 +++++++++++++++ src/rules/mod.rs | 2 + src/rules/registry.rs | 8 ++ src/unit_tests/example_db.rs | 54 ++++++++++-- src/unit_tests/reduction_graph.rs | 22 +++++ ...nimumvertexcover_minimummaximalmatching.rs | 83 +++++++++++++++++++ src/unit_tests/rules/registry.rs | 5 ++ 8 files changed, 278 insertions(+), 11 deletions(-) create mode 100644 src/rules/minimumvertexcover_minimummaximalmatching.rs create mode 100644 src/unit_tests/rules/minimumvertexcover_minimummaximalmatching.rs diff --git a/docs/paper/reductions.typ b/docs/paper/reductions.typ index 61e5b9af..83b38209 100644 --- a/docs/paper/reductions.typ +++ b/docs/paper/reductions.typ @@ -530,7 +530,7 @@ ] #block(width: 100%, inset: (x: 2em, y: 1em))[ - *Abstract.* We present formal definitions for computational problems and polynomial-time reductions implemented in the `problem-reductions` library. For each reduction, we state theorems with constructive proofs that preserve solution structure. + *Abstract.* We present formal definitions for computational problems and polynomial-time reductions implemented in the `problem-reductions` library. For each reduction, we state a theorem with a constructive proof; when a reduction is proof-only rather than solver-executable, that restriction is stated explicitly in the rule text. ] @@ -541,7 +541,7 @@ = Introduction -A _reduction_ from problem $A$ to problem $B$, denoted $A arrow.long B$, is a polynomial-time transformation of $A$-instances into $B$-instances such that: (1) the transformation runs in polynomial time, (2) solutions to $B$ can be efficiently mapped back to solutions of $A$, and (3) optimal solutions are preserved. The library implements #graph-data.edges.len() reductions connecting #graph-data.nodes.len() problem types. +A _reduction_ from problem $A$ to problem $B$, denoted $A arrow.long B$, is a polynomial-time transformation of $A$-instances into $B$-instances such that: (1) the transformation runs in polynomial time, (2) solutions to $B$ can be efficiently mapped back to solutions of $A$, and (3) optimal solutions are preserved. The library implements #graph-data.edges.len() catalogued edges connecting #graph-data.nodes.len() problem types; most are solver-executable witness, aggregate, or Turing reductions, while a few are proof-only NP-hardness embeddings that are excluded from runtime path search. == Notation @@ -9237,6 +9237,49 @@ Each reduction is presented as a *Rule* (with linked problem names and overhead _Solution extraction._ For IS solution $S$, return $C = V backslash S$, i.e.\ flip each variable: $c_v = 1 - s_v$. ] +#let mvc_mmm = load-example("MinimumVertexCover", "MinimumMaximalMatching") +#let mvc_mmm_sol = mvc_mmm.solutions.at(0) +#reduction-rule("MinimumVertexCover", "MinimumMaximalMatching", + example: true, + example-caption: [Cycle $C_5$: the forward implication is exact, but the backward gap is strict], + extra: [ + #{ + let target-edges = mvc_mmm.target.instance.graph.edges + let source-cover = mvc_mmm_sol.source_config.enumerate().filter(((i, x)) => x == 1).map(((i, x)) => i) + let matching = mvc_mmm_sol.target_config.enumerate().filter(((i, x)) => x == 1).map(((i, x)) => target-edges.at(i)) + let fmt-edge(e) = "(" + str(e.at(0)) + ", " + str(e.at(1)) + ")" + [ + #pred-commands( + "pred create MinimumVertexCover --graph 0-1,1-2,2-3,3-4,4-0 --weights 1,1,1,1,1 -o mvc.json", + "pred solve mvc.json", + "pred create MinimumMaximalMatching --graph 0-1,1-2,2-3,3-4,4-0 -o mmm.json", + "pred solve mmm.json", + ) + + *Step 1 -- Shared instance.* Both problems use the same 5-cycle, so $n = #graph-num-vertices(mvc_mmm.source.instance)$ and $|E| = #graph-num-edges(mvc_mmm.source.instance)$. + + *Step 2 -- Source optimum.* The canonical minimum vertex cover is $C = {#source-cover.map(str).join(", ")}$, so $"mvc"(C_5) = #source-cover.len() = 3$. + + *Step 3 -- Target optimum.* The canonical minimum maximal matching is $M = {#matching.map(fmt-edge).join(", ")}$, so $"mmm"(C_5) = #matching.len() = 2$. + + *Step 4 -- Backward gap.* The endpoint set of $M$ is ${0, 1, 2, 3}$, a valid vertex cover of size $4$. Pruning can recover an optimal cover of size $3$, but not one of size $2$, so the same-bound backward implication fails. + + *Runtime note:* This catalog edge is proof-only. The CLI can solve the two instances separately, but runtime reduction search does not traverse this edge because there is no exact witness or aggregate extractor. + ] + } + ], +)[ + This size-preserving identity map records the forward implication used in the classical NP-hardness proof for Minimum Maximal Matching (equivalently, Minimum Edge Dominating Set) on bounded-degree graphs: every unit-weight vertex cover of $G$ can be greedily converted into a maximal matching of size at most the cover size. The converse loses a factor of two in general, so the edge is documented but intentionally disabled for runtime reduction search. +][ + _Construction._ Given a unit-weight Minimum Vertex Cover instance $(G = (V, E), K)$, build the Minimum Maximal Matching instance on the same graph $G$. The target uses one binary variable per source edge, so the graph structure and size fields are unchanged. + + _Correctness._ ($arrow.r.double$) Let $C subset.eq V$ be a vertex cover with $|C| lt.eq K$. Start with $M = emptyset$ and process the vertices of $C$ in arbitrary order. Whenever $v in C$ is unmatched, choose any edge $\{v, u\} in E$ whose other endpoint $u$ is also unmatched, add that edge to $M$, and mark both endpoints matched. Because only unmatched endpoints are paired, $M$ is a matching. If some edge $\{x, y\} in E$ were disjoint from every edge of $M$ at the end, then both $x$ and $y$ would still be unmatched. Since $C$ covers every edge, at least one endpoint, say $x$, lies in $C$, and when the algorithm processed $x$ it could have added $\{x, y\}$, a contradiction. Hence $M$ is maximal and $|M| lt.eq |C| lt.eq K$. + + ($arrow.l.double$) Let $M$ be any maximal matching. The set of all endpoints of edges in $M$ is a vertex cover, so $"mvc"(G) lt.eq 2 dot |M|$. This yields the standard bound $"mmm"(G) lt.eq "mvc"(G) lt.eq 2 dot "mmm"(G)$, but it does not recover an exact same-bound inverse. On $C_5$, the target optimum is $2$ while the source optimum is $3$. + + _Solution extraction._ No runtime extractor is registered. The endpoint map always returns a valid vertex cover and greedy pruning can shrink it, but neither approach guarantees an optimal cover from an optimal maximal matching witness, and the target optimum value does not determine the source optimum value exactly. +] + #let mvc_lcs = load-example("MinimumVertexCover", "LongestCommonSubsequence") #let mvc_lcs_sol = mvc_lcs.solutions.at(0) #reduction-rule("MinimumVertexCover", "LongestCommonSubsequence", diff --git a/src/rules/minimumvertexcover_minimummaximalmatching.rs b/src/rules/minimumvertexcover_minimummaximalmatching.rs new file mode 100644 index 00000000..3556e510 --- /dev/null +++ b/src/rules/minimumvertexcover_minimummaximalmatching.rs @@ -0,0 +1,68 @@ +//! Forward-only reduction from MinimumVertexCover (unit-weight) to +//! MinimumMaximalMatching. +//! +//! The construction is the identity map on the underlying graph. This edge is +//! registered for topology and documentation purposes only: it intentionally has +//! no witness, aggregate, or Turing execution capability because an optimal +//! maximal matching does not determine an optimal vertex cover in general +//! (for example, on `C5`, `mmm(G) = 2` but `mvc(G) = 3`). + +use crate::models::graph::{MinimumMaximalMatching, MinimumVertexCover}; +use crate::rules::{EdgeCapabilities, ReductionEntry, ReductionOverhead}; +use crate::topology::SimpleGraph; +use crate::traits::Problem; +use crate::types::{One, ProblemSize}; +use std::any::Any; + +fn source_problem_size(any: &dyn Any) -> ProblemSize { + let source = any + .downcast_ref::>() + .expect("MinimumVertexCover -> MinimumMaximalMatching source type mismatch"); + ProblemSize::new(vec![ + ("num_vertices", source.num_vertices()), + ("num_edges", source.num_edges()), + ]) +} + +inventory::submit! { + ReductionEntry { + source_name: MinimumVertexCover::::NAME, + target_name: MinimumMaximalMatching::::NAME, + source_variant_fn: as Problem>::variant, + target_variant_fn: as Problem>::variant, + overhead_fn: || ReductionOverhead::identity(&["num_vertices", "num_edges"]), + module_path: module_path!(), + reduce_fn: None, + reduce_aggregate_fn: None, + capabilities: EdgeCapabilities::none(), + overhead_eval_fn: source_problem_size, + source_size_fn: source_problem_size, + } +} + +#[cfg(feature = "example-db")] +pub(crate) fn canonical_rule_example_specs() -> Vec { + use crate::example_db::specs::assemble_rule_example; + use crate::export::SolutionPair; + + vec![crate::example_db::specs::RuleExampleSpec { + id: "minimumvertexcover_to_minimummaximalmatching", + build: || { + let edges = vec![(0, 1), (1, 2), (2, 3), (3, 4), (4, 0)]; + let source = MinimumVertexCover::new(SimpleGraph::new(5, edges.clone()), vec![One; 5]); + let target = MinimumMaximalMatching::new(SimpleGraph::new(5, edges)); + assemble_rule_example( + &source, + &target, + vec![SolutionPair { + source_config: vec![1, 1, 0, 1, 0], + target_config: vec![1, 0, 1, 0, 0], + }], + ) + }, + }] +} + +#[cfg(test)] +#[path = "../unit_tests/rules/minimumvertexcover_minimummaximalmatching.rs"] +mod tests; diff --git a/src/rules/mod.rs b/src/rules/mod.rs index 0ac05ad6..c13a3f66 100644 --- a/src/rules/mod.rs +++ b/src/rules/mod.rs @@ -79,6 +79,7 @@ pub(crate) mod minimumvertexcover_maximumindependentset; pub(crate) mod minimumvertexcover_minimumfeedbackarcset; pub(crate) mod minimumvertexcover_minimumfeedbackvertexset; pub(crate) mod minimumvertexcover_minimumhittingset; +pub(crate) mod minimumvertexcover_minimummaximalmatching; pub(crate) mod minimumvertexcover_minimumsetcovering; pub(crate) mod naesatisfiability_maxcut; pub(crate) mod naesatisfiability_partitionintoperfectmatchings; @@ -448,6 +449,7 @@ pub(crate) fn canonical_rule_example_specs() -> Vec Self { + Self { + witness: false, + aggregate: false, + turing: false, + } + } + pub const fn witness_only() -> Self { Self { witness: true, diff --git a/src/unit_tests/example_db.rs b/src/unit_tests/example_db.rs index 04d4751e..dcd40932 100644 --- a/src/unit_tests/example_db.rs +++ b/src/unit_tests/example_db.rs @@ -586,7 +586,9 @@ fn rule_specs_solution_pairs_are_consistent() { ) .unwrap_or_else(|e| panic!("Failed to load target for {label}: {e}")); - // Try witness path first; fall back to aggregate for aggregate-only edges + // Try witness path first; fall back to aggregate for aggregate-only edges. + // Some authored direct reductions are proof-only and intentionally have + // no runtime capability in any mode. let witness_path = graph.find_cheapest_path( &example.source.problem, &example.source.variant, @@ -595,10 +597,8 @@ fn rule_specs_solution_pairs_are_consistent() { &crate::types::ProblemSize::new(vec![]), &crate::rules::MinimizeSteps, ); - let aggregate_only = witness_path.is_none(); - if aggregate_only { - // Verify the aggregate path exists - let agg_path = graph.find_cheapest_path_mode( + if witness_path.is_none() { + let aggregate_path = graph.find_cheapest_path_mode( &example.source.problem, &example.source.variant, &example.target.problem, @@ -607,10 +607,28 @@ fn rule_specs_solution_pairs_are_consistent() { &crate::types::ProblemSize::new(vec![]), &crate::rules::MinimizeSteps, ); - assert!( - agg_path.is_some(), - "No reduction path (witness or aggregate) for {label}" - ); + if aggregate_path.is_none() { + assert!( + graph.has_direct_reduction_by_name(&example.source.problem, &example.target.problem), + "No reduction path (witness or aggregate) or direct proof-only edge for {label}" + ); + assert!( + !graph.has_direct_reduction_by_name_mode( + &example.source.problem, + &example.target.problem, + crate::rules::ReductionMode::Witness, + ), + "Proof-only edge unexpectedly exposed witness mode for {label}" + ); + assert!( + !graph.has_direct_reduction_by_name_mode( + &example.source.problem, + &example.target.problem, + crate::rules::ReductionMode::Aggregate, + ), + "Proof-only edge unexpectedly exposed aggregate mode for {label}" + ); + } } // Only do witness round-trip when a witness path exists @@ -1021,6 +1039,24 @@ fn test_find_rule_example_minimumvertexcover_to_minimumhittingset() { assert_eq!(example.target.problem, "MinimumHittingSet"); } +#[test] +fn test_find_rule_example_minimumvertexcover_to_minimummaximalmatching() { + let source = ProblemRef { + name: "MinimumVertexCover".to_string(), + variant: BTreeMap::from([ + ("graph".to_string(), "SimpleGraph".to_string()), + ("weight".to_string(), "One".to_string()), + ]), + }; + let target = ProblemRef { + name: "MinimumMaximalMatching".to_string(), + variant: BTreeMap::from([("graph".to_string(), "SimpleGraph".to_string())]), + }; + let example = find_rule_example(&source, &target).unwrap(); + assert_eq!(example.source.problem, "MinimumVertexCover"); + assert_eq!(example.target.problem, "MinimumMaximalMatching"); +} + #[test] fn test_find_rule_example_pp2_to_boundedcomponentspanningforest() { let source = ProblemRef { diff --git a/src/unit_tests/reduction_graph.rs b/src/unit_tests/reduction_graph.rs index 590b40e7..fbc7a638 100644 --- a/src/unit_tests/reduction_graph.rs +++ b/src/unit_tests/reduction_graph.rs @@ -702,6 +702,28 @@ fn test_has_direct_reduction_by_name_mode() { )); } +#[test] +fn test_minimumvertexcover_to_minimummaximalmatching_is_proof_only_direct_edge() { + let graph = ReductionGraph::new(); + + assert!(graph.has_direct_reduction_by_name("MinimumVertexCover", "MinimumMaximalMatching",)); + assert!(!graph.has_direct_reduction_by_name_mode( + "MinimumVertexCover", + "MinimumMaximalMatching", + ReductionMode::Witness, + )); + assert!(!graph.has_direct_reduction_by_name_mode( + "MinimumVertexCover", + "MinimumMaximalMatching", + ReductionMode::Aggregate, + )); + assert!(!graph.has_direct_reduction_by_name_mode( + "MinimumVertexCover", + "MinimumMaximalMatching", + ReductionMode::Turing, + )); +} + #[test] fn test_find_all_paths_mode_witness() { let graph = ReductionGraph::new(); diff --git a/src/unit_tests/rules/minimumvertexcover_minimummaximalmatching.rs b/src/unit_tests/rules/minimumvertexcover_minimummaximalmatching.rs new file mode 100644 index 00000000..624d75f2 --- /dev/null +++ b/src/unit_tests/rules/minimumvertexcover_minimummaximalmatching.rs @@ -0,0 +1,83 @@ +use crate::models::graph::{MinimumMaximalMatching, MinimumVertexCover}; +use crate::rules::{ReductionGraph, ReductionMode}; +use crate::solvers::{BruteForce, Solver}; +use crate::topology::SimpleGraph; +use crate::types::{Min, One}; + +fn graph_from_mask(n: usize, mask: usize) -> SimpleGraph { + let mut edges = Vec::new(); + let mut bit = 0usize; + for u in 0..n { + for v in (u + 1)..n { + if (mask >> bit) & 1 == 1 { + edges.push((u, v)); + } + bit += 1; + } + } + SimpleGraph::new(n, edges) +} + +#[test] +fn test_minimumvertexcover_to_minimummaximalmatching_c5_gap() { + let graph = SimpleGraph::new(5, vec![(0, 1), (1, 2), (2, 3), (3, 4), (4, 0)]); + let mvc = MinimumVertexCover::new(graph.clone(), vec![One; 5]); + let mmm = MinimumMaximalMatching::new(graph); + let solver = BruteForce::new(); + + assert_eq!(solver.solve(&mvc), Min(Some(3))); + assert_eq!(solver.solve(&mmm), Min(Some(2))); +} + +#[test] +fn test_minimumvertexcover_to_minimummaximalmatching_forward_bound_on_small_graphs() { + let solver = BruteForce::new(); + + for n in 0usize..=5 { + let num_possible_edges = n * (n.saturating_sub(1)) / 2; + for mask in 0usize..(1usize << num_possible_edges) { + let graph = graph_from_mask(n, mask); + let mvc = MinimumVertexCover::new(graph.clone(), vec![One; n]); + let mmm = MinimumMaximalMatching::new(graph); + let mvc_value = solver.solve(&mvc); + let mmm_value = solver.solve(&mmm); + + let Min(Some(mvc_size)) = mvc_value else { + panic!("MinimumVertexCover should always have an optimal solution"); + }; + let Min(Some(mmm_size)) = mmm_value else { + panic!("MinimumMaximalMatching should always have an optimal solution"); + }; + let mvc_size: usize = mvc_size + .try_into() + .expect("unit-weight MVC optimum should fit into usize"); + + assert!( + mmm_size <= mvc_size, + "expected mmm(G) <= mvc(G) for n={n}, mask={mask:#b}, got {mmm_size} > {mvc_size}", + ); + } + } +} + +#[test] +fn test_minimumvertexcover_to_minimummaximalmatching_has_no_runtime_modes() { + let graph = ReductionGraph::new(); + + assert!(graph.has_direct_reduction_by_name("MinimumVertexCover", "MinimumMaximalMatching",)); + assert!(!graph.has_direct_reduction_by_name_mode( + "MinimumVertexCover", + "MinimumMaximalMatching", + ReductionMode::Witness, + )); + assert!(!graph.has_direct_reduction_by_name_mode( + "MinimumVertexCover", + "MinimumMaximalMatching", + ReductionMode::Aggregate, + )); + assert!(!graph.has_direct_reduction_by_name_mode( + "MinimumVertexCover", + "MinimumMaximalMatching", + ReductionMode::Turing, + )); +} diff --git a/src/unit_tests/rules/registry.rs b/src/unit_tests/rules/registry.rs index 3fdef0c9..eeabcf01 100644 --- a/src/unit_tests/rules/registry.rs +++ b/src/unit_tests/rules/registry.rs @@ -472,6 +472,11 @@ fn test_edge_capabilities_constructors() { let both = EdgeCapabilities::both(); assert!(both.witness); assert!(both.aggregate); + + let none = EdgeCapabilities::none(); + assert!(!none.witness); + assert!(!none.aggregate); + assert!(!none.turing); } #[test] From 0bcdd29da9f8f9edbe740421a045b022be47637a Mon Sep 17 00:00:00 2001 From: GiggleLiu Date: Tue, 7 Apr 2026 23:18:47 +0800 Subject: [PATCH 09/13] feat: add MinimumCoveringByCliques to ILP --- docs/paper/reductions.typ | 22 +++ src/rules/minimumcoveringbycliques_ilp.rs | 155 ++++++++++++++++++ src/rules/mod.rs | 3 + src/unit_tests/reduction_graph.rs | 12 ++ .../rules/minimumcoveringbycliques_ilp.rs | 62 +++++++ tests/suites/reductions.rs | 26 +++ 6 files changed, 280 insertions(+) create mode 100644 src/rules/minimumcoveringbycliques_ilp.rs create mode 100644 src/unit_tests/rules/minimumcoveringbycliques_ilp.rs diff --git a/docs/paper/reductions.typ b/docs/paper/reductions.typ index 83b38209..bafd0534 100644 --- a/docs/paper/reductions.typ +++ b/docs/paper/reductions.typ @@ -11495,6 +11495,28 @@ The following reductions to Integer Linear Programming are straightforward formu _Solution extraction._ $M = {e : x_e = 1}$. ] +#reduction-rule("MinimumCoveringByCliques", "ILP")[ + Use one potential clique slot per source edge, with binary vertex-membership, slot-activation, and edge-covered-by-slot variables. +][ + _Construction._ Let $m = |E|$ and index the clique slots by $k in {0, dots, m-1}$. Introduce binary variables $x_(v,k)$ for $v in V$ and $k in {0, dots, m-1}$, where $x_(v,k) = 1$ means vertex $v$ is placed in clique slot $k$; binary activation variables $z_k$; and binary variables $y_(e,k)$ for $e = {u, v} in E$, where $y_(e,k) = 1$ means edge $e$ is covered by slot $k$. The ILP is: + $ + "minimize" quad & sum_(k=0)^(m-1) z_k \ + "subject to" quad & x_(u,k) + x_(v,k) <= 1 quad forall k,\ forall {u, v} in.not E \ + & x_(v,k) <= z_k quad forall v in V,\ forall k \ + & y_({u,v},k) <= x_(u,k) quad forall {u,v} in E,\ forall k \ + & y_({u,v},k) <= x_(v,k) quad forall {u,v} in E,\ forall k \ + & y_({u,v},k) >= x_(u,k) + x_(v,k) - 1 quad forall {u,v} in E,\ forall k \ + & sum_(k=0)^(m-1) y_(e,k) >= 1 quad forall e in E \ + & x_(v,k), z_k, y_(e,k) in {0, 1} + $. + + _Correctness._ ($arrow.r.double$) Given an edge-clique cover $C_0, dots, C_(t-1)$ with $t <= m$, map clique $C_k$ to slot $k$: set $z_k = 1$, set $x_(v,k) = 1$ exactly for $v in C_k$, and set $y_(e,k) = 1$ exactly for the edges $e$ whose endpoints both lie in $C_k$. Because each $C_k$ is a clique, no non-edge constraint is violated. Every covered edge satisfies at least one coverage inequality, so the ILP objective is at most $t$. + + ($arrow.l.double$) Conversely, let $(x, z, y)$ be any feasible ILP solution. For each slot $k$, the vertices with $x_(v,k) = 1$ form a clique because every non-edge pair is forbidden from appearing together in that slot. If $y_({u,v},k) = 1$, the McCormick constraints force both endpoints $u$ and $v$ into slot $k$, so the edge is indeed contained in that clique. The coverage inequalities therefore certify that every source edge lies in at least one clique slot, giving a valid edge-clique cover. Since the objective counts active slots, minimizing it yields a minimum cover. + + _Solution extraction._ For each source edge $e$, choose any slot $k$ with $y_(e,k) = 1$ and output the label $k$. The extracted edge-to-slot labeling is valid because every slot induces a clique and every edge is assigned to at least one covering slot. +] + #reduction-rule("PartiallyOrderedKnapsack", "ILP")[ Standard knapsack with precedence constraints: item $b$ can only be selected if item $a$ is also selected for each precedence $(a, b)$. ][ diff --git a/src/rules/minimumcoveringbycliques_ilp.rs b/src/rules/minimumcoveringbycliques_ilp.rs new file mode 100644 index 00000000..52c64311 --- /dev/null +++ b/src/rules/minimumcoveringbycliques_ilp.rs @@ -0,0 +1,155 @@ +//! Reduction from MinimumCoveringByCliques to ILP. +//! +//! We use one potential clique slot per source edge, matching the source-model +//! encoding where each edge is assigned a group label in `[0, |E|)`. +//! +//! Variables: +//! - `x_(v,k)`: vertex `v` is selected into clique slot `k` +//! - `z_k`: clique slot `k` is active +//! - `y_(e,k)`: edge `e = {u,v}` is covered by slot `k`, linearized as +//! `x_(u,k) * x_(v,k)` +//! +//! Constraints: +//! - Non-edges cannot appear together in the same clique slot +//! - `x_(v,k) <= z_k` +//! - Every edge is covered by at least one clique slot +//! - McCormick constraints enforce `y_(e,k) = x_(u,k) * x_(v,k)` +//! +//! Objective: minimize the number of active clique slots. + +use crate::models::algebraic::{LinearConstraint, ObjectiveSense, ILP}; +use crate::models::graph::MinimumCoveringByCliques; +use crate::reduction; +use crate::rules::ilp_helpers::mccormick_product; +use crate::rules::traits::{ReduceTo, ReductionResult}; +use crate::topology::{Graph, SimpleGraph}; + +#[derive(Debug, Clone)] +pub struct ReductionMinimumCoveringByCliquesToILP { + target: ILP, + num_edges: usize, + y_offset: usize, +} + +impl ReductionResult for ReductionMinimumCoveringByCliquesToILP { + type Source = MinimumCoveringByCliques; + type Target = ILP; + + fn target_problem(&self) -> &ILP { + &self.target + } + + fn extract_solution(&self, target_solution: &[usize]) -> Vec { + if self.num_edges == 0 { + return vec![]; + } + + (0..self.num_edges) + .map(|edge_idx| { + (0..self.num_edges) + .find(|&slot| { + target_solution[self.y_offset + edge_idx * self.num_edges + slot] == 1 + }) + .unwrap_or(0) + }) + .collect() + } +} + +#[reduction( + overhead = { + num_vars = "num_vertices * num_edges + num_edges + num_edges * num_edges", + num_constraints = "num_vertices * num_edges + (num_vertices * (num_vertices - 1) / 2 - num_edges) * num_edges + 3 * num_edges * num_edges + num_edges", + } +)] +impl ReduceTo> for MinimumCoveringByCliques { + type Result = ReductionMinimumCoveringByCliquesToILP; + + fn reduce_to(&self) -> Self::Result { + let graph = self.graph(); + let num_vertices = graph.num_vertices(); + let edges = graph.edges(); + let num_edges = edges.len(); + let num_slots = num_edges; + + let x_idx = |vertex: usize, slot: usize| -> usize { vertex * num_slots + slot }; + let z_offset = num_vertices * num_slots; + let z_idx = |slot: usize| -> usize { z_offset + slot }; + let y_offset = z_offset + num_slots; + let y_idx = + |edge_idx: usize, slot: usize| -> usize { y_offset + edge_idx * num_slots + slot }; + + let mut constraints = Vec::new(); + + for slot in 0..num_slots { + for u in 0..num_vertices { + constraints.push(LinearConstraint::le( + vec![(x_idx(u, slot), 1.0), (z_idx(slot), -1.0)], + 0.0, + )); + } + } + + for slot in 0..num_slots { + for u in 0..num_vertices { + for v in (u + 1)..num_vertices { + if !graph.has_edge(u, v) { + constraints.push(LinearConstraint::le( + vec![(x_idx(u, slot), 1.0), (x_idx(v, slot), 1.0)], + 1.0, + )); + } + } + } + } + + for (edge_idx, &(u, v)) in edges.iter().enumerate() { + for slot in 0..num_slots { + constraints.extend(mccormick_product( + y_idx(edge_idx, slot), + x_idx(u, slot), + x_idx(v, slot), + )); + } + } + + for edge_idx in 0..num_edges { + let terms: Vec<(usize, f64)> = (0..num_slots) + .map(|slot| (y_idx(edge_idx, slot), 1.0)) + .collect(); + constraints.push(LinearConstraint::ge(terms, 1.0)); + } + + let objective: Vec<(usize, f64)> = (0..num_slots).map(|slot| (z_idx(slot), 1.0)).collect(); + let target = ILP::new( + y_offset + num_edges * num_slots, + constraints, + objective, + ObjectiveSense::Minimize, + ); + + ReductionMinimumCoveringByCliquesToILP { + target, + num_edges, + y_offset, + } + } +} + +#[cfg(feature = "example-db")] +pub(crate) fn canonical_rule_example_specs() -> Vec { + vec![crate::example_db::specs::RuleExampleSpec { + id: "minimumcoveringbycliques_to_ilp", + build: || { + let source = MinimumCoveringByCliques::new(SimpleGraph::new( + 4, + vec![(0, 1), (0, 2), (0, 3), (1, 2), (2, 3)], + )); + crate::example_db::specs::rule_example_via_ilp::<_, bool>(source) + }, + }] +} + +#[cfg(test)] +#[path = "../unit_tests/rules/minimumcoveringbycliques_ilp.rs"] +mod tests; diff --git a/src/rules/mod.rs b/src/rules/mod.rs index c13a3f66..1fd5c787 100644 --- a/src/rules/mod.rs +++ b/src/rules/mod.rs @@ -220,6 +220,8 @@ pub(crate) mod maximumsetpacking_ilp; #[cfg(feature = "ilp-solver")] pub(crate) mod minimumcapacitatedspanningtree_ilp; #[cfg(feature = "ilp-solver")] +pub(crate) mod minimumcoveringbycliques_ilp; +#[cfg(feature = "ilp-solver")] pub(crate) mod minimumcutintoboundedsets_ilp; #[cfg(feature = "ilp-solver")] pub(crate) mod minimumdominatingset_ilp; @@ -529,6 +531,7 @@ pub(crate) fn canonical_rule_example_specs() -> Vec>::reduce_to(&source); + let ilp = reduction.target_problem(); + + assert_eq!(ilp.num_vars, 12); + assert_eq!(ilp.constraints.len(), 22); + assert_eq!(ilp.sense, ObjectiveSense::Minimize); +} + +#[test] +fn test_minimumcoveringbycliques_to_ilp_closed_loop() { + let source = MinimumCoveringByCliques::new(SimpleGraph::new( + 4, + vec![(0, 1), (0, 2), (0, 3), (1, 2), (2, 3)], + )); + let reduction: ReductionMinimumCoveringByCliquesToILP = + ReduceTo::>::reduce_to(&source); + + let bf_value = BruteForce::new().solve(&source); + let ilp_solution = ILPSolver::new() + .solve(reduction.target_problem()) + .expect("ILP should be solvable"); + let extracted = reduction.extract_solution(&ilp_solution); + + assert_eq!(source.evaluate(&extracted), Min(Some(2))); + assert_eq!(source.evaluate(&extracted), bf_value); +} + +#[test] +fn test_minimumcoveringbycliques_to_ilp_empty_graph() { + let source = MinimumCoveringByCliques::new(SimpleGraph::new(3, vec![])); + let reduction: ReductionMinimumCoveringByCliquesToILP = + ReduceTo::>::reduce_to(&source); + let ilp = reduction.target_problem(); + + assert_eq!(ilp.num_vars, 0); + assert_eq!(ilp.constraints.len(), 0); + assert_eq!(reduction.extract_solution(&[]), Vec::::new()); + assert_eq!(source.evaluate(&[]), Min(Some(0))); +} + +#[test] +fn test_minimumcoveringbycliques_to_ilp_bf_vs_ilp() { + let source = MinimumCoveringByCliques::new(SimpleGraph::new( + 4, + vec![(0, 1), (0, 2), (0, 3), (1, 2), (2, 3)], + )); + let reduction: ReductionMinimumCoveringByCliquesToILP = + ReduceTo::>::reduce_to(&source); + crate::rules::test_helpers::assert_bf_vs_ilp(&source, &reduction); +} diff --git a/tests/suites/reductions.rs b/tests/suites/reductions.rs index 453f7baf..3e1d4457 100644 --- a/tests/suites/reductions.rs +++ b/tests/suites/reductions.rs @@ -4,9 +4,12 @@ //! solutions can be properly extracted through the reduction pipeline. use problemreductions::models::algebraic::{LinearConstraint, ObjectiveSense, ILP}; +use problemreductions::models::graph::MinimumCoveringByCliques; use problemreductions::prelude::*; use problemreductions::rules::{Minimize, ReductionGraph}; +use problemreductions::solvers::ILPSolver; use problemreductions::topology::{Graph, SimpleGraph}; +use problemreductions::types::Min; use problemreductions::variant::{K2, K3}; /// Tests for MaximumIndependentSet <-> MinimumVertexCover reductions. @@ -295,6 +298,29 @@ mod sg_qubo_reductions { } } +/// Tests for MinimumCoveringByCliques -> ILP reductions. +#[cfg(feature = "ilp-solver")] +mod minimum_covering_by_cliques_ilp_reductions { + use super::*; + + #[test] + fn test_covering_by_cliques_to_ilp_closed_loop() { + let source = + MinimumCoveringByCliques::new(SimpleGraph::new(4, vec![(0, 1), (1, 2), (2, 3)])); + + let reduction = + as ReduceTo>>::reduce_to(&source); + let ilp = reduction.target_problem(); + + let ilp_solution = ILPSolver::new() + .solve(ilp) + .expect("MinimumCoveringByCliques -> ILP should be solvable"); + let extracted = reduction.extract_solution(&ilp_solution); + + assert_eq!(source.evaluate(&extracted), Min(Some(3))); + } +} + /// Tests for Maximum2Satisfiability -> MaxCut reductions. mod max2sat_maxcut_reductions { use super::*; From 44999696e7412535bdda2e5e9f559b3a8d0cd0a2 Mon Sep 17 00:00:00 2001 From: GiggleLiu Date: Tue, 7 Apr 2026 23:42:51 +0800 Subject: [PATCH 10/13] feat: add SubsetSum and IntegerKnapsack reductions --- docs/paper/reductions.typ | 110 ++++++++++++++++++ src/rules/integerknapsack_ilp.rs | 87 ++++++++++++++ src/rules/mod.rs | 6 + src/rules/subsetsum_integerknapsack.rs | 109 +++++++++++++++++ src/unit_tests/reduction_graph.rs | 34 ++++++ src/unit_tests/rules/integerknapsack_ilp.rs | 97 +++++++++++++++ .../rules/subsetsum_integerknapsack.rs | 92 +++++++++++++++ 7 files changed, 535 insertions(+) create mode 100644 src/rules/integerknapsack_ilp.rs create mode 100644 src/rules/subsetsum_integerknapsack.rs create mode 100644 src/unit_tests/rules/integerknapsack_ilp.rs create mode 100644 src/unit_tests/rules/subsetsum_integerknapsack.rs diff --git a/docs/paper/reductions.typ b/docs/paper/reductions.typ index bafd0534..d55ce9b8 100644 --- a/docs/paper/reductions.typ +++ b/docs/paper/reductions.typ @@ -10795,6 +10795,63 @@ The following reductions to Integer Linear Programming are straightforward formu _Solution extraction._ Identity: return the binary variable vector $bold(x)$ as the knapsack selection. ] +#let ik_ilp = load-example("IntegerKnapsack", "ILP") +#let ik_ilp_sol = ik_ilp.solutions.at(0) +#reduction-rule("IntegerKnapsack", "ILP", + example: true, + example-caption: [$n = #ik_ilp.source.instance.sizes.len()$ items, capacity $B = #ik_ilp.source.instance.capacity$], + extra: [ + #{ + let sizes = ik_ilp.source.instance.sizes + let values = ik_ilp.source.instance.values + let B = ik_ilp.source.instance.capacity + let upper = sizes.map(s => calc.floor(B / s)) + let chosen = ik_ilp_sol.source_config.enumerate().filter(((i, c)) => c > 0) + let total_size = chosen.map(((i, c)) => c * sizes.at(i)).sum() + let total_value = chosen.map(((i, c)) => c * values.at(i)).sum() + [ + #pred-commands( + "pred create --example " + problem-spec(ik_ilp.source) + " -o integer-knapsack.json", + "pred reduce integer-knapsack.json --to " + target-spec(ik_ilp) + " -o bundle.json", + "pred solve bundle.json", + "pred evaluate integer-knapsack.json --config " + ik_ilp_sol.source_config.map(str).join(","), + ) + + *Step 1 -- Source instance.* The canonical Integer Knapsack instance has sizes $(#sizes.map(str).join(", "))$, values $(#values.map(str).join(", "))$, and capacity $B = #B$. + + *Step 2 -- Build the ILP.* Introduce one integer variable per item multiplicity: + $#range(sizes.len()).map(i => $c_#i$).join(", ") in NN$. + The capacity constraint is + $ #sizes.enumerate().map(((i, s)) => $#s c_#i$).join($+$) <= #B $, + and the explicit upper bounds are $(#upper.map(str).join(", "))$, i.e. $c_i <= floor.l B / s_i floor.r$ for every item. + + *Step 3 -- Verify the canonical witness.* The ILP optimum is $(#ik_ilp_sol.target_config.map(str).join(", "))$, which extracts identically to the source multiplicities $(#ik_ilp_sol.source_config.map(str).join(", "))$. The selected terms contribute total size $#total_size <= B$ and total value $#total_value$ #sym.checkmark. + + *Uniqueness:* The fixture stores one canonical optimum, here $(0, 0, 2)$. + ] + } + ], +)[ + This linear-size reduction reformulates Integer Knapsack as a non-negative integer program @papadimitriou-steiglitz1982: each item multiplicity becomes an ILP variable, the knapsack capacity is a single linear inequality, and explicit upper bounds $c_i <= floor.l B / s_i floor.r$ preserve the exact witness domain of the source problem. The target therefore has $n$ variables and $n + 1$ constraints. +][ + _Construction._ Given item sizes $s_0, dots, s_(n-1) in ZZ^+$, values $v_0, dots, v_(n-1) in ZZ^+$, and capacity $B in NN$, introduce one non-negative integer variable $c_i$ for each item. Add the capacity constraint + $ + sum_(i=0)^(n-1) s_i c_i <= B + $ + and, for each $i$, the upper bound + $ + c_i <= floor.l B / s_i floor.r. + $ + Maximize the linear objective + $ + sum_(i=0)^(n-1) v_i c_i. + $ + + _Correctness._ ($arrow.r.double$) Any feasible Integer Knapsack multiplicity vector $bold(c)$ already satisfies $sum_i s_i c_i <= B$, and every source multiplicity also satisfies $c_i <= floor.l B / s_i floor.r$, so the same vector is feasible for the ILP and attains exactly the same objective value $sum_i v_i c_i$. ($arrow.l.double$) Any feasible ILP solution satisfies the same capacity inequality and the same per-item multiplicity bounds, so it is a valid Integer Knapsack witness with identical total value. Therefore optimal solutions correspond one-to-one and preserve the optimum value. + + _Solution extraction._ Identity: return the ILP variable vector $bold(c)$ as the Integer Knapsack multiplicities. +] + #let clique_mis = load-example("MaximumClique", "MaximumIndependentSet") #let clique_mis_sol = clique_mis.solutions.at(0) #reduction-rule("MaximumClique", "MaximumIndependentSet", @@ -14659,6 +14716,59 @@ The following table shows concrete variable overhead for example instances, take _Solution extraction._ Given a Partition solution $c in {0,1}^m$: if $d = 0$, return $c[0..n]$. If $Sigma > 2T$, the $S$-elements on the same side as the padding form the subset summing to $T$. If $Sigma < 2T$, the $S$-elements on the opposite side from the padding form the subset summing to $T$. ] +#let ss_ik = load-example("SubsetSum", "IntegerKnapsack") +#let ss_ik_sol = ss_ik.solutions.at(0) +#reduction-rule("SubsetSum", "IntegerKnapsack", + example: true, + example-caption: [#subsetsum-num-elements(ss_ik.source.instance) elements, target $B = #ss_ik.source.instance.target$: exact forward witness, but multiplicities create a backward gap], + extra: [ + #{ + let sizes = ss_ik.source.instance.sizes.map(s => int(s)) + let B = int(ss_ik.source.instance.target) + let chosen = ss_ik_sol.source_config.enumerate().filter(((i, x)) => x == 1).map(((i, x)) => i) + let chosen_sum = chosen.map(i => sizes.at(i)).sum() + [ + #pred-commands( + "pred create --example " + problem-spec(ss_ik.source) + " -o subsetsum.json", + "pred solve subsetsum.json", + "pred create --example " + problem-spec(ss_ik.target) + " -o integer-knapsack.json", + "pred solve integer-knapsack.json", + ) + + *Step 1 -- Source instance.* The canonical Subset Sum instance has sizes $(#sizes.map(str).join(", "))$ and target $B = #B$. The stored witness $(#ss_ik_sol.source_config.map(str).join(", "))$ selects elements ${#chosen.map(str).join(", ")}$, whose values sum to $#chosen_sum = B$ #sym.checkmark. + + *Step 2 -- Build the target.* Copy each source size into both the size and value lists. The Integer Knapsack instance therefore has sizes $(#ss_ik.target.instance.sizes.map(str).join(", "))$, values $(#ss_ik.target.instance.values.map(str).join(", "))$, and the same capacity $B = #ss_ik.target.instance.capacity$. + + *Step 3 -- Verify the forward witness.* Reuse the same 0-1 vector as multiplicities: $(#ss_ik_sol.target_config.map(str).join(", "))$. Its total size is $#chosen_sum <= #ss_ik.target.instance.capacity$, and because size equals value coordinate-wise, its total value is also $#chosen_sum = B$ #sym.checkmark. + + *Step 4 -- Backward gap.* For the source instance $A = {3}$ with target $B = 6$, Subset Sum is NO, but Integer Knapsack can set multiplicity $c_0 = 2$ and achieve total size/value $6$. This is why the catalog records the edge for proof topology only and disables all runtime reduction modes. + ] + } + ], +)[ + This size-preserving embedding from Garey and Johnson's Integer Knapsack entry @garey1979[MP10] copies each Subset Sum number into both the size and value of a knapsack item and sets the capacity to the target sum. Any exact subset-sum witness becomes a feasible Integer Knapsack witness of value $B$. The converse fails for the implemented unbounded model because target witnesses may use multiplicities greater than $1$, so the edge is documented but intentionally proof-only. +][ + _Construction._ Given Subset Sum instance $(S = {a_1, dots, a_n}, B)$, create $n$ Integer Knapsack items. For each $i$, set the item size and value to the same number: + $ + s_i = a_i, quad v_i = a_i. + $ + Set the knapsack capacity to $B$. The target therefore has the same number of items as the source has elements. + + _Correctness._ ($arrow.r.double$) If $I subset.eq {1, dots, n}$ satisfies $sum_(i in I) a_i = B$, define multiplicities $c_i = 1$ for $i in I$ and $c_i = 0$ otherwise. Then + $ + sum_i c_i s_i = sum_(i in I) a_i = B <= B + $ + and, because $v_i = s_i$, also + $ + sum_i c_i v_i = B. + $ + So every YES instance of Subset Sum maps to an Integer Knapsack witness achieving value $B$. + + ($arrow.l.double$) The backward implication is false for the implemented target model. Integer Knapsack allows arbitrary non-negative multiplicities, while Subset Sum is 0-1. For example, with $S = {3}$ and $B = 6$, the target witness $c_0 = 2$ is feasible and attains value $6$, but the source has no subset summing to $6$. Hence neither exact witness recovery nor exact optimum-value recovery is available from the target side. + + _Solution extraction._ No runtime extractor is registered. The forward map is enough for the NP-hardness proof, but unbounded multiplicities prevent an exact inverse map back to Subset Sum. +] + // 2. Satisfiability → NonTautology (#868) #let sat_nt = load-example("Satisfiability", "NonTautology") #let sat_nt_sol = sat_nt.solutions.at(0) diff --git a/src/rules/integerknapsack_ilp.rs b/src/rules/integerknapsack_ilp.rs new file mode 100644 index 00000000..d5e7ef33 --- /dev/null +++ b/src/rules/integerknapsack_ilp.rs @@ -0,0 +1,87 @@ +//! Reduction from IntegerKnapsack to ILP. +//! +//! Each item multiplicity becomes a non-negative integer ILP variable. The +//! capacity inequality is kept directly, and explicit upper bounds +//! `c_i <= floor(B / s_i)` preserve the exact witness domain of the source. + +use crate::models::algebraic::{LinearConstraint, ObjectiveSense, ILP}; +use crate::models::set::IntegerKnapsack; +use crate::reduction; +use crate::rules::traits::{ReduceTo, ReductionResult}; + +#[derive(Debug, Clone)] +pub struct ReductionIntegerKnapsackToILP { + target: ILP, +} + +impl ReductionResult for ReductionIntegerKnapsackToILP { + type Source = IntegerKnapsack; + type Target = ILP; + + fn target_problem(&self) -> &ILP { + &self.target + } + + fn extract_solution(&self, target_solution: &[usize]) -> Vec { + target_solution.to_vec() + } +} + +#[reduction( + overhead = { + num_vars = "num_items", + num_constraints = "num_items + 1", + } +)] +impl ReduceTo> for IntegerKnapsack { + type Result = ReductionIntegerKnapsackToILP; + + fn reduce_to(&self) -> Self::Result { + let num_vars = self.num_items(); + let mut constraints = Vec::with_capacity(num_vars + 1); + + constraints.push(LinearConstraint::le( + self.sizes() + .iter() + .enumerate() + .map(|(i, &size)| (i, size as f64)) + .collect(), + self.capacity() as f64, + )); + + for (i, &size) in self.sizes().iter().enumerate() { + let upper_bound = self.capacity() / size; + assert!( + upper_bound <= i32::MAX as i64, + "IntegerKnapsack -> ILP requires multiplicity bounds to fit in ILP variable bounds" + ); + constraints.push(LinearConstraint::le(vec![(i, 1.0)], upper_bound as f64)); + } + + let objective = self + .values() + .iter() + .enumerate() + .map(|(i, &value)| (i, value as f64)) + .collect(); + + ReductionIntegerKnapsackToILP { + target: ILP::new(num_vars, constraints, objective, ObjectiveSense::Maximize), + } + } +} + +#[cfg(feature = "example-db")] +pub(crate) fn canonical_rule_example_specs() -> Vec { + vec![crate::example_db::specs::RuleExampleSpec { + id: "integerknapsack_to_ilp", + build: || { + let source = IntegerKnapsack::new(vec![3, 4, 5], vec![4, 5, 7], 10); + crate::example_db::specs::rule_example_via_ilp::<_, i32>(source) + }, + }] +} + +#[cfg(test)] +#[path = "../unit_tests/rules/integerknapsack_ilp.rs"] +mod tests; diff --git a/src/rules/mod.rs b/src/rules/mod.rs index 1fd5c787..23f213d1 100644 --- a/src/rules/mod.rs +++ b/src/rules/mod.rs @@ -36,6 +36,8 @@ pub(crate) mod hamiltonianpath_degreeconstrainedspanningtree; pub(crate) mod hamiltonianpath_isomorphicspanningtree; pub(crate) mod hamiltonianpathbetweentwovertices_longestpath; pub(crate) mod ilp_i32_ilp_bool; +#[cfg(feature = "ilp-solver")] +pub(crate) mod integerknapsack_ilp; pub(crate) mod kclique_balancedcompletebipartitesubgraph; pub(crate) mod kclique_conjunctivebooleanquery; pub(crate) mod kclique_subgraphisomorphism; @@ -113,6 +115,7 @@ pub(crate) mod spinglass_qubo; pub(crate) mod subsetsum_capacityassignment; pub(crate) mod subsetsum_closestvectorproblem; pub(crate) mod subsetsum_integerexpressionmembership; +pub(crate) mod subsetsum_integerknapsack; pub(crate) mod subsetsum_partition; #[cfg(test)] pub(crate) mod test_helpers; @@ -389,6 +392,8 @@ pub(crate) fn canonical_rule_example_specs() -> Vec Vec i64 { + value + .to_i64() + .unwrap_or_else(|| panic!("SubsetSum -> IntegerKnapsack requires {what} to fit in i64")) +} + +fn biguint_to_usize(value: &BigUint, what: &str) -> usize { + value + .to_usize() + .unwrap_or_else(|| panic!("SubsetSum -> IntegerKnapsack requires {what} to fit in usize")) +} + +fn subset_sum_source_size(any: &dyn Any) -> ProblemSize { + let source = any + .downcast_ref::() + .expect("SubsetSum -> IntegerKnapsack source type mismatch"); + ProblemSize::new(vec![ + ("num_elements", source.num_elements()), + ("target", biguint_to_usize(source.target(), "target")), + ]) +} + +fn subset_sum_to_integer_knapsack_overhead(any: &dyn Any) -> ProblemSize { + let source = any + .downcast_ref::() + .expect("SubsetSum -> IntegerKnapsack source type mismatch"); + ProblemSize::new(vec![ + ("num_items", source.num_elements()), + ("capacity", biguint_to_usize(source.target(), "target")), + ]) +} + +inventory::submit! { + ReductionEntry { + source_name: SubsetSum::NAME, + target_name: IntegerKnapsack::NAME, + source_variant_fn: ::variant, + target_variant_fn: ::variant, + overhead_fn: || ReductionOverhead::new(vec![ + ("num_items", Expr::Var("num_elements")), + ("capacity", Expr::Var("target")), + ]), + module_path: module_path!(), + reduce_fn: None, + reduce_aggregate_fn: None, + capabilities: EdgeCapabilities::none(), + overhead_eval_fn: subset_sum_to_integer_knapsack_overhead, + source_size_fn: subset_sum_source_size, + } +} + +#[cfg(feature = "example-db")] +pub(crate) fn canonical_rule_example_specs() -> Vec { + use crate::example_db::specs::assemble_rule_example; + use crate::export::SolutionPair; + + vec![crate::example_db::specs::RuleExampleSpec { + id: "subsetsum_to_integerknapsack", + build: || { + let source = SubsetSum::new(vec![3u32, 7, 1, 8, 5], 16u32); + let target = IntegerKnapsack::new( + source + .sizes() + .iter() + .map(|size| biguint_to_i64(size, "sizes")) + .collect(), + source + .sizes() + .iter() + .map(|value| biguint_to_i64(value, "sizes")) + .collect(), + biguint_to_i64(source.target(), "target"), + ); + + assemble_rule_example( + &source, + &target, + vec![SolutionPair { + source_config: vec![1, 0, 0, 1, 1], + target_config: vec![1, 0, 0, 1, 1], + }], + ) + }, + }] +} + +#[cfg(test)] +#[path = "../unit_tests/rules/subsetsum_integerknapsack.rs"] +mod tests; diff --git a/src/unit_tests/reduction_graph.rs b/src/unit_tests/reduction_graph.rs index 325ac28d..89b0a854 100644 --- a/src/unit_tests/reduction_graph.rs +++ b/src/unit_tests/reduction_graph.rs @@ -195,6 +195,40 @@ fn test_json_export() { assert!(categories.len() >= 3, "Should have multiple categories"); } +#[test] +fn test_subsetsum_to_integerknapsack_is_proof_only() { + let graph = ReductionGraph::new(); + + assert!(graph.has_direct_reduction_by_name("SubsetSum", "IntegerKnapsack")); + assert!(!graph.has_direct_reduction_by_name_mode( + "SubsetSum", + "IntegerKnapsack", + ReductionMode::Witness, + )); + assert!(!graph.has_direct_reduction_by_name_mode( + "SubsetSum", + "IntegerKnapsack", + ReductionMode::Aggregate, + )); + assert!(!graph.has_direct_reduction_by_name_mode( + "SubsetSum", + "IntegerKnapsack", + ReductionMode::Turing, + )); +} + +#[cfg(feature = "ilp-solver")] +#[test] +fn test_integerknapsack_to_ilp_is_runtime_witness_edge() { + let graph = ReductionGraph::new(); + + assert!(graph.has_direct_reduction_by_name_mode( + "IntegerKnapsack", + "ILP", + ReductionMode::Witness, + )); +} + // ---- Path finding (variant-level API) ---- #[test] diff --git a/src/unit_tests/rules/integerknapsack_ilp.rs b/src/unit_tests/rules/integerknapsack_ilp.rs new file mode 100644 index 00000000..2fb5f1f3 --- /dev/null +++ b/src/unit_tests/rules/integerknapsack_ilp.rs @@ -0,0 +1,97 @@ +#[cfg(feature = "example-db")] +use super::canonical_rule_example_specs; +use crate::models::algebraic::{Comparison, ObjectiveSense, ILP}; +use crate::models::set::IntegerKnapsack; +use crate::rules::test_helpers::assert_bf_vs_ilp; +use crate::rules::{ReduceTo, ReductionResult}; +use crate::solvers::ILPSolver; + +#[test] +fn test_integerknapsack_to_ilp_closed_loop() { + let source = IntegerKnapsack::new(vec![3, 4, 5], vec![4, 5, 7], 10); + let reduction = ReduceTo::>::reduce_to(&source); + + assert_bf_vs_ilp(&source, &reduction); + + let ilp_solution = ILPSolver::new() + .solve(reduction.target_problem()) + .expect("ILP should be solvable"); + let extracted = reduction.extract_solution(&ilp_solution); + assert_eq!(extracted, vec![0, 0, 2]); +} + +#[test] +fn test_integerknapsack_to_ilp_structure() { + let source = IntegerKnapsack::new(vec![3, 4, 5], vec![4, 5, 7], 10); + let reduction = ReduceTo::>::reduce_to(&source); + let ilp = reduction.target_problem(); + + assert_eq!(ilp.num_vars(), 3); + assert_eq!(ilp.num_constraints(), 4); + assert_eq!(ilp.sense, ObjectiveSense::Maximize); + assert_eq!(ilp.objective, vec![(0, 4.0), (1, 5.0), (2, 7.0)]); + + let capacity = &ilp.constraints[0]; + assert_eq!(capacity.cmp, Comparison::Le); + assert_eq!(capacity.rhs, 10.0); + assert_eq!(capacity.terms, vec![(0, 3.0), (1, 4.0), (2, 5.0)]); + + let bounds: Vec<_> = ilp.constraints[1..] + .iter() + .map(|constraint| (constraint.terms.clone(), constraint.cmp, constraint.rhs)) + .collect(); + assert_eq!( + bounds, + vec![ + (vec![(0, 1.0)], Comparison::Le, 3.0), + (vec![(1, 1.0)], Comparison::Le, 2.0), + (vec![(2, 1.0)], Comparison::Le, 2.0), + ] + ); +} + +#[test] +fn test_integerknapsack_to_ilp_zero_capacity() { + let source = IntegerKnapsack::new(vec![1, 2], vec![10, 20], 0); + let reduction = ReduceTo::>::reduce_to(&source); + + let ilp_solution = ILPSolver::new() + .solve(reduction.target_problem()) + .expect("zero-capacity ILP should still be solvable"); + let extracted = reduction.extract_solution(&ilp_solution); + assert_eq!(extracted, vec![0, 0]); +} + +#[test] +#[should_panic( + expected = "IntegerKnapsack -> ILP requires multiplicity bounds to fit in ILP variable bounds" +)] +fn test_integerknapsack_to_ilp_rejects_too_large_multiplicity_bounds() { + let source = IntegerKnapsack::new(vec![1], vec![1], i32::MAX as i64 + 1); + let _: super::ReductionIntegerKnapsackToILP = ReduceTo::>::reduce_to(&source); +} + +#[cfg(feature = "example-db")] +#[test] +fn test_integerknapsack_to_ilp_canonical_example_spec() { + let example = (canonical_rule_example_specs() + .into_iter() + .find(|spec| spec.id == "integerknapsack_to_ilp") + .expect("missing canonical IntegerKnapsack -> ILP example spec") + .build)(); + + assert_eq!(example.source.problem, "IntegerKnapsack"); + assert_eq!(example.target.problem, "ILP"); + assert_eq!(example.source.instance["capacity"], 10); + assert_eq!(example.target.instance["num_vars"], 3); + assert_eq!( + example.target.instance["constraints"] + .as_array() + .expect("constraints array") + .len(), + 4 + ); + assert_eq!(example.solutions.len(), 1); + assert_eq!(example.solutions[0].source_config, vec![0, 0, 2]); + assert_eq!(example.solutions[0].target_config, vec![0, 0, 2]); +} diff --git a/src/unit_tests/rules/subsetsum_integerknapsack.rs b/src/unit_tests/rules/subsetsum_integerknapsack.rs new file mode 100644 index 00000000..82173dbe --- /dev/null +++ b/src/unit_tests/rules/subsetsum_integerknapsack.rs @@ -0,0 +1,92 @@ +#[cfg(feature = "example-db")] +use super::canonical_rule_example_specs; +use crate::models::misc::SubsetSum; +use crate::models::set::IntegerKnapsack; +use crate::solvers::{BruteForce, Solver}; +use crate::traits::Problem; +use crate::types::Max; +use num_traits::ToPrimitive; + +fn subset_sum_embedding(source: &SubsetSum) -> IntegerKnapsack { + IntegerKnapsack::new( + source + .sizes() + .iter() + .map(|size| { + size.to_i64() + .expect("test fixture sizes should fit in i64 for IntegerKnapsack") + }) + .collect(), + source + .sizes() + .iter() + .map(|value| { + value + .to_i64() + .expect("test fixture values should fit in i64 for IntegerKnapsack") + }) + .collect(), + source + .target() + .to_i64() + .expect("test fixture target should fit in i64 for IntegerKnapsack"), + ) +} + +#[test] +fn test_subsetsum_to_integerknapsack_forward_example() { + let source = SubsetSum::new(vec![3u32, 7, 1, 8, 5], 16u32); + let target = subset_sum_embedding(&source); + let source_witness = vec![1, 0, 0, 1, 1]; + + assert!(source.evaluate(&source_witness).is_valid()); + assert_eq!(target.evaluate(&source_witness), Max(Some(16))); +} + +#[test] +fn test_subsetsum_to_integerknapsack_counterexample_demonstrates_gap() { + let source = SubsetSum::new(vec![3u32], 6u32); + let target = subset_sum_embedding(&source); + let solver = BruteForce::new(); + + assert!(solver.find_witness(&source).is_none()); + assert_eq!(solver.solve(&target), Max(Some(6))); +} + +#[cfg(feature = "example-db")] +#[test] +fn test_subsetsum_to_integerknapsack_canonical_example_spec() { + let example = (canonical_rule_example_specs() + .into_iter() + .find(|spec| spec.id == "subsetsum_to_integerknapsack") + .expect("missing canonical SubsetSum -> IntegerKnapsack example spec") + .build)(); + + assert_eq!(example.source.problem, "SubsetSum"); + assert_eq!(example.target.problem, "IntegerKnapsack"); + assert_eq!( + example.target.instance["sizes"], + serde_json::json!([3, 7, 1, 8, 5]) + ); + assert_eq!( + example.target.instance["values"], + serde_json::json!([3, 7, 1, 8, 5]) + ); + assert_eq!(example.target.instance["capacity"], 16); + assert_eq!(example.solutions.len(), 1); + assert_eq!(example.solutions[0].source_config, vec![1, 0, 0, 1, 1]); + assert_eq!(example.solutions[0].target_config, vec![1, 0, 0, 1, 1]); + + let source: SubsetSum = serde_json::from_value(example.source.instance.clone()) + .expect("source example deserializes"); + let target: IntegerKnapsack = serde_json::from_value(example.target.instance.clone()) + .expect("target example deserializes"); + + assert!(source + .evaluate(&example.solutions[0].source_config) + .is_valid()); + assert_eq!( + target.evaluate(&example.solutions[0].target_config), + Max(Some(16)) + ); +} From 6a48c87d0fde263f6cc410e69a02cf9ac4821d60 Mon Sep 17 00:00:00 2001 From: GiggleLiu Date: Wed, 8 Apr 2026 00:22:25 +0800 Subject: [PATCH 11/13] feat: add 3SAT to FeasibleRegisterAssignment + FRA to ILP reductions (#905) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Implements Sethi's Reduction 3 / Theorem 5.11 with p/q/r/rbar clause gadgets, cyclic links, and shared-register variable leaf pairs. Also adds the companion FeasibleRegisterAssignment → ILP rule. Co-Authored-By: Claude Opus 4.6 (1M context) --- .../misc/feasible_register_assignment.rs | 12 ++ src/rules/feasibleregisterassignment_ilp.rs | 160 ++++++++++++++ ...tisfiability_feasibleregisterassignment.rs | 198 ++++++++++++++++++ src/rules/mod.rs | 7 +- .../misc/feasible_register_assignment.rs | 7 + .../rules/feasibleregisterassignment_ilp.rs | 54 +++++ ...tisfiability_feasibleregisterassignment.rs | 93 ++++++++ tests/main.rs | 2 + .../suites/register_assignment_reductions.rs | 107 ++++++++++ 9 files changed, 639 insertions(+), 1 deletion(-) create mode 100644 src/rules/feasibleregisterassignment_ilp.rs create mode 100644 src/rules/ksatisfiability_feasibleregisterassignment.rs create mode 100644 src/unit_tests/rules/feasibleregisterassignment_ilp.rs create mode 100644 src/unit_tests/rules/ksatisfiability_feasibleregisterassignment.rs create mode 100644 tests/suites/register_assignment_reductions.rs diff --git a/src/models/misc/feasible_register_assignment.rs b/src/models/misc/feasible_register_assignment.rs index d6657840..64c0e340 100644 --- a/src/models/misc/feasible_register_assignment.rs +++ b/src/models/misc/feasible_register_assignment.rs @@ -187,6 +187,18 @@ impl FeasibleRegisterAssignment { self.num_registers } + /// Count unordered vertex pairs that share a register. + pub fn num_same_register_pairs(&self) -> usize { + let mut counts = vec![0usize; self.num_registers]; + for ®ister in &self.assignment { + counts[register] += 1; + } + counts + .into_iter() + .map(|count| count.saturating_sub(1) * count / 2) + .sum() + } + /// Get the arcs. pub fn arcs(&self) -> &[(usize, usize)] { &self.arcs diff --git a/src/rules/feasibleregisterassignment_ilp.rs b/src/rules/feasibleregisterassignment_ilp.rs new file mode 100644 index 00000000..409c0218 --- /dev/null +++ b/src/rules/feasibleregisterassignment_ilp.rs @@ -0,0 +1,160 @@ +//! Reduction from Feasible Register Assignment to ILP (Integer Linear Programming). +//! +//! The formulation uses non-negative integer variables: +//! - `t_v`: evaluation position of vertex `v` +//! - `L_v`: latest position among `v` and all dependents of `v` +//! - `z_uv`: binary order selector for each unordered pair `{u, v}` +//! +//! The pair-order constraints force the `t_v` values to form a permutation of +//! `{0, ..., n-1}`. For same-register pairs, the extra constraints enforce +//! interval non-overlap: if `u` is before `v`, then `v` must be scheduled no +//! earlier than the latest dependent of `u`. + +use crate::models::algebraic::{LinearConstraint, ObjectiveSense, ILP}; +use crate::models::misc::FeasibleRegisterAssignment; +use crate::reduction; +use crate::rules::traits::{ReduceTo, ReductionResult}; + +#[derive(Debug, Clone)] +pub struct ReductionFeasibleRegisterAssignmentToILP { + target: ILP, + num_vertices: usize, +} + +impl ReductionResult for ReductionFeasibleRegisterAssignmentToILP { + type Source = FeasibleRegisterAssignment; + type Target = ILP; + + fn target_problem(&self) -> &ILP { + &self.target + } + + fn extract_solution(&self, target_solution: &[usize]) -> Vec { + target_solution[..self.num_vertices].to_vec() + } +} + +#[reduction(overhead = { + num_vars = "2 * num_vertices + num_vertices * (num_vertices - 1) / 2", + num_constraints = "3 * num_vertices * (num_vertices - 1) / 2 + 3 * num_vertices + 2 * num_arcs + 2 * num_same_register_pairs", +})] +impl ReduceTo> for FeasibleRegisterAssignment { + type Result = ReductionFeasibleRegisterAssignmentToILP; + + fn reduce_to(&self) -> Self::Result { + let n = self.num_vertices(); + let pair_list: Vec<(usize, usize)> = (0..n) + .flat_map(|u| ((u + 1)..n).map(move |v| (u, v))) + .collect(); + let same_register_pairs: Vec<(usize, usize, usize)> = pair_list + .iter() + .copied() + .enumerate() + .filter(|(_, (u, v))| self.assignment()[*u] == self.assignment()[*v]) + .map(|(pair_idx, (u, v))| (u, v, pair_idx)) + .collect(); + + let num_pair_vars = pair_list.len(); + let num_vars = 2 * n + num_pair_vars; + let big_m = n as f64; + + let time_idx = |vertex: usize| -> usize { vertex }; + let latest_idx = |vertex: usize| -> usize { n + vertex }; + let order_idx = |pair_idx: usize| -> usize { 2 * n + pair_idx }; + + let mut constraints = + Vec::with_capacity(3 * num_pair_vars + 3 * n + 2 * self.num_arcs() + 2 * same_register_pairs.len()); + + for vertex in 0..n { + constraints.push(LinearConstraint::le( + vec![(time_idx(vertex), 1.0)], + (n.saturating_sub(1)) as f64, + )); + constraints.push(LinearConstraint::le( + vec![(latest_idx(vertex), 1.0)], + (n.saturating_sub(1)) as f64, + )); + constraints.push(LinearConstraint::ge( + vec![(latest_idx(vertex), 1.0), (time_idx(vertex), -1.0)], + 0.0, + )); + } + + for &(dependent, dependency) in self.arcs() { + constraints.push(LinearConstraint::ge( + vec![(time_idx(dependent), 1.0), (time_idx(dependency), -1.0)], + 1.0, + )); + constraints.push(LinearConstraint::ge( + vec![(latest_idx(dependency), 1.0), (time_idx(dependent), -1.0)], + 0.0, + )); + } + + for (pair_idx, &(u, v)) in pair_list.iter().enumerate() { + let order_var = order_idx(pair_idx); + constraints.push(LinearConstraint::le(vec![(order_var, 1.0)], 1.0)); + constraints.push(LinearConstraint::ge( + vec![ + (time_idx(v), 1.0), + (time_idx(u), -1.0), + (order_var, -big_m), + ], + 1.0 - big_m, + )); + constraints.push(LinearConstraint::ge( + vec![ + (time_idx(u), 1.0), + (time_idx(v), -1.0), + (order_var, big_m), + ], + 1.0, + )); + } + + for &(u, v, pair_idx) in &same_register_pairs { + let order_var = order_idx(pair_idx); + constraints.push(LinearConstraint::ge( + vec![ + (time_idx(v), 1.0), + (latest_idx(u), -1.0), + (order_var, -big_m), + ], + -big_m, + )); + constraints.push(LinearConstraint::ge( + vec![ + (time_idx(u), 1.0), + (latest_idx(v), -1.0), + (order_var, big_m), + ], + 0.0, + )); + } + + ReductionFeasibleRegisterAssignmentToILP { + target: ILP::new(num_vars, constraints, vec![], ObjectiveSense::Minimize), + num_vertices: n, + } + } +} + +#[cfg(feature = "example-db")] +pub(crate) fn canonical_rule_example_specs() -> Vec { + vec![crate::example_db::specs::RuleExampleSpec { + id: "feasibleregisterassignment_to_ilp", + build: || { + let source = FeasibleRegisterAssignment::new( + 4, + vec![(0, 1), (0, 2), (1, 3)], + 2, + vec![0, 1, 0, 0], + ); + crate::example_db::specs::rule_example_via_ilp::<_, i32>(source) + }, + }] +} + +#[cfg(test)] +#[path = "../unit_tests/rules/feasibleregisterassignment_ilp.rs"] +mod tests; diff --git a/src/rules/ksatisfiability_feasibleregisterassignment.rs b/src/rules/ksatisfiability_feasibleregisterassignment.rs new file mode 100644 index 00000000..94edd5ca --- /dev/null +++ b/src/rules/ksatisfiability_feasibleregisterassignment.rs @@ -0,0 +1,198 @@ +//! Reduction from KSatisfiability (3-SAT) to Feasible Register Assignment. +//! +//! This follows Sethi's Reduction 3 / Theorem 5.11: +//! - Variable leaf pairs `s_pos[k], s_neg[k]` share register `S[k]` +//! - Each literal occurrence adds `p[i,j], q[i,j], r[i,j], rbar[i,j]` +//! - `r[i,j]` and `rbar[i,j]` share register `R[i,j]` +//! - Clause gadgets are linked cyclically through `(q[i,1], rbar[i,2])`, +//! `(q[i,2], rbar[i,3])`, `(q[i,3], rbar[i,1])` +//! - A realization yields a truth assignment by comparing the order of +//! `s_pos[k]` and `s_neg[k]` + +use crate::models::formula::KSatisfiability; +use crate::models::misc::FeasibleRegisterAssignment; +use crate::reduction; +use crate::rules::traits::{ReduceTo, ReductionResult}; +use crate::variant::K3; + +fn s_pos_idx(var: usize) -> usize { + var +} + +fn s_neg_idx(num_vars: usize, var: usize) -> usize { + num_vars + var +} + +fn literal_base(num_vars: usize, clause_idx: usize, literal_pos: usize) -> usize { + 2 * num_vars + 12 * clause_idx + 4 * literal_pos +} + +fn p_idx(num_vars: usize, clause_idx: usize, literal_pos: usize) -> usize { + literal_base(num_vars, clause_idx, literal_pos) +} + +fn q_idx(num_vars: usize, clause_idx: usize, literal_pos: usize) -> usize { + literal_base(num_vars, clause_idx, literal_pos) + 1 +} + +fn r_idx(num_vars: usize, clause_idx: usize, literal_pos: usize) -> usize { + literal_base(num_vars, clause_idx, literal_pos) + 2 +} + +fn rbar_idx(num_vars: usize, clause_idx: usize, literal_pos: usize) -> usize { + literal_base(num_vars, clause_idx, literal_pos) + 3 +} + +fn p_register(num_vars: usize, clause_idx: usize, literal_pos: usize) -> usize { + num_vars + 3 * (3 * clause_idx + literal_pos) +} + +fn q_register(num_vars: usize, clause_idx: usize, literal_pos: usize) -> usize { + p_register(num_vars, clause_idx, literal_pos) + 1 +} + +fn r_register(num_vars: usize, clause_idx: usize, literal_pos: usize) -> usize { + p_register(num_vars, clause_idx, literal_pos) + 2 +} + +#[derive(Debug, Clone)] +pub struct Reduction3SATToFeasibleRegisterAssignment { + target: FeasibleRegisterAssignment, + num_vars: usize, +} + +impl ReductionResult for Reduction3SATToFeasibleRegisterAssignment { + type Source = KSatisfiability; + type Target = FeasibleRegisterAssignment; + + fn target_problem(&self) -> &Self::Target { + &self.target + } + + fn extract_solution(&self, target_solution: &[usize]) -> Vec { + (0..self.num_vars) + .map(|var| { + usize::from( + target_solution[s_pos_idx(var)] < target_solution[s_neg_idx(self.num_vars, var)], + ) + }) + .collect() + } +} + +#[reduction(overhead = { + num_vertices = "2 * num_vars + 12 * num_clauses", + num_arcs = "15 * num_clauses", + num_registers = "num_vars + 9 * num_clauses", +})] +impl ReduceTo for KSatisfiability { + type Result = Reduction3SATToFeasibleRegisterAssignment; + + fn reduce_to(&self) -> Self::Result { + let num_vars = self.num_vars(); + let num_clauses = self.num_clauses(); + let num_vertices = 2 * num_vars + 12 * num_clauses; + let num_registers = num_vars + 9 * num_clauses; + let mut assignment = vec![0usize; num_vertices]; + let mut arcs = Vec::with_capacity(15 * num_clauses); + + for var in 0..num_vars { + assignment[s_pos_idx(var)] = var; + assignment[s_neg_idx(num_vars, var)] = var; + } + + for (clause_idx, clause) in self.clauses().iter().enumerate() { + for literal_pos in 0..3 { + assignment[p_idx(num_vars, clause_idx, literal_pos)] = + p_register(num_vars, clause_idx, literal_pos); + assignment[q_idx(num_vars, clause_idx, literal_pos)] = + q_register(num_vars, clause_idx, literal_pos); + assignment[r_idx(num_vars, clause_idx, literal_pos)] = + r_register(num_vars, clause_idx, literal_pos); + assignment[rbar_idx(num_vars, clause_idx, literal_pos)] = + r_register(num_vars, clause_idx, literal_pos); + + arcs.push(( + q_idx(num_vars, clause_idx, literal_pos), + p_idx(num_vars, clause_idx, literal_pos), + )); + arcs.push(( + p_idx(num_vars, clause_idx, literal_pos), + r_idx(num_vars, clause_idx, literal_pos), + )); + } + + arcs.push(( + q_idx(num_vars, clause_idx, 0), + rbar_idx(num_vars, clause_idx, 1), + )); + arcs.push(( + q_idx(num_vars, clause_idx, 1), + rbar_idx(num_vars, clause_idx, 2), + )); + arcs.push(( + q_idx(num_vars, clause_idx, 2), + rbar_idx(num_vars, clause_idx, 0), + )); + + for (literal_pos, &literal) in clause.literals.iter().enumerate() { + let var = literal.unsigned_abs() as usize - 1; + let (literal_leaf, opposite_leaf) = if literal > 0 { + (s_pos_idx(var), s_neg_idx(num_vars, var)) + } else { + (s_neg_idx(num_vars, var), s_pos_idx(var)) + }; + arcs.push((r_idx(num_vars, clause_idx, literal_pos), literal_leaf)); + arcs.push((rbar_idx(num_vars, clause_idx, literal_pos), opposite_leaf)); + } + } + + Reduction3SATToFeasibleRegisterAssignment { + target: FeasibleRegisterAssignment::new(num_vertices, arcs, num_registers, assignment), + num_vars, + } + } +} + +#[cfg(feature = "example-db")] +pub(crate) fn canonical_rule_example_specs() -> Vec { + use crate::export::SolutionPair; + use crate::models::algebraic::ILP; + use crate::models::formula::CNFClause; + use crate::solvers::ILPSolver; + + vec![crate::example_db::specs::RuleExampleSpec { + id: "ksatisfiability_to_feasibleregisterassignment", + build: || { + let source = KSatisfiability::::new( + 3, + vec![ + CNFClause::new(vec![1, -2, 3]), + CNFClause::new(vec![-1, 2, -3]), + ], + ); + let to_fra = + as ReduceTo>::reduce_to(&source); + let to_ilp = >>::reduce_to( + to_fra.target_problem(), + ); + let ilp_solution = ILPSolver::new() + .solve(to_ilp.target_problem()) + .expect("canonical FRA example must reduce to a feasible ILP"); + let target_config = to_ilp.extract_solution(&ilp_solution); + let source_config = to_fra.extract_solution(&target_config); + crate::example_db::specs::assemble_rule_example( + &source, + to_fra.target_problem(), + vec![SolutionPair { + source_config, + target_config, + }], + ) + }, + }] +} + +#[cfg(test)] +#[path = "../unit_tests/rules/ksatisfiability_feasibleregisterassignment.rs"] +mod tests; diff --git a/src/rules/mod.rs b/src/rules/mod.rs index 23f213d1..38205d0e 100644 --- a/src/rules/mod.rs +++ b/src/rules/mod.rs @@ -50,6 +50,7 @@ mod ksatisfiability_casts; pub(crate) mod ksatisfiability_cyclicordering; pub(crate) mod ksatisfiability_decisionminimumvertexcover; pub(crate) mod ksatisfiability_directedtwocommodityintegralflow; +pub(crate) mod ksatisfiability_feasibleregisterassignment; pub(crate) mod ksatisfiability_kclique; pub(crate) mod ksatisfiability_kernel; pub(crate) mod ksatisfiability_minimumvertexcover; @@ -171,6 +172,8 @@ pub(crate) mod exactcoverby3sets_ilp; #[cfg(feature = "ilp-solver")] pub(crate) mod expectedretrievalcost_ilp; #[cfg(feature = "ilp-solver")] +pub(crate) mod feasibleregisterassignment_ilp; +#[cfg(feature = "ilp-solver")] pub(crate) mod factoring_ilp; #[cfg(feature = "ilp-solver")] pub(crate) mod flowshopscheduling_ilp; @@ -404,6 +407,8 @@ pub(crate) fn canonical_rule_example_specs() -> Vec Vec Vec FeasibleRegisterAssignment { + FeasibleRegisterAssignment::new(4, vec![(0, 1), (0, 2), (1, 3)], 2, vec![0, 1, 0, 0]) +} + +#[test] +fn test_feasible_register_assignment_to_ilp_structure() { + let source = feasible_example(); + let reduction = ReduceTo::>::reduce_to(&source); + let ilp = reduction.target_problem(); + + assert_eq!(ilp.num_vars, 14); + assert_eq!(ilp.constraints.len(), 42); + assert_eq!(ilp.objective, vec![]); + assert_eq!(ilp.sense, ObjectiveSense::Minimize); +} + +#[test] +fn test_feasible_register_assignment_to_ilp_closed_loop() { + let source = feasible_example(); + let reduction = ReduceTo::>::reduce_to(&source); + + let ilp_solution = ILPSolver::new() + .solve(reduction.target_problem()) + .expect("feasible source instance should yield a feasible ILP"); + let extracted = reduction.extract_solution(&ilp_solution); + + assert_eq!(source.evaluate(&extracted), Or(true)); + let mut sorted = extracted.clone(); + sorted.sort_unstable(); + assert_eq!(sorted, vec![0, 1, 2, 3]); +} + +#[test] +fn test_feasible_register_assignment_to_ilp_infeasible() { + let source = FeasibleRegisterAssignment::new(3, vec![(0, 1), (0, 2), (1, 2)], 1, vec![0, 0, 0]); + let reduction = ReduceTo::>::reduce_to(&source); + + assert!( + ILPSolver::new().solve(reduction.target_problem()).is_none(), + "register-conflict source instance should reduce to an infeasible ILP" + ); +} + +#[test] +fn test_feasible_register_assignment_to_ilp_bf_vs_ilp() { + let source = feasible_example(); + let reduction = ReduceTo::>::reduce_to(&source); + crate::rules::test_helpers::assert_bf_vs_ilp(&source, &reduction); +} diff --git a/src/unit_tests/rules/ksatisfiability_feasibleregisterassignment.rs b/src/unit_tests/rules/ksatisfiability_feasibleregisterassignment.rs new file mode 100644 index 00000000..c9c10fb7 --- /dev/null +++ b/src/unit_tests/rules/ksatisfiability_feasibleregisterassignment.rs @@ -0,0 +1,93 @@ +use super::*; +use crate::models::algebraic::ILP; +use crate::models::formula::CNFClause; +use crate::solvers::ILPSolver; +use crate::traits::Problem; +use crate::types::Or; +use std::collections::BTreeSet; + +fn issue_example() -> KSatisfiability { + KSatisfiability::::new( + 3, + vec![ + CNFClause::new(vec![1, -2, 3]), + CNFClause::new(vec![-1, 2, -3]), + ], + ) +} + +#[test] +fn test_ksatisfiability_to_feasible_register_assignment_structure() { + let source = issue_example(); + let reduction = ReduceTo::::reduce_to(&source); + let target = reduction.target_problem(); + + assert_eq!(target.num_vertices(), 30); + assert_eq!(target.num_arcs(), 30); + assert_eq!(target.num_registers(), 21); + + assert_eq!(target.assignment()[s_pos_idx(0)], target.assignment()[s_neg_idx(3, 0)]); + assert_eq!(target.assignment()[s_pos_idx(1)], target.assignment()[s_neg_idx(3, 1)]); + assert_eq!(target.assignment()[s_pos_idx(2)], target.assignment()[s_neg_idx(3, 2)]); + assert_eq!(target.assignment()[r_idx(3, 0, 0)], target.assignment()[rbar_idx(3, 0, 0)]); + assert_eq!(target.assignment()[r_idx(3, 1, 2)], target.assignment()[rbar_idx(3, 1, 2)]); + + let arc_set: BTreeSet<_> = target.arcs().iter().copied().collect(); + assert!(arc_set.contains(&(q_idx(3, 0, 0), p_idx(3, 0, 0)))); + assert!(arc_set.contains(&(p_idx(3, 0, 0), r_idx(3, 0, 0)))); + assert!(arc_set.contains(&(q_idx(3, 0, 0), rbar_idx(3, 0, 1)))); + assert!(arc_set.contains(&(q_idx(3, 0, 1), rbar_idx(3, 0, 2)))); + assert!(arc_set.contains(&(q_idx(3, 0, 2), rbar_idx(3, 0, 0)))); + assert!(arc_set.contains(&(r_idx(3, 0, 0), s_pos_idx(0)))); + assert!(arc_set.contains(&(rbar_idx(3, 0, 0), s_neg_idx(3, 0)))); + assert!(arc_set.contains(&(r_idx(3, 0, 1), s_neg_idx(3, 1)))); + assert!(arc_set.contains(&(rbar_idx(3, 0, 1), s_pos_idx(1)))); + assert!(arc_set.contains(&(r_idx(3, 1, 2), s_neg_idx(3, 2)))); + assert!(arc_set.contains(&(rbar_idx(3, 1, 2), s_pos_idx(2)))); +} + +#[test] +fn test_ksatisfiability_to_feasible_register_assignment_extract_solution() { + let source = KSatisfiability::::new(2, vec![CNFClause::new(vec![1, -2, 1])]); + let reduction = ReduceTo::::reduce_to(&source); + let mut realization: Vec = (0..reduction.target_problem().num_vertices()).collect(); + realization.swap(s_pos_idx(1), s_neg_idx(2, 1)); + + let extracted = reduction.extract_solution(&realization); + + assert_eq!(extracted, vec![1, 0]); +} + +#[test] +fn test_ksatisfiability_to_feasible_register_assignment_closed_loop_via_ilp() { + let source = issue_example(); + let reduction = ReduceTo::::reduce_to(&source); + let fra_to_ilp = ReduceTo::>::reduce_to(reduction.target_problem()); + + let ilp_solution = ILPSolver::new() + .solve(fra_to_ilp.target_problem()) + .expect("satisfiable FRA gadget should reduce to a feasible ILP"); + let fra_solution = fra_to_ilp.extract_solution(&ilp_solution); + assert_eq!(reduction.target_problem().evaluate(&fra_solution), Or(true)); + + let extracted = reduction.extract_solution(&fra_solution); + assert_eq!(source.evaluate(&extracted), Or(true)); +} + +#[test] +fn test_ksatisfiability_to_feasible_register_assignment_unsatisfiable_instance() { + let source = KSatisfiability::::new( + 1, + vec![ + CNFClause::new(vec![1, 1, 1]), + CNFClause::new(vec![-1, -1, -1]), + ], + ); + let reduction = ReduceTo::::reduce_to(&source); + let fra_to_ilp = ReduceTo::>::reduce_to(reduction.target_problem()); + + assert!( + ILPSolver::new().solve(fra_to_ilp.target_problem()).is_none(), + "an unsatisfiable source formula should yield an infeasible FRA instance" + ); +} diff --git a/tests/main.rs b/tests/main.rs index 777283ae..0e347095 100644 --- a/tests/main.rs +++ b/tests/main.rs @@ -8,6 +8,8 @@ mod integration; mod jl_parity; #[path = "suites/ksatisfiability_simultaneous_incongruences.rs"] mod ksatisfiability_simultaneous_incongruences; +#[path = "suites/register_assignment_reductions.rs"] +mod register_assignment_reductions; #[path = "suites/reductions.rs"] mod reductions; #[path = "suites/simultaneous_incongruences.rs"] diff --git a/tests/suites/register_assignment_reductions.rs b/tests/suites/register_assignment_reductions.rs new file mode 100644 index 00000000..35540302 --- /dev/null +++ b/tests/suites/register_assignment_reductions.rs @@ -0,0 +1,107 @@ +use problemreductions::models::algebraic::ILP; +use problemreductions::models::formula::{CNFClause, KSatisfiability}; +use problemreductions::models::misc::FeasibleRegisterAssignment; +use problemreductions::prelude::*; +use problemreductions::rules::{MinimizeSteps, ReductionGraph, ReductionPath}; +use problemreductions::solvers::ILPSolver; +use problemreductions::types::{Or, ProblemSize}; +use problemreductions::variant::K3; + +fn ksat_to_fra_path() -> ReductionPath { + let graph = ReductionGraph::new(); + let src = ReductionGraph::variant_to_map(&KSatisfiability::::variant()); + let dst = ReductionGraph::variant_to_map(&FeasibleRegisterAssignment::variant()); + graph + .find_cheapest_path( + "KSatisfiability", + &src, + "FeasibleRegisterAssignment", + &dst, + &ProblemSize::new(vec![]), + &MinimizeSteps, + ) + .expect("expected a direct KSatisfiability -> FeasibleRegisterAssignment path") +} + +fn fra_to_ilp_path() -> ReductionPath { + let graph = ReductionGraph::new(); + let src = ReductionGraph::variant_to_map(&FeasibleRegisterAssignment::variant()); + let dst = ReductionGraph::variant_to_map(&ILP::::variant()); + graph + .find_cheapest_path( + "FeasibleRegisterAssignment", + &src, + "ILP", + &dst, + &ProblemSize::new(vec![]), + &MinimizeSteps, + ) + .expect("expected a direct FeasibleRegisterAssignment -> ILP path") +} + +#[test] +fn test_ksat_to_fra_structure_and_closed_loop_via_ilp() { + let source = KSatisfiability::::new( + 3, + vec![ + CNFClause::new(vec![1, -2, 3]), + CNFClause::new(vec![-1, 2, -3]), + ], + ); + + let graph = ReductionGraph::new(); + let ksat_path = ksat_to_fra_path(); + assert_eq!( + ksat_path.type_names(), + vec!["KSatisfiability", "FeasibleRegisterAssignment"] + ); + let ksat_chain = graph + .reduce_along_path(&ksat_path, &source as &dyn std::any::Any) + .expect("KSAT -> FRA reduction should execute"); + let fra = ksat_chain.target_problem::(); + + assert_eq!(fra.num_vertices(), 30); + assert_eq!(fra.num_arcs(), 30); + assert_eq!(fra.num_registers(), 21); + + let fra_path = fra_to_ilp_path(); + assert_eq!(fra_path.type_names(), vec!["FeasibleRegisterAssignment", "ILP"]); + let fra_chain = graph + .reduce_along_path(&fra_path, fra as &dyn std::any::Any) + .expect("FRA -> ILP reduction should execute"); + let ilp = fra_chain.target_problem::>(); + + let ilp_solution = ILPSolver::new() + .solve(ilp) + .expect("satisfiable FRA instance should reduce to a feasible ILP"); + let fra_solution = fra_chain.extract_solution(&ilp_solution); + assert_eq!(fra.evaluate(&fra_solution), Or(true)); + + let sat_solution = ksat_chain.extract_solution(&fra_solution); + assert_eq!(source.evaluate(&sat_solution), Or(true)); +} + +#[test] +fn test_unsatisfiable_ksat_stays_infeasible_through_fra_to_ilp() { + let source = KSatisfiability::::new( + 1, + vec![ + CNFClause::new(vec![1, 1, 1]), + CNFClause::new(vec![-1, -1, -1]), + ], + ); + + let graph = ReductionGraph::new(); + let ksat_chain = graph + .reduce_along_path(&ksat_to_fra_path(), &source as &dyn std::any::Any) + .expect("KSAT -> FRA reduction should execute"); + let fra = ksat_chain.target_problem::(); + let fra_chain = graph + .reduce_along_path(&fra_to_ilp_path(), fra as &dyn std::any::Any) + .expect("FRA -> ILP reduction should execute"); + + assert!( + ILPSolver::new().solve(fra_chain.target_problem::>()).is_none(), + "unsatisfiable source instance should yield an infeasible ILP" + ); +} From 8085763317f6506255a92dda506ef9de130984d1 Mon Sep 17 00:00:00 2001 From: GiggleLiu Date: Wed, 8 Apr 2026 09:40:01 +0800 Subject: [PATCH 12/13] docs: add paper entries for FRA reductions (#905) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Add reduction-rule entries for KSatisfiability → FeasibleRegisterAssignment (Sethi Reduction 3) and FeasibleRegisterAssignment → ILP. Co-Authored-By: Claude Opus 4.6 (1M context) --- docs/paper/reductions.typ | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) diff --git a/docs/paper/reductions.typ b/docs/paper/reductions.typ index d55ce9b8..85115827 100644 --- a/docs/paper/reductions.typ +++ b/docs/paper/reductions.typ @@ -14026,6 +14026,30 @@ The following table shows concrete variable overhead for example instances, take _Solution extraction._ For each variable lobe, inspect the first lower-branch arc leaving its entry. Output $x_i = 1$ exactly when commodity 1 uses that arc. ] +#reduction-rule("KSatisfiability", "FeasibleRegisterAssignment", + example: false, +)[ + Sethi's Reduction 3 @sethi1975 @garey1979[PO2] builds a DAG with shared-register variable leaf pairs and $p\/q\/r\/overline(r)$ clause gadgets with cyclic links, plus a preassigned register allocation. The target has $2n + 12m$ vertices, $15m$ arcs, and $K = n + 9m$ registers. +][ + _Construction._ For each variable $x_k$, create two leaf nodes $s_k^+, s_k^-$ sharing register $S_k$. For each literal occurrence $Y_(i,j)$ in clause $C_i$, create four nodes $p_(i,j), q_(i,j), r_(i,j), overline(r)_(i,j)$ with internal arcs $q_(i,j) -> p_(i,j) -> r_(i,j)$ and cyclic links $q_(i,1) -> overline(r)_(i,2)$, $q_(i,2) -> overline(r)_(i,3)$, $q_(i,3) -> overline(r)_(i,1)$. Nodes $r_(i,j)$ and $overline(r)_(i,j)$ share register $R_(i,j)$. If $Y_(i,j) = x_k$: $r_(i,j) -> s_k^+$ and $overline(r)_(i,j) -> s_k^-$; if $Y_(i,j) = overline(x)_k$: swap the attachments. + + _Correctness._ ($arrow.r.double$) If $phi$ is satisfiable, place the truth-selected leaf first for each variable, then unlock each clause gadget starting from a satisfied literal. ($arrow.l.double$) The cyclic links force at least one position $j$ per clause where $r_(i,j)$ appears before $overline(r)_(i,j)$; shared-register order transfer forces the corresponding literal leaf to appear first, encoding a true literal. + + _Solution extraction._ For each variable $x_k$, set $tau(x_k) = 1$ iff $s_k^+$ appears before $s_k^-$ in the realization. +] + +#reduction-rule("FeasibleRegisterAssignment", "ILP", + example: false, +)[ + Direct ILP formulation of the feasible register assignment problem: binary permutation matrix variables, topological ordering constraints, and register-conflict constraints via shared-register ordering indicators. +][ + _Construction._ Binary variables $x_(v,t) in {0,1}$ (vertex $v$ at position $t$). Permutation: each row and column sums to $1$. Topological: for arc $(u,v)$, $sum_(t) t dot x_(v,t) < sum_(t) t dot x_(u,t)$. Register conflict: for vertices $v,w$ sharing a register, an ordering indicator $b_(v,w)$ with big-$M$ constraints ensures all dependents of the first-computed vertex complete before the second uses the register. Feasibility objective (Value $=$ Or). + + _Correctness._ The ILP is feasible iff a valid evaluation ordering respecting the register assignment exists. + + _Solution extraction._ Read vertex positions from the permutation matrix. +] + #let part_swi = load-example("Partition", "SequencingWithinIntervals") #let part_swi_sol = part_swi.solutions.at(0) #reduction-rule("Partition", "SequencingWithinIntervals", From 6bb08aeb8f940be52bea9319f4cb419b50b47d72 Mon Sep 17 00:00:00 2001 From: GiggleLiu Date: Wed, 8 Apr 2026 09:44:57 +0800 Subject: [PATCH 13/13] fix: gate ILPSolver imports behind ilp-solver feature Address Copilot review comments: ILPSolver and related imports in integration tests were unconditional but only used in feature-gated blocks. Gate them with #[cfg(feature = "ilp-solver")]. Co-Authored-By: Claude Opus 4.6 (1M context) --- tests/main.rs | 1 + tests/suites/reductions.rs | 3 +++ 2 files changed, 4 insertions(+) diff --git a/tests/main.rs b/tests/main.rs index 0e347095..a1aa9fa8 100644 --- a/tests/main.rs +++ b/tests/main.rs @@ -8,6 +8,7 @@ mod integration; mod jl_parity; #[path = "suites/ksatisfiability_simultaneous_incongruences.rs"] mod ksatisfiability_simultaneous_incongruences; +#[cfg(feature = "ilp-solver")] #[path = "suites/register_assignment_reductions.rs"] mod register_assignment_reductions; #[path = "suites/reductions.rs"] diff --git a/tests/suites/reductions.rs b/tests/suites/reductions.rs index 3e1d4457..325847fa 100644 --- a/tests/suites/reductions.rs +++ b/tests/suites/reductions.rs @@ -4,11 +4,14 @@ //! solutions can be properly extracted through the reduction pipeline. use problemreductions::models::algebraic::{LinearConstraint, ObjectiveSense, ILP}; +#[cfg(feature = "ilp-solver")] use problemreductions::models::graph::MinimumCoveringByCliques; use problemreductions::prelude::*; use problemreductions::rules::{Minimize, ReductionGraph}; +#[cfg(feature = "ilp-solver")] use problemreductions::solvers::ILPSolver; use problemreductions::topology::{Graph, SimpleGraph}; +#[cfg(feature = "ilp-solver")] use problemreductions::types::Min; use problemreductions::variant::{K2, K3};