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::satisfiability::{CNFClause, KSatisfiability, Satisfiability};
10use crate::rules::traits::{ReduceTo, ReductionResult};
11use crate::traits::Problem;
12use crate::types::ProblemSize;
13use num_traits::{Num, Zero};
14use std::ops::AddAssign;
15
16/// Result of reducing general SAT to K-SAT.
17///
18/// This reduction transforms a SAT formula into an equisatisfiable K-SAT formula
19/// by introducing ancilla (auxiliary) variables.
20#[derive(Debug, Clone)]
21pub struct ReductionSATToKSAT<const K: usize, W> {
22    /// Number of original variables in the source problem.
23    source_num_vars: usize,
24    /// The target K-SAT problem.
25    target: KSatisfiability<K, W>,
26    /// Size of the source problem.
27    source_size: ProblemSize,
28}
29
30impl<const K: usize, W> ReductionResult for ReductionSATToKSAT<K, W>
31where
32    W: Clone + Default + PartialOrd + Num + Zero + AddAssign + From<i32> + 'static,
33{
34    type Source = Satisfiability<W>;
35    type Target = KSatisfiability<K, W>;
36
37    fn target_problem(&self) -> &Self::Target {
38        &self.target
39    }
40
41    fn extract_solution(&self, target_solution: &[usize]) -> Vec<usize> {
42        // Only return the original variables, discarding ancillas
43        target_solution[..self.source_num_vars].to_vec()
44    }
45
46    fn source_size(&self) -> ProblemSize {
47        self.source_size.clone()
48    }
49
50    fn target_size(&self) -> ProblemSize {
51        self.target.problem_size()
52    }
53}
54
55/// Add a clause to the K-SAT formula, splitting or padding as necessary.
56///
57/// # Algorithm
58/// - If clause has exactly K literals: add as-is
59/// - If clause has < K literals: pad with ancilla variables (both positive and negative)
60/// - If clause has > K literals: split recursively using ancilla variables
61///
62/// # Arguments
63/// * `k` - Target number of literals per clause
64/// * `clause` - The clause to add
65/// * `result_clauses` - Output vector to append clauses to
66/// * `next_var` - Next available variable number (1-indexed)
67///
68/// # Returns
69/// Updated next_var after any ancilla variables are created
70fn add_clause_to_ksat(
71    k: usize,
72    clause: &CNFClause,
73    result_clauses: &mut Vec<CNFClause>,
74    mut next_var: i32,
75) -> i32 {
76    let len = clause.len();
77
78    if len == k {
79        // Exact size: add as-is
80        result_clauses.push(clause.clone());
81    } else if len < k {
82        // Too few literals: pad with ancilla variables
83        // Create both positive and negative versions to maintain satisfiability
84        // (a v b) with k=3 becomes (a v b v x) AND (a v b v -x)
85        let ancilla = next_var;
86        next_var += 1;
87
88        // Add clause with positive ancilla
89        let mut lits_pos = clause.literals.clone();
90        lits_pos.push(ancilla);
91        next_var = add_clause_to_ksat(k, &CNFClause::new(lits_pos), result_clauses, next_var);
92
93        // Add clause with negative ancilla
94        let mut lits_neg = clause.literals.clone();
95        lits_neg.push(-ancilla);
96        next_var = add_clause_to_ksat(k, &CNFClause::new(lits_neg), result_clauses, next_var);
97    } else {
98        // Too many literals: split using ancilla variable
99        // (a v b v c v d) with k=3 becomes (a v b v x) AND (-x v c v d)
100        assert!(k >= 3, "K must be at least 3 for splitting");
101
102        let ancilla = next_var;
103        next_var += 1;
104
105        // First clause: first k-1 literals + positive ancilla
106        let mut first_lits: Vec<i32> = clause.literals[..k - 1].to_vec();
107        first_lits.push(ancilla);
108        result_clauses.push(CNFClause::new(first_lits));
109
110        // Remaining clause: negative ancilla + remaining literals
111        let mut remaining_lits = vec![-ancilla];
112        remaining_lits.extend_from_slice(&clause.literals[k - 1..]);
113        let remaining_clause = CNFClause::new(remaining_lits);
114
115        // Recursively process the remaining clause
116        next_var = add_clause_to_ksat(k, &remaining_clause, result_clauses, next_var);
117    }
118
119    next_var
120}
121
122/// Implementation of SAT -> K-SAT reduction.
123///
124/// Note: We implement this for specific K values rather than generic K
125/// because Rust's type system requires concrete implementations for
126/// the `ReduceTo` trait pattern used in this crate.
127macro_rules! impl_sat_to_ksat {
128    ($k:expr) => {
129        impl<W> ReduceTo<KSatisfiability<$k, W>> for Satisfiability<W>
130        where
131            W: Clone + Default + PartialOrd + Num + Zero + AddAssign + From<i32> + 'static,
132        {
133            type Result = ReductionSATToKSAT<$k, W>;
134
135            fn reduce_to(&self) -> Self::Result {
136                let source_num_vars = self.num_vars();
137                let mut result_clauses = Vec::new();
138                let mut next_var = (source_num_vars + 1) as i32; // 1-indexed
139
140                for clause in self.clauses() {
141                    next_var =
142                        add_clause_to_ksat($k, clause, &mut result_clauses, next_var);
143                }
144
145                // Calculate total number of variables (original + ancillas)
146                let total_vars = (next_var - 1) as usize;
147
148                let target = KSatisfiability::<$k, W>::new(total_vars, result_clauses);
149
150                ReductionSATToKSAT {
151                    source_num_vars,
152                    target,
153                    source_size: self.problem_size(),
154                }
155            }
156        }
157    };
158}
159
160// Implement for common K values
161impl_sat_to_ksat!(3);
162impl_sat_to_ksat!(4);
163impl_sat_to_ksat!(5);
164
165/// Result of reducing K-SAT to general SAT.
166///
167/// This is a trivial embedding since K-SAT is a special case of SAT.
168#[derive(Debug, Clone)]
169pub struct ReductionKSATToSAT<const K: usize, W> {
170    /// The target SAT problem.
171    target: Satisfiability<W>,
172    /// Size of the source problem.
173    source_size: ProblemSize,
174}
175
176impl<const K: usize, W> ReductionResult for ReductionKSATToSAT<K, W>
177where
178    W: Clone + Default + PartialOrd + Num + Zero + AddAssign + From<i32> + 'static,
179{
180    type Source = KSatisfiability<K, W>;
181    type Target = Satisfiability<W>;
182
183    fn target_problem(&self) -> &Self::Target {
184        &self.target
185    }
186
187    fn extract_solution(&self, target_solution: &[usize]) -> Vec<usize> {
188        // Direct mapping - no transformation needed
189        target_solution.to_vec()
190    }
191
192    fn source_size(&self) -> ProblemSize {
193        self.source_size.clone()
194    }
195
196    fn target_size(&self) -> ProblemSize {
197        self.target.problem_size()
198    }
199}
200
201impl<const K: usize, W> ReduceTo<Satisfiability<W>> for KSatisfiability<K, W>
202where
203    W: Clone + Default + PartialOrd + Num + Zero + AddAssign + From<i32> + 'static,
204{
205    type Result = ReductionKSATToSAT<K, W>;
206
207    fn reduce_to(&self) -> Self::Result {
208        let clauses = self.clauses().to_vec();
209        let target = Satisfiability::new(self.num_vars(), clauses);
210
211        ReductionKSATToSAT {
212            target,
213            source_size: self.problem_size(),
214        }
215    }
216}
217
218#[cfg(test)]
219mod tests {
220    use super::*;
221    use crate::solvers::{BruteForce, Solver};
222
223    #[test]
224    fn test_sat_to_3sat_exact_size() {
225        // Clause already has 3 literals - should remain unchanged
226        let sat = Satisfiability::<i32>::new(3, vec![CNFClause::new(vec![1, 2, 3])]);
227
228        let reduction = ReduceTo::<KSatisfiability<3, i32>>::reduce_to(&sat);
229        let ksat = reduction.target_problem();
230
231        assert_eq!(ksat.num_vars(), 3);
232        assert_eq!(ksat.num_clauses(), 1);
233        assert_eq!(ksat.clauses()[0].literals, vec![1, 2, 3]);
234    }
235
236    #[test]
237    fn test_sat_to_3sat_padding() {
238        // Clause has 2 literals - should be padded to 3
239        // (a v b) becomes (a v b v x) AND (a v b v -x)
240        let sat = Satisfiability::<i32>::new(2, vec![CNFClause::new(vec![1, 2])]);
241
242        let reduction = ReduceTo::<KSatisfiability<3, i32>>::reduce_to(&sat);
243        let ksat = reduction.target_problem();
244
245        // Should have 2 clauses (positive and negative ancilla)
246        assert_eq!(ksat.num_clauses(), 2);
247        // All clauses should have exactly 3 literals
248        for clause in ksat.clauses() {
249            assert_eq!(clause.len(), 3);
250        }
251    }
252
253    #[test]
254    fn test_sat_to_3sat_splitting() {
255        // Clause has 4 literals - should be split
256        // (a v b v c v d) becomes (a v b v x) AND (-x v c v d)
257        let sat = Satisfiability::<i32>::new(4, vec![CNFClause::new(vec![1, 2, 3, 4])]);
258
259        let reduction = ReduceTo::<KSatisfiability<3, i32>>::reduce_to(&sat);
260        let ksat = reduction.target_problem();
261
262        // Should have 2 clauses after splitting
263        assert_eq!(ksat.num_clauses(), 2);
264        // All clauses should have exactly 3 literals
265        for clause in ksat.clauses() {
266            assert_eq!(clause.len(), 3);
267        }
268
269        // Verify structure: first clause has positive ancilla, second has negative
270        let c1 = &ksat.clauses()[0];
271        let c2 = &ksat.clauses()[1];
272        // First clause: [1, 2, 5] (ancilla is var 5)
273        assert_eq!(c1.literals[0], 1);
274        assert_eq!(c1.literals[1], 2);
275        let ancilla = c1.literals[2];
276        assert!(ancilla > 0);
277        // Second clause: [-5, 3, 4]
278        assert_eq!(c2.literals[0], -ancilla);
279        assert_eq!(c2.literals[1], 3);
280        assert_eq!(c2.literals[2], 4);
281    }
282
283    #[test]
284    fn test_sat_to_3sat_large_clause() {
285        // Clause has 5 literals - requires multiple splits
286        // (a v b v c v d v e) -> (a v b v x1) AND (-x1 v c v x2) AND (-x2 v d v e)
287        let sat = Satisfiability::<i32>::new(5, vec![CNFClause::new(vec![1, 2, 3, 4, 5])]);
288
289        let reduction = ReduceTo::<KSatisfiability<3, i32>>::reduce_to(&sat);
290        let ksat = reduction.target_problem();
291
292        // Should have 3 clauses after splitting
293        assert_eq!(ksat.num_clauses(), 3);
294        // All clauses should have exactly 3 literals
295        for clause in ksat.clauses() {
296            assert_eq!(clause.len(), 3);
297        }
298    }
299
300    #[test]
301    fn test_sat_to_3sat_single_literal() {
302        // Single literal clause - needs padding twice
303        // (a) becomes (a v x v y) where we pad twice
304        let sat = Satisfiability::<i32>::new(1, vec![CNFClause::new(vec![1])]);
305
306        let reduction = ReduceTo::<KSatisfiability<3, i32>>::reduce_to(&sat);
307        let ksat = reduction.target_problem();
308
309        // With recursive padding: (a) -> (a v x) AND (a v -x)
310        // Then each of those gets padded again
311        // (a v x) -> (a v x v y) AND (a v x v -y)
312        // (a v -x) -> (a v -x v z) AND (a v -x v -z)
313        // Total: 4 clauses
314        assert_eq!(ksat.num_clauses(), 4);
315        for clause in ksat.clauses() {
316            assert_eq!(clause.len(), 3);
317        }
318    }
319
320    #[test]
321    fn test_sat_to_3sat_preserves_satisfiability() {
322        // Create a SAT formula and verify the 3-SAT version is equisatisfiable
323        let sat = Satisfiability::<i32>::new(
324            3,
325            vec![
326                CNFClause::new(vec![1, 2]),          // Needs padding
327                CNFClause::new(vec![-1, 2, 3]),      // Already 3 literals
328                CNFClause::new(vec![1, -2, 3, -3]), // Needs splitting (tautology for testing)
329            ],
330        );
331
332        let reduction = ReduceTo::<KSatisfiability<3, i32>>::reduce_to(&sat);
333        let ksat = reduction.target_problem();
334
335        // Solve both problems
336        let solver = BruteForce::new();
337
338        let sat_solutions = solver.find_best(&sat);
339        let ksat_solutions = solver.find_best(ksat);
340
341        // If SAT is satisfiable, K-SAT should be too
342        let sat_satisfiable = sat_solutions.iter().any(|s| sat.solution_size(s).is_valid);
343        let ksat_satisfiable = ksat_solutions.iter().any(|s| ksat.solution_size(s).is_valid);
344
345        assert_eq!(sat_satisfiable, ksat_satisfiable);
346
347        // Extract solutions should map back correctly
348        if ksat_satisfiable {
349            for ksat_sol in &ksat_solutions {
350                if ksat.solution_size(ksat_sol).is_valid {
351                    let sat_sol = reduction.extract_solution(ksat_sol);
352                    assert_eq!(sat_sol.len(), 3); // Original variable count
353                }
354            }
355        }
356    }
357
358    #[test]
359    fn test_sat_to_3sat_solution_extraction() {
360        let sat = Satisfiability::<i32>::new(2, vec![CNFClause::new(vec![1, 2])]);
361
362        let reduction = ReduceTo::<KSatisfiability<3, i32>>::reduce_to(&sat);
363        let ksat = reduction.target_problem();
364
365        // Solve K-SAT
366        let solver = BruteForce::new();
367        let ksat_solutions = solver.find_best(ksat);
368
369        // Extract and verify solutions
370        for ksat_sol in &ksat_solutions {
371            if ksat.solution_size(ksat_sol).is_valid {
372                let sat_sol = reduction.extract_solution(ksat_sol);
373                // Should only have original 2 variables
374                assert_eq!(sat_sol.len(), 2);
375                // Should satisfy original problem
376                assert!(sat.solution_size(&sat_sol).is_valid);
377            }
378        }
379    }
380
381    #[test]
382    fn test_3sat_to_sat() {
383        let ksat = KSatisfiability::<3, i32>::new(
384            3,
385            vec![
386                CNFClause::new(vec![1, 2, 3]),
387                CNFClause::new(vec![-1, -2, 3]),
388            ],
389        );
390
391        let reduction = ReduceTo::<Satisfiability<i32>>::reduce_to(&ksat);
392        let sat = reduction.target_problem();
393
394        assert_eq!(sat.num_vars(), 3);
395        assert_eq!(sat.num_clauses(), 2);
396
397        // Verify clauses are preserved
398        assert_eq!(sat.clauses()[0].literals, vec![1, 2, 3]);
399        assert_eq!(sat.clauses()[1].literals, vec![-1, -2, 3]);
400    }
401
402    #[test]
403    fn test_3sat_to_sat_solution_extraction() {
404        let ksat = KSatisfiability::<3, i32>::new(3, vec![CNFClause::new(vec![1, 2, 3])]);
405
406        let reduction = ReduceTo::<Satisfiability<i32>>::reduce_to(&ksat);
407
408        let sol = vec![1, 0, 1];
409        let extracted = reduction.extract_solution(&sol);
410        assert_eq!(extracted, vec![1, 0, 1]);
411    }
412
413    #[test]
414    fn test_roundtrip_sat_3sat_sat() {
415        // SAT -> 3-SAT -> SAT roundtrip
416        let original_sat = Satisfiability::<i32>::new(
417            3,
418            vec![CNFClause::new(vec![1, -2]), CNFClause::new(vec![2, 3])],
419        );
420
421        // SAT -> 3-SAT
422        let to_ksat = ReduceTo::<KSatisfiability<3, i32>>::reduce_to(&original_sat);
423        let ksat = to_ksat.target_problem();
424
425        // 3-SAT -> SAT
426        let to_sat = ReduceTo::<Satisfiability<i32>>::reduce_to(ksat);
427        let final_sat = to_sat.target_problem();
428
429        // Solve all three
430        let solver = BruteForce::new();
431
432        let orig_solutions = solver.find_best(&original_sat);
433        let ksat_solutions = solver.find_best(ksat);
434        let final_solutions = solver.find_best(final_sat);
435
436        // All should be satisfiable
437        assert!(orig_solutions.iter().any(|s| original_sat.solution_size(s).is_valid));
438        assert!(ksat_solutions.iter().any(|s| ksat.solution_size(s).is_valid));
439        assert!(final_solutions.iter().any(|s| final_sat.solution_size(s).is_valid));
440    }
441
442    #[test]
443    fn test_sat_to_4sat() {
444        let sat = Satisfiability::<i32>::new(
445            4,
446            vec![
447                CNFClause::new(vec![1, 2]),       // Needs padding
448                CNFClause::new(vec![1, 2, 3, 4]), // Exact
449                CNFClause::new(vec![1, 2, 3, 4, -1]), // Needs splitting
450            ],
451        );
452
453        let reduction = ReduceTo::<KSatisfiability<4, i32>>::reduce_to(&sat);
454        let ksat = reduction.target_problem();
455
456        // All clauses should have exactly 4 literals
457        for clause in ksat.clauses() {
458            assert_eq!(clause.len(), 4);
459        }
460    }
461
462    #[test]
463    fn test_problem_sizes() {
464        let sat = Satisfiability::<i32>::new(3, vec![CNFClause::new(vec![1, 2, 3, 4])]);
465
466        let reduction = ReduceTo::<KSatisfiability<3, i32>>::reduce_to(&sat);
467
468        let source_size = reduction.source_size();
469        let target_size = reduction.target_size();
470
471        assert_eq!(source_size.get("num_vars"), Some(3));
472        assert_eq!(target_size.get("k"), Some(3));
473    }
474
475    #[test]
476    fn test_empty_sat_to_3sat() {
477        let sat = Satisfiability::<i32>::new(3, vec![]);
478
479        let reduction = ReduceTo::<KSatisfiability<3, i32>>::reduce_to(&sat);
480        let ksat = reduction.target_problem();
481
482        assert_eq!(ksat.num_clauses(), 0);
483        assert_eq!(ksat.num_vars(), 3);
484    }
485
486    #[test]
487    fn test_mixed_clause_sizes() {
488        let sat = Satisfiability::<i32>::new(
489            5,
490            vec![
491                CNFClause::new(vec![1]),                // 1 literal
492                CNFClause::new(vec![2, 3]),             // 2 literals
493                CNFClause::new(vec![1, 2, 3]),          // 3 literals
494                CNFClause::new(vec![1, 2, 3, 4]),       // 4 literals
495                CNFClause::new(vec![1, 2, 3, 4, 5]),    // 5 literals
496            ],
497        );
498
499        let reduction = ReduceTo::<KSatisfiability<3, i32>>::reduce_to(&sat);
500        let ksat = reduction.target_problem();
501
502        // All clauses should have exactly 3 literals
503        for clause in ksat.clauses() {
504            assert_eq!(clause.len(), 3);
505        }
506
507        // Verify satisfiability is preserved
508        let solver = BruteForce::new();
509        let sat_solutions = solver.find_best(&sat);
510        let ksat_solutions = solver.find_best(ksat);
511
512        let sat_satisfiable = sat_solutions.iter().any(|s| sat.solution_size(s).is_valid);
513        let ksat_satisfiable = ksat_solutions.iter().any(|s| ksat.solution_size(s).is_valid);
514        assert_eq!(sat_satisfiable, ksat_satisfiable);
515    }
516
517    #[test]
518    fn test_unsatisfiable_formula() {
519        // (x) AND (-x) is unsatisfiable
520        let sat = Satisfiability::<i32>::new(
521            1,
522            vec![CNFClause::new(vec![1]), CNFClause::new(vec![-1])],
523        );
524
525        let reduction = ReduceTo::<KSatisfiability<3, i32>>::reduce_to(&sat);
526        let ksat = reduction.target_problem();
527
528        let solver = BruteForce::new();
529
530        // Both should be unsatisfiable
531        let sat_solutions = solver.find_best(&sat);
532        let ksat_solutions = solver.find_best(ksat);
533
534        let sat_satisfiable = sat_solutions.iter().any(|s| sat.solution_size(s).is_valid);
535        let ksat_satisfiable = ksat_solutions.iter().any(|s| ksat.solution_size(s).is_valid);
536
537        assert!(!sat_satisfiable);
538        assert!(!ksat_satisfiable);
539    }
540}
541
542// Register reductions with inventory for auto-discovery
543use crate::poly;
544use crate::rules::registry::{ReductionEntry, ReductionOverhead};
545
546inventory::submit! {
547    ReductionEntry {
548        source_name: "Satisfiability",
549        target_name: "KSatisfiability",
550        source_graph: "CNF",
551        target_graph: "KCNF",
552        overhead_fn: || ReductionOverhead::new(vec![
553            ("num_clauses", poly!(num_clauses)),
554            ("num_vars", poly!(num_vars)),
555        ]),
556    }
557}
558
559inventory::submit! {
560    ReductionEntry {
561        source_name: "KSatisfiability",
562        target_name: "Satisfiability",
563        source_graph: "KCNF",
564        target_graph: "CNF",
565        overhead_fn: || ReductionOverhead::new(vec![
566            ("num_clauses", poly!(num_clauses)),
567            ("num_vars", poly!(num_vars)),
568        ]),
569    }
570}
problemreductions/rules/sat_ksat.rs

problemreductions/rules/
sat_ksat.rs
