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        if literals.is_empty() {
142            self.add_edge(self.true_vertex(), self.true_vertex());
143            return;
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    /// Number of clauses in the source SAT problem.
222    num_clauses: usize,
223}
224
225impl ReductionResult for ReductionSATToColoring {
226    type Source = Satisfiability;
227    type Target = KColoring<K3, SimpleGraph>;
228
229    fn target_problem(&self) -> &Self::Target {
230        &self.target
231    }
232
233    /// Extract a SAT solution from a KColoring solution.
234    ///
235    /// The coloring solution maps each vertex to a color (0, 1, or 2).
236    /// The color of vertex 0 represents TRUE, independently of color labels.
237    fn extract_solution(
238        &self,
239        target_solution: &<Self::Target as crate::traits::Problem>::Solution,
240    ) -> crate::rules::ExtractionResult<<Self::Source as crate::traits::Problem>::Solution> {
241        crate::rules::traits::validate_target_witness(
242            self.target_problem(),
243            target_solution,
244            |value| value.0,
245            "target coloring is not valid",
246        )?;
247        Ok(self
248            .pos_vertices
249            .iter()
250            .map(|&vertex| target_solution[vertex] == target_solution[0])
251            .collect())
252    }
253}
254
255impl ReductionSATToColoring {
256    /// Get the number of clauses in the source SAT problem.
257    pub fn num_clauses(&self) -> usize {
258        self.num_clauses
259    }
260
261    /// Get the positive vertices mapping.
262    pub fn pos_vertices(&self) -> &[usize] {
263        &self.pos_vertices
264    }
265
266    /// Get the negative vertices mapping.
267    pub fn neg_vertices(&self) -> &[usize] {
268        &self.neg_vertices
269    }
270}
271
272#[crate::aggregate_reduction(identity)]
273impl crate::rules::AggregateReductionResult for ReductionSATToColoring {}
274
275#[reduction(
276    transform = upper_bound {
277        num_vertices = "2 * num_vars + 3 + 5 * num_literals",
278        num_edges = "3 + 3 * num_vars + 11 * num_literals + 2 * num_clauses",
279        num_colors = "3",
280    }
281)]
282impl ReduceTo<KColoring<K3, SimpleGraph>> for Satisfiability {
283    type Result = ReductionSATToColoring;
284
285    fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
286        let mut constructor = SATColoringConstructor::new(self.num_vars());
287
288        // Add each clause to the graph
289        for clause in self.clauses() {
290            constructor.add_clause(&clause.literals);
291        }
292
293        let target = constructor.build_coloring();
294
295        Ok(ReductionSATToColoring {
296            target,
297            pos_vertices: constructor.pos_vertices,
298            neg_vertices: constructor.neg_vertices,
299            num_clauses: self.num_clauses(),
300        })
301    }
302}
303
304#[cfg(feature = "example-db")]
305pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
306    use crate::export::SolutionPair;
307    use crate::models::formula::{CNFClause, Satisfiability};
308
309    vec![crate::example_db::specs::RuleExampleSpec {
310        id: "satisfiability_to_kcoloring",
311        build: || {
312            let source = Satisfiability::new(
313                5,
314                vec![
315                    CNFClause::new(vec![1]),
316                    CNFClause::new(vec![-3]),
317                    CNFClause::new(vec![5]),
318                ],
319            );
320            crate::example_db::specs::rule_example_with_witness::<_, KColoring<K3, SimpleGraph>>(
321                source,
322                SolutionPair {
323                    source_config: serde_json::json!(vec![true, true, false, true, true]),
324                    target_config: serde_json::json!(vec![2, 1, 0, 2, 2, 1, 2, 2, 1, 1, 2, 1, 1]),
325                },
326            )
327        },
328    }]
329}
330
331#[cfg(test)]
332#[path = "../unit_tests/rules/sat_coloring.rs"]
333mod tests;
problemreductions/rules/sat_coloring.rs

problemreductions/rules/
sat_coloring.rs
