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: &[i64]) {
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(
244        &self,
245        target_solution: &<Self::Target as crate::traits::Problem>::Solution,
246    ) -> crate::rules::ExtractionResult<<Self::Source as crate::traits::Problem>::Solution> {
247        crate::rules::traits::validate_target_solution(self.target_problem(), target_solution)?;
248
249        Ok({
250            // First determine which color is TRUE, FALSE, and AUX
251            // Vertices 0, 1, 2 are TRUE, FALSE, AUX respectively
252            let true_color = target_solution[0];
253            let false_color = target_solution[1];
254            let aux_color = target_solution[2];
255
256            if true_color == false_color || true_color == aux_color || false_color == aux_color {
257                return Err(crate::rules::ExtractionError::invalid(
258                    "target coloring does not distinguish true, false, and auxiliary colors",
259                ));
260            }
261
262            let mut assignment = vec![false; self.num_source_variables];
263
264            for (i, &pos_vertex) in self.pos_vertices.iter().enumerate() {
265                let vertex_color = target_solution[pos_vertex];
266
267                // Sanity check: variable vertices should not have AUX color
268                if vertex_color == aux_color {
269                    return Err(crate::rules::ExtractionError::invalid(format!(
270                        "variable {i} has the auxiliary color"
271                    )));
272                }
273
274                // If positive literal has TRUE color, variable is true (1)
275                // Otherwise, variable is false (0)
276                assignment[i] = vertex_color == true_color;
277            }
278
279            assignment
280        })
281    }
282}
283
284impl ReductionSATToColoring {
285    /// Get the number of clauses in the source SAT problem.
286    pub fn num_clauses(&self) -> usize {
287        self.num_clauses
288    }
289
290    /// Get the positive vertices mapping.
291    pub fn pos_vertices(&self) -> &[usize] {
292        &self.pos_vertices
293    }
294
295    /// Get the negative vertices mapping.
296    pub fn neg_vertices(&self) -> &[usize] {
297        &self.neg_vertices
298    }
299}
300
301#[reduction(
302    transform = exact {
303        num_vertices = "2 * num_vars + 3 + 5 * (num_literals - num_clauses)",
304        num_edges = "3 + 3 * num_vars + 11 * num_literals - 9 * num_clauses",
305        num_colors = "3",
306    }
307)]
308impl ReduceTo<KColoring<K3, SimpleGraph>> for Satisfiability {
309    type Result = ReductionSATToColoring;
310
311    fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
312        let mut constructor = SATColoringConstructor::new(self.num_vars());
313
314        // Add each clause to the graph
315        for clause in self.clauses() {
316            constructor.add_clause(&clause.literals);
317        }
318
319        let target = constructor.build_coloring();
320
321        Ok(ReductionSATToColoring {
322            target,
323            pos_vertices: constructor.pos_vertices,
324            neg_vertices: constructor.neg_vertices,
325            num_source_variables: self.num_vars(),
326            num_clauses: self.num_clauses(),
327        })
328    }
329}
330
331#[cfg(feature = "example-db")]
332pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
333    use crate::export::SolutionPair;
334    use crate::models::formula::{CNFClause, Satisfiability};
335
336    vec![crate::example_db::specs::RuleExampleSpec {
337        id: "satisfiability_to_kcoloring",
338        build: || {
339            let source = Satisfiability::new(
340                5,
341                vec![
342                    CNFClause::new(vec![1]),
343                    CNFClause::new(vec![-3]),
344                    CNFClause::new(vec![5]),
345                ],
346            );
347            crate::example_db::specs::rule_example_with_witness::<_, KColoring<K3, SimpleGraph>>(
348                source,
349                SolutionPair {
350                    source_config: serde_json::json!(vec![true, true, false, true, true]),
351                    target_config: serde_json::json!(vec![2, 1, 0, 2, 2, 1, 2, 2, 1, 1, 2, 1, 1]),
352                },
353            )
354        },
355    }]
356}
357
358#[cfg(test)]
359#[path = "../unit_tests/rules/sat_coloring.rs"]
360mod tests;
problemreductions/rules/sat_coloring.rs

problemreductions/rules/
sat_coloring.rs
