problemreductions/rules/
ksatisfiability_acyclicpartition.rs

1//! Reduction from KSatisfiability (3-SAT) to AcyclicPartition.
2//!
3//! The repository's `AcyclicPartition` model is the weighted quotient-DAG
4//! partition problem, not the "partition vertices into two induced acyclic
5//! subgraphs" variant described in issue #247. The implemented rule therefore
6//! uses a witness-preserving composition:
7//! 3-SAT -> SubsetSum -> Partition -> AcyclicPartition.
8
9use crate::models::formula::KSatisfiability;
10use crate::models::graph::AcyclicPartition;
11use crate::models::misc::{Partition, SubsetSum};
12use crate::reduction;
13use crate::rules::ksatisfiability_subsetsum::Reduction3SATToSubsetSum;
14use crate::rules::subsetsum_partition::ReductionSubsetSumToPartition;
15use crate::rules::traits::{ReduceTo, ReductionResult};
16use crate::topology::DirectedGraph;
17use crate::variant::K3;
18
19#[derive(Debug, Clone)]
20struct ReductionPartitionToAcyclicPartition {
21    target: AcyclicPartition<i32>,
22    source_num_elements: usize,
23    source_vertex: usize,
24    sink_vertex: usize,
25}
26
27impl ReductionPartitionToAcyclicPartition {
28    fn new(source: &Partition) -> Self {
29        let num_elements = source.num_elements();
30        let source_vertex = num_elements;
31        let sink_vertex = num_elements + 1;
32        let total_sum = source.total_sum();
33
34        let arcs: Vec<(usize, usize)> = (0..num_elements)
35            .flat_map(|item| [(source_vertex, item), (item, sink_vertex)])
36            .collect();
37
38        let mut vertex_weights: Vec<i32> = source
39            .sizes()
40            .iter()
41            .copied()
42            .map(|size| {
43                let doubled = size
44                    .checked_mul(2)
45                    .expect("Partition -> AcyclicPartition item weight overflow");
46                u64_to_i32(
47                    doubled,
48                    "Partition -> AcyclicPartition requires doubled sizes to fit in i32",
49                )
50            })
51            .collect();
52
53        let endpoint_weight = total_sum
54            .checked_add(1)
55            .expect("Partition -> AcyclicPartition endpoint weight overflow");
56        let even_prefix = total_sum - (total_sum % 2);
57        let weight_bound = endpoint_weight
58            .checked_add(even_prefix)
59            .expect("Partition -> AcyclicPartition weight bound overflow");
60
61        vertex_weights.push(u64_to_i32(
62            endpoint_weight,
63            "Partition -> AcyclicPartition requires endpoint weight to fit in i32",
64        ));
65        vertex_weights.push(u64_to_i32(
66            endpoint_weight,
67            "Partition -> AcyclicPartition requires endpoint weight to fit in i32",
68        ));
69
70        let arc_costs = vec![1; arcs.len()];
71        let target = AcyclicPartition::new(
72            DirectedGraph::new(num_elements + 2, arcs),
73            vertex_weights,
74            arc_costs,
75            u64_to_i32(
76                weight_bound,
77                "Partition -> AcyclicPartition requires weight bound to fit in i32",
78            ),
79            usize_to_i32(
80                num_elements,
81                "Partition -> AcyclicPartition requires num_elements to fit in i32",
82            ),
83        );
84
85        Self {
86            target,
87            source_num_elements: num_elements,
88            source_vertex,
89            sink_vertex,
90        }
91    }
92}
93
94impl ReductionResult for ReductionPartitionToAcyclicPartition {
95    type Source = Partition;
96    type Target = AcyclicPartition<i32>;
97
98    fn target_problem(&self) -> &Self::Target {
99        &self.target
100    }
101
102    fn extract_solution(&self, target_solution: &[usize]) -> Vec<usize> {
103        if target_solution.len() != self.source_num_elements + 2 {
104            return vec![0; self.source_num_elements];
105        }
106
107        let source_label = target_solution[self.source_vertex];
108        let sink_label = target_solution[self.sink_vertex];
109        debug_assert_ne!(
110            source_label, sink_label,
111            "valid target witnesses must place source and sink in different blocks"
112        );
113
114        (0..self.source_num_elements)
115            .map(|item| usize::from(target_solution[item] == sink_label))
116            .collect()
117    }
118}
119
120/// Result of reducing KSatisfiability<K3> to AcyclicPartition<i32>.
121#[derive(Debug, Clone)]
122pub struct Reduction3SATToAcyclicPartition {
123    sat_to_subset: Reduction3SATToSubsetSum,
124    subset_to_partition: ReductionSubsetSumToPartition,
125    partition_to_acyclic: ReductionPartitionToAcyclicPartition,
126}
127
128impl ReductionResult for Reduction3SATToAcyclicPartition {
129    type Source = KSatisfiability<K3>;
130    type Target = AcyclicPartition<i32>;
131
132    fn target_problem(&self) -> &Self::Target {
133        self.partition_to_acyclic.target_problem()
134    }
135
136    fn extract_solution(&self, target_solution: &[usize]) -> Vec<usize> {
137        let partition_solution = self.partition_to_acyclic.extract_solution(target_solution);
138        let subset_solution = self
139            .subset_to_partition
140            .extract_solution(&partition_solution);
141        self.sat_to_subset.extract_solution(&subset_solution)
142    }
143}
144
145fn u64_to_i32(value: u64, context: &str) -> i32 {
146    i32::try_from(value).expect(context)
147}
148
149fn usize_to_i32(value: usize, context: &str) -> i32 {
150    i32::try_from(value).expect(context)
151}
152
153#[reduction(
154    overhead = {
155        num_vertices = "2 * num_vars + 2 * num_clauses + 3",
156        num_arcs = "4 * num_vars + 4 * num_clauses + 2",
157    }
158)]
159impl ReduceTo<AcyclicPartition<i32>> for KSatisfiability<K3> {
160    type Result = Reduction3SATToAcyclicPartition;
161
162    fn reduce_to(&self) -> Self::Result {
163        let sat_to_subset = <KSatisfiability<K3> as ReduceTo<SubsetSum>>::reduce_to(self);
164        let subset_to_partition =
165            <SubsetSum as ReduceTo<Partition>>::reduce_to(sat_to_subset.target_problem());
166        let partition_to_acyclic =
167            ReductionPartitionToAcyclicPartition::new(subset_to_partition.target_problem());
168
169        Reduction3SATToAcyclicPartition {
170            sat_to_subset,
171            subset_to_partition,
172            partition_to_acyclic,
173        }
174    }
175}
176
177#[cfg(feature = "example-db")]
178pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
179    use crate::export::SolutionPair;
180    use crate::models::formula::CNFClause;
181
182    vec![crate::example_db::specs::RuleExampleSpec {
183        id: "ksatisfiability_to_acyclicpartition",
184        build: || {
185            crate::example_db::specs::rule_example_with_witness::<_, AcyclicPartition<i32>>(
186                KSatisfiability::<K3>::new(1, vec![CNFClause::new(vec![1, 1, 1])]),
187                SolutionPair {
188                    source_config: vec![1],
189                    target_config: vec![1, 0, 1, 1, 0, 0, 1],
190                },
191            )
192        },
193    }]
194}
195
196#[cfg(test)]
197#[path = "../unit_tests/rules/ksatisfiability_acyclicpartition.rs"]
198mod tests;
problemreductions/rules/ksatisfiability_acyclicpartition.rs

problemreductions/rules/
ksatisfiability_acyclicpartition.rs
