problemreductions/rules/
sat_ksat.rs

1//! Reductions between Satisfiability and K-Satisfiability problems.
2//!
3//! SAT -> K-SAT: Convert general CNF to K-literal clauses using:
4//! - Padding with ancilla variables for clauses with < K literals
5//! - Splitting with ancilla variables for clauses with > K literals
6//!
7//! K-SAT -> SAT: Trivial embedding (K-SAT is a special case of SAT)
8
9use crate::models::formula::{CNFClause, KSatisfiability, Satisfiability};
10use crate::reduction;
11use crate::rules::traits::{ReduceTo, ReductionResult};
12use crate::variant::{KValue, K2, K3, KN};
13
14/// Result of reducing general SAT to K-SAT.
15///
16/// This reduction transforms a SAT formula into an equisatisfiable K-SAT formula
17/// by introducing ancilla (auxiliary) variables.
18#[derive(Debug, Clone)]
19pub struct ReductionSATToKSAT<K: KValue> {
20    /// Number of original variables in the source problem.
21    source_num_vars: usize,
22    /// The target K-SAT problem.
23    target: KSatisfiability<K>,
24}
25
26impl<K: KValue> ReductionResult for ReductionSATToKSAT<K> {
27    type Source = Satisfiability;
28    type Target = KSatisfiability<K>;
29
30    fn target_problem(&self) -> &Self::Target {
31        &self.target
32    }
33
34    fn extract_solution(&self, target_solution: &[usize]) -> Vec<usize> {
35        // Only return the original variables, discarding ancillas
36        target_solution[..self.source_num_vars].to_vec()
37    }
38}
39
40/// Add a clause to the K-SAT formula, splitting or padding as necessary.
41///
42/// # Algorithm
43/// - If clause has exactly K literals: add as-is
44/// - If clause has < K literals: pad with ancilla variables (both positive and negative)
45/// - If clause has > K literals: split recursively using ancilla variables
46///
47/// # Arguments
48/// * `k` - Target number of literals per clause
49/// * `clause` - The clause to add
50/// * `result_clauses` - Output vector to append clauses to
51/// * `next_var` - Next available variable number (1-indexed)
52///
53/// # Returns
54/// Updated next_var after any ancilla variables are created
55fn add_clause_to_ksat(
56    k: usize,
57    clause: &CNFClause,
58    result_clauses: &mut Vec<CNFClause>,
59    mut next_var: i32,
60) -> i32 {
61    let len = clause.len();
62
63    if len == k {
64        // Exact size: add as-is
65        result_clauses.push(clause.clone());
66    } else if len < k {
67        // Too few literals: pad with ancilla variables
68        // Create both positive and negative versions to maintain satisfiability
69        // (a v b) with k=3 becomes (a v b v x) AND (a v b v -x)
70        let ancilla = next_var;
71        next_var += 1;
72
73        // Add clause with positive ancilla
74        let mut lits_pos = clause.literals.clone();
75        lits_pos.push(ancilla);
76        next_var = add_clause_to_ksat(k, &CNFClause::new(lits_pos), result_clauses, next_var);
77
78        // Add clause with negative ancilla
79        let mut lits_neg = clause.literals.clone();
80        lits_neg.push(-ancilla);
81        next_var = add_clause_to_ksat(k, &CNFClause::new(lits_neg), result_clauses, next_var);
82    } else {
83        // Too many literals: split using ancilla variable
84        // (a v b v c v d) with k=3 becomes (a v b v x) AND (-x v c v d)
85        assert!(k >= 3, "K must be at least 3 for splitting");
86
87        let ancilla = next_var;
88        next_var += 1;
89
90        // First clause: first k-1 literals + positive ancilla
91        let mut first_lits: Vec<i32> = clause.literals[..k - 1].to_vec();
92        first_lits.push(ancilla);
93        result_clauses.push(CNFClause::new(first_lits));
94
95        // Remaining clause: negative ancilla + remaining literals
96        let mut remaining_lits = vec![-ancilla];
97        remaining_lits.extend_from_slice(&clause.literals[k - 1..]);
98        let remaining_clause = CNFClause::new(remaining_lits);
99
100        // Recursively process the remaining clause
101        next_var = add_clause_to_ksat(k, &remaining_clause, result_clauses, next_var);
102    }
103
104    next_var
105}
106
107/// Implementation of SAT -> K-SAT reduction.
108///
109/// Note: We implement this for specific K values rather than generic K
110/// because the `#[reduction]` proc macro requires concrete types.
111macro_rules! impl_sat_to_ksat {
112    ($ktype:ty, $k:expr) => {
113        #[rustfmt::skip]
114        #[reduction(overhead = {
115            num_clauses = "4 * num_clauses + num_literals",
116            num_vars = "num_vars + 3 * num_clauses + num_literals",
117        })]
118        impl ReduceTo<KSatisfiability<$ktype>> for Satisfiability {
119            type Result = ReductionSATToKSAT<$ktype>;
120
121            fn reduce_to(&self) -> Self::Result {
122                let source_num_vars = self.num_vars();
123                let mut result_clauses = Vec::new();
124                let mut next_var = (source_num_vars + 1) as i32; // 1-indexed
125
126                for clause in self.clauses() {
127                    next_var = add_clause_to_ksat($k, clause, &mut result_clauses, next_var);
128                }
129
130                // Calculate total number of variables (original + ancillas)
131                let total_vars = (next_var - 1) as usize;
132
133                let target = KSatisfiability::<$ktype>::new(total_vars, result_clauses);
134
135                ReductionSATToKSAT {
136                    source_num_vars,
137                    target,
138                }
139            }
140        }
141    };
142}
143
144// Implement for K=3 (the canonical NP-complete case)
145impl_sat_to_ksat!(K3, 3);
146
147/// Result of reducing K-SAT to general SAT.
148///
149/// This is a trivial embedding since K-SAT is a special case of SAT.
150#[derive(Debug, Clone)]
151pub struct ReductionKSATToSAT<K: KValue> {
152    /// The target SAT problem.
153    target: Satisfiability,
154    _phantom: std::marker::PhantomData<K>,
155}
156
157impl<K: KValue> ReductionResult for ReductionKSATToSAT<K> {
158    type Source = KSatisfiability<K>;
159    type Target = Satisfiability;
160
161    fn target_problem(&self) -> &Self::Target {
162        &self.target
163    }
164
165    fn extract_solution(&self, target_solution: &[usize]) -> Vec<usize> {
166        // Direct mapping - no transformation needed
167        target_solution.to_vec()
168    }
169}
170
171/// Helper function for KSAT -> SAT reduction logic (generic over K).
172fn reduce_ksat_to_sat<K: KValue>(ksat: &KSatisfiability<K>) -> ReductionKSATToSAT<K> {
173    let clauses = ksat.clauses().to_vec();
174    let target = Satisfiability::new(ksat.num_vars(), clauses);
175
176    ReductionKSATToSAT {
177        target,
178        _phantom: std::marker::PhantomData,
179    }
180}
181
182/// Macro for concrete KSAT -> SAT reduction impls.
183/// The `#[reduction]` macro requires concrete types.
184macro_rules! impl_ksat_to_sat {
185    ($ktype:ty) => {
186#[rustfmt::skip]
187        #[reduction(overhead = {
188            num_clauses = "num_clauses",
189            num_vars = "num_vars",
190            num_literals = "num_literals",
191        })]
192        impl ReduceTo<Satisfiability> for KSatisfiability<$ktype> {
193            type Result = ReductionKSATToSAT<$ktype>;
194
195            fn reduce_to(&self) -> Self::Result {
196                reduce_ksat_to_sat(self)
197            }
198        }
199    };
200}
201
202// Register KN for the reduction graph (covers all K values as the generic entry)
203impl_ksat_to_sat!(KN);
204
205// K3 and K2 keep their ReduceTo<Satisfiability> impls for typed use,
206// but are NOT registered as separate primitive graph edges (KN covers them).
207impl ReduceTo<Satisfiability> for KSatisfiability<K3> {
208    type Result = ReductionKSATToSAT<K3>;
209    fn reduce_to(&self) -> Self::Result {
210        reduce_ksat_to_sat(self)
211    }
212}
213
214impl ReduceTo<Satisfiability> for KSatisfiability<K2> {
215    type Result = ReductionKSATToSAT<K2>;
216    fn reduce_to(&self) -> Self::Result {
217        reduce_ksat_to_sat(self)
218    }
219}
220
221#[cfg(feature = "example-db")]
222pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
223    use crate::export::SolutionPair;
224    use crate::models::formula::CNFClause;
225
226    vec![
227        crate::example_db::specs::RuleExampleSpec {
228            id: "satisfiability_to_ksatisfiability",
229            build: || {
230                let source = Satisfiability::new(
231                    5,
232                    vec![
233                        CNFClause::new(vec![1]),
234                        CNFClause::new(vec![2, -3]),
235                        CNFClause::new(vec![-1, 3, 4]),
236                        CNFClause::new(vec![2, -4, 5]),
237                        CNFClause::new(vec![1, -2, 3, -5]),
238                        CNFClause::new(vec![-1, 2, -3, 4, 5]),
239                    ],
240                );
241                crate::example_db::specs::rule_example_with_witness::<_, KSatisfiability<K3>>(
242                    source,
243                    SolutionPair {
244                        source_config: vec![1, 1, 1, 0, 1],
245                        target_config: vec![1, 1, 1, 0, 1, 0, 0, 0, 0, 1, 1, 1],
246                    },
247                )
248            },
249        },
250        crate::example_db::specs::RuleExampleSpec {
251            id: "ksatisfiability_to_satisfiability",
252            build: || {
253                let source = KSatisfiability::<KN>::new(
254                    4,
255                    vec![
256                        CNFClause::new(vec![1, -2, 3]),
257                        CNFClause::new(vec![-1, 3, 4]),
258                        CNFClause::new(vec![2, -3, -4]),
259                    ],
260                );
261                crate::example_db::specs::rule_example_with_witness::<_, Satisfiability>(
262                    source,
263                    SolutionPair {
264                        source_config: vec![1, 1, 1, 0],
265                        target_config: vec![1, 1, 1, 0],
266                    },
267                )
268            },
269        },
270    ]
271}
272
273#[cfg(test)]
274#[path = "../unit_tests/rules/sat_ksat.rs"]
275mod tests;
problemreductions/rules/sat_ksat.rs

problemreductions/rules/
sat_ksat.rs
