problemreductions/rules/
sat_coloring.rs

1//! Reduction from Satisfiability (SAT) to 3-Coloring.
2//!
3//! The reduction works as follows:
4//! 1. Create 3 special vertices: TRUE, FALSE, AUX (connected as a triangle)
5//! 2. For each variable x, create vertices for x and NOT_x:
6//!    - Connect x to AUX, NOT_x to AUX (they can't be auxiliary color)
7//!    - Connect x to NOT_x (they must have different colors)
8//! 3. For each clause, build an OR-gadget that forces output to be TRUE color
9//!    - The OR-gadget is built recursively for multi-literal clauses
10
11use crate::models::graph::Coloring;
12use crate::models::satisfiability::Satisfiability;
13use crate::rules::sat_independentset::BoolVar;
14use crate::rules::traits::{ReduceTo, ReductionResult};
15use crate::traits::Problem;
16use crate::types::ProblemSize;
17use num_traits::{Num, Zero};
18use std::collections::HashMap;
19use std::marker::PhantomData;
20use std::ops::AddAssign;
21
22/// Helper struct for constructing the graph for the SAT to 3-Coloring reduction.
23struct SATColoringConstructor {
24    /// The edges of the graph being constructed.
25    edges: Vec<(usize, usize)>,
26    /// Current number of vertices.
27    num_vertices: usize,
28    /// Mapping from positive variable index (0-indexed) to vertex index.
29    pos_vertices: Vec<usize>,
30    /// Mapping from negative variable index (0-indexed) to vertex index.
31    neg_vertices: Vec<usize>,
32    /// Mapping from BoolVar to vertex index.
33    vmap: HashMap<(usize, bool), usize>,
34}
35
36impl SATColoringConstructor {
37    /// Create a new SATColoringConstructor for `num_vars` variables.
38    ///
39    /// Initial graph structure:
40    /// - Vertices 0, 1, 2: TRUE, FALSE, AUX (forming a triangle)
41    /// - For each variable i (0-indexed):
42    ///   - Vertex 3 + i: positive literal (x_i)
43    ///   - Vertex 3 + num_vars + i: negative literal (NOT x_i)
44    fn new(num_vars: usize) -> Self {
45        let num_vertices = 2 * num_vars + 3;
46        let mut edges = Vec::new();
47
48        // Create triangle: TRUE(0), FALSE(1), AUX(2)
49        edges.push((0, 1));
50        edges.push((0, 2));
51        edges.push((1, 2));
52
53        // Create variable vertices and edges
54        let mut pos_vertices = Vec::with_capacity(num_vars);
55        let mut neg_vertices = Vec::with_capacity(num_vars);
56        let mut vmap = HashMap::new();
57
58        for i in 0..num_vars {
59            let pos_v = 3 + i;
60            let neg_v = 3 + num_vars + i;
61            pos_vertices.push(pos_v);
62            neg_vertices.push(neg_v);
63
64            // Connect to AUX (they can't be auxiliary color)
65            edges.push((pos_v, 2));
66            edges.push((neg_v, 2));
67
68            // Connect pos and neg of the same variable (they must have different colors)
69            edges.push((pos_v, neg_v));
70
71            // Build vmap
72            vmap.insert((i, false), pos_v); // positive literal
73            vmap.insert((i, true), neg_v); // negative literal
74        }
75
76        Self {
77            edges,
78            num_vertices,
79            pos_vertices,
80            neg_vertices,
81            vmap,
82        }
83    }
84
85    /// Get the TRUE vertex index.
86    fn true_vertex(&self) -> usize {
87        0
88    }
89
90    /// Get the FALSE vertex index.
91    fn false_vertex(&self) -> usize {
92        1
93    }
94
95    /// Get the AUX (ancilla) vertex index.
96    fn aux_vertex(&self) -> usize {
97        2
98    }
99
100    /// Add edge to connect vertex to AUX.
101    fn attach_to_aux(&mut self, idx: usize) {
102        self.add_edge(idx, self.aux_vertex());
103    }
104
105    /// Add edge to connect vertex to FALSE.
106    fn attach_to_false(&mut self, idx: usize) {
107        self.add_edge(idx, self.false_vertex());
108    }
109
110    /// Add edge to connect vertex to TRUE.
111    fn attach_to_true(&mut self, idx: usize) {
112        self.add_edge(idx, self.true_vertex());
113    }
114
115    /// Add an edge between two vertices.
116    fn add_edge(&mut self, u: usize, v: usize) {
117        self.edges.push((u, v));
118    }
119
120    /// Add vertices to the graph.
121    fn add_vertices(&mut self, n: usize) -> Vec<usize> {
122        let start = self.num_vertices;
123        self.num_vertices += n;
124        (start..self.num_vertices).collect()
125    }
126
127    /// Force a vertex to have the TRUE color.
128    /// This is done by connecting it to both AUX and FALSE.
129    fn set_true(&mut self, idx: usize) {
130        self.attach_to_aux(idx);
131        self.attach_to_false(idx);
132    }
133
134    /// Get the vertex index for a literal.
135    fn get_vertex(&self, var: &BoolVar) -> usize {
136        self.vmap[&(var.name, var.neg)]
137    }
138
139    /// Add a clause to the graph.
140    /// For a single-literal clause, just set the literal to TRUE.
141    /// For multi-literal clauses, build OR-gadgets recursively.
142    fn add_clause(&mut self, literals: &[i32]) {
143        assert!(!literals.is_empty(), "Clause must have at least one literal");
144
145        let first_var = BoolVar::from_literal(literals[0]);
146        let mut output_node = self.get_vertex(&first_var);
147
148        // Build OR-gadget chain for remaining literals
149        for &lit in &literals[1..] {
150            let var = BoolVar::from_literal(lit);
151            let input2 = self.get_vertex(&var);
152            output_node = self.add_or_gadget(output_node, input2);
153        }
154
155        // Force the output to be TRUE
156        self.set_true(output_node);
157    }
158
159    /// Add an OR-gadget that computes OR of two inputs.
160    ///
161    /// The OR-gadget ensures that if any input has TRUE color, the output can have TRUE color.
162    /// If both inputs have FALSE color, the output must have FALSE color.
163    ///
164    /// The gadget adds 5 vertices: ancilla1, ancilla2, entrance1, entrance2, output
165    ///
166    /// Returns the output vertex index.
167    fn add_or_gadget(&mut self, input1: usize, input2: usize) -> usize {
168        // Add 5 new vertices
169        let new_vertices = self.add_vertices(5);
170        let ancilla1 = new_vertices[0];
171        let ancilla2 = new_vertices[1];
172        let entrance1 = new_vertices[2];
173        let entrance2 = new_vertices[3];
174        let output = new_vertices[4];
175
176        // Connect output to AUX
177        self.attach_to_aux(output);
178
179        // Connect ancilla1 to TRUE
180        self.attach_to_true(ancilla1);
181
182        // Build the gadget structure (based on Julia implementation)
183        // (ancilla1, ancilla2), (ancilla2, input1), (ancilla2, input2),
184        // (entrance1, entrance2), (output, ancilla1), (input1, entrance2),
185        // (input2, entrance1), (entrance1, output), (entrance2, output)
186        self.add_edge(ancilla1, ancilla2);
187        self.add_edge(ancilla2, input1);
188        self.add_edge(ancilla2, input2);
189        self.add_edge(entrance1, entrance2);
190        self.add_edge(output, ancilla1);
191        self.add_edge(input1, entrance2);
192        self.add_edge(input2, entrance1);
193        self.add_edge(entrance1, output);
194        self.add_edge(entrance2, output);
195
196        output
197    }
198
199    /// Build the final Coloring problem.
200    fn build_coloring(&self) -> Coloring {
201        Coloring::new(self.num_vertices, 3, self.edges.clone())
202    }
203}
204
205/// Result of reducing Satisfiability to Coloring.
206///
207/// This struct contains:
208/// - The target Coloring problem (3-coloring)
209/// - Mappings from variable indices to vertex indices
210/// - Information about the source problem
211#[derive(Debug, Clone)]
212pub struct ReductionSATToColoring<W> {
213    /// The target Coloring problem.
214    target: Coloring,
215    /// Mapping from variable index (0-indexed) to positive literal vertex index.
216    pos_vertices: Vec<usize>,
217    /// Mapping from variable index (0-indexed) to negative literal vertex index.
218    neg_vertices: Vec<usize>,
219    /// Number of variables in the source SAT problem.
220    num_source_variables: usize,
221    /// Number of clauses in the source SAT problem.
222    num_clauses: usize,
223    /// Size of the source problem.
224    source_size: ProblemSize,
225    /// Phantom data to tie this reduction to the source type's weight parameter.
226    _phantom: PhantomData<W>,
227}
228
229impl<W> ReductionResult for ReductionSATToColoring<W>
230where
231    W: Clone + Default + PartialOrd + Num + Zero + AddAssign + 'static,
232{
233    type Source = Satisfiability<W>;
234    type Target = Coloring;
235
236    fn target_problem(&self) -> &Self::Target {
237        &self.target
238    }
239
240    /// Extract a SAT solution from a Coloring solution.
241    ///
242    /// The coloring solution maps each vertex to a color (0, 1, or 2).
243    /// - Color 0: TRUE
244    /// - Color 1: FALSE
245    /// - Color 2: AUX
246    ///
247    /// For each variable, we check if its positive literal vertex has TRUE color (0).
248    /// If so, the variable is assigned true (1); otherwise false (0).
249    fn extract_solution(&self, target_solution: &[usize]) -> Vec<usize> {
250        // First determine which color is TRUE, FALSE, and AUX
251        // Vertices 0, 1, 2 are TRUE, FALSE, AUX respectively
252        assert!(
253            target_solution.len() >= 3,
254            "Invalid solution: coloring must have at least 3 vertices"
255        );
256        let true_color = target_solution[0];
257        let false_color = target_solution[1];
258        let aux_color = target_solution[2];
259
260        // Sanity checks
261        assert!(
262            true_color != false_color && true_color != aux_color,
263            "Invalid coloring solution: special vertices must have distinct colors"
264        );
265
266        let mut assignment = vec![0usize; self.num_source_variables];
267
268        for (i, &pos_vertex) in self.pos_vertices.iter().enumerate() {
269            let vertex_color = target_solution[pos_vertex];
270
271            // Sanity check: variable vertices should not have AUX color
272            assert!(
273                vertex_color != aux_color,
274                "Invalid coloring solution: variable vertex has auxiliary color"
275            );
276
277            // If positive literal has TRUE color, variable is true (1)
278            // Otherwise, variable is false (0)
279            assignment[i] = if vertex_color == true_color { 1 } else { 0 };
280        }
281
282        assignment
283    }
284
285    fn source_size(&self) -> ProblemSize {
286        self.source_size.clone()
287    }
288
289    fn target_size(&self) -> ProblemSize {
290        self.target.problem_size()
291    }
292}
293
294impl<W> ReductionSATToColoring<W> {
295    /// Get the number of clauses in the source SAT problem.
296    pub fn num_clauses(&self) -> usize {
297        self.num_clauses
298    }
299
300    /// Get the positive vertices mapping.
301    pub fn pos_vertices(&self) -> &[usize] {
302        &self.pos_vertices
303    }
304
305    /// Get the negative vertices mapping.
306    pub fn neg_vertices(&self) -> &[usize] {
307        &self.neg_vertices
308    }
309}
310
311impl<W> ReduceTo<Coloring> for Satisfiability<W>
312where
313    W: Clone + Default + PartialOrd + Num + Zero + AddAssign + From<i32> + 'static,
314{
315    type Result = ReductionSATToColoring<W>;
316
317    fn reduce_to(&self) -> Self::Result {
318        let mut constructor = SATColoringConstructor::new(self.num_vars());
319
320        // Add each clause to the graph
321        for clause in self.clauses() {
322            constructor.add_clause(&clause.literals);
323        }
324
325        let target = constructor.build_coloring();
326
327        ReductionSATToColoring {
328            target,
329            pos_vertices: constructor.pos_vertices,
330            neg_vertices: constructor.neg_vertices,
331            num_source_variables: self.num_vars(),
332            num_clauses: self.num_clauses(),
333            source_size: self.problem_size(),
334            _phantom: PhantomData,
335        }
336    }
337}
338
339#[cfg(test)]
340mod tests {
341    use super::*;
342    use crate::models::satisfiability::CNFClause;
343    use crate::solvers::{BruteForce, Solver};
344
345    #[test]
346    fn test_constructor_basic_structure() {
347        let constructor = SATColoringConstructor::new(2);
348
349        // Should have 2*2 + 3 = 7 vertices
350        assert_eq!(constructor.num_vertices, 7);
351
352        // Check pos_vertices and neg_vertices
353        assert_eq!(constructor.pos_vertices, vec![3, 4]);
354        assert_eq!(constructor.neg_vertices, vec![5, 6]);
355
356        // Check vmap
357        assert_eq!(constructor.vmap[&(0, false)], 3);
358        assert_eq!(constructor.vmap[&(0, true)], 5);
359        assert_eq!(constructor.vmap[&(1, false)], 4);
360        assert_eq!(constructor.vmap[&(1, true)], 6);
361    }
362
363    #[test]
364    fn test_special_vertex_accessors() {
365        let constructor = SATColoringConstructor::new(1);
366        assert_eq!(constructor.true_vertex(), 0);
367        assert_eq!(constructor.false_vertex(), 1);
368        assert_eq!(constructor.aux_vertex(), 2);
369    }
370
371    #[test]
372    fn test_simple_sat_to_coloring() {
373        // Simple SAT: (x1) - one clause with one literal
374        let sat = Satisfiability::<i32>::new(1, vec![CNFClause::new(vec![1])]);
375        let reduction = ReduceTo::<Coloring>::reduce_to(&sat);
376        let coloring = reduction.target_problem();
377
378        // Should have 2*1 + 3 = 5 base vertices
379        // Plus edges to set x1 to TRUE (attached to AUX and FALSE)
380        assert!(coloring.num_vertices() >= 5);
381    }
382
383    #[test]
384    fn test_reduction_structure() {
385        // Satisfiable formula: (x1 OR x2) AND (NOT x1 OR x2)
386        // Just verify the reduction builds the correct structure
387        let sat = Satisfiability::<i32>::new(
388            2,
389            vec![CNFClause::new(vec![1, 2]), CNFClause::new(vec![-1, 2])],
390        );
391
392        let reduction = ReduceTo::<Coloring>::reduce_to(&sat);
393        let coloring = reduction.target_problem();
394
395        // Base vertices: 3 (TRUE, FALSE, AUX) + 2*2 (pos and neg for each var) = 7
396        // Each 2-literal clause adds 5 vertices for OR gadget = 2 * 5 = 10
397        // Total: 7 + 10 = 17 vertices
398        assert_eq!(coloring.num_vertices(), 17);
399        assert_eq!(coloring.num_colors(), 3);
400        assert_eq!(reduction.pos_vertices().len(), 2);
401        assert_eq!(reduction.neg_vertices().len(), 2);
402    }
403
404    #[test]
405    fn test_unsatisfiable_formula() {
406        // Unsatisfiable: (x1) AND (NOT x1)
407        let sat = Satisfiability::<i32>::new(
408            1,
409            vec![CNFClause::new(vec![1]), CNFClause::new(vec![-1])],
410        );
411
412        let reduction = ReduceTo::<Coloring>::reduce_to(&sat);
413        let coloring = reduction.target_problem();
414
415        // Solve the coloring problem
416        let solver = BruteForce::new();
417        let solutions = solver.find_best(coloring);
418
419        // For an unsatisfiable formula, the coloring should have no valid solutions
420        // OR no valid coloring exists that extracts to a satisfying SAT assignment
421        let mut found_satisfying = false;
422        for sol in &solutions {
423            if coloring.solution_size(sol).is_valid {
424                let sat_sol = reduction.extract_solution(sol);
425                let assignment: Vec<bool> = sat_sol.iter().map(|&v| v == 1).collect();
426                if sat.is_satisfying(&assignment) {
427                    found_satisfying = true;
428                    break;
429                }
430            }
431        }
432
433        // The coloring should not yield a satisfying SAT assignment
434        // because the formula is unsatisfiable
435        // Note: The coloring graph itself may still be colorable,
436        // but the constraints should make it impossible for both
437        // x1 and NOT x1 to be TRUE color simultaneously
438        // Actually, let's check if ANY coloring solution produces a valid SAT solution
439        // If the formula is unsat, no valid coloring should extract to a satisfying assignment
440        assert!(
441            !found_satisfying,
442            "Unsatisfiable formula should not produce satisfying assignment"
443        );
444    }
445
446    #[test]
447    fn test_three_literal_clause_structure() {
448        // (x1 OR x2 OR x3)
449        let sat = Satisfiability::<i32>::new(3, vec![CNFClause::new(vec![1, 2, 3])]);
450
451        let reduction = ReduceTo::<Coloring>::reduce_to(&sat);
452        let coloring = reduction.target_problem();
453
454        // Base vertices: 3 + 2*3 = 9
455        // 3-literal clause needs 2 OR gadgets (x1 OR x2, then result OR x3)
456        // Each OR gadget adds 5 vertices, so 2*5 = 10
457        // Total: 9 + 10 = 19 vertices
458        assert_eq!(coloring.num_vertices(), 19);
459        assert_eq!(coloring.num_colors(), 3);
460        assert_eq!(reduction.pos_vertices().len(), 3);
461        assert_eq!(reduction.neg_vertices().len(), 3);
462    }
463
464    #[test]
465    fn test_source_and_target_size() {
466        let sat = Satisfiability::<i32>::new(
467            3,
468            vec![CNFClause::new(vec![1, 2]), CNFClause::new(vec![-1, 3])],
469        );
470        let reduction = ReduceTo::<Coloring>::reduce_to(&sat);
471
472        let source_size = reduction.source_size();
473        let target_size = reduction.target_size();
474
475        assert_eq!(source_size.get("num_vars"), Some(3));
476        assert_eq!(source_size.get("num_clauses"), Some(2));
477        assert!(target_size.get("num_vertices").is_some());
478        assert!(target_size.get("num_colors").unwrap() == 3);
479    }
480
481    #[test]
482    fn test_extract_solution_basic() {
483        // Simple case: one variable, one clause (x1)
484        let sat = Satisfiability::<i32>::new(1, vec![CNFClause::new(vec![1])]);
485        let reduction = ReduceTo::<Coloring>::reduce_to(&sat);
486
487        // Manually construct a valid coloring where x1 has TRUE color
488        // Vertices: 0=TRUE, 1=FALSE, 2=AUX, 3=x1, 4=NOT_x1
489        // Colors: TRUE=0, FALSE=1, AUX=2
490        // For x1 to be true, pos_vertex[0]=3 should have color 0 (TRUE)
491
492        // A valid coloring that satisfies x1=TRUE:
493        // - Vertex 0 (TRUE): color 0
494        // - Vertex 1 (FALSE): color 1
495        // - Vertex 2 (AUX): color 2
496        // - Vertex 3 (x1): color 0 (TRUE) - connected to AUX(2), NOT_x1(4)
497        // - Vertex 4 (NOT_x1): color 1 (FALSE) - connected to AUX(2), x1(3)
498
499        // However, the actual coloring depends on the full graph structure
500        // Let's just verify the extraction logic works by checking type signatures
501        assert_eq!(reduction.pos_vertices().len(), 1);
502        assert_eq!(reduction.neg_vertices().len(), 1);
503    }
504
505    #[test]
506    fn test_complex_formula_structure() {
507        // (x1 OR x2) AND (NOT x1 OR x3) AND (NOT x2 OR NOT x3)
508        let sat = Satisfiability::<i32>::new(
509            3,
510            vec![
511                CNFClause::new(vec![1, 2]),     // x1 OR x2
512                CNFClause::new(vec![-1, 3]),    // NOT x1 OR x3
513                CNFClause::new(vec![-2, -3]),   // NOT x2 OR NOT x3
514            ],
515        );
516
517        let reduction = ReduceTo::<Coloring>::reduce_to(&sat);
518        let coloring = reduction.target_problem();
519
520        // Base vertices: 3 + 2*3 = 9
521        // 3 clauses each with 2 literals, each needs 1 OR gadget = 3*5 = 15
522        // Total: 9 + 15 = 24 vertices
523        assert_eq!(coloring.num_vertices(), 24);
524        assert_eq!(coloring.num_colors(), 3);
525        assert_eq!(reduction.num_clauses(), 3);
526    }
527
528    #[test]
529    fn test_single_literal_clauses() {
530        // (x1) AND (x2) - both must be true
531        let sat = Satisfiability::<i32>::new(
532            2,
533            vec![CNFClause::new(vec![1]), CNFClause::new(vec![2])],
534        );
535
536        let reduction = ReduceTo::<Coloring>::reduce_to(&sat);
537        let coloring = reduction.target_problem();
538
539        let solver = BruteForce::new();
540        let solutions = solver.find_best(coloring);
541
542        let mut found_correct = false;
543        for sol in &solutions {
544            if coloring.solution_size(sol).is_valid {
545                let sat_sol = reduction.extract_solution(sol);
546                if sat_sol == vec![1, 1] {
547                    found_correct = true;
548                    break;
549                }
550            }
551        }
552
553        assert!(
554            found_correct,
555            "Should find solution where both x1 and x2 are true"
556        );
557    }
558
559    #[test]
560    fn test_empty_sat() {
561        // Empty SAT (trivially satisfiable)
562        let sat = Satisfiability::<i32>::new(0, vec![]);
563        let reduction = ReduceTo::<Coloring>::reduce_to(&sat);
564
565        assert_eq!(reduction.num_clauses(), 0);
566        assert!(reduction.pos_vertices().is_empty());
567        assert!(reduction.neg_vertices().is_empty());
568
569        let coloring = reduction.target_problem();
570        // Just the 3 special vertices
571        assert_eq!(coloring.num_vertices(), 3);
572    }
573
574    #[test]
575    fn test_num_clauses_accessor() {
576        let sat = Satisfiability::<i32>::new(
577            2,
578            vec![CNFClause::new(vec![1, 2]), CNFClause::new(vec![-1])],
579        );
580        let reduction = ReduceTo::<Coloring>::reduce_to(&sat);
581        assert_eq!(reduction.num_clauses(), 2);
582    }
583
584    #[test]
585    fn test_or_gadget_construction() {
586        // Test that OR gadget is correctly added
587        let mut constructor = SATColoringConstructor::new(2);
588        let initial_vertices = constructor.num_vertices;
589
590        // Add an OR gadget
591        let input1 = constructor.pos_vertices[0]; // x1
592        let input2 = constructor.pos_vertices[1]; // x2
593        let output = constructor.add_or_gadget(input1, input2);
594
595        // Should add 5 vertices
596        assert_eq!(constructor.num_vertices, initial_vertices + 5);
597
598        // Output should be the last added vertex
599        assert_eq!(output, constructor.num_vertices - 1);
600    }
601
602    #[test]
603    fn test_manual_coloring_extraction() {
604        // Test solution extraction with a manually constructed coloring solution
605        // for a simple 1-variable SAT problem: (x1)
606        let sat = Satisfiability::<i32>::new(1, vec![CNFClause::new(vec![1])]);
607        let reduction = ReduceTo::<Coloring>::reduce_to(&sat);
608        let coloring = reduction.target_problem();
609
610        // The graph structure for (x1) with set_true:
611        // - Vertices 0, 1, 2: TRUE, FALSE, AUX (triangle)
612        // - Vertex 3: x1 (pos)
613        // - Vertex 4: NOT x1 (neg)
614        // After set_true(3): x1 is connected to AUX and FALSE
615        // So x1 must have TRUE color
616
617        // A valid 3-coloring where x1 has TRUE color:
618        // TRUE=0, FALSE=1, AUX=2
619        // x1 must have color 0 (connected to 1 and 2)
620        // NOT_x1 must have color 1 (connected to 2 and x1=0)
621        let valid_coloring = vec![0, 1, 2, 0, 1];
622
623        assert_eq!(coloring.num_vertices(), 5);
624        let extracted = reduction.extract_solution(&valid_coloring);
625        // x1 should be true (1) because vertex 3 has color 0 which equals TRUE vertex's color
626        assert_eq!(extracted, vec![1]);
627    }
628
629    #[test]
630    fn test_extraction_with_different_color_assignment() {
631        // Test that extraction works with different color assignments
632        // (colors may be permuted but semantics preserved)
633        let sat = Satisfiability::<i32>::new(1, vec![CNFClause::new(vec![1])]);
634        let reduction = ReduceTo::<Coloring>::reduce_to(&sat);
635
636        // Different valid coloring: TRUE=2, FALSE=0, AUX=1
637        // x1 must have color 2 (TRUE), NOT_x1 must have color 0 (FALSE)
638        let coloring_permuted = vec![2, 0, 1, 2, 0];
639        let extracted = reduction.extract_solution(&coloring_permuted);
640        // x1 should still be true because its color equals TRUE vertex's color
641        assert_eq!(extracted, vec![1]);
642
643        // Another permutation: TRUE=1, FALSE=2, AUX=0
644        // x1 has color 1 (TRUE), NOT_x1 has color 2 (FALSE)
645        let coloring_permuted2 = vec![1, 2, 0, 1, 2];
646        let extracted2 = reduction.extract_solution(&coloring_permuted2);
647        assert_eq!(extracted2, vec![1]);
648    }
649}
650
651// Register reduction with inventory for auto-discovery
652use crate::poly;
653use crate::rules::registry::{ReductionEntry, ReductionOverhead};
654
655inventory::submit! {
656    ReductionEntry {
657        source_name: "Satisfiability",
658        target_name: "Coloring",
659        source_graph: "CNF",
660        target_graph: "SimpleGraph",
661        overhead_fn: || ReductionOverhead::new(vec![
662            ("num_vertices", poly!(3 * num_vars)),
663            ("num_colors", poly!(3)),
664        ]),
665    }
666}
problemreductions/rules/sat_coloring.rs

problemreductions/rules/
sat_coloring.rs
