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

problemreductions/rules/
sat_ksat.rs
