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, i64>>` 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, i64>>.
17#[derive(Debug, Clone)]
18pub struct Reduction3SATToDecisionMVC {
19    target: Decision<MinimumVertexCover<SimpleGraph, i64>>,
20    base_reduction: Reduction3SATToMVC,
21}
22
23impl ReductionResult for Reduction3SATToDecisionMVC {
24    type Source = KSatisfiability<K3>;
25    type Target = Decision<MinimumVertexCover<SimpleGraph, i64>>;
26
27    fn target_problem(&self) -> &Self::Target {
28        &self.target
29    }
30
31    fn extract_solution(
32        &self,
33        target_solution: &<Self::Target as crate::traits::Problem>::Solution,
34    ) -> crate::rules::ExtractionResult<<Self::Source as crate::traits::Problem>::Solution> {
35        self.base_reduction.extract_solution(target_solution)
36    }
37}
38
39#[reduction(
40    transform = exact {
41        num_vertices = "2 * num_vars + 3 * num_clauses",
42        num_edges = "num_vars + 6 * num_clauses",
43    }
44)]
45impl ReduceTo<Decision<MinimumVertexCover<SimpleGraph, i64>>> for KSatisfiability<K3> {
46    type Result = Reduction3SATToDecisionMVC;
47
48    fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
49        let base_reduction = <KSatisfiability<K3> as ReduceTo<
50            MinimumVertexCover<SimpleGraph, i64>,
51        >>::reduce_to(self)?;
52        let bound = self
53            .num_clauses()
54            .checked_mul(2)
55            .and_then(|value| value.checked_add(self.num_vars()))
56            .and_then(|value| i64::try_from(value).ok())
57            .ok_or_else(|| {
58                crate::rules::ReductionError::integer_overflow::<
59                    KSatisfiability<K3>,
60                    Decision<MinimumVertexCover<SimpleGraph, i64>>,
61                >("computing the target cover bound")
62            })?;
63        let target = Decision::new(base_reduction.target_problem().clone(), bound);
64
65        Ok(Reduction3SATToDecisionMVC {
66            target,
67            base_reduction,
68        })
69    }
70}
71
72#[cfg(feature = "example-db")]
73pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
74    use crate::export::SolutionPair;
75    use crate::models::formula::CNFClause;
76
77    vec![crate::example_db::specs::RuleExampleSpec {
78        id: "ksatisfiability_to_decisionminimumvertexcover",
79        build: || {
80            let source = KSatisfiability::<K3>::new(
81                3,
82                vec![
83                    CNFClause::new(vec![1, 2, 3]),
84                    CNFClause::new(vec![-1, -2, 3]),
85                ],
86            );
87            crate::example_db::specs::rule_example_with_witness::<
88                _,
89                Decision<MinimumVertexCover<SimpleGraph, i64>>,
90            >(
91                source,
92                SolutionPair {
93                    source_config: serde_json::json!(vec![false, false, true]),
94                    target_config: serde_json::json!(vec![
95                        false, true, false, true, true, false, true, true, false, true, true, false
96                    ]),
97                },
98            )
99        },
100    }]
101}
102
103#[cfg(test)]
104#[path = "../unit_tests/rules/ksatisfiability_decisionminimumvertexcover.rs"]
105mod tests;
problemreductions/rules/ksatisfiability_decisionminimumvertexcover.rs

problemreductions/rules/
ksatisfiability_decisionminimumvertexcover.rs
