problemreductions/rules/
ksatisfiability_decisionminimumvertexcover.rs

1//! Reduction from KSatisfiability (3-SAT) to Decision Minimum Vertex Cover.
2//!
3//! This wraps the classical Garey & Johnson Theorem 3.3 construction in the
4//! `Decision<MinimumVertexCover<SimpleGraph, i32>>` wrapper, with threshold
5//! `k = n + 2m` for `n` variables and `m` clauses.
6
7use crate::models::decision::Decision;
8use crate::models::formula::KSatisfiability;
9use crate::models::graph::MinimumVertexCover;
10use crate::reduction;
11use crate::rules::ksatisfiability_minimumvertexcover::Reduction3SATToMVC;
12use crate::rules::traits::{ReduceTo, ReductionResult};
13use crate::topology::SimpleGraph;
14use crate::variant::K3;
15
16/// Result of reducing KSatisfiability<K3> to Decision<MinimumVertexCover<SimpleGraph, i32>>.
17#[derive(Debug, Clone)]
18pub struct Reduction3SATToDecisionMVC {
19    target: Decision<MinimumVertexCover<SimpleGraph, i32>>,
20    base_reduction: Reduction3SATToMVC,
21}
22
23impl ReductionResult for Reduction3SATToDecisionMVC {
24    type Source = KSatisfiability<K3>;
25    type Target = Decision<MinimumVertexCover<SimpleGraph, i32>>;
26
27    fn target_problem(&self) -> &Self::Target {
28        &self.target
29    }
30
31    fn extract_solution(&self, target_solution: &[usize]) -> Vec<usize> {
32        self.base_reduction.extract_solution(target_solution)
33    }
34}
35
36#[reduction(
37    overhead = {
38        num_vertices = "2 * num_vars + 3 * num_clauses",
39        num_edges = "num_vars + 6 * num_clauses",
40        k = "num_vars + 2 * num_clauses",
41    }
42)]
43impl ReduceTo<Decision<MinimumVertexCover<SimpleGraph, i32>>> for KSatisfiability<K3> {
44    type Result = Reduction3SATToDecisionMVC;
45
46    fn reduce_to(&self) -> Self::Result {
47        let base_reduction = <KSatisfiability<K3> as ReduceTo<
48            MinimumVertexCover<SimpleGraph, i32>,
49        >>::reduce_to(self);
50        let bound = i32::try_from(self.num_vars() + 2 * self.num_clauses())
51            .expect("decision minimum vertex cover bound must fit in i32");
52        let target = Decision::new(base_reduction.target_problem().clone(), bound);
53
54        Reduction3SATToDecisionMVC {
55            target,
56            base_reduction,
57        }
58    }
59}
60
61#[cfg(feature = "example-db")]
62pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
63    use crate::export::SolutionPair;
64    use crate::models::formula::CNFClause;
65
66    vec![crate::example_db::specs::RuleExampleSpec {
67        id: "ksatisfiability_to_decisionminimumvertexcover",
68        build: || {
69            let source = KSatisfiability::<K3>::new(
70                3,
71                vec![
72                    CNFClause::new(vec![1, 2, 3]),
73                    CNFClause::new(vec![-1, -2, 3]),
74                ],
75            );
76            crate::example_db::specs::rule_example_with_witness::<
77                _,
78                Decision<MinimumVertexCover<SimpleGraph, i32>>,
79            >(
80                source,
81                SolutionPair {
82                    source_config: vec![0, 0, 1],
83                    target_config: vec![0, 1, 0, 1, 1, 0, 1, 1, 0, 1, 1, 0],
84                },
85            )
86        },
87    }]
88}
89
90#[cfg(test)]
91#[path = "../unit_tests/rules/ksatisfiability_decisionminimumvertexcover.rs"]
92mod tests;
problemreductions/rules/ksatisfiability_decisionminimumvertexcover.rs

problemreductions/rules/
ksatisfiability_decisionminimumvertexcover.rs
