problemreductions/rules/
ksatisfiability_monochromatictriangle.rs

1//! Reduction from 3-SAT to edge colouring without monochromatic triangles.
2//!
3//! The construction uses the signal-sender framework of Burr, Erdős and Lovász
4//! (On graphs of Ramsey type, 1976). Here an equality sender is two K5 copies
5//! sharing a private triangle: their two complementary edges must have the same
6//! colour. NAE clause triangles are linked to disjoint literal signal edges by
7//! these senders, so their colour constraints actually encode the formula.
8//!
9//! See the full sender, composition and extraction proof in reductions.typ.
10
11use crate::models::formula::{KSatisfiability, NAESatisfiability, Satisfiability};
12use crate::models::graph::MonochromaticTriangle;
13use crate::reduction;
14use crate::rules::sat_helpers::SatVariableAllocator;
15use crate::rules::satisfiability_naesatisfiability::ReductionSATToNAESAT;
16use crate::rules::traits::{ReduceTo, ReductionResult};
17use crate::topology::SimpleGraph;
18use crate::variant::K3;
19
20/// Append the fifteen nonterminal edges of an equality sender.
21///
22/// The terminal edges already exist and have four distinct endpoints. The
23/// three vertices starting at `private` belong only to this sender. Both K5
24/// copies induce the same private triangle; their complementary edges have
25/// its majority colour in every valid colouring. Either equal colour extends.
26fn add_equality_sender(
27    edges: &mut Vec<(usize, usize)>,
28    first: (usize, usize),
29    second: (usize, usize),
30    private: usize,
31) {
32    let [u, v, w] = [private, private + 1, private + 2];
33    edges.extend([(u, v), (u, w), (v, w)]);
34    for endpoint in [first.0, first.1, second.0, second.1] {
35        edges.extend([(endpoint, u), (endpoint, v), (endpoint, w)]);
36    }
37}
38
39/// Result of reducing KSatisfiability<K3> to MonochromaticTriangle.
40#[derive(Debug, Clone)]
41pub struct Reduction3SATToMonochromaticTriangle {
42    target: MonochromaticTriangle<SimpleGraph>,
43    nae_reduction: ReductionSATToNAESAT,
44}
45
46impl ReductionResult for Reduction3SATToMonochromaticTriangle {
47    type Source = KSatisfiability<K3>;
48    type Target = MonochromaticTriangle<SimpleGraph>;
49
50    fn target_problem(&self) -> &Self::Target {
51        &self.target
52    }
53
54    fn extract_solution(
55        &self,
56        target_solution: &<Self::Target as crate::traits::Problem>::Solution,
57    ) -> crate::rules::ExtractionResult<<Self::Source as crate::traits::Problem>::Solution> {
58        crate::rules::traits::validate_target_solution(self.target_problem(), target_solution)?;
59        let nae_solution = (0..self.nae_reduction.target_problem().num_vars())
60            .map(|index| target_solution[2 * index])
61            .collect();
62        // Reuse the formal SAT -> NAE extraction (including sentinel
63        // normalization); no assignment search or speculative complement.
64        self.nae_reduction.extract_solution(&nae_solution)
65    }
66}
67
68#[reduction(
69    transform = upper_bound {
70        num_vertices = "16 * num_vars + 40 * num_clauses + 16",
71        num_edges = "50 * num_vars + 146 * num_clauses + 50",
72        num_triangles = "58 * num_vars + 174 * num_clauses + 58",
73    }
74)]
75impl ReduceTo<MonochromaticTriangle<SimpleGraph>> for KSatisfiability<K3> {
76    type Result = Reduction3SATToMonochromaticTriangle;
77
78    fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
79        let sat = ReduceTo::<Satisfiability>::reduce_to(self)?;
80        let nae_reduction = ReduceTo::<NAESatisfiability>::reduce_to(sat.target_problem())?;
81        let nae = nae_reduction.target_problem();
82        let auxiliary_count = nae.clauses().iter().filter(|c| c.len() == 4).count();
83        let overflow = || {
84            crate::rules::ReductionError::integer_overflow::<Self, MonochromaticTriangle<SimpleGraph>>(
85                "computing signal-sender graph size",
86            )
87        };
88        let variable_count = nae
89            .num_vars()
90            .checked_add(auxiliary_count)
91            .ok_or_else(overflow)?;
92        let triple_count = variable_count
93            .checked_add(nae.num_clauses())
94            .and_then(|n| n.checked_add(auxiliary_count))
95            .ok_or_else(overflow)?;
96        let num_vertices = variable_count
97            .checked_mul(4)
98            .and_then(|n| triple_count.checked_mul(12).and_then(|t| n.checked_add(t)))
99            .ok_or_else(overflow)?;
100        let num_edges = variable_count
101            .checked_mul(2)
102            .and_then(|n| triple_count.checked_mul(48).and_then(|t| n.checked_add(t)))
103            .ok_or_else(overflow)?;
104
105        let mut variables =
106            SatVariableAllocator::new("KSatisfiability -> MonochromaticTriangle", nae.num_vars())
107                .map_err(
108                crate::rules::ReductionError::construction::<
109                    Self,
110                    MonochromaticTriangle<SimpleGraph>,
111                >,
112            )?;
113        let mut triples = Vec::with_capacity(triple_count);
114        for index in 0..variable_count {
115            let literal = i64::try_from(index + 1).map_err(|_| overflow())?;
116            triples.push([literal, literal, -literal]);
117        }
118        for clause in nae.clauses() {
119            let literals = &clause.literals;
120            if literals.len() == 4 {
121                let z = variables.allocate().map_err(
122                    crate::rules::ReductionError::construction::<
123                        Self,
124                        MonochromaticTriangle<SimpleGraph>,
125                    >,
126                )?;
127                triples.push([literals[0], literals[1], z]);
128                triples.push([-z, literals[2], literals[3]]);
129            } else {
130                // NAE(a,b) = NAE(a,b,b). Formal SAT -> NAE produces only
131                // lengths 2, 3 and 4, including NAE(s,s) for an empty clause.
132                triples.push([literals[0], literals[1], literals[literals.len() - 1]]);
133            }
134        }
135
136        let mut edges = Vec::with_capacity(num_edges);
137        for index in 0..variable_count {
138            edges.extend([(4 * index, 4 * index + 1), (4 * index + 2, 4 * index + 3)]);
139        }
140        // All following offsets are bounded by the checked total above.
141        let mut next_vertex = 4 * variable_count;
142        for triple in triples {
143            let [a, b, c] = [next_vertex, next_vertex + 1, next_vertex + 2];
144            next_vertex += 3;
145            let sides = [(a, b), (a, c), (b, c)];
146            edges.extend(sides);
147            for (literal, side) in triple.into_iter().zip(sides) {
148                let index = usize::try_from(literal.unsigned_abs() - 1)
149                    .expect("validated SAT variable index fits usize");
150                let endpoint = 4 * index + if literal < 0 { 2 } else { 0 };
151                add_equality_sender(&mut edges, (endpoint, endpoint + 1), side, next_vertex);
152                next_vertex += 3;
153            }
154        }
155        debug_assert_eq!(next_vertex, num_vertices);
156        debug_assert_eq!(edges.len(), num_edges);
157        let target = MonochromaticTriangle::new(SimpleGraph::new(num_vertices, edges));
158        Ok(Reduction3SATToMonochromaticTriangle {
159            target,
160            nae_reduction,
161        })
162    }
163}
164
165#[cfg(feature = "example-db")]
166pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
167    use crate::export::SolutionPair;
168    use crate::models::formula::CNFClause;
169    use crate::solvers::ILPSolver;
170
171    vec![crate::example_db::specs::RuleExampleSpec {
172        id: "ksatisfiability_to_monochromatictriangle",
173        build: || {
174            let source = KSatisfiability::<K3>::new(3, vec![CNFClause::new(vec![1, 2, 3])]);
175            let reduction = ReduceTo::<MonochromaticTriangle<SimpleGraph>>::reduce_to(&source)
176                .expect("reduction should succeed");
177            let target_config = ILPSolver::new()
178                .solve(reduction.target_problem())
179                .expect("canonical target must be colourable");
180            let source_config = reduction.extract_solution(&target_config).unwrap();
181            crate::example_db::specs::assemble_rule_example(
182                &source,
183                reduction.target_problem(),
184                vec![SolutionPair {
185                    source_config: serde_json::to_value(source_config)
186                        .expect("solution serialization must succeed"),
187                    target_config: serde_json::to_value(target_config)
188                        .expect("solution serialization must succeed"),
189                }],
190            )
191        },
192    }]
193}
194
195#[cfg(test)]
196#[path = "../unit_tests/rules/ksatisfiability_monochromatictriangle.rs"]
197mod tests;
problemreductions/rules/ksatisfiability_monochromatictriangle.rs

problemreductions/rules/
ksatisfiability_monochromatictriangle.rs
