problemreductions/rules/
ksatisfiability_oneinthreesatisfiability.rs

1//! Reduction from KSatisfiability (3-SAT) to One-In-Three Satisfiability.
2//!
3//! Schaefer's Lemma 3.5 (STOC 1978) expresses a three-input disjunction
4//! using five one-in-three constraints. Missing native clause positions
5//! use the forced false variable; appearing source variables are compacted
6//! and restored through an inverse map during extraction.
7
8use crate::models::formula::{CNFClause, KSatisfiability, OneInThreeSatisfiability};
9use crate::reduction;
10use crate::rules::sat_helpers::SatVariableAllocator;
11use crate::rules::traits::{ReduceTo, ReductionResult};
12use crate::variant::K3;
13use std::collections::BTreeSet;
14
15#[derive(Debug, Clone)]
16pub struct Reduction3SATToOneInThreeSAT {
17    source_num_vars: usize,
18    source_variables: Vec<usize>,
19    target: OneInThreeSatisfiability,
20}
21
22impl ReductionResult for Reduction3SATToOneInThreeSAT {
23    type Source = KSatisfiability<K3>;
24    type Target = OneInThreeSatisfiability;
25
26    fn target_problem(&self) -> &Self::Target {
27        &self.target
28    }
29
30    fn extract_solution(
31        &self,
32        target_solution: &<Self::Target as crate::traits::Problem>::Solution,
33    ) -> crate::rules::ExtractionResult<<Self::Source as crate::traits::Problem>::Solution> {
34        let value =
35            crate::rules::traits::validate_target_solution(self.target_problem(), target_solution)?;
36        if !value.0 {
37            return Err(crate::rules::ExtractionError::invalid(
38                "target assignment does not satisfy every one-in-three clause",
39            ));
40        }
41        let mut assignment = vec![false; self.source_num_vars];
42        for (compact, &original) in self.source_variables.iter().enumerate() {
43            assignment[original] = target_solution[compact];
44        }
45        Ok(assignment)
46    }
47}
48
49#[reduction(
50    transform = upper_bound {
51        num_vars = "num_vars + 2 + 6 * num_clauses",
52        num_clauses = "1 + 5 * num_clauses",
53    })]
54impl ReduceTo<OneInThreeSatisfiability> for KSatisfiability<K3> {
55    type Result = Reduction3SATToOneInThreeSAT;
56
57    fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
58        let source_num_vars = self.num_vars();
59        let source_variables: Vec<_> = self
60            .clauses()
61            .iter()
62            .flat_map(|clause| clause.literals.iter())
63            .map(|literal| {
64                usize::try_from(literal.unsigned_abs()).expect("native SAT indices fit usize") - 1
65            })
66            .collect::<BTreeSet<_>>()
67            .into_iter()
68            .collect();
69        let mut variables = SatVariableAllocator::new(
70            "KSatisfiability -> OneInThreeSatisfiability",
71            source_variables.len(),
72        )
73        .map_err(
74            crate::rules::ReductionError::construction::<
75                KSatisfiability<K3>,
76                OneInThreeSatisfiability,
77            >,
78        )?;
79        let sentinels = variables.allocate_many(2).map_err(
80            crate::rules::ReductionError::construction::<
81                KSatisfiability<K3>,
82                OneInThreeSatisfiability,
83            >,
84        )?;
85        let z_false = sentinels[0];
86        let z_true = sentinels[1];
87
88        let capacity = self
89            .num_clauses()
90            .checked_mul(5)
91            .and_then(|count| count.checked_add(1))
92            .ok_or_else(|| {
93                crate::rules::ReductionError::integer_overflow::<
94                    KSatisfiability<K3>,
95                    OneInThreeSatisfiability,
96                >("computing the target clause count")
97            })?;
98        let mut clauses = Vec::with_capacity(capacity);
99        clauses.push(CNFClause::new(vec![z_false, z_false, z_true]));
100
101        for clause in self.clauses() {
102            // Adding false disjuncts preserves every native clause, including
103            // the empty disjunction, while using the same three-input gadget.
104            let mut literals = [z_false; 3];
105            for (position, &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 variable = i64::try_from(compact + 1).expect("compact SAT indices fit i64");
113                literals[position] = if literal > 0 { variable } else { -variable };
114            }
115            let [l1, l2, l3] = literals;
116            let allocated = variables.allocate_many(6).map_err(
117                crate::rules::ReductionError::construction::<
118                    KSatisfiability<K3>,
119                    OneInThreeSatisfiability,
120                >,
121            )?;
122            let [a, b, c, d, e, f] = allocated.as_slice() else {
123                return Err(crate::rules::ReductionError::invalid_target::<
124                    KSatisfiability<K3>,
125                    OneInThreeSatisfiability,
126                >(
127                    "SAT allocator returned an unexpected variable count"
128                ));
129            };
130
131            clauses.push(CNFClause::new(vec![l1, *a, *d]));
132            clauses.push(CNFClause::new(vec![l2, *b, *d]));
133            clauses.push(CNFClause::new(vec![*a, *b, *e]));
134            clauses.push(CNFClause::new(vec![*c, *d, *f]));
135            clauses.push(CNFClause::new(vec![l3, *c, z_false]));
136        }
137
138        let target = OneInThreeSatisfiability::try_new(variables.num_vars(), clauses).map_err(
139            crate::rules::ReductionError::construction::<Self, OneInThreeSatisfiability>,
140        )?;
141
142        Ok(Reduction3SATToOneInThreeSAT {
143            source_num_vars,
144            source_variables,
145            target,
146        })
147    }
148}
149
150#[cfg(feature = "example-db")]
151pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
152    use crate::export::SolutionPair;
153
154    vec![crate::example_db::specs::RuleExampleSpec {
155        id: "ksatisfiability_to_oneinthreesatisfiability",
156        build: || {
157            let source = KSatisfiability::<K3>::new(3, vec![CNFClause::new(vec![1, 2, 3])]);
158            crate::example_db::specs::rule_example_with_witness::<_, OneInThreeSatisfiability>(
159                source,
160                SolutionPair {
161                    source_config: serde_json::json!(vec![false, false, true]),
162                    target_config: serde_json::json!(vec![
163                        false, false, true, false, true, false, false, false, true, true, false
164                    ]),
165                },
166            )
167        },
168    }]
169}
170
171#[cfg(test)]
172#[path = "../unit_tests/rules/ksatisfiability_oneinthreesatisfiability.rs"]
173mod tests;
problemreductions/rules/ksatisfiability_oneinthreesatisfiability.rs

problemreductions/rules/
ksatisfiability_oneinthreesatisfiability.rs
