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_witness(
59            self.target_problem(),
60            target_solution,
61            |value| value.0,
62            "target witness does not satisfy the target problem",
63        )?;
64        let nae_solution = (0..self.nae_reduction.target_problem().num_vars())
65            .map(|index| target_solution[2 * index])
66            .collect();
67        // Reuse the formal SAT -> NAE extraction (including sentinel
68        // normalization); no assignment search or speculative complement.
69        self.nae_reduction.extract_solution(&nae_solution)
70    }
71}
72
73#[crate::aggregate_reduction(identity)]
74impl crate::rules::AggregateReductionResult for Reduction3SATToMonochromaticTriangle {}
75
76#[reduction(
77    transform = upper_bound {
78        num_vertices = "16 * num_vars + 40 * num_clauses + 16",
79        num_edges = "50 * num_vars + 146 * num_clauses + 50",
80        num_triangles = "58 * num_vars + 174 * num_clauses + 58",
81    }
82)]
83impl ReduceTo<MonochromaticTriangle<SimpleGraph>> for KSatisfiability<K3> {
84    type Result = Reduction3SATToMonochromaticTriangle;
85
86    fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
87        let sat = ReduceTo::<Satisfiability>::reduce_to(self)?;
88        let nae_reduction = ReduceTo::<NAESatisfiability>::reduce_to(sat.target_problem())?;
89        let nae = nae_reduction.target_problem();
90        let auxiliary_count = nae.clauses().iter().filter(|c| c.len() == 4).count();
91        let overflow = || {
92            crate::rules::ReductionError::integer_overflow::<Self, MonochromaticTriangle<SimpleGraph>>(
93                "computing signal-sender graph size",
94            )
95        };
96        let variable_count = nae
97            .num_vars()
98            .checked_add(auxiliary_count)
99            .ok_or_else(overflow)?;
100        let triple_count = variable_count
101            .checked_add(nae.num_clauses())
102            .and_then(|n| n.checked_add(auxiliary_count))
103            .ok_or_else(overflow)?;
104        let num_vertices = variable_count
105            .checked_mul(4)
106            .and_then(|n| triple_count.checked_mul(12).and_then(|t| n.checked_add(t)))
107            .ok_or_else(overflow)?;
108        let num_edges = variable_count
109            .checked_mul(2)
110            .and_then(|n| triple_count.checked_mul(48).and_then(|t| n.checked_add(t)))
111            .ok_or_else(overflow)?;
112
113        let mut variables =
114            SatVariableAllocator::new("KSatisfiability -> MonochromaticTriangle", nae.num_vars())
115                .map_err(
116                crate::rules::ReductionError::construction::<
117                    Self,
118                    MonochromaticTriangle<SimpleGraph>,
119                >,
120            )?;
121        let mut triples = Vec::with_capacity(triple_count);
122        for index in 0..variable_count {
123            let literal = i64::try_from(index + 1).map_err(|_| overflow())?;
124            triples.push([literal, literal, -literal]);
125        }
126        for clause in nae.clauses() {
127            let literals = &clause.literals;
128            if literals.len() == 4 {
129                let z = variables.allocate().map_err(
130                    crate::rules::ReductionError::construction::<
131                        Self,
132                        MonochromaticTriangle<SimpleGraph>,
133                    >,
134                )?;
135                triples.push([literals[0], literals[1], z]);
136                triples.push([-z, literals[2], literals[3]]);
137            } else {
138                // NAE(a,b) = NAE(a,b,b). Formal SAT -> NAE produces only
139                // lengths 2, 3 and 4, including NAE(s,s) for an empty clause.
140                triples.push([literals[0], literals[1], literals[literals.len() - 1]]);
141            }
142        }
143
144        let mut edges = Vec::with_capacity(num_edges);
145        for index in 0..variable_count {
146            edges.extend([(4 * index, 4 * index + 1), (4 * index + 2, 4 * index + 3)]);
147        }
148        // All following offsets are bounded by the checked total above.
149        let mut next_vertex = 4 * variable_count;
150        for triple in triples {
151            let [a, b, c] = [next_vertex, next_vertex + 1, next_vertex + 2];
152            next_vertex += 3;
153            let sides = [(a, b), (a, c), (b, c)];
154            edges.extend(sides);
155            for (literal, side) in triple.into_iter().zip(sides) {
156                let index = usize::try_from(literal.unsigned_abs() - 1)
157                    .expect("validated SAT variable index fits usize");
158                let endpoint = 4 * index + if literal < 0 { 2 } else { 0 };
159                add_equality_sender(&mut edges, (endpoint, endpoint + 1), side, next_vertex);
160                next_vertex += 3;
161            }
162        }
163        debug_assert_eq!(next_vertex, num_vertices);
164        debug_assert_eq!(edges.len(), num_edges);
165        let target = MonochromaticTriangle::new(SimpleGraph::new(num_vertices, edges));
166        Ok(Reduction3SATToMonochromaticTriangle {
167            target,
168            nae_reduction,
169        })
170    }
171}
172
173#[cfg(feature = "example-db")]
174pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
175    use crate::export::SolutionPair;
176    use crate::models::formula::CNFClause;
177    use crate::solvers::ILPSolver;
178
179    vec![crate::example_db::specs::RuleExampleSpec {
180        id: "ksatisfiability_to_monochromatictriangle",
181        build: || {
182            let source = KSatisfiability::<K3>::new(3, vec![CNFClause::new(vec![1, 2, 3])]);
183            let reduction = ReduceTo::<MonochromaticTriangle<SimpleGraph>>::reduce_to(&source)
184                .expect("reduction should succeed");
185            let target_config = ILPSolver::new()
186                .solve(reduction.target_problem())
187                .expect("canonical target must be colourable");
188            let source_config = reduction.extract_solution(&target_config).unwrap();
189            crate::example_db::specs::assemble_rule_example(
190                &source,
191                reduction.target_problem(),
192                vec![SolutionPair {
193                    source_config: serde_json::to_value(source_config)
194                        .expect("solution serialization must succeed"),
195                    target_config: serde_json::to_value(target_config)
196                        .expect("solution serialization must succeed"),
197                }],
198            )
199        },
200    }]
201}
202
203#[cfg(test)]
204#[path = "../unit_tests/rules/ksatisfiability_monochromatictriangle.rs"]
205mod tests;
problemreductions/rules/ksatisfiability_monochromatictriangle.rs

problemreductions/rules/
ksatisfiability_monochromatictriangle.rs
