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        crate::rules::traits::validate_target_witness(
37            self.target_problem(),
38            target_solution,
39            |value| value.0,
40            "target vertex selection is not a kernel",
41        )?;
42        let mut assignment = vec![false; self.source_num_vars];
43        for (compact, &original) in self.source_variables.iter().enumerate() {
44            assignment[original] = target_solution[2 * compact];
45        }
46        Ok(assignment)
47    }
48}
49
50#[crate::aggregate_reduction(identity)]
51impl crate::rules::AggregateReductionResult for Reduction3SatToKernel {}
52
53#[reduction(
54    transform = upper_bound {
55        num_vertices = "2 * num_vars + 3 * num_clauses",
56        num_arcs = "2 * num_vars + 6 * num_clauses",
57    }
58)]
59impl ReduceTo<Kernel> for KSatisfiability<K3> {
60    type Result = Reduction3SatToKernel;
61
62    fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
63        let source_variables: Vec<_> = self
64            .clauses()
65            .iter()
66            .flat_map(|clause| clause.literals.iter())
67            .map(|literal| {
68                usize::try_from(literal.unsigned_abs()).expect("native SAT indices fit usize") - 1
69            })
70            .collect::<BTreeSet<_>>()
71            .into_iter()
72            .collect();
73        let num_vars = source_variables.len();
74        let num_clauses = self.num_clauses();
75        let overflow =
76            |operation| crate::rules::ReductionError::integer_overflow::<Self, Kernel>(operation);
77        let variable_vertices = num_vars
78            .checked_mul(2)
79            .ok_or_else(|| overflow("counting variable vertices"))?;
80        let clause_vertices = num_clauses
81            .checked_mul(3)
82            .ok_or_else(|| overflow("counting clause vertices"))?;
83        let num_vertices = variable_vertices
84            .checked_add(clause_vertices)
85            .ok_or_else(|| overflow("counting target vertices"))?;
86        let arc_capacity = num_clauses
87            .checked_mul(6)
88            .and_then(|clause_arcs| variable_vertices.checked_add(clause_arcs))
89            .ok_or_else(|| overflow("counting target arcs"))?;
90        let mut arcs = Vec::with_capacity(arc_capacity);
91
92        for variable in 0..num_vars {
93            let positive = 2 * variable;
94            let negative = positive + 1;
95            arcs.push((positive, negative));
96            arcs.push((negative, positive));
97        }
98
99        for (clause_index, clause) in self.clauses().iter().enumerate() {
100            let clause_base = 2 * num_vars + 3 * clause_index;
101            arcs.push((clause_base, clause_base + 1));
102            arcs.push((clause_base + 1, clause_base + 2));
103            arcs.push((clause_base + 2, clause_base));
104
105            for (literal_index, &literal) in clause.literals.iter().enumerate() {
106                let original = usize::try_from(literal.unsigned_abs())
107                    .expect("native SAT indices fit usize")
108                    - 1;
109                let compact = source_variables
110                    .binary_search(&original)
111                    .expect("all appearing variables were collected");
112                let literal_vertex = 2 * compact + usize::from(literal < 0);
113                arcs.push((clause_base + literal_index, literal_vertex));
114            }
115        }
116
117        Ok(Reduction3SatToKernel {
118            target: Kernel::new(DirectedGraph::new(num_vertices, arcs)),
119            source_num_vars: self.num_vars(),
120            source_variables,
121        })
122    }
123}
124
125#[cfg(feature = "example-db")]
126pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
127    use crate::export::SolutionPair;
128    use crate::models::formula::CNFClause;
129
130    vec![crate::example_db::specs::RuleExampleSpec {
131        id: "ksatisfiability_to_kernel",
132        build: || {
133            crate::example_db::specs::rule_example_with_witness::<_, Kernel>(
134                KSatisfiability::<K3>::new(
135                    3,
136                    vec![
137                        CNFClause::new(vec![1, 2, 3]),
138                        CNFClause::new(vec![-1, -2, 3]),
139                    ],
140                ),
141                SolutionPair {
142                    source_config: serde_json::json!(vec![true, true, true]),
143                    target_config: serde_json::json!(vec![
144                        true, false, true, false, true, false, false, false, false, false, true,
145                        false
146                    ]),
147                },
148            )
149        },
150    }]
151}
152#[cfg(test)]
153#[path = "../unit_tests/rules/ksatisfiability_kernel.rs"]
154mod tests;
problemreductions/rules/ksatisfiability_kernel.rs

problemreductions/rules/
ksatisfiability_kernel.rs
