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        crate::rules::traits::validate_target_witness(
35            self.target_problem(),
36            target_solution,
37            |value| value.0,
38            "target assignment does not satisfy every one-in-three clause",
39        )?;
40        let mut assignment = vec![false; self.source_num_vars];
41        for (compact, &original) in self.source_variables.iter().enumerate() {
42            assignment[original] = target_solution[compact];
43        }
44        Ok(assignment)
45    }
46}
47
48#[crate::aggregate_reduction(identity)]
49impl crate::rules::AggregateReductionResult for Reduction3SATToOneInThreeSAT {}
50
51#[reduction(
52    transform = upper_bound {
53        num_vars = "num_vars + 2 + 6 * num_clauses",
54        num_clauses = "1 + 5 * num_clauses",
55    })]
56impl ReduceTo<OneInThreeSatisfiability> for KSatisfiability<K3> {
57    type Result = Reduction3SATToOneInThreeSAT;
58
59    fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
60        let source_num_vars = self.num_vars();
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 mut variables = SatVariableAllocator::new(
72            "KSatisfiability -> OneInThreeSatisfiability",
73            source_variables.len(),
74        )
75        .map_err(
76            crate::rules::ReductionError::construction::<
77                KSatisfiability<K3>,
78                OneInThreeSatisfiability,
79            >,
80        )?;
81        let sentinels = variables.allocate_many(2).map_err(
82            crate::rules::ReductionError::construction::<
83                KSatisfiability<K3>,
84                OneInThreeSatisfiability,
85            >,
86        )?;
87        let z_false = sentinels[0];
88        let z_true = sentinels[1];
89
90        let capacity = self
91            .num_clauses()
92            .checked_mul(5)
93            .and_then(|count| count.checked_add(1))
94            .ok_or_else(|| {
95                crate::rules::ReductionError::integer_overflow::<
96                    KSatisfiability<K3>,
97                    OneInThreeSatisfiability,
98                >("computing the target clause count")
99            })?;
100        let mut clauses = Vec::with_capacity(capacity);
101        clauses.push(CNFClause::new(vec![z_false, z_false, z_true]));
102
103        for clause in self.clauses() {
104            // Adding false disjuncts preserves every native clause, including
105            // the empty disjunction, while using the same three-input gadget.
106            let mut literals = [z_false; 3];
107            for (position, &literal) in clause.literals.iter().enumerate() {
108                let original = usize::try_from(literal.unsigned_abs())
109                    .expect("native SAT indices fit usize")
110                    - 1;
111                let compact = source_variables
112                    .binary_search(&original)
113                    .expect("all appearing variables were collected");
114                let variable = i64::try_from(compact + 1).expect("compact SAT indices fit i64");
115                literals[position] = if literal > 0 { variable } else { -variable };
116            }
117            let [l1, l2, l3] = literals;
118            let allocated = variables.allocate_many(6).map_err(
119                crate::rules::ReductionError::construction::<
120                    KSatisfiability<K3>,
121                    OneInThreeSatisfiability,
122                >,
123            )?;
124            let [a, b, c, d, e, f] = allocated.as_slice() else {
125                return Err(crate::rules::ReductionError::invalid_target::<
126                    KSatisfiability<K3>,
127                    OneInThreeSatisfiability,
128                >(
129                    "SAT allocator returned an unexpected variable count"
130                ));
131            };
132
133            clauses.push(CNFClause::new(vec![l1, *a, *d]));
134            clauses.push(CNFClause::new(vec![l2, *b, *d]));
135            clauses.push(CNFClause::new(vec![*a, *b, *e]));
136            clauses.push(CNFClause::new(vec![*c, *d, *f]));
137            clauses.push(CNFClause::new(vec![l3, *c, z_false]));
138        }
139
140        let target = OneInThreeSatisfiability::try_new(variables.num_vars(), clauses).map_err(
141            crate::rules::ReductionError::construction::<Self, OneInThreeSatisfiability>,
142        )?;
143
144        Ok(Reduction3SATToOneInThreeSAT {
145            source_num_vars,
146            source_variables,
147            target,
148        })
149    }
150}
151
152#[cfg(feature = "example-db")]
153pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
154    use crate::export::SolutionPair;
155
156    vec![crate::example_db::specs::RuleExampleSpec {
157        id: "ksatisfiability_to_oneinthreesatisfiability",
158        build: || {
159            let source = KSatisfiability::<K3>::new(3, vec![CNFClause::new(vec![1, 2, 3])]);
160            crate::example_db::specs::rule_example_with_witness::<_, OneInThreeSatisfiability>(
161                source,
162                SolutionPair {
163                    source_config: serde_json::json!(vec![false, false, true]),
164                    target_config: serde_json::json!(vec![
165                        false, false, true, false, true, false, false, false, true, true, false
166                    ]),
167                },
168            )
169        },
170    }]
171}
172
173#[cfg(test)]
174#[path = "../unit_tests/rules/ksatisfiability_oneinthreesatisfiability.rs"]
175mod tests;
problemreductions/rules/ksatisfiability_oneinthreesatisfiability.rs

problemreductions/rules/
ksatisfiability_oneinthreesatisfiability.rs
