problemreductions/rules/
ksatisfiability_monochromatictriangle.rs

1//! Reduction from KSatisfiability (3-SAT) to MonochromaticTriangle.
2//!
3//! For each variable, create positive/negative literal vertices joined by a
4//! negation edge. Each clause adds three fresh intermediates that form a clause
5//! triangle, plus six fan edges from the clause literals to those intermediates.
6//! The resulting graph has a triangle-free 2-edge-coloring iff the source
7//! formula is satisfiable.
8
9use crate::models::formula::KSatisfiability;
10use crate::models::graph::MonochromaticTriangle;
11use crate::reduction;
12use crate::rules::traits::{ReduceTo, ReductionResult};
13use crate::topology::SimpleGraph;
14use crate::traits::Problem;
15use crate::variant::K3;
16use std::collections::HashMap;
17
18fn normalized_edge(u: usize, v: usize) -> (usize, usize) {
19    if u < v {
20        (u, v)
21    } else {
22        (v, u)
23    }
24}
25
26fn literal_vertex(num_vars: usize, literal: i32) -> usize {
27    if literal > 0 {
28        literal as usize - 1
29    } else {
30        num_vars + literal.unsigned_abs() as usize - 1
31    }
32}
33
34/// Result of reducing KSatisfiability<K3> to MonochromaticTriangle.
35#[derive(Debug, Clone)]
36pub struct Reduction3SATToMonochromaticTriangle {
37    target: MonochromaticTriangle<SimpleGraph>,
38    source: KSatisfiability<K3>,
39    negation_edge_indices: Vec<usize>,
40}
41
42impl ReductionResult for Reduction3SATToMonochromaticTriangle {
43    type Source = KSatisfiability<K3>;
44    type Target = MonochromaticTriangle<SimpleGraph>;
45
46    fn target_problem(&self) -> &Self::Target {
47        &self.target
48    }
49
50    fn extract_solution(&self, target_solution: &[usize]) -> Vec<usize> {
51        let direct: Vec<usize> = self
52            .negation_edge_indices
53            .iter()
54            .map(
55                |&edge_idx| match target_solution.get(edge_idx).copied().unwrap_or(1) {
56                    0 => 1,
57                    _ => 0,
58                },
59            )
60            .collect();
61        if self.source.evaluate(&direct).0 {
62            return direct;
63        }
64
65        let complement: Vec<usize> = direct.iter().map(|&value| 1 - value).collect();
66        if self.source.evaluate(&complement).0 {
67            return complement;
68        }
69
70        direct
71    }
72}
73
74#[reduction(
75    overhead = {
76        num_vertices = "2 * num_vars + 3 * num_clauses",
77        num_edges = "num_vars + 9 * num_clauses",
78    }
79)]
80impl ReduceTo<MonochromaticTriangle<SimpleGraph>> for KSatisfiability<K3> {
81    type Result = Reduction3SATToMonochromaticTriangle;
82
83    fn reduce_to(&self) -> Self::Result {
84        let num_vars = self.num_vars();
85        let num_clauses = self.num_clauses();
86        let mut edges = Vec::with_capacity(num_vars + 9 * num_clauses);
87
88        for var in 0..num_vars {
89            edges.push((var, num_vars + var));
90        }
91
92        for (clause_idx, clause) in self.clauses().iter().enumerate() {
93            let clause_base = 2 * num_vars + 3 * clause_idx;
94            let m12 = clause_base;
95            let m13 = clause_base + 1;
96            let m23 = clause_base + 2;
97            let literal_vertices: Vec<usize> = clause
98                .literals
99                .iter()
100                .map(|&literal| literal_vertex(num_vars, literal))
101                .collect();
102            let v1 = literal_vertices[0];
103            let v2 = literal_vertices[1];
104            let v3 = literal_vertices[2];
105
106            edges.extend_from_slice(&[
107                (v1, m12),
108                (v2, m12),
109                (v1, m13),
110                (v3, m13),
111                (v2, m23),
112                (v3, m23),
113                (m12, m13),
114                (m12, m23),
115                (m13, m23),
116            ]);
117        }
118
119        let target =
120            MonochromaticTriangle::new(SimpleGraph::new(2 * num_vars + 3 * num_clauses, edges));
121        let edge_indices: HashMap<(usize, usize), usize> = target
122            .edge_list()
123            .iter()
124            .copied()
125            .enumerate()
126            .map(|(idx, (u, v))| (normalized_edge(u, v), idx))
127            .collect();
128        let negation_edge_indices = (0..num_vars)
129            .map(|var| edge_indices[&normalized_edge(var, num_vars + var)])
130            .collect();
131
132        Reduction3SATToMonochromaticTriangle {
133            target,
134            source: self.clone(),
135            negation_edge_indices,
136        }
137    }
138}
139
140#[cfg(feature = "example-db")]
141pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
142    use crate::export::SolutionPair;
143    use crate::models::formula::CNFClause;
144    use crate::solvers::BruteForce;
145
146    vec![crate::example_db::specs::RuleExampleSpec {
147        id: "ksatisfiability_to_monochromatictriangle",
148        build: || {
149            let source = KSatisfiability::<K3>::new(3, vec![CNFClause::new(vec![1, 2, 3])]);
150            let reduction =
151                <KSatisfiability<K3> as ReduceTo<MonochromaticTriangle<SimpleGraph>>>::reduce_to(
152                    &source,
153                );
154            let target_config = BruteForce::new()
155                .find_witness(reduction.target_problem())
156                .expect("canonical MonochromaticTriangle example must be feasible");
157            let source_config = reduction.extract_solution(&target_config);
158            crate::example_db::specs::assemble_rule_example(
159                &source,
160                reduction.target_problem(),
161                vec![SolutionPair {
162                    source_config,
163                    target_config,
164                }],
165            )
166        },
167    }]
168}
169
170#[cfg(test)]
171#[path = "../unit_tests/rules/ksatisfiability_monochromatictriangle.rs"]
172mod tests;
problemreductions/rules/ksatisfiability_monochromatictriangle.rs

problemreductions/rules/
ksatisfiability_monochromatictriangle.rs
