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::formula::Satisfiability;
12use crate::models::graph::KColoring;
13use crate::reduction;
14use crate::rules::sat_maximumindependentset::BoolVar;
15use crate::rules::traits::{ReduceTo, ReductionResult};
16use crate::topology::SimpleGraph;
17use crate::variant::K3;
18use std::collections::HashMap;
19
20/// Helper struct for constructing the graph for the SAT to 3-Coloring reduction.
21struct SATColoringConstructor {
22    /// The edges of the graph being constructed.
23    edges: Vec<(usize, usize)>,
24    /// Current number of vertices.
25    num_vertices: usize,
26    /// Mapping from positive variable index (0-indexed) to vertex index.
27    pos_vertices: Vec<usize>,
28    /// Mapping from negative variable index (0-indexed) to vertex index.
29    neg_vertices: Vec<usize>,
30    /// Mapping from BoolVar to vertex index.
31    vmap: HashMap<(usize, bool), usize>,
32}
33
34impl SATColoringConstructor {
35    /// Create a new SATColoringConstructor for `num_vars` variables.
36    ///
37    /// Initial graph structure:
38    /// - Vertices 0, 1, 2: TRUE, FALSE, AUX (forming a triangle)
39    /// - For each variable i (0-indexed):
40    ///   - Vertex 3 + i: positive literal (x_i)
41    ///   - Vertex 3 + num_vars + i: negative literal (NOT x_i)
42    fn new(num_vars: usize) -> Self {
43        let num_vertices = 2 * num_vars + 3;
44        let mut edges = Vec::new();
45
46        // Create triangle: TRUE(0), FALSE(1), AUX(2)
47        edges.push((0, 1));
48        edges.push((0, 2));
49        edges.push((1, 2));
50
51        // Create variable vertices and edges
52        let mut pos_vertices = Vec::with_capacity(num_vars);
53        let mut neg_vertices = Vec::with_capacity(num_vars);
54        let mut vmap = HashMap::new();
55
56        for i in 0..num_vars {
57            let pos_v = 3 + i;
58            let neg_v = 3 + num_vars + i;
59            pos_vertices.push(pos_v);
60            neg_vertices.push(neg_v);
61
62            // Connect to AUX (they can't be auxiliary color)
63            edges.push((pos_v, 2));
64            edges.push((neg_v, 2));
65
66            // Connect pos and neg of the same variable (they must have different colors)
67            edges.push((pos_v, neg_v));
68
69            // Build vmap
70            vmap.insert((i, false), pos_v); // positive literal
71            vmap.insert((i, true), neg_v); // negative literal
72        }
73
74        Self {
75            edges,
76            num_vertices,
77            pos_vertices,
78            neg_vertices,
79            vmap,
80        }
81    }
82
83    /// Get the TRUE vertex index.
84    fn true_vertex(&self) -> usize {
85        0
86    }
87
88    /// Get the FALSE vertex index.
89    fn false_vertex(&self) -> usize {
90        1
91    }
92
93    /// Get the AUX (ancilla) vertex index.
94    fn aux_vertex(&self) -> usize {
95        2
96    }
97
98    /// Add edge to connect vertex to AUX.
99    fn attach_to_aux(&mut self, idx: usize) {
100        self.add_edge(idx, self.aux_vertex());
101    }
102
103    /// Add edge to connect vertex to FALSE.
104    fn attach_to_false(&mut self, idx: usize) {
105        self.add_edge(idx, self.false_vertex());
106    }
107
108    /// Add edge to connect vertex to TRUE.
109    fn attach_to_true(&mut self, idx: usize) {
110        self.add_edge(idx, self.true_vertex());
111    }
112
113    /// Add an edge between two vertices.
114    fn add_edge(&mut self, u: usize, v: usize) {
115        self.edges.push((u, v));
116    }
117
118    /// Add vertices to the graph.
119    fn add_vertices(&mut self, n: usize) -> Vec<usize> {
120        let start = self.num_vertices;
121        self.num_vertices += n;
122        (start..self.num_vertices).collect()
123    }
124
125    /// Force a vertex to have the TRUE color.
126    /// This is done by connecting it to both AUX and FALSE.
127    fn set_true(&mut self, idx: usize) {
128        self.attach_to_aux(idx);
129        self.attach_to_false(idx);
130    }
131
132    /// Get the vertex index for a literal.
133    fn get_vertex(&self, var: &BoolVar) -> usize {
134        self.vmap[&(var.name, var.neg)]
135    }
136
137    /// Add a clause to the graph.
138    /// For a single-literal clause, just set the literal to TRUE.
139    /// For multi-literal clauses, build OR-gadgets recursively.
140    fn add_clause(&mut self, literals: &[i32]) {
141        assert!(
142            !literals.is_empty(),
143            "Clause must have at least one literal"
144        );
145
146        let first_var = BoolVar::from_literal(literals[0]);
147        let mut output_node = self.get_vertex(&first_var);
148
149        // Build OR-gadget chain for remaining literals
150        for &lit in &literals[1..] {
151            let var = BoolVar::from_literal(lit);
152            let input2 = self.get_vertex(&var);
153            output_node = self.add_or_gadget(output_node, input2);
154        }
155
156        // Force the output to be TRUE
157        self.set_true(output_node);
158    }
159
160    /// Add an OR-gadget that computes OR of two inputs.
161    ///
162    /// The OR-gadget ensures that if any input has TRUE color, the output can have TRUE color.
163    /// If both inputs have FALSE color, the output must have FALSE color.
164    ///
165    /// The gadget adds 5 vertices: ancilla1, ancilla2, entrance1, entrance2, output
166    ///
167    /// Returns the output vertex index.
168    fn add_or_gadget(&mut self, input1: usize, input2: usize) -> usize {
169        // Add 5 new vertices
170        let new_vertices = self.add_vertices(5);
171        let ancilla1 = new_vertices[0];
172        let ancilla2 = new_vertices[1];
173        let entrance1 = new_vertices[2];
174        let entrance2 = new_vertices[3];
175        let output = new_vertices[4];
176
177        // Connect output to AUX
178        self.attach_to_aux(output);
179
180        // Connect ancilla1 to TRUE
181        self.attach_to_true(ancilla1);
182
183        // Build the gadget structure (based on Julia implementation)
184        // (ancilla1, ancilla2), (ancilla2, input1), (ancilla2, input2),
185        // (entrance1, entrance2), (output, ancilla1), (input1, entrance2),
186        // (input2, entrance1), (entrance1, output), (entrance2, output)
187        self.add_edge(ancilla1, ancilla2);
188        self.add_edge(ancilla2, input1);
189        self.add_edge(ancilla2, input2);
190        self.add_edge(entrance1, entrance2);
191        self.add_edge(output, ancilla1);
192        self.add_edge(input1, entrance2);
193        self.add_edge(input2, entrance1);
194        self.add_edge(entrance1, output);
195        self.add_edge(entrance2, output);
196
197        output
198    }
199
200    /// Build the final KColoring problem.
201    fn build_coloring(&self) -> KColoring<K3, SimpleGraph> {
202        KColoring::<K3, _>::new(SimpleGraph::new(self.num_vertices, self.edges.clone()))
203    }
204}
205
206/// Result of reducing Satisfiability to KColoring.
207///
208/// This struct contains:
209/// - The target KColoring problem (3-coloring)
210/// - Mappings from variable indices to vertex indices
211/// - Information about the source problem
212#[derive(Debug, Clone)]
213pub struct ReductionSATToColoring {
214    /// The target KColoring problem.
215    target: KColoring<K3, SimpleGraph>,
216    /// Mapping from variable index (0-indexed) to positive literal vertex index.
217    pos_vertices: Vec<usize>,
218    /// Mapping from variable index (0-indexed) to negative literal vertex index.
219    neg_vertices: Vec<usize>,
220    /// Number of variables in the source SAT problem.
221    num_source_variables: usize,
222    /// Number of clauses in the source SAT problem.
223    num_clauses: usize,
224}
225
226impl ReductionResult for ReductionSATToColoring {
227    type Source = Satisfiability;
228    type Target = KColoring<K3, SimpleGraph>;
229
230    fn target_problem(&self) -> &Self::Target {
231        &self.target
232    }
233
234    /// Extract a SAT solution from a KColoring solution.
235    ///
236    /// The coloring solution maps each vertex to a color (0, 1, or 2).
237    /// - Color 0: TRUE
238    /// - Color 1: FALSE
239    /// - Color 2: AUX
240    ///
241    /// For each variable, we check if its positive literal vertex has TRUE color (0).
242    /// If so, the variable is assigned true (1); otherwise false (0).
243    fn extract_solution(&self, target_solution: &[usize]) -> Vec<usize> {
244        // First determine which color is TRUE, FALSE, and AUX
245        // Vertices 0, 1, 2 are TRUE, FALSE, AUX respectively
246        assert!(
247            target_solution.len() >= 3,
248            "Invalid solution: coloring must have at least 3 vertices"
249        );
250        let true_color = target_solution[0];
251        let false_color = target_solution[1];
252        let aux_color = target_solution[2];
253
254        // Sanity checks
255        assert!(
256            true_color != false_color && true_color != aux_color,
257            "Invalid coloring solution: special vertices must have distinct colors"
258        );
259
260        let mut assignment = vec![0usize; self.num_source_variables];
261
262        for (i, &pos_vertex) in self.pos_vertices.iter().enumerate() {
263            let vertex_color = target_solution[pos_vertex];
264
265            // Sanity check: variable vertices should not have AUX color
266            assert!(
267                vertex_color != aux_color,
268                "Invalid coloring solution: variable vertex has auxiliary color"
269            );
270
271            // If positive literal has TRUE color, variable is true (1)
272            // Otherwise, variable is false (0)
273            assignment[i] = if vertex_color == true_color { 1 } else { 0 };
274        }
275
276        assignment
277    }
278}
279
280impl ReductionSATToColoring {
281    /// Get the number of clauses in the source SAT problem.
282    pub fn num_clauses(&self) -> usize {
283        self.num_clauses
284    }
285
286    /// Get the positive vertices mapping.
287    pub fn pos_vertices(&self) -> &[usize] {
288        &self.pos_vertices
289    }
290
291    /// Get the negative vertices mapping.
292    pub fn neg_vertices(&self) -> &[usize] {
293        &self.neg_vertices
294    }
295}
296
297#[reduction(
298    overhead = {
299        num_vertices = "num_vars + num_literals",
300        num_edges = "num_vars + num_literals",
301    }
302)]
303impl ReduceTo<KColoring<K3, SimpleGraph>> for Satisfiability {
304    type Result = ReductionSATToColoring;
305
306    fn reduce_to(&self) -> Self::Result {
307        let mut constructor = SATColoringConstructor::new(self.num_vars());
308
309        // Add each clause to the graph
310        for clause in self.clauses() {
311            constructor.add_clause(&clause.literals);
312        }
313
314        let target = constructor.build_coloring();
315
316        ReductionSATToColoring {
317            target,
318            pos_vertices: constructor.pos_vertices,
319            neg_vertices: constructor.neg_vertices,
320            num_source_variables: self.num_vars(),
321            num_clauses: self.num_clauses(),
322        }
323    }
324}
325
326#[cfg(test)]
327#[path = "../unit_tests/rules/sat_coloring.rs"]
328mod tests;
problemreductions/rules/sat_coloring.rs

problemreductions/rules/
sat_coloring.rs
