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//! Reference: Karp 1972; Sipser Theorem 7.56; CLRS §34.5.5
11
12use crate::models::formula::KSatisfiability;
13use crate::models::misc::SubsetSum;
14use crate::reduction;
15use crate::rules::traits::{ReduceTo, ReductionResult};
16use crate::variant::K3;
17
18/// Result of reducing KSatisfiability<K3> to SubsetSum.
19#[derive(Debug, Clone)]
20pub struct Reduction3SATToSubsetSum {
21    target: SubsetSum,
22    source_num_vars: usize,
23}
24
25impl ReductionResult for Reduction3SATToSubsetSum {
26    type Source = KSatisfiability<K3>;
27    type Target = SubsetSum;
28
29    fn target_problem(&self) -> &Self::Target {
30        &self.target
31    }
32
33    fn extract_solution(&self, target_solution: &[usize]) -> Vec<usize> {
34        // Variable integers are the first 2n elements in 0-based indexing:
35        // for variable i (0 <= i < n), y_i is stored at index 2*i and z_i at index 2*i + 1.
36        // If y_i is selected (target_solution[2*i] == 1), set x_i = 1; otherwise x_i = 0.
37        (0..self.source_num_vars)
38            .map(|i| {
39                let y_selected = target_solution[2 * i] == 1;
40                if y_selected {
41                    1
42                } else {
43                    0
44                }
45            })
46            .collect()
47    }
48}
49
50/// Build a base-10 integer from a digit array (most significant first).
51///
52/// digits[0] is the most significant digit, digits[num_digits-1] is the least.
53fn digits_to_integer(digits: &[i64]) -> i64 {
54    let mut value: i64 = 0;
55    for &d in digits {
56        value = value * 10 + d;
57    }
58    value
59}
60
61#[reduction(
62    overhead = { num_elements = "2 * num_vars + 2 * num_clauses" }
63)]
64impl ReduceTo<SubsetSum> for KSatisfiability<K3> {
65    type Result = Reduction3SATToSubsetSum;
66
67    fn reduce_to(&self) -> Self::Result {
68        let n = self.num_vars();
69        let m = self.num_clauses();
70        let num_digits = n + m;
71        assert!(
72            num_digits <= 18,
73            "3-SAT to SubsetSum reduction requires n + m <= 18 for i64 encoding \
74             (got n={n}, m={m}, n+m={num_digits})"
75        );
76
77        let mut sizes = Vec::with_capacity(2 * n + 2 * m);
78
79        // Step 1: Variable integers (2n integers)
80        for i in 0..n {
81            // y_i: d_i = 1, d_{n+j} = 1 if x_{i+1} appears positive in C_j
82            let mut y_digits = vec![0i64; num_digits];
83            y_digits[i] = 1;
84            for (j, clause) in self.clauses().iter().enumerate() {
85                for &lit in &clause.literals {
86                    let var_idx = (lit.unsigned_abs() as usize) - 1;
87                    if var_idx == i && lit > 0 {
88                        y_digits[n + j] = 1;
89                    }
90                }
91            }
92            sizes.push(digits_to_integer(&y_digits));
93
94            // z_i: d_i = 1, d_{n+j} = 1 if ¬x_{i+1} appears in C_j
95            let mut z_digits = vec![0i64; num_digits];
96            z_digits[i] = 1;
97            for (j, clause) in self.clauses().iter().enumerate() {
98                for &lit in &clause.literals {
99                    let var_idx = (lit.unsigned_abs() as usize) - 1;
100                    if var_idx == i && lit < 0 {
101                        z_digits[n + j] = 1;
102                    }
103                }
104            }
105            sizes.push(digits_to_integer(&z_digits));
106        }
107
108        // Step 2: Slack integers (2m integers)
109        for j in 0..m {
110            // g_j: d_{n+j} = 1
111            let mut g_digits = vec![0i64; num_digits];
112            g_digits[n + j] = 1;
113            sizes.push(digits_to_integer(&g_digits));
114
115            // h_j: d_{n+j} = 2
116            let mut h_digits = vec![0i64; num_digits];
117            h_digits[n + j] = 2;
118            sizes.push(digits_to_integer(&h_digits));
119        }
120
121        // Step 3: Target
122        let mut target_digits = vec![0i64; num_digits];
123        for d in target_digits.iter_mut().take(n) {
124            *d = 1;
125        }
126        for d in target_digits.iter_mut().skip(n).take(m) {
127            *d = 4;
128        }
129        let target = digits_to_integer(&target_digits);
130
131        Reduction3SATToSubsetSum {
132            target: SubsetSum::new(sizes, target),
133            source_num_vars: n,
134        }
135    }
136}
137
138#[cfg(test)]
139#[path = "../unit_tests/rules/ksatisfiability_subsetsum.rs"]
140mod tests;
problemreductions/rules/ksatisfiability_subsetsum.rs

problemreductions/rules/
ksatisfiability_subsetsum.rs
