problemreductions/rules/
ksatisfiability_subsetsum.rs

1//! Reduction from KSatisfiability (3-SAT) to SubsetSum.
2//!
3//! Classical Karp reduction using base-10 digit encoding. Each integer has
4//! (n + m) digits, where n is the number of variables and m is the number
5//! of clauses. Variable digits ensure exactly one of y_i/z_i per variable;
6//! clause digits count satisfied literals, padded to 4 by slack integers.
7//!
8//! No carries occur because the maximum digit sum is at most 3 + 2 = 5 < 10.
9//!
10//! Uses `SubsetSum` with arbitrary-precision integers so the encoding does not
11//! overflow on large instances.
12//!
13//! Reference: Karp 1972; Sipser Theorem 7.56; CLRS §34.5.5
14
15use crate::models::formula::KSatisfiability;
16use crate::models::misc::SubsetSum;
17use crate::reduction;
18use crate::rules::traits::{ReduceTo, ReductionResult};
19use crate::variant::K3;
20use num_bigint::BigUint;
21use num_traits::Zero;
22
23/// Result of reducing KSatisfiability<K3> to SubsetSum.
24#[derive(Debug, Clone)]
25pub struct Reduction3SATToSubsetSum {
26    target: SubsetSum,
27    source_num_vars: usize,
28}
29
30impl ReductionResult for Reduction3SATToSubsetSum {
31    type Source = KSatisfiability<K3>;
32    type Target = SubsetSum;
33
34    fn target_problem(&self) -> &Self::Target {
35        &self.target
36    }
37
38    fn extract_solution(&self, target_solution: &[usize]) -> Vec<usize> {
39        // Variable integers are the first 2n elements in 0-based indexing:
40        // for variable i (0 <= i < n), y_i is stored at index 2*i and z_i at index 2*i + 1.
41        // If y_i is selected (target_solution[2*i] == 1), set x_i = 1; otherwise x_i = 0.
42        (0..self.source_num_vars)
43            .map(|i| {
44                let y_selected = target_solution[2 * i] == 1;
45                if y_selected {
46                    1
47                } else {
48                    0
49                }
50            })
51            .collect()
52    }
53}
54
55/// Build a base-10 integer from a digit array (most significant first).
56///
57/// digits[0] is the most significant digit, digits[num_digits-1] is the least.
58fn digits_to_integer(digits: &[u8]) -> BigUint {
59    let mut value = BigUint::zero();
60    let ten = BigUint::from(10u8);
61    for &d in digits {
62        value = value * &ten + BigUint::from(d);
63    }
64    value
65}
66
67#[reduction(
68    overhead = { num_elements = "2 * num_vars + 2 * num_clauses" }
69)]
70impl ReduceTo<SubsetSum> for KSatisfiability<K3> {
71    type Result = Reduction3SATToSubsetSum;
72
73    fn reduce_to(&self) -> Self::Result {
74        let n = self.num_vars();
75        let m = self.num_clauses();
76        let num_digits = n + m;
77
78        let mut sizes = Vec::with_capacity(2 * n + 2 * m);
79
80        // Step 1: Variable integers (2n integers)
81        for i in 0..n {
82            // y_i: d_i = 1, d_{n+j} = 1 if x_{i+1} appears positive in C_j
83            let mut y_digits = vec![0u8; num_digits];
84            y_digits[i] = 1;
85            for (j, clause) in self.clauses().iter().enumerate() {
86                for &lit in &clause.literals {
87                    let var_idx = (lit.unsigned_abs() as usize) - 1;
88                    if var_idx == i && lit > 0 {
89                        y_digits[n + j] = 1;
90                    }
91                }
92            }
93            sizes.push(digits_to_integer(&y_digits));
94
95            // z_i: d_i = 1, d_{n+j} = 1 if ¬x_{i+1} appears in C_j
96            let mut z_digits = vec![0u8; num_digits];
97            z_digits[i] = 1;
98            for (j, clause) in self.clauses().iter().enumerate() {
99                for &lit in &clause.literals {
100                    let var_idx = (lit.unsigned_abs() as usize) - 1;
101                    if var_idx == i && lit < 0 {
102                        z_digits[n + j] = 1;
103                    }
104                }
105            }
106            sizes.push(digits_to_integer(&z_digits));
107        }
108
109        // Step 2: Slack integers (2m integers)
110        for j in 0..m {
111            // g_j: d_{n+j} = 1
112            let mut g_digits = vec![0u8; num_digits];
113            g_digits[n + j] = 1;
114            sizes.push(digits_to_integer(&g_digits));
115
116            // h_j: d_{n+j} = 2
117            let mut h_digits = vec![0u8; num_digits];
118            h_digits[n + j] = 2;
119            sizes.push(digits_to_integer(&h_digits));
120        }
121
122        // Step 3: Target
123        let mut target_digits = vec![0u8; num_digits];
124        for d in target_digits.iter_mut().take(n) {
125            *d = 1;
126        }
127        for d in target_digits.iter_mut().skip(n).take(m) {
128            *d = 4;
129        }
130        let target = digits_to_integer(&target_digits);
131
132        Reduction3SATToSubsetSum {
133            target: SubsetSum::new_unchecked(sizes, target),
134            source_num_vars: n,
135        }
136    }
137}
138
139#[cfg(feature = "example-db")]
140pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
141    use crate::export::SolutionPair;
142    use crate::models::formula::CNFClause;
143    use crate::models::misc::SubsetSum;
144
145    vec![crate::example_db::specs::RuleExampleSpec {
146        id: "ksatisfiability_to_subsetsum",
147        build: || {
148            let source = KSatisfiability::<K3>::new(
149                3,
150                vec![
151                    CNFClause::new(vec![1, 2, 3]),
152                    CNFClause::new(vec![-1, -2, 3]),
153                ],
154            );
155            crate::example_db::specs::rule_example_with_witness::<_, SubsetSum>(
156                source,
157                SolutionPair {
158                    source_config: vec![0, 0, 1],
159                    target_config: vec![0, 1, 0, 1, 1, 0, 1, 1, 1, 0],
160                },
161            )
162        },
163    }]
164}
165
166#[cfg(test)]
167#[path = "../unit_tests/rules/ksatisfiability_subsetsum.rs"]
168mod tests;
problemreductions/rules/ksatisfiability_subsetsum.rs

problemreductions/rules/
ksatisfiability_subsetsum.rs
