problemreductions/rules/
sat_dominatingset.rs

1//! Reduction from Satisfiability (SAT) to DominatingSet.
2//!
3//! The reduction follows this construction:
4//! 1. For each variable x_i, create a "variable gadget" with 3 vertices:
5//!    - Vertex for positive literal x_i
6//!    - Vertex for negative literal NOT x_i
7//!    - A dummy vertex
8//!      These 3 vertices form a complete triangle (clique).
9//! 2. For each clause C_j, create a clause vertex.
10//! 3. Connect each clause vertex to the literal vertices that appear in that clause.
11//!
12//! A dominating set of size = num_variables corresponds to a satisfying assignment:
13//! - Selecting the positive literal vertex means the variable is true
14//! - Selecting the negative literal vertex means the variable is false
15//! - Selecting the dummy vertex means the variable can be either (unused in any clause)
16
17use crate::models::graph::DominatingSet;
18use crate::models::satisfiability::Satisfiability;
19use crate::rules::sat_independentset::BoolVar;
20use crate::rules::traits::{ReduceTo, ReductionResult};
21use crate::traits::Problem;
22use crate::types::ProblemSize;
23use num_traits::{Num, Zero};
24use std::ops::AddAssign;
25
26/// Result of reducing Satisfiability to DominatingSet.
27///
28/// This struct contains:
29/// - The target DominatingSet problem
30/// - The number of literals (variables) in the source SAT problem
31/// - The number of clauses in the source SAT problem
32#[derive(Debug, Clone)]
33pub struct ReductionSATToDS<W> {
34    /// The target DominatingSet problem.
35    target: DominatingSet<W>,
36    /// The number of variables in the source SAT problem.
37    num_literals: usize,
38    /// The number of clauses in the source SAT problem.
39    num_clauses: usize,
40    /// Size of the source problem.
41    source_size: ProblemSize,
42}
43
44impl<W> ReductionResult for ReductionSATToDS<W>
45where
46    W: Clone + Default + PartialOrd + Num + Zero + AddAssign + 'static,
47{
48    type Source = Satisfiability<W>;
49    type Target = DominatingSet<W>;
50
51    fn target_problem(&self) -> &Self::Target {
52        &self.target
53    }
54
55    /// Extract a SAT solution from a DominatingSet solution.
56    ///
57    /// The dominating set solution encodes variable assignments:
58    /// - For each variable x_i (0-indexed), vertices are at positions 3*i, 3*i+1, 3*i+2
59    ///   - 3*i: positive literal x_i (selecting means x_i = true)
60    ///   - 3*i+1: negative literal NOT x_i (selecting means x_i = false)
61    ///   - 3*i+2: dummy vertex (selecting means x_i can be either)
62    ///
63    /// If more than num_literals vertices are selected, the solution is invalid
64    /// and we return a default assignment.
65    fn extract_solution(&self, target_solution: &[usize]) -> Vec<usize> {
66        let selected_count: usize = target_solution.iter().sum();
67
68        // If more vertices selected than variables, not a minimal dominating set
69        // corresponding to a satisfying assignment
70        if selected_count > self.num_literals {
71            // Return default assignment (all false)
72            return vec![0; self.num_literals];
73        }
74
75        let mut assignment = vec![0usize; self.num_literals];
76
77        for (i, &value) in target_solution.iter().enumerate() {
78            if value == 1 {
79                // Only consider variable gadget vertices (first 3*num_literals vertices)
80                if i >= 3 * self.num_literals {
81                    continue; // Skip clause vertices
82                }
83
84                let var_index = i / 3;
85                let vertex_type = i % 3;
86
87                match vertex_type {
88                    0 => {
89                        // Positive literal selected: x_i = true
90                        assignment[var_index] = 1;
91                    }
92                    1 => {
93                        // Negative literal selected: x_i = false
94                        assignment[var_index] = 0;
95                    }
96                    2 => {
97                        // Dummy vertex selected: variable is unconstrained
98                        // Default to false (already 0), but could be anything
99                    }
100                    _ => unreachable!(),
101                }
102            }
103        }
104
105        assignment
106    }
107
108    fn source_size(&self) -> ProblemSize {
109        self.source_size.clone()
110    }
111
112    fn target_size(&self) -> ProblemSize {
113        self.target.problem_size()
114    }
115}
116
117impl<W> ReductionSATToDS<W> {
118    /// Get the number of literals (variables) in the source SAT problem.
119    pub fn num_literals(&self) -> usize {
120        self.num_literals
121    }
122
123    /// Get the number of clauses in the source SAT problem.
124    pub fn num_clauses(&self) -> usize {
125        self.num_clauses
126    }
127}
128
129impl<W> ReduceTo<DominatingSet<W>> for Satisfiability<W>
130where
131    W: Clone + Default + PartialOrd + Num + Zero + AddAssign + From<i32> + 'static,
132{
133    type Result = ReductionSATToDS<W>;
134
135    fn reduce_to(&self) -> Self::Result {
136        let num_variables = self.num_vars();
137        let num_clauses = self.num_clauses();
138
139        // Total vertices: 3 per variable (for variable gadget) + 1 per clause
140        let num_vertices = 3 * num_variables + num_clauses;
141
142        let mut edges: Vec<(usize, usize)> = Vec::new();
143
144        // Step 1: Create variable gadgets
145        // For each variable i (0-indexed), vertices are at positions:
146        //   3*i: positive literal x_i
147        //   3*i+1: negative literal NOT x_i
148        //   3*i+2: dummy vertex
149        // These form a complete triangle (clique of 3)
150        for i in 0..num_variables {
151            let base = 3 * i;
152            // Add all edges of the triangle
153            edges.push((base, base + 1));
154            edges.push((base, base + 2));
155            edges.push((base + 1, base + 2));
156        }
157
158        // Step 2: Connect clause vertices to literal vertices
159        // Clause j gets vertex at position 3*num_variables + j
160        for (j, clause) in self.clauses().iter().enumerate() {
161            let clause_vertex = 3 * num_variables + j;
162
163            for &lit in &clause.literals {
164                let var = BoolVar::from_literal(lit);
165                // var.name is 0-indexed
166                // If positive literal, connect to vertex 3*var.name
167                // If negative literal, connect to vertex 3*var.name + 1
168                let literal_vertex = if var.neg {
169                    3 * var.name + 1
170                } else {
171                    3 * var.name
172                };
173                edges.push((literal_vertex, clause_vertex));
174            }
175        }
176
177        let target = DominatingSet::new(num_vertices, edges);
178
179        ReductionSATToDS {
180            target,
181            num_literals: num_variables,
182            num_clauses,
183            source_size: self.problem_size(),
184        }
185    }
186}
187
188#[cfg(test)]
189mod tests {
190    use super::*;
191    use crate::models::satisfiability::CNFClause;
192    use crate::solvers::{BruteForce, Solver};
193
194    #[test]
195    fn test_simple_sat_to_ds() {
196        // Simple SAT: (x1) - one variable, one clause
197        let sat = Satisfiability::<i32>::new(1, vec![CNFClause::new(vec![1])]);
198        let reduction = ReduceTo::<DominatingSet<i32>>::reduce_to(&sat);
199        let ds_problem = reduction.target_problem();
200
201        // Should have 3 vertices (variable gadget) + 1 clause vertex = 4 vertices
202        assert_eq!(ds_problem.num_vertices(), 4);
203
204        // Edges: 3 for triangle + 1 from positive literal to clause = 4
205        // Triangle edges: (0,1), (0,2), (1,2)
206        // Clause edge: (0, 3) since x1 positive connects to clause vertex
207        assert_eq!(ds_problem.num_edges(), 4);
208    }
209
210    #[test]
211    fn test_two_variable_sat_to_ds() {
212        // SAT: (x1 OR x2)
213        let sat = Satisfiability::<i32>::new(2, vec![CNFClause::new(vec![1, 2])]);
214        let reduction = ReduceTo::<DominatingSet<i32>>::reduce_to(&sat);
215        let ds_problem = reduction.target_problem();
216
217        // 2 variables * 3 = 6 gadget vertices + 1 clause vertex = 7
218        assert_eq!(ds_problem.num_vertices(), 7);
219
220        // Edges:
221        // - 3 edges for first triangle: (0,1), (0,2), (1,2)
222        // - 3 edges for second triangle: (3,4), (3,5), (4,5)
223        // - 2 edges from literals to clause: (0,6), (3,6)
224        assert_eq!(ds_problem.num_edges(), 8);
225    }
226
227    #[test]
228    fn test_satisfiable_formula() {
229        // SAT: (x1 OR x2) AND (NOT x1 OR x2)
230        // Satisfiable with x2 = true
231        let sat = Satisfiability::<i32>::new(
232            2,
233            vec![
234                CNFClause::new(vec![1, 2]),  // x1 OR x2
235                CNFClause::new(vec![-1, 2]), // NOT x1 OR x2
236            ],
237        );
238        let reduction = ReduceTo::<DominatingSet<i32>>::reduce_to(&sat);
239        let ds_problem = reduction.target_problem();
240
241        // Solve the dominating set problem
242        let solver = BruteForce::new();
243        let solutions = solver.find_best(ds_problem);
244
245        // Minimum dominating set should be of size 2 (one per variable)
246        let min_size = solutions[0].iter().sum::<usize>();
247        assert_eq!(min_size, 2, "Minimum dominating set should have 2 vertices");
248
249        // Extract and verify at least one solution satisfies SAT
250        let mut found_satisfying = false;
251        for sol in &solutions {
252            let sat_sol = reduction.extract_solution(sol);
253            let assignment: Vec<bool> = sat_sol.iter().map(|&v| v == 1).collect();
254            if sat.is_satisfying(&assignment) {
255                found_satisfying = true;
256                break;
257            }
258        }
259        assert!(found_satisfying, "Should find a satisfying assignment");
260    }
261
262    #[test]
263    fn test_unsatisfiable_formula() {
264        // SAT: (x1) AND (NOT x1) - unsatisfiable
265        let sat = Satisfiability::<i32>::new(
266            1,
267            vec![CNFClause::new(vec![1]), CNFClause::new(vec![-1])],
268        );
269        let reduction = ReduceTo::<DominatingSet<i32>>::reduce_to(&sat);
270        let ds_problem = reduction.target_problem();
271
272        // Vertices: 3 (gadget) + 2 (clauses) = 5
273        assert_eq!(ds_problem.num_vertices(), 5);
274
275        let solver = BruteForce::new();
276        let solutions = solver.find_best(ds_problem);
277
278        // For unsatisfiable formula, the minimum dominating set will need
279        // more than num_variables vertices OR won't produce a valid assignment
280        // Actually, in this case we can still dominate with just selecting
281        // one literal vertex (it dominates its gadget AND one clause),
282        // but then the other clause isn't dominated.
283        // So we need at least 2 vertices: one for each clause's requirement.
284
285        // The key insight is that both clauses share the same variable gadget
286        // but require opposite literals. To dominate both clause vertices,
287        // we need to select BOTH literal vertices (0 and 1) or the dummy +
288        // something else.
289
290        // Verify no extracted solution satisfies the formula
291        for sol in &solutions {
292            let sat_sol = reduction.extract_solution(sol);
293            let assignment: Vec<bool> = sat_sol.iter().map(|&v| v == 1).collect();
294            // This unsatisfiable formula should not have a satisfying assignment
295            assert!(
296                !sat.is_satisfying(&assignment),
297                "Unsatisfiable formula should not be satisfied"
298            );
299        }
300    }
301
302    #[test]
303    fn test_three_sat_example() {
304        // 3-SAT: (x1 OR x2 OR x3) AND (NOT x1 OR NOT x2 OR x3) AND (x1 OR NOT x2 OR NOT x3)
305        let sat = Satisfiability::<i32>::new(
306            3,
307            vec![
308                CNFClause::new(vec![1, 2, 3]),    // x1 OR x2 OR x3
309                CNFClause::new(vec![-1, -2, 3]),  // NOT x1 OR NOT x2 OR x3
310                CNFClause::new(vec![1, -2, -3]),  // x1 OR NOT x2 OR NOT x3
311            ],
312        );
313
314        let reduction = ReduceTo::<DominatingSet<i32>>::reduce_to(&sat);
315        let ds_problem = reduction.target_problem();
316
317        // 3 variables * 3 = 9 gadget vertices + 3 clauses = 12
318        assert_eq!(ds_problem.num_vertices(), 12);
319
320        let solver = BruteForce::new();
321        let solutions = solver.find_best(ds_problem);
322
323        // Minimum should be 3 (one per variable)
324        let min_size = solutions[0].iter().sum::<usize>();
325        assert_eq!(min_size, 3, "Minimum dominating set should have 3 vertices");
326
327        // Verify extracted solutions
328        let mut found_satisfying = false;
329        for sol in &solutions {
330            let sat_sol = reduction.extract_solution(sol);
331            let assignment: Vec<bool> = sat_sol.iter().map(|&v| v == 1).collect();
332            if sat.is_satisfying(&assignment) {
333                found_satisfying = true;
334                break;
335            }
336        }
337        assert!(found_satisfying, "Should find a satisfying assignment for 3-SAT");
338    }
339
340    #[test]
341    fn test_extract_solution_positive_literal() {
342        // (x1) - select positive literal
343        let sat = Satisfiability::<i32>::new(1, vec![CNFClause::new(vec![1])]);
344        let reduction = ReduceTo::<DominatingSet<i32>>::reduce_to(&sat);
345
346        // Solution: select vertex 0 (positive literal x1)
347        // This dominates vertices 1, 2 (gadget) and vertex 3 (clause)
348        let ds_sol = vec![1, 0, 0, 0];
349        let sat_sol = reduction.extract_solution(&ds_sol);
350        assert_eq!(sat_sol, vec![1]); // x1 = true
351    }
352
353    #[test]
354    fn test_extract_solution_negative_literal() {
355        // (NOT x1) - select negative literal
356        let sat = Satisfiability::<i32>::new(1, vec![CNFClause::new(vec![-1])]);
357        let reduction = ReduceTo::<DominatingSet<i32>>::reduce_to(&sat);
358
359        // Solution: select vertex 1 (negative literal NOT x1)
360        // This dominates vertices 0, 2 (gadget) and vertex 3 (clause)
361        let ds_sol = vec![0, 1, 0, 0];
362        let sat_sol = reduction.extract_solution(&ds_sol);
363        assert_eq!(sat_sol, vec![0]); // x1 = false
364    }
365
366    #[test]
367    fn test_extract_solution_dummy() {
368        // (x1 OR x2) where only x1 matters
369        let sat = Satisfiability::<i32>::new(2, vec![CNFClause::new(vec![1])]);
370        let reduction = ReduceTo::<DominatingSet<i32>>::reduce_to(&sat);
371
372        // Select: vertex 0 (x1 positive) and vertex 5 (x2 dummy)
373        // Vertex 0 dominates: itself, 1, 2, and clause 6
374        // Vertex 5 dominates: 3, 4, and itself
375        let ds_sol = vec![1, 0, 0, 0, 0, 1, 0];
376        let sat_sol = reduction.extract_solution(&ds_sol);
377        assert_eq!(sat_sol, vec![1, 0]); // x1 = true, x2 = false (from dummy)
378    }
379
380    #[test]
381    fn test_source_and_target_size() {
382        let sat = Satisfiability::<i32>::new(
383            3,
384            vec![CNFClause::new(vec![1, 2]), CNFClause::new(vec![-1, 3])],
385        );
386        let reduction = ReduceTo::<DominatingSet<i32>>::reduce_to(&sat);
387
388        let source_size = reduction.source_size();
389        let target_size = reduction.target_size();
390
391        assert_eq!(source_size.get("num_vars"), Some(3));
392        assert_eq!(source_size.get("num_clauses"), Some(2));
393        // 3 vars * 3 = 9 gadget vertices + 2 clause vertices = 11
394        assert_eq!(target_size.get("num_vertices"), Some(11));
395    }
396
397    #[test]
398    fn test_empty_sat() {
399        // Empty SAT (trivially satisfiable)
400        let sat = Satisfiability::<i32>::new(0, vec![]);
401        let reduction = ReduceTo::<DominatingSet<i32>>::reduce_to(&sat);
402        let ds_problem = reduction.target_problem();
403
404        assert_eq!(ds_problem.num_vertices(), 0);
405        assert_eq!(ds_problem.num_edges(), 0);
406        assert_eq!(reduction.num_clauses(), 0);
407        assert_eq!(reduction.num_literals(), 0);
408    }
409
410    #[test]
411    fn test_multiple_literals_same_variable() {
412        // Clause with repeated variable: (x1 OR NOT x1) - tautology
413        let sat = Satisfiability::<i32>::new(1, vec![CNFClause::new(vec![1, -1])]);
414        let reduction = ReduceTo::<DominatingSet<i32>>::reduce_to(&sat);
415        let ds_problem = reduction.target_problem();
416
417        // 3 gadget vertices + 1 clause vertex = 4
418        assert_eq!(ds_problem.num_vertices(), 4);
419
420        // Edges:
421        // - 3 for triangle
422        // - 2 from literals to clause (both positive and negative literals connect)
423        assert_eq!(ds_problem.num_edges(), 5);
424    }
425
426    #[test]
427    fn test_sat_ds_solution_correspondence() {
428        // Comprehensive test: verify that solutions extracted from DS satisfy SAT
429        let sat = Satisfiability::<i32>::new(
430            2,
431            vec![CNFClause::new(vec![1, 2]), CNFClause::new(vec![-1, -2])],
432        );
433
434        // Solve SAT directly
435        let sat_solver = BruteForce::new();
436        let direct_sat_solutions = sat_solver.find_best(&sat);
437
438        // Solve via reduction
439        let reduction = ReduceTo::<DominatingSet<i32>>::reduce_to(&sat);
440        let ds_problem = reduction.target_problem();
441        let ds_solutions = sat_solver.find_best(ds_problem);
442
443        // Direct SAT solutions should all be valid
444        for sol in &direct_sat_solutions {
445            let assignment: Vec<bool> = sol.iter().map(|&v| v == 1).collect();
446            assert!(sat.is_satisfying(&assignment));
447        }
448
449        // DS solutions with minimum size should correspond to valid SAT solutions
450        let min_size = ds_solutions[0].iter().sum::<usize>();
451        if min_size == 2 {
452            // Only if min dominating set = num_vars
453            let mut found_satisfying = false;
454            for sol in &ds_solutions {
455                if sol.iter().sum::<usize>() == 2 {
456                    let sat_sol = reduction.extract_solution(sol);
457                    let assignment: Vec<bool> = sat_sol.iter().map(|&v| v == 1).collect();
458                    if sat.is_satisfying(&assignment) {
459                        found_satisfying = true;
460                        break;
461                    }
462                }
463            }
464            assert!(found_satisfying, "At least one DS solution should give a SAT solution");
465        }
466    }
467
468    #[test]
469    fn test_accessors() {
470        let sat = Satisfiability::<i32>::new(
471            2,
472            vec![CNFClause::new(vec![1, -2])],
473        );
474        let reduction = ReduceTo::<DominatingSet<i32>>::reduce_to(&sat);
475
476        assert_eq!(reduction.num_literals(), 2);
477        assert_eq!(reduction.num_clauses(), 1);
478    }
479
480    #[test]
481    fn test_extract_solution_too_many_selected() {
482        // Test that extract_solution handles invalid (non-minimal) dominating sets
483        let sat = Satisfiability::<i32>::new(1, vec![CNFClause::new(vec![1])]);
484        let reduction = ReduceTo::<DominatingSet<i32>>::reduce_to(&sat);
485
486        // Select all 4 vertices (more than num_literals=1)
487        let ds_sol = vec![1, 1, 1, 1];
488        let sat_sol = reduction.extract_solution(&ds_sol);
489        // Should return default (all false)
490        assert_eq!(sat_sol, vec![0]);
491    }
492
493    #[test]
494    fn test_negated_variable_connection() {
495        // (NOT x1 OR NOT x2) - both negated
496        let sat = Satisfiability::<i32>::new(2, vec![CNFClause::new(vec![-1, -2])]);
497        let reduction = ReduceTo::<DominatingSet<i32>>::reduce_to(&sat);
498        let ds_problem = reduction.target_problem();
499
500        // 2 * 3 = 6 gadget vertices + 1 clause = 7
501        assert_eq!(ds_problem.num_vertices(), 7);
502
503        // Edges:
504        // - 3 for first triangle: (0,1), (0,2), (1,2)
505        // - 3 for second triangle: (3,4), (3,5), (4,5)
506        // - 2 from negated literals to clause: (1,6), (4,6)
507        assert_eq!(ds_problem.num_edges(), 8);
508    }
509}
510
511// Register reduction with inventory for auto-discovery
512use crate::poly;
513use crate::rules::registry::{ReductionEntry, ReductionOverhead};
514
515inventory::submit! {
516    ReductionEntry {
517        source_name: "Satisfiability",
518        target_name: "DominatingSet",
519        source_graph: "CNF",
520        target_graph: "SimpleGraph",
521        overhead_fn: || ReductionOverhead::new(vec![
522            ("num_vertices", poly!(num_vars)),
523            ("num_edges", poly!(num_clauses)),
524        ]),
525    }
526}
problemreductions/rules/sat_dominatingset.rs

problemreductions/rules/
sat_dominatingset.rs
