problemreductions/rules/
sat_ksat.rs

1//! Reductions between Satisfiability and K-Satisfiability problems.
2//!
3//! SAT -> K-SAT: Convert general CNF to K-literal clauses using:
4//! - Padding with ancilla variables for clauses with < K literals
5//! - Splitting with ancilla variables for clauses with > K literals
6//!
7//! K-SAT -> SAT: Trivial embedding (K-SAT is a special case of SAT)
8
9use crate::models::formula::{CNFClause, KSatisfiability, Satisfiability};
10use crate::reduction;
11use crate::rules::sat_helpers::SatVariableAllocator;
12use crate::rules::traits::{ReduceTo, ReductionResult};
13use crate::variant::{KValue, K2, K3, KN};
14
15/// Result of reducing general SAT to K-SAT.
16///
17/// This reduction transforms a SAT formula into an equisatisfiable K-SAT formula
18/// by introducing ancilla (auxiliary) variables.
19#[derive(Debug, Clone)]
20pub struct ReductionSATToKSAT<K: KValue> {
21    /// Number of original variables in the source problem.
22    source_num_vars: usize,
23    /// The target K-SAT problem.
24    target: KSatisfiability<K>,
25}
26
27impl<K: KValue> ReductionResult for ReductionSATToKSAT<K> {
28    type Source = Satisfiability;
29    type Target = KSatisfiability<K>;
30
31    fn target_problem(&self) -> &Self::Target {
32        &self.target
33    }
34
35    fn extract_solution(
36        &self,
37        target_solution: &<Self::Target as crate::traits::Problem>::Solution,
38    ) -> crate::rules::ExtractionResult<<Self::Source as crate::traits::Problem>::Solution> {
39        crate::rules::traits::validate_target_solution(self.target_problem(), target_solution)?;
40
41        Ok({
42            // Only return the original variables, discarding ancillas
43            target_solution[..self.source_num_vars].to_vec()
44        })
45    }
46}
47
48/// Add a clause to the K-SAT formula, splitting or padding as necessary.
49///
50/// # Algorithm
51/// - If clause has exactly K literals: add as-is
52/// - If clause has < K literals: pad with ancilla variables (both positive and negative)
53/// - If clause has > K literals: split recursively using ancilla variables
54///
55/// # Arguments
56/// * `k` - Target number of literals per clause
57/// * `clause` - The clause to add
58/// * `result_clauses` - Output vector to append clauses to
59fn add_clause_to_ksat(
60    k: usize,
61    clause: &CNFClause,
62    result_clauses: &mut Vec<CNFClause>,
63    variables: &mut SatVariableAllocator,
64) -> Result<(), crate::registry::ConstructionError> {
65    let len = clause.len();
66
67    if len == k {
68        // Exact size: add as-is
69        result_clauses.push(clause.clone());
70    } else if len < k {
71        // Too few literals: pad with ancilla variables
72        // Create both positive and negative versions to maintain satisfiability
73        // (a v b) with k=3 becomes (a v b v x) AND (a v b v -x)
74        let ancilla = variables.allocate()?;
75
76        // Add clause with positive ancilla
77        let mut lits_pos = clause.literals.clone();
78        lits_pos.push(ancilla);
79        add_clause_to_ksat(k, &CNFClause::new(lits_pos), result_clauses, variables)?;
80
81        // Add clause with negative ancilla
82        let mut lits_neg = clause.literals.clone();
83        lits_neg.push(-ancilla);
84        add_clause_to_ksat(k, &CNFClause::new(lits_neg), result_clauses, variables)?;
85    } else {
86        // Too many literals: split using ancilla variable
87        // (a v b v c v d) with k=3 becomes (a v b v x) AND (-x v c v d)
88        if k < 3 {
89            return Err(format!(
90                "cannot split a clause with {} literals into {k}-literal clauses",
91                clause.len()
92            )
93            .into());
94        }
95
96        let ancilla = variables.allocate()?;
97
98        // First clause: first k-1 literals + positive ancilla
99        let mut first_lits: Vec<i64> = clause.literals[..k - 1].to_vec();
100        first_lits.push(ancilla);
101        result_clauses.push(CNFClause::new(first_lits));
102
103        // Remaining clause: negative ancilla + remaining literals
104        let mut remaining_lits = vec![-ancilla];
105        remaining_lits.extend_from_slice(&clause.literals[k - 1..]);
106        let remaining_clause = CNFClause::new(remaining_lits);
107
108        // Recursively process the remaining clause
109        add_clause_to_ksat(k, &remaining_clause, result_clauses, variables)?;
110    }
111
112    Ok(())
113}
114
115/// Implementation of SAT -> K-SAT reduction.
116///
117/// Note: We implement this for specific K values rather than generic K
118/// because the `#[reduction]` proc macro requires concrete types.
119macro_rules! impl_sat_to_ksat {
120    ($ktype:ty, $k:expr) => {
121        #[rustfmt::skip]
122        #[reduction(
123    transform = upper_bound {
124        num_clauses = "4 * num_clauses + num_literals",
125        num_vars = "num_vars + 3 * num_clauses + num_literals",
126    },
127    unavailable = {
128        num_literals = "the exact target parameter is not represented by this reduction's symbolic transform",
129    }
130)]
131        impl ReduceTo<KSatisfiability<$ktype>> for Satisfiability {
132            type Result = ReductionSATToKSAT<$ktype>;
133
134            fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
135                let source_num_vars = self.num_vars();
136                let mut result_clauses = Vec::new();
137                let mut variables = SatVariableAllocator::new(
138                    "Satisfiability -> KSatisfiability",
139                    source_num_vars,
140                ).map_err(crate::rules::ReductionError::construction::<
141                    Satisfiability,
142                    KSatisfiability<$ktype>,
143                >)?;
144
145                for clause in self.clauses() {
146                    add_clause_to_ksat($k, clause, &mut result_clauses, &mut variables)
147                        .map_err(crate::rules::ReductionError::construction::<
148                            Satisfiability,
149                            KSatisfiability<$ktype>,
150                        >)?;
151                }
152
153                let target = KSatisfiability::<$ktype>::new(variables.num_vars(), result_clauses);
154
155                Ok(ReductionSATToKSAT {
156                    source_num_vars,
157                    target,
158                })
159            }
160        }
161    };
162}
163
164// Implement for K=3 (the canonical NP-complete case)
165impl_sat_to_ksat!(K3, 3);
166
167/// Result of reducing K-SAT to general SAT.
168///
169/// This is a trivial embedding since K-SAT is a special case of SAT.
170#[derive(Debug, Clone)]
171pub struct ReductionKSATToSAT<K: KValue> {
172    /// The target SAT problem.
173    target: Satisfiability,
174    _phantom: std::marker::PhantomData<K>,
175}
176
177impl<K: KValue> ReductionResult for ReductionKSATToSAT<K> {
178    type Source = KSatisfiability<K>;
179    type Target = Satisfiability;
180
181    fn target_problem(&self) -> &Self::Target {
182        &self.target
183    }
184
185    fn extract_solution(
186        &self,
187        target_solution: &<Self::Target as crate::traits::Problem>::Solution,
188    ) -> crate::rules::ExtractionResult<<Self::Source as crate::traits::Problem>::Solution> {
189        crate::rules::traits::validate_target_solution(self.target_problem(), target_solution)?;
190
191        Ok({
192            // Direct mapping - no transformation needed
193            target_solution.to_vec()
194        })
195    }
196}
197
198/// Helper function for KSAT -> SAT reduction logic (generic over K).
199fn reduce_ksat_to_sat<K: KValue>(ksat: &KSatisfiability<K>) -> ReductionKSATToSAT<K> {
200    let clauses = ksat.clauses().to_vec();
201    let target = Satisfiability::new(ksat.num_vars(), clauses);
202
203    ReductionKSATToSAT {
204        target,
205        _phantom: std::marker::PhantomData,
206    }
207}
208
209/// Macro for concrete KSAT -> SAT reduction impls.
210/// The `#[reduction]` macro requires concrete types.
211macro_rules! impl_ksat_to_sat {
212    ($ktype:ty) => {
213#[rustfmt::skip]
214        #[reduction(
215    transform = exact {
216        num_clauses = "num_clauses",
217        num_vars = "num_vars",
218        num_literals = "num_literals",
219    })]
220        impl ReduceTo<Satisfiability> for KSatisfiability<$ktype> {
221            type Result = ReductionKSATToSAT<$ktype>;
222
223            fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
224                Ok(reduce_ksat_to_sat(self))
225            }
226        }
227    };
228}
229
230// Register KN for the reduction graph (covers all K values as the generic entry)
231impl_ksat_to_sat!(KN);
232
233// K3 and K2 keep their ReduceTo<Satisfiability> impls for typed use,
234// but are NOT registered as separate primitive graph edges (KN covers them).
235impl ReduceTo<Satisfiability> for KSatisfiability<K3> {
236    type Result = ReductionKSATToSAT<K3>;
237    fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
238        Ok(reduce_ksat_to_sat(self))
239    }
240}
241
242impl ReduceTo<Satisfiability> for KSatisfiability<K2> {
243    type Result = ReductionKSATToSAT<K2>;
244    fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
245        Ok(reduce_ksat_to_sat(self))
246    }
247}
248
249#[cfg(feature = "example-db")]
250pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
251    use crate::export::SolutionPair;
252    use crate::models::formula::CNFClause;
253
254    vec![
255        crate::example_db::specs::RuleExampleSpec {
256            id: "satisfiability_to_ksatisfiability",
257            build: || {
258                let source = Satisfiability::new(
259                    5,
260                    vec![
261                        CNFClause::new(vec![1]),
262                        CNFClause::new(vec![2, -3]),
263                        CNFClause::new(vec![-1, 3, 4]),
264                        CNFClause::new(vec![2, -4, 5]),
265                        CNFClause::new(vec![1, -2, 3, -5]),
266                        CNFClause::new(vec![-1, 2, -3, 4, 5]),
267                    ],
268                );
269                crate::example_db::specs::rule_example_with_witness::<_, KSatisfiability<K3>>(
270                    source,
271                    SolutionPair {
272                        source_config: serde_json::json!(vec![true, true, true, false, true]),
273                        target_config: serde_json::json!(vec![
274                            true, true, true, false, true, false, false, false, false, true, true,
275                            true
276                        ]),
277                    },
278                )
279            },
280        },
281        crate::example_db::specs::RuleExampleSpec {
282            id: "ksatisfiability_to_satisfiability",
283            build: || {
284                let source = KSatisfiability::<KN>::new(
285                    4,
286                    vec![
287                        CNFClause::new(vec![1, -2, 3]),
288                        CNFClause::new(vec![-1, 3, 4]),
289                        CNFClause::new(vec![2, -3, -4]),
290                    ],
291                );
292                crate::example_db::specs::rule_example_with_witness::<_, Satisfiability>(
293                    source,
294                    SolutionPair {
295                        source_config: serde_json::json!(vec![true, true, true, false]),
296                        target_config: serde_json::json!(vec![true, true, true, false]),
297                    },
298                )
299            },
300        },
301    ]
302}
303
304#[cfg(test)]
305#[path = "../unit_tests/rules/sat_ksat.rs"]
306mod tests;
problemreductions/rules/sat_ksat.rs

problemreductions/rules/
sat_ksat.rs
