problemreductions/rules/
ksatisfiability_minimumvertexcover.rs

1//! Reduction from KSatisfiability (3-SAT) to MinimumVertexCover.
2//!
3//! Classical Garey & Johnson reduction (Theorem 3.3). For each variable u_i,
4//! add two vertices {u_i, not-u_i} connected by a truth-setting edge. For each
5//! clause c_j, add 3 vertices forming a satisfaction-testing triangle. For each
6//! literal l_k in clause c_j, add a communication edge from the triangle vertex
7//! j_k to the literal vertex l_k.
8//!
9//! The resulting graph has a vertex cover of size n + 2m if and only if the
10//! 3-SAT formula is satisfiable (n = num_vars, m = num_clauses).
11//!
12//! Reference: Garey & Johnson, "Computers and Intractability", 1979, Theorem 3.3
13
14use crate::models::formula::KSatisfiability;
15use crate::models::graph::MinimumVertexCover;
16use crate::reduction;
17use crate::rules::traits::{ReduceTo, ReductionResult};
18use crate::topology::SimpleGraph;
19use crate::variant::K3;
20
21/// Result of reducing KSatisfiability<K3> to MinimumVertexCover.
22#[derive(Debug, Clone)]
23pub struct Reduction3SATToMVC {
24    target: MinimumVertexCover<SimpleGraph, i64>,
25    source_num_vars: usize,
26}
27
28impl ReductionResult for Reduction3SATToMVC {
29    type Source = KSatisfiability<K3>;
30    type Target = MinimumVertexCover<SimpleGraph, i64>;
31
32    fn target_problem(&self) -> &Self::Target {
33        &self.target
34    }
35
36    /// Extract a SAT assignment from a vertex cover solution.
37    ///
38    /// Vertex layout: indices 0..2n are literal vertices (even = positive,
39    /// odd = negated). For variable i, vertex 2*i is u_i and vertex 2*i+1
40    /// is not-u_i. Each truth-setting edge forces exactly one of these two
41    /// into any minimum vertex cover. If u_i is in the cover, set x_i = 1;
42    /// if not-u_i is in the cover, set x_i = 0.
43    fn extract_solution(
44        &self,
45        target_solution: &<Self::Target as crate::traits::Problem>::Solution,
46    ) -> crate::rules::ExtractionResult<<Self::Source as crate::traits::Problem>::Solution> {
47        crate::rules::traits::validate_target_solution(self.target_problem(), target_solution)?;
48
49        Ok({
50            (0..self.source_num_vars)
51                .map(|i| {
52                    // u_i is at index 2*i, not-u_i is at index 2*i+1
53                    target_solution[2 * i]
54                })
55                .collect()
56        })
57    }
58}
59
60#[reduction(
61    transform = exact {
62        num_vertices = "2 * num_vars + 3 * num_clauses",
63        num_edges = "num_vars + 6 * num_clauses",
64    }
65)]
66impl ReduceTo<MinimumVertexCover<SimpleGraph, i64>> for KSatisfiability<K3> {
67    type Result = Reduction3SATToMVC;
68
69    fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
70        let n = self.num_vars();
71        let m = self.num_clauses();
72        let total_vertices = 2 * n + 3 * m;
73        let mut edges: Vec<(usize, usize)> = Vec::with_capacity(n + 6 * m);
74
75        // Step 1: Truth-setting components.
76        // For each variable i, add edge (2*i, 2*i+1) connecting u_i and not-u_i.
77        for i in 0..n {
78            edges.push((2 * i, 2 * i + 1));
79        }
80
81        // Step 2: Satisfaction-testing components (triangles) and communication edges.
82        // For each clause j, triangle vertices are at indices 2*n + 3*j, 2*n + 3*j + 1, 2*n + 3*j + 2.
83        for (j, clause) in self.clauses().iter().enumerate() {
84            let base = 2 * n + 3 * j;
85
86            // Triangle edges within clause j
87            edges.push((base, base + 1));
88            edges.push((base + 1, base + 2));
89            edges.push((base, base + 2));
90
91            // Communication edges: connect triangle vertex k to the literal vertex
92            for (k, &lit) in clause.literals.iter().enumerate() {
93                let var_idx = lit.unsigned_abs() as usize - 1; // 0-indexed variable
94                let literal_vertex = if lit > 0 {
95                    2 * var_idx // positive literal vertex
96                } else {
97                    2 * var_idx + 1 // negated literal vertex
98                };
99                edges.push((base + k, literal_vertex));
100            }
101        }
102
103        let graph = SimpleGraph::new(total_vertices, edges);
104        let weights = vec![1i64; total_vertices];
105        let target = MinimumVertexCover::new(graph, weights);
106
107        Ok(Reduction3SATToMVC {
108            target,
109            source_num_vars: n,
110        })
111    }
112}
113
114#[cfg(feature = "example-db")]
115pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
116    use crate::export::SolutionPair;
117    use crate::models::formula::CNFClause;
118
119    vec![crate::example_db::specs::RuleExampleSpec {
120        id: "ksatisfiability_to_minimumvertexcover",
121        build: || {
122            let source = KSatisfiability::<K3>::new(
123                3,
124                vec![
125                    CNFClause::new(vec![1, 2, 3]),
126                    CNFClause::new(vec![-1, -2, 3]),
127                ],
128            );
129            crate::example_db::specs::rule_example_with_witness::<
130                _,
131                MinimumVertexCover<SimpleGraph, i64>,
132            >(
133                source,
134                SolutionPair {
135                    // x1=0, x2=0, x3=1 satisfies both clauses
136                    source_config: serde_json::json!(vec![false, false, true]),
137                    // Literal vertices: u1(0), ~u1(1), u2(2), ~u2(3), u3(4), ~u3(5)
138                    // Clause 0 triangle: v6, v7, v8 (literals x1, x2, x3)
139                    // Clause 1 triangle: v9, v10, v11 (literals ~x1, ~x2, x3)
140                    // VC: from truth-setting, pick ~u1(1), ~u2(3), u3(4)
141                    // Clause 0: u1,u2 not in cover -> pick v6,v7; u3 in cover -> v8 free
142                    // Clause 1: ~u1,~u2,u3 all in cover -> pick any 2: v9,v10
143                    // Total cover size = 3 + 2 + 2 = 7 = n + 2m
144                    target_config: serde_json::json!(vec![
145                        false, true, false, true, true, false, true, true, false, true, true, false
146                    ]),
147                },
148            )
149        },
150    }]
151}
152
153#[cfg(test)]
154#[path = "../unit_tests/rules/ksatisfiability_minimumvertexcover.rs"]
155mod tests;
problemreductions/rules/ksatisfiability_minimumvertexcover.rs

problemreductions/rules/
ksatisfiability_minimumvertexcover.rs
