problemreductions/rules/
ksatisfiability_decisionminimumvertexcover.rs

1//! Reduction from KSatisfiability (3-SAT) to Decision<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::decision::Decision;
15use crate::models::formula::KSatisfiability;
16use crate::models::graph::MinimumVertexCover;
17use crate::reduction;
18use crate::rules::traits::{ReduceTo, ReductionResult};
19use crate::topology::SimpleGraph;
20use crate::types::One;
21use crate::variant::K3;
22
23/// Result of reducing KSatisfiability<K3> to Decision<MinimumVertexCover>.
24#[derive(Debug, Clone)]
25pub struct Reduction3SATToDecisionMVC {
26    target: Decision<MinimumVertexCover<SimpleGraph, One>>,
27    source_num_vars: usize,
28}
29
30impl ReductionResult for Reduction3SATToDecisionMVC {
31    type Source = KSatisfiability<K3>;
32    type Target = Decision<MinimumVertexCover<SimpleGraph, One>>;
33
34    fn target_problem(&self) -> &Self::Target {
35        &self.target
36    }
37
38    /// Extract a SAT assignment from a vertex cover solution.
39    ///
40    /// Vertex layout: indices 0..2n are literal vertices (even = positive,
41    /// odd = negated). For variable i, vertex 2*i is u_i and vertex 2*i+1
42    /// is not-u_i. Each truth-setting edge forces exactly one of these two
43    /// into any cover meeting the target bound. If u_i is in the cover, set x_i = 1;
44    /// if not-u_i is in the cover, set x_i = 0.
45    fn extract_solution(
46        &self,
47        target_solution: &<Self::Target as crate::traits::Problem>::Solution,
48    ) -> crate::rules::ExtractionResult<<Self::Source as crate::traits::Problem>::Solution> {
49        crate::rules::traits::validate_target_witness(
50            self.target_problem(),
51            target_solution,
52            |value| value.0,
53            "target witness does not certify a YES answer for the source",
54        )?;
55
56        Ok({
57            (0..self.source_num_vars)
58                .map(|i| {
59                    // u_i is at index 2*i, not-u_i is at index 2*i+1
60                    target_solution[2 * i]
61                })
62                .collect()
63        })
64    }
65}
66
67#[crate::aggregate_reduction(identity)]
68impl crate::rules::AggregateReductionResult for Reduction3SATToDecisionMVC {}
69
70#[reduction(
71    transform = exact {
72        num_vertices = "2 * num_vars + 3 * num_clauses",
73        num_edges = "num_vars + 6 * num_clauses",
74    }
75)]
76impl ReduceTo<Decision<MinimumVertexCover<SimpleGraph, One>>> for KSatisfiability<K3> {
77    type Result = Reduction3SATToDecisionMVC;
78
79    fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
80        let n = self.num_vars();
81        let m = self.num_clauses();
82        let total_vertices = 2 * n + 3 * m;
83        let mut edges: Vec<(usize, usize)> = Vec::with_capacity(n + 6 * m);
84
85        // Step 1: Truth-setting components.
86        // For each variable i, add edge (2*i, 2*i+1) connecting u_i and not-u_i.
87        for i in 0..n {
88            edges.push((2 * i, 2 * i + 1));
89        }
90
91        // Step 2: Satisfaction-testing components (triangles) and communication edges.
92        // For each clause j, triangle vertices are at indices 2*n + 3*j, 2*n + 3*j + 1, 2*n + 3*j + 2.
93        for (j, clause) in self.clauses().iter().enumerate() {
94            let base = 2 * n + 3 * j;
95
96            // Triangle edges within clause j
97            edges.push((base, base + 1));
98            edges.push((base + 1, base + 2));
99            edges.push((base, base + 2));
100
101            // Communication edges: connect triangle vertex k to the literal vertex
102            for k in 0..3 {
103                if clause.literals.is_empty() {
104                    // All three clause vertices must be selected, exceeding
105                    // the two-per-clause bound for an empty (false) clause.
106                    edges.push((base + k, base + k));
107                    continue;
108                }
109                // Repeating a literal pads a short clause without changing it.
110                let lit = clause.literals[k % clause.literals.len()];
111                let var_idx = lit.unsigned_abs() as usize - 1; // 0-indexed variable
112                let literal_vertex = if lit > 0 {
113                    2 * var_idx // positive literal vertex
114                } else {
115                    2 * var_idx + 1 // negated literal vertex
116                };
117                edges.push((base + k, literal_vertex));
118            }
119        }
120
121        let graph = SimpleGraph::new(total_vertices, edges);
122        let weights = vec![One; total_vertices];
123        let target = MinimumVertexCover::new(graph, weights);
124
125        Ok(Reduction3SATToDecisionMVC {
126            target: Decision::new(
127                target,
128                <Self as ReduceTo<Decision<MinimumVertexCover<SimpleGraph, One>>>>::exact_i64(
129                    n + 2 * m,
130                    "computing the cover bound",
131                )?,
132            ),
133            source_num_vars: n,
134        })
135    }
136}
137
138#[cfg(feature = "example-db")]
139pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
140    use crate::export::SolutionPair;
141    use crate::models::formula::CNFClause;
142
143    vec![crate::example_db::specs::RuleExampleSpec {
144        id: "ksatisfiability_to_decisionminimumvertexcover",
145        build: || {
146            let source = KSatisfiability::<K3>::new(
147                3,
148                vec![
149                    CNFClause::new(vec![1, 2, 3]),
150                    CNFClause::new(vec![-1, -2, 3]),
151                ],
152            );
153            crate::example_db::specs::rule_example_with_witness::<
154                _,
155                Decision<MinimumVertexCover<SimpleGraph, One>>,
156            >(
157                source,
158                SolutionPair {
159                    // x1=0, x2=0, x3=1 satisfies both clauses
160                    source_config: serde_json::json!(vec![false, false, true]),
161                    // Literal vertices: u1(0), ~u1(1), u2(2), ~u2(3), u3(4), ~u3(5)
162                    // Clause 0 triangle: v6, v7, v8 (literals x1, x2, x3)
163                    // Clause 1 triangle: v9, v10, v11 (literals ~x1, ~x2, x3)
164                    // VC: from truth-setting, pick ~u1(1), ~u2(3), u3(4)
165                    // Clause 0: u1,u2 not in cover -> pick v6,v7; u3 in cover -> v8 free
166                    // Clause 1: ~u1,~u2,u3 all in cover -> pick any 2: v9,v10
167                    // Total cover size = 3 + 2 + 2 = 7 = n + 2m
168                    target_config: serde_json::json!(vec![
169                        false, true, false, true, true, false, true, true, false, true, true, false
170                    ]),
171                },
172            )
173        },
174    }]
175}
176
177#[cfg(test)]
178#[path = "../unit_tests/rules/ksatisfiability_decisionminimumvertexcover.rs"]
179mod tests;
problemreductions/rules/ksatisfiability_decisionminimumvertexcover.rs

problemreductions/rules/
ksatisfiability_decisionminimumvertexcover.rs
