problemreductions/rules/
ksatisfiability_kernel.rs

1//! Reduction from 3-SAT to Kernel.
2//!
3//! This is Chvatal's 1973 construction using variable digons and clause
4//! 3-cycles with arcs to literal vertices.
5
6use crate::models::formula::KSatisfiability;
7use crate::models::graph::Kernel;
8use crate::reduction;
9use crate::rules::traits::{ReduceTo, ReductionResult};
10use crate::topology::DirectedGraph;
11use crate::variant::K3;
12
13/// Result of reducing 3-SAT to Kernel.
14#[derive(Debug, Clone)]
15pub struct Reduction3SatToKernel {
16    target: Kernel,
17    source_num_vars: usize,
18}
19
20impl ReductionResult for Reduction3SatToKernel {
21    type Source = KSatisfiability<K3>;
22    type Target = Kernel;
23
24    fn target_problem(&self) -> &Self::Target {
25        &self.target
26    }
27
28    fn extract_solution(&self, target_solution: &[usize]) -> Vec<usize> {
29        (0..self.source_num_vars)
30            .map(|i| usize::from(target_solution.get(2 * i).copied().unwrap_or(0) == 1))
31            .collect()
32    }
33}
34
35fn literal_vertex(literal: i32) -> usize {
36    let variable = literal.unsigned_abs() as usize - 1;
37    if literal > 0 {
38        2 * variable
39    } else {
40        2 * variable + 1
41    }
42}
43
44#[reduction(
45    overhead = {
46        num_vertices = "2 * num_vars + 3 * num_clauses",
47        num_arcs = "2 * num_vars + 6 * num_clauses",
48    }
49)]
50impl ReduceTo<Kernel> for KSatisfiability<K3> {
51    type Result = Reduction3SatToKernel;
52
53    fn reduce_to(&self) -> Self::Result {
54        let num_vars = self.num_vars();
55        let num_clauses = self.num_clauses();
56        let mut arcs = Vec::with_capacity(2 * num_vars + 6 * num_clauses);
57
58        for variable in 0..num_vars {
59            let positive = 2 * variable;
60            let negative = positive + 1;
61            arcs.push((positive, negative));
62            arcs.push((negative, positive));
63        }
64
65        for (clause_index, clause) in self.clauses().iter().enumerate() {
66            let clause_base = 2 * num_vars + 3 * clause_index;
67            arcs.push((clause_base, clause_base + 1));
68            arcs.push((clause_base + 1, clause_base + 2));
69            arcs.push((clause_base + 2, clause_base));
70
71            for (literal_index, &literal) in clause.literals.iter().enumerate() {
72                arcs.push((clause_base + literal_index, literal_vertex(literal)));
73            }
74        }
75
76        Reduction3SatToKernel {
77            target: Kernel::new(DirectedGraph::new(2 * num_vars + 3 * num_clauses, arcs)),
78            source_num_vars: num_vars,
79        }
80    }
81}
82
83#[cfg(feature = "example-db")]
84pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
85    use crate::export::SolutionPair;
86    use crate::models::formula::CNFClause;
87
88    vec![crate::example_db::specs::RuleExampleSpec {
89        id: "ksatisfiability_to_kernel",
90        build: || {
91            crate::example_db::specs::rule_example_with_witness::<_, Kernel>(
92                KSatisfiability::<K3>::new(
93                    3,
94                    vec![
95                        CNFClause::new(vec![1, 2, 3]),
96                        CNFClause::new(vec![-1, -2, 3]),
97                    ],
98                ),
99                SolutionPair {
100                    source_config: vec![1, 1, 1],
101                    target_config: vec![1, 0, 1, 0, 1, 0, 0, 0, 0, 0, 1, 0],
102                },
103            )
104        },
105    }]
106}
107#[cfg(test)]
108#[path = "../unit_tests/rules/ksatisfiability_kernel.rs"]
109mod tests;
problemreductions/rules/ksatisfiability_kernel.rs

problemreductions/rules/
ksatisfiability_kernel.rs
