problemreductions/rules/
sat_independentset.rs

1//! Reduction from Satisfiability (SAT) to IndependentSet.
2//!
3//! The reduction creates one vertex for each literal occurrence in each clause.
4//! Edges are added:
5//! 1. Between all literals within the same clause (forming a clique per clause)
6//! 2. Between complementary literals (x and NOT x) across different clauses
7//!
8//! A satisfying assignment corresponds to an independent set of size = num_clauses,
9//! where we pick exactly one literal from each clause.
10
11use crate::models::graph::IndependentSet;
12use crate::models::satisfiability::Satisfiability;
13use crate::rules::traits::{ReduceTo, ReductionResult};
14use crate::traits::Problem;
15use crate::types::ProblemSize;
16use num_traits::{Num, Zero};
17use std::ops::AddAssign;
18
19/// A literal in the SAT problem, representing a variable or its negation.
20#[derive(Debug, Clone, PartialEq, Eq)]
21pub struct BoolVar {
22    /// The variable name/index (0-indexed).
23    pub name: usize,
24    /// Whether this literal is negated.
25    pub neg: bool,
26}
27
28impl BoolVar {
29    /// Create a new literal.
30    pub fn new(name: usize, neg: bool) -> Self {
31        Self { name, neg }
32    }
33
34    /// Create a literal from a signed integer (1-indexed, as in DIMACS format).
35    /// Positive means the variable, negative means its negation.
36    pub fn from_literal(lit: i32) -> Self {
37        let name = lit.unsigned_abs() as usize - 1; // Convert to 0-indexed
38        let neg = lit < 0;
39        Self { name, neg }
40    }
41
42    /// Check if this literal is the complement of another.
43    pub fn is_complement(&self, other: &BoolVar) -> bool {
44        self.name == other.name && self.neg != other.neg
45    }
46}
47
48/// Result of reducing Satisfiability to IndependentSet.
49///
50/// This struct contains:
51/// - The target IndependentSet problem
52/// - A mapping from vertex indices to literals
53/// - The list of source variable indices
54/// - The number of clauses in the original SAT problem
55#[derive(Debug, Clone)]
56pub struct ReductionSATToIS<W> {
57    /// The target IndependentSet problem.
58    target: IndependentSet<W>,
59    /// Mapping from vertex index to the literal it represents.
60    literals: Vec<BoolVar>,
61    /// The number of variables in the source SAT problem.
62    num_source_variables: usize,
63    /// The number of clauses in the source SAT problem.
64    num_clauses: usize,
65    /// Size of the source problem.
66    source_size: ProblemSize,
67}
68
69impl<W> ReductionResult for ReductionSATToIS<W>
70where
71    W: Clone + Default + PartialOrd + Num + Zero + AddAssign + 'static,
72{
73    type Source = Satisfiability<W>;
74    type Target = IndependentSet<W>;
75
76    fn target_problem(&self) -> &Self::Target {
77        &self.target
78    }
79
80    /// Extract a SAT solution from an IndependentSet solution.
81    ///
82    /// For each selected vertex (representing a literal), we set the corresponding
83    /// variable to make that literal true. Variables not covered by any selected
84    /// literal default to false.
85    fn extract_solution(&self, target_solution: &[usize]) -> Vec<usize> {
86        let mut assignment = vec![0usize; self.num_source_variables];
87        let mut covered = vec![false; self.num_source_variables];
88
89        for (vertex_idx, &selected) in target_solution.iter().enumerate() {
90            if selected == 1 {
91                let literal = &self.literals[vertex_idx];
92                // If the literal is positive (neg=false), variable should be true (1)
93                // If the literal is negated (neg=true), variable should be false (0)
94                assignment[literal.name] = if literal.neg { 0 } else { 1 };
95                covered[literal.name] = true;
96            }
97        }
98
99        // Variables not covered can be assigned any value (we use 0)
100        // They are already initialized to 0
101        assignment
102    }
103
104    fn source_size(&self) -> ProblemSize {
105        self.source_size.clone()
106    }
107
108    fn target_size(&self) -> ProblemSize {
109        self.target.problem_size()
110    }
111}
112
113impl<W> ReductionSATToIS<W> {
114    /// Get the number of clauses in the source SAT problem.
115    pub fn num_clauses(&self) -> usize {
116        self.num_clauses
117    }
118
119    /// Get a reference to the literals mapping.
120    pub fn literals(&self) -> &[BoolVar] {
121        &self.literals
122    }
123}
124
125impl<W> ReduceTo<IndependentSet<W>> for Satisfiability<W>
126where
127    W: Clone + Default + PartialOrd + Num + Zero + AddAssign + From<i32> + 'static,
128{
129    type Result = ReductionSATToIS<W>;
130
131    fn reduce_to(&self) -> Self::Result {
132        let mut literals: Vec<BoolVar> = Vec::new();
133        let mut edges: Vec<(usize, usize)> = Vec::new();
134        let mut vertex_count = 0;
135
136        // First pass: add vertices for each literal in each clause
137        // and add clique edges within each clause
138        for clause in self.clauses() {
139            let clause_start = vertex_count;
140
141            // Add vertices for each literal in this clause
142            for &lit in &clause.literals {
143                literals.push(BoolVar::from_literal(lit));
144                vertex_count += 1;
145            }
146
147            // Add clique edges within this clause
148            for i in clause_start..vertex_count {
149                for j in (i + 1)..vertex_count {
150                    edges.push((i, j));
151                }
152            }
153        }
154
155        // Second pass: add edges between complementary literals across clauses
156        // Since we only add clique edges within clauses in the first pass,
157        // complementary literals in different clauses won't already have an edge
158        for i in 0..vertex_count {
159            for j in (i + 1)..vertex_count {
160                if literals[i].is_complement(&literals[j]) {
161                    edges.push((i, j));
162                }
163            }
164        }
165
166        let target = IndependentSet::new(vertex_count, edges);
167
168        ReductionSATToIS {
169            target,
170            literals,
171            num_source_variables: self.num_vars(),
172            num_clauses: self.num_clauses(),
173            source_size: self.problem_size(),
174        }
175    }
176}
177
178#[cfg(test)]
179mod tests {
180    use super::*;
181    use crate::models::satisfiability::CNFClause;
182    use crate::solvers::{BruteForce, Solver};
183
184    #[test]
185    fn test_boolvar_creation() {
186        let var = BoolVar::new(0, false);
187        assert_eq!(var.name, 0);
188        assert!(!var.neg);
189
190        let neg_var = BoolVar::new(1, true);
191        assert_eq!(neg_var.name, 1);
192        assert!(neg_var.neg);
193    }
194
195    #[test]
196    fn test_boolvar_from_literal() {
197        // Positive literal: variable 1 (1-indexed) -> variable 0 (0-indexed), not negated
198        let var = BoolVar::from_literal(1);
199        assert_eq!(var.name, 0);
200        assert!(!var.neg);
201
202        // Negative literal: variable 2 (1-indexed) -> variable 1 (0-indexed), negated
203        let neg_var = BoolVar::from_literal(-2);
204        assert_eq!(neg_var.name, 1);
205        assert!(neg_var.neg);
206    }
207
208    #[test]
209    fn test_boolvar_complement() {
210        let x = BoolVar::new(0, false);
211        let not_x = BoolVar::new(0, true);
212        let y = BoolVar::new(1, false);
213
214        assert!(x.is_complement(&not_x));
215        assert!(not_x.is_complement(&x));
216        assert!(!x.is_complement(&y));
217        assert!(!x.is_complement(&x));
218    }
219
220    #[test]
221    fn test_simple_sat_to_is() {
222        // Simple SAT: (x1) - one clause with one literal
223        let sat = Satisfiability::<i32>::new(1, vec![CNFClause::new(vec![1])]);
224        let reduction = ReduceTo::<IndependentSet<i32>>::reduce_to(&sat);
225        let is_problem = reduction.target_problem();
226
227        // Should have 1 vertex (one literal)
228        assert_eq!(is_problem.num_vertices(), 1);
229        // No edges (single vertex can't form a clique)
230        assert_eq!(is_problem.num_edges(), 0);
231    }
232
233    #[test]
234    fn test_two_clause_sat_to_is() {
235        // SAT: (x1) AND (NOT x1)
236        // This is unsatisfiable
237        let sat = Satisfiability::<i32>::new(
238            1,
239            vec![CNFClause::new(vec![1]), CNFClause::new(vec![-1])],
240        );
241        let reduction = ReduceTo::<IndependentSet<i32>>::reduce_to(&sat);
242        let is_problem = reduction.target_problem();
243
244        // Should have 2 vertices
245        assert_eq!(is_problem.num_vertices(), 2);
246        // Should have 1 edge (between x1 and NOT x1)
247        assert_eq!(is_problem.num_edges(), 1);
248
249        // Maximum IS should have size 1 (can't select both)
250        let solver = BruteForce::new();
251        let solutions = solver.find_best(is_problem);
252        for sol in &solutions {
253            assert_eq!(sol.iter().sum::<usize>(), 1);
254        }
255    }
256
257    #[test]
258    fn test_satisfiable_formula() {
259        // SAT: (x1 OR x2) AND (NOT x1 OR x2) AND (x1 OR NOT x2)
260        // Satisfiable with x1=true, x2=true or x1=false, x2=true
261        let sat = Satisfiability::<i32>::new(
262            2,
263            vec![
264                CNFClause::new(vec![1, 2]),   // x1 OR x2
265                CNFClause::new(vec![-1, 2]),  // NOT x1 OR x2
266                CNFClause::new(vec![1, -2]),  // x1 OR NOT x2
267            ],
268        );
269        let reduction = ReduceTo::<IndependentSet<i32>>::reduce_to(&sat);
270        let is_problem = reduction.target_problem();
271
272        // Should have 6 vertices (2 literals per clause, 3 clauses)
273        assert_eq!(is_problem.num_vertices(), 6);
274
275        // Count edges:
276        // - 3 edges within clauses (one per clause, since each clause has 2 literals)
277        // - Edges between complementary literals across clauses:
278        //   - x1 (clause 0, vertex 0) and NOT x1 (clause 1, vertex 2)
279        //   - x2 (clause 0, vertex 1) and NOT x2 (clause 2, vertex 5)
280        //   - x2 (clause 1, vertex 3) and NOT x2 (clause 2, vertex 5)
281        //   - x1 (clause 2, vertex 4) and NOT x1 (clause 1, vertex 2)
282        // Total: 3 (clique) + 4 (complement) = 7 edges
283
284        // Solve the IS problem
285        let solver = BruteForce::new();
286        let is_solutions = solver.find_best(is_problem);
287
288        // Max IS should be 3 (one literal per clause)
289        for sol in &is_solutions {
290            assert_eq!(sol.iter().sum::<usize>(), 3);
291        }
292
293        // Extract SAT solutions and verify they satisfy the original formula
294        for sol in &is_solutions {
295            let sat_sol = reduction.extract_solution(sol);
296            let assignment: Vec<bool> = sat_sol.iter().map(|&v| v == 1).collect();
297            assert!(
298                sat.is_satisfying(&assignment),
299                "Extracted solution {:?} should satisfy the SAT formula",
300                assignment
301            );
302        }
303    }
304
305    #[test]
306    fn test_unsatisfiable_formula() {
307        // SAT: (x1) AND (NOT x1) - unsatisfiable
308        let sat = Satisfiability::<i32>::new(
309            1,
310            vec![CNFClause::new(vec![1]), CNFClause::new(vec![-1])],
311        );
312        let reduction = ReduceTo::<IndependentSet<i32>>::reduce_to(&sat);
313        let is_problem = reduction.target_problem();
314
315        let solver = BruteForce::new();
316        let is_solutions = solver.find_best(is_problem);
317
318        // Max IS can only be 1 (not 2 = num_clauses)
319        // This indicates the formula is unsatisfiable
320        for sol in &is_solutions {
321            assert!(
322                sol.iter().sum::<usize>() < reduction.num_clauses(),
323                "For unsatisfiable formula, IS size should be less than num_clauses"
324            );
325        }
326    }
327
328    #[test]
329    fn test_three_sat_example() {
330        // 3-SAT: (x1 OR x2 OR x3) AND (NOT x1 OR NOT x2 OR x3) AND (x1 OR NOT x2 OR NOT x3)
331        let sat = Satisfiability::<i32>::new(
332            3,
333            vec![
334                CNFClause::new(vec![1, 2, 3]),     // x1 OR x2 OR x3
335                CNFClause::new(vec![-1, -2, 3]),   // NOT x1 OR NOT x2 OR x3
336                CNFClause::new(vec![1, -2, -3]),   // x1 OR NOT x2 OR NOT x3
337            ],
338        );
339
340        let reduction = ReduceTo::<IndependentSet<i32>>::reduce_to(&sat);
341        let is_problem = reduction.target_problem();
342
343        // Should have 9 vertices (3 literals per clause, 3 clauses)
344        assert_eq!(is_problem.num_vertices(), 9);
345
346        let solver = BruteForce::new();
347        let is_solutions = solver.find_best(is_problem);
348
349        // Check that max IS has size 3 (satisfiable)
350        let max_size = is_solutions[0].iter().sum::<usize>();
351        assert_eq!(max_size, 3, "3-SAT should be satisfiable with IS size = 3");
352
353        // Verify extracted solutions
354        for sol in &is_solutions {
355            let sat_sol = reduction.extract_solution(sol);
356            let assignment: Vec<bool> = sat_sol.iter().map(|&v| v == 1).collect();
357            assert!(sat.is_satisfying(&assignment));
358        }
359    }
360
361    #[test]
362    fn test_extract_solution_basic() {
363        // Simple case: (x1 OR x2)
364        let sat = Satisfiability::<i32>::new(2, vec![CNFClause::new(vec![1, 2])]);
365        let reduction = ReduceTo::<IndependentSet<i32>>::reduce_to(&sat);
366
367        // Select vertex 0 (literal x1)
368        let is_sol = vec![1, 0];
369        let sat_sol = reduction.extract_solution(&is_sol);
370        assert_eq!(sat_sol, vec![1, 0]); // x1=true, x2=false
371
372        // Select vertex 1 (literal x2)
373        let is_sol = vec![0, 1];
374        let sat_sol = reduction.extract_solution(&is_sol);
375        assert_eq!(sat_sol, vec![0, 1]); // x1=false, x2=true
376    }
377
378    #[test]
379    fn test_extract_solution_with_negation() {
380        // (NOT x1) - selecting NOT x1 means x1 should be false
381        let sat = Satisfiability::<i32>::new(1, vec![CNFClause::new(vec![-1])]);
382        let reduction = ReduceTo::<IndependentSet<i32>>::reduce_to(&sat);
383
384        let is_sol = vec![1];
385        let sat_sol = reduction.extract_solution(&is_sol);
386        assert_eq!(sat_sol, vec![0]); // x1=false (so NOT x1 is true)
387    }
388
389    #[test]
390    fn test_clique_edges_in_clause() {
391        // A clause with 3 literals should form a clique (3 edges)
392        let sat = Satisfiability::<i32>::new(3, vec![CNFClause::new(vec![1, 2, 3])]);
393        let reduction = ReduceTo::<IndependentSet<i32>>::reduce_to(&sat);
394        let is_problem = reduction.target_problem();
395
396        // 3 vertices, 3 edges (complete graph K3)
397        assert_eq!(is_problem.num_vertices(), 3);
398        assert_eq!(is_problem.num_edges(), 3);
399    }
400
401    #[test]
402    fn test_complement_edges_across_clauses() {
403        // (x1) AND (NOT x1) AND (x2) - three clauses
404        // Vertices: 0 (x1), 1 (NOT x1), 2 (x2)
405        // Edges: (0,1) for complement x1 and NOT x1
406        let sat = Satisfiability::<i32>::new(
407            2,
408            vec![
409                CNFClause::new(vec![1]),
410                CNFClause::new(vec![-1]),
411                CNFClause::new(vec![2]),
412            ],
413        );
414        let reduction = ReduceTo::<IndependentSet<i32>>::reduce_to(&sat);
415        let is_problem = reduction.target_problem();
416
417        assert_eq!(is_problem.num_vertices(), 3);
418        assert_eq!(is_problem.num_edges(), 1); // Only the complement edge
419    }
420
421    #[test]
422    fn test_source_and_target_size() {
423        let sat = Satisfiability::<i32>::new(
424            3,
425            vec![CNFClause::new(vec![1, 2]), CNFClause::new(vec![-1, 3])],
426        );
427        let reduction = ReduceTo::<IndependentSet<i32>>::reduce_to(&sat);
428
429        let source_size = reduction.source_size();
430        let target_size = reduction.target_size();
431
432        assert_eq!(source_size.get("num_vars"), Some(3));
433        assert_eq!(source_size.get("num_clauses"), Some(2));
434        assert_eq!(target_size.get("num_vertices"), Some(4)); // 2 + 2 literals
435    }
436
437    #[test]
438    fn test_empty_sat() {
439        // Empty SAT (trivially satisfiable)
440        let sat = Satisfiability::<i32>::new(0, vec![]);
441        let reduction = ReduceTo::<IndependentSet<i32>>::reduce_to(&sat);
442        let is_problem = reduction.target_problem();
443
444        assert_eq!(is_problem.num_vertices(), 0);
445        assert_eq!(is_problem.num_edges(), 0);
446        assert_eq!(reduction.num_clauses(), 0);
447    }
448
449    #[test]
450    fn test_sat_is_solution_correspondence() {
451        // Comprehensive test: solve both SAT and IS, compare solutions
452        let sat = Satisfiability::<i32>::new(
453            2,
454            vec![CNFClause::new(vec![1, 2]), CNFClause::new(vec![-1, -2])],
455        );
456
457        // Solve SAT directly
458        let sat_solver = BruteForce::new();
459        let direct_sat_solutions = sat_solver.find_best(&sat);
460
461        // Solve via reduction
462        let reduction = ReduceTo::<IndependentSet<i32>>::reduce_to(&sat);
463        let is_problem = reduction.target_problem();
464        let is_solutions = sat_solver.find_best(is_problem);
465
466        // Extract SAT solutions from IS
467        let extracted_sat_solutions: Vec<_> = is_solutions
468            .iter()
469            .map(|s| reduction.extract_solution(s))
470            .collect();
471
472        // All extracted solutions should be valid SAT solutions
473        for sol in &extracted_sat_solutions {
474            let assignment: Vec<bool> = sol.iter().map(|&v| v == 1).collect();
475            assert!(sat.is_satisfying(&assignment));
476        }
477
478        // Direct SAT solutions and extracted solutions should be compatible
479        // (same satisfying assignments, though representation might differ)
480        for sol in &direct_sat_solutions {
481            let assignment: Vec<bool> = sol.iter().map(|&v| v == 1).collect();
482            assert!(sat.is_satisfying(&assignment));
483        }
484    }
485
486    #[test]
487    fn test_literals_accessor() {
488        let sat = Satisfiability::<i32>::new(
489            2,
490            vec![CNFClause::new(vec![1, -2])],
491        );
492        let reduction = ReduceTo::<IndependentSet<i32>>::reduce_to(&sat);
493
494        let literals = reduction.literals();
495        assert_eq!(literals.len(), 2);
496        assert_eq!(literals[0], BoolVar::new(0, false)); // x1
497        assert_eq!(literals[1], BoolVar::new(1, true));  // NOT x2
498    }
499}
500
501// Register reduction with inventory for auto-discovery
502use crate::poly;
503use crate::rules::registry::{ReductionEntry, ReductionOverhead};
504
505inventory::submit! {
506    ReductionEntry {
507        source_name: "Satisfiability",
508        target_name: "IndependentSet",
509        source_graph: "CNF",
510        target_graph: "SimpleGraph",
511        overhead_fn: || ReductionOverhead::new(vec![
512            ("num_vertices", poly!(7 * num_clauses)),
513            ("num_edges", poly!(21 * num_clauses)),
514        ]),
515    }
516}
problemreductions/rules/sat_independentset.rs

problemreductions/rules/
sat_independentset.rs
