problemreductions/rules/
exactcoverby3sets_ilp.rs

1//! Reduction from ExactCoverBy3Sets to ILP (Integer Linear Programming).
2//!
3//! Binary variable x_j per triple; for each element e, require Σ x_j = 1
4//! (exact cover). Additional constraint Σ x_j = universe_size/3.
5
6use crate::models::algebraic::{LinearConstraint, ObjectiveSense, ILP};
7use crate::models::set::ExactCoverBy3Sets;
8use crate::reduction;
9use crate::rules::traits::{ReduceTo, ReductionResult};
10
11#[derive(Debug, Clone)]
12pub struct ReductionX3CToILP {
13    target: ILP<bool>,
14}
15
16impl ReductionResult for ReductionX3CToILP {
17    type Source = ExactCoverBy3Sets;
18    type Target = ILP<bool>;
19
20    fn target_problem(&self) -> &ILP<bool> {
21        &self.target
22    }
23
24    fn extract_solution(
25        &self,
26        target_solution: &<Self::Target as crate::traits::Problem>::Solution,
27    ) -> crate::rules::ExtractionResult<<Self::Source as crate::traits::Problem>::Solution> {
28        crate::rules::traits::validate_target_witness(
29            self.target_problem(),
30            target_solution,
31            |value| value.value.is_some(),
32            "target ILP assignment is infeasible",
33        )?;
34
35        Ok(target_solution.iter().map(|&value| value == 1).collect())
36    }
37}
38
39#[crate::aggregate_reduction(ilp_feasibility)]
40impl crate::rules::AggregateReductionResult for ReductionX3CToILP {}
41
42#[reduction(transform = {
43    exact {
44        num_vars = "num_subsets",
45        num_constraints = "universe_size + 1",
46        num_nonzeros = "4 * num_subsets",
47    },
48    upper_bound {
49        max_constraint_magnitude_bits = "universe_size + 1",
50    },
51})]
52impl ReduceTo<ILP<bool>> for ExactCoverBy3Sets {
53    type Result = ReductionX3CToILP;
54
55    fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
56        let num_vars = self.num_subsets();
57        let mut constraints = Vec::new();
58
59        // For each element e: Σ_{j: e ∈ triple_j} x_j = 1
60        for element in 0..self.universe_size() {
61            let terms: Vec<(usize, i64)> = self
62                .subsets()
63                .iter()
64                .enumerate()
65                .filter(|(_, subset)| subset.contains(&element))
66                .map(|(j, _)| (j, 1))
67                .collect();
68            constraints.push(LinearConstraint::eq(terms, 1));
69        }
70
71        // Σ x_j = universe_size / 3
72        let cardinality_terms: Vec<(usize, i64)> = (0..num_vars).map(|j| (j, 1)).collect();
73        constraints.push(LinearConstraint::eq(
74            cardinality_terms,
75            <Self as ReduceTo<ILP<bool>>>::exact_i64(
76                self.universe_size() / 3,
77                "encoding the exact-cover cardinality",
78            )?,
79        ));
80
81        let target = ILP::new(num_vars, constraints, vec![], ObjectiveSense::Minimize)
82            .map_err(<Self as ReduceTo<ILP<bool>>>::target_construction)?;
83        Ok(ReductionX3CToILP { target })
84    }
85}
86
87#[cfg(feature = "example-db")]
88pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
89    use crate::export::SolutionPair;
90    vec![crate::example_db::specs::RuleExampleSpec {
91        id: "exactcoverby3sets_to_ilp",
92        build: || {
93            let source =
94                ExactCoverBy3Sets::new(6, vec![[0, 1, 2], [3, 4, 5], [0, 3, 4], [1, 2, 5]]);
95            crate::example_db::specs::rule_example_with_witness::<_, ILP<bool>>(
96                source,
97                SolutionPair {
98                    source_config: serde_json::json!(vec![true, true, false, false]),
99                    target_config: serde_json::json!(vec![1, 1, 0, 0]),
100                },
101            )
102        },
103    }]
104}
105
106#[cfg(test)]
107#[path = "../unit_tests/rules/exactcoverby3sets_ilp.rs"]
108mod tests;
problemreductions/rules/exactcoverby3sets_ilp.rs

problemreductions/rules/
exactcoverby3sets_ilp.rs
