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. Appearing variables are compacted
5//! with an inverse map; native clauses of length zero through three keep
6//! their original occurrence arcs, including the empty clause's kernel-free cycle.
7
8use crate::models::formula::KSatisfiability;
9use crate::models::graph::Kernel;
10use crate::reduction;
11use crate::rules::traits::{ReduceTo, ReductionResult};
12use crate::topology::DirectedGraph;
13use crate::variant::K3;
14use std::collections::BTreeSet;
15
16/// Result of reducing 3-SAT to Kernel.
17#[derive(Debug, Clone)]
18pub struct Reduction3SatToKernel {
19    target: Kernel,
20    source_num_vars: usize,
21    source_variables: Vec<usize>,
22}
23
24impl ReductionResult for Reduction3SatToKernel {
25    type Source = KSatisfiability<K3>;
26    type Target = Kernel;
27
28    fn target_problem(&self) -> &Self::Target {
29        &self.target
30    }
31
32    fn extract_solution(
33        &self,
34        target_solution: &<Self::Target as crate::traits::Problem>::Solution,
35    ) -> crate::rules::ExtractionResult<<Self::Source as crate::traits::Problem>::Solution> {
36        let value =
37            crate::rules::traits::validate_target_solution(self.target_problem(), target_solution)?;
38        if !value.0 {
39            return Err(crate::rules::ExtractionError::invalid(
40                "target vertex selection is not a kernel",
41            ));
42        }
43        let mut assignment = vec![false; self.source_num_vars];
44        for (compact, &original) in self.source_variables.iter().enumerate() {
45            assignment[original] = target_solution[2 * compact];
46        }
47        Ok(assignment)
48    }
49}
50
51#[reduction(
52    transform = upper_bound {
53        num_vertices = "2 * num_vars + 3 * num_clauses",
54        num_arcs = "2 * num_vars + 6 * num_clauses",
55    }
56)]
57impl ReduceTo<Kernel> for KSatisfiability<K3> {
58    type Result = Reduction3SatToKernel;
59
60    fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
61        let source_variables: Vec<_> = self
62            .clauses()
63            .iter()
64            .flat_map(|clause| clause.literals.iter())
65            .map(|literal| {
66                usize::try_from(literal.unsigned_abs()).expect("native SAT indices fit usize") - 1
67            })
68            .collect::<BTreeSet<_>>()
69            .into_iter()
70            .collect();
71        let num_vars = source_variables.len();
72        let num_clauses = self.num_clauses();
73        let overflow =
74            |operation| crate::rules::ReductionError::integer_overflow::<Self, Kernel>(operation);
75        let variable_vertices = num_vars
76            .checked_mul(2)
77            .ok_or_else(|| overflow("counting variable vertices"))?;
78        let clause_vertices = num_clauses
79            .checked_mul(3)
80            .ok_or_else(|| overflow("counting clause vertices"))?;
81        let num_vertices = variable_vertices
82            .checked_add(clause_vertices)
83            .ok_or_else(|| overflow("counting target vertices"))?;
84        let arc_capacity = num_clauses
85            .checked_mul(6)
86            .and_then(|clause_arcs| variable_vertices.checked_add(clause_arcs))
87            .ok_or_else(|| overflow("counting target arcs"))?;
88        let mut arcs = Vec::with_capacity(arc_capacity);
89
90        for variable in 0..num_vars {
91            let positive = 2 * variable;
92            let negative = positive + 1;
93            arcs.push((positive, negative));
94            arcs.push((negative, positive));
95        }
96
97        for (clause_index, clause) in self.clauses().iter().enumerate() {
98            let clause_base = 2 * num_vars + 3 * clause_index;
99            arcs.push((clause_base, clause_base + 1));
100            arcs.push((clause_base + 1, clause_base + 2));
101            arcs.push((clause_base + 2, clause_base));
102
103            for (literal_index, &literal) in clause.literals.iter().enumerate() {
104                let original = usize::try_from(literal.unsigned_abs())
105                    .expect("native SAT indices fit usize")
106                    - 1;
107                let compact = source_variables
108                    .binary_search(&original)
109                    .expect("all appearing variables were collected");
110                let literal_vertex = 2 * compact + usize::from(literal < 0);
111                arcs.push((clause_base + literal_index, literal_vertex));
112            }
113        }
114
115        Ok(Reduction3SatToKernel {
116            target: Kernel::new(DirectedGraph::new(num_vertices, arcs)),
117            source_num_vars: self.num_vars(),
118            source_variables,
119        })
120    }
121}
122
123#[cfg(feature = "example-db")]
124pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
125    use crate::export::SolutionPair;
126    use crate::models::formula::CNFClause;
127
128    vec![crate::example_db::specs::RuleExampleSpec {
129        id: "ksatisfiability_to_kernel",
130        build: || {
131            crate::example_db::specs::rule_example_with_witness::<_, Kernel>(
132                KSatisfiability::<K3>::new(
133                    3,
134                    vec![
135                        CNFClause::new(vec![1, 2, 3]),
136                        CNFClause::new(vec![-1, -2, 3]),
137                    ],
138                ),
139                SolutionPair {
140                    source_config: serde_json::json!(vec![true, true, true]),
141                    target_config: serde_json::json!(vec![
142                        true, false, true, false, true, false, false, false, false, false, true,
143                        false
144                    ]),
145                },
146            )
147        },
148    }]
149}
150#[cfg(test)]
151#[path = "../unit_tests/rules/ksatisfiability_kernel.rs"]
152mod tests;
problemreductions/rules/ksatisfiability_kernel.rs

problemreductions/rules/
ksatisfiability_kernel.rs
