problemreductions/rules/
ksatisfiability_simultaneousincongruences.rs

1//! Reduction from 3-SAT to Simultaneous Incongruences.
2//!
3//! Uses distinct odd primes to encode variable assignments via residues
4//! 1 (true) and 2 (false), then forbids each clause's unique falsifying
5//! residue class via the Chinese Remainder Theorem.
6
7use std::collections::BTreeMap;
8
9use crate::models::algebraic::SimultaneousIncongruences;
10use crate::models::formula::{ksat::first_n_odd_primes, CNFClause, KSatisfiability};
11use crate::reduction;
12use crate::rules::traits::{ReduceTo, ReductionResult};
13use crate::variant::K3;
14
15#[derive(Debug, Clone)]
16pub struct Reduction3SATToSimultaneousIncongruences {
17    target: SimultaneousIncongruences,
18    variable_primes: Vec<u64>,
19}
20
21impl ReductionResult for Reduction3SATToSimultaneousIncongruences {
22    type Source = KSatisfiability<K3>;
23    type Target = SimultaneousIncongruences;
24
25    fn target_problem(&self) -> &Self::Target {
26        &self.target
27    }
28
29    fn extract_solution(
30        &self,
31        target_solution: &<Self::Target as crate::traits::Problem>::Solution,
32    ) -> crate::rules::ExtractionResult<<Self::Source as crate::traits::Problem>::Solution> {
33        crate::rules::traits::validate_target_solution(self.target_problem(), target_solution)?;
34
35        Ok({
36            let x = u64::try_from(*target_solution).map_err(|_| {
37                crate::rules::ExtractionError::invalid(
38                    "target value cannot be represented in the CRT implementation domain",
39                )
40            })?;
41            self.variable_primes
42                .iter()
43                .map(|&prime| x % prime == 1)
44                .collect()
45        })
46    }
47}
48
49fn falsifying_residue(literal: i64) -> u64 {
50    if literal > 0 {
51        2
52    } else {
53        1
54    }
55}
56
57fn modular_inverse(value: u64, modulus: u64) -> Option<u64> {
58    let mut t = 0i128;
59    let mut new_t = 1i128;
60    let mut r = modulus as i128;
61    let mut new_r = value as i128;
62
63    while new_r != 0 {
64        let quotient = r / new_r;
65        (t, new_t) = (new_t, t - quotient * new_t);
66        (r, new_r) = (new_r, r - quotient * new_r);
67    }
68
69    if r != 1 {
70        return None;
71    }
72    if t < 0 {
73        t += modulus as i128;
74    }
75    Some(t as u64)
76}
77
78fn crt_residue(congruences: &[(u64, u64)]) -> Result<(u64, u64), &'static str> {
79    let modulus = congruences
80        .iter()
81        .try_fold(1u64, |product, &(m, _)| product.checked_mul(m))
82        .ok_or("CRT modulus product overflow")?;
83
84    let residue = congruences
85        .iter()
86        .try_fold(0u128, |acc, &(modulus_i, residue_i)| {
87            let partial = modulus / modulus_i;
88            let inverse = modular_inverse(partial % modulus_i, modulus_i)
89                .ok_or("CRT moduli must be pairwise coprime")?;
90            let term = u128::from(residue_i)
91                .checked_mul(u128::from(partial))
92                .and_then(|value| value.checked_mul(u128::from(inverse)))
93                .ok_or("CRT residue term overflow")?;
94            acc.checked_add(term).ok_or("CRT residue sum overflow")
95        })?
96        % modulus as u128;
97
98    Ok((residue as u64, modulus))
99}
100
101fn clause_bad_residue(
102    clause: &CNFClause,
103    variable_primes: &[u64],
104) -> Result<(u64, u64), &'static str> {
105    let mut residue_by_var = BTreeMap::new();
106    let mut contradictory_var = None;
107
108    for &literal in &clause.literals {
109        let var_index =
110            usize::try_from(literal.unsigned_abs()).map_err(|_| "literal index exceeds usize")? - 1;
111        let residue = falsifying_residue(literal);
112
113        match residue_by_var.insert(var_index, residue) {
114            Some(existing) if existing != residue => {
115                contradictory_var = Some(var_index);
116                residue_by_var.insert(var_index, 0);
117                break;
118            }
119            Some(existing) => {
120                residue_by_var.insert(var_index, existing);
121            }
122            None => {}
123        }
124    }
125
126    if let Some(var_index) = contradictory_var {
127        for &literal in &clause.literals {
128            let candidate = usize::try_from(literal.unsigned_abs())
129                .map_err(|_| "literal index exceeds usize")?
130                - 1;
131            if candidate != var_index {
132                residue_by_var
133                    .entry(candidate)
134                    .or_insert_with(|| falsifying_residue(literal));
135            }
136        }
137    }
138
139    let congruences = residue_by_var
140        .into_iter()
141        .map(|(var_index, residue)| {
142            variable_primes
143                .get(var_index)
144                .copied()
145                .map(|prime| (prime, residue))
146                .ok_or("clause variable index exceeds num_vars")
147        })
148        .collect::<Result<Vec<_>, _>>()?;
149
150    crt_residue(&congruences)
151}
152
153fn ensure_prime_product_fits_target(
154    variable_primes: &[u64],
155) -> Result<(), crate::registry::ConstructionError> {
156    let mut product = 1u128;
157    for &prime in variable_primes {
158        product = product.checked_mul(prime as u128).ok_or_else(|| {
159            format!(
160                "variable-prime product overflows for {} variables",
161                variable_primes.len()
162            )
163        })?;
164        if product > i64::MAX as u128 {
165            return Err(format!(
166                "variable-prime product {product} for {} variables exceeds the target i64 domain",
167                variable_primes.len()
168            )
169            .into());
170        }
171    }
172    Ok(())
173}
174
175#[reduction(
176    transform = unavailable {
177        num_pairs = "the number of residue pairs depends on the first num_vars odd primes and is not expressible in the size-expression language",
178    }
179)]
180impl ReduceTo<SimultaneousIncongruences> for KSatisfiability<K3> {
181    type Result = Reduction3SATToSimultaneousIncongruences;
182
183    fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
184        let variable_primes = first_n_odd_primes(self.num_vars());
185        ensure_prime_product_fits_target(&variable_primes).map_err(|message| {
186            crate::rules::ReductionError::invalid_target::<
187                KSatisfiability<K3>,
188                SimultaneousIncongruences,
189            >(message.to_string())
190        })?;
191
192        let mut pairs = Vec::new();
193
194        for &prime in &variable_primes {
195            // Use (prime, prime) to forbid x ≡ 0 (mod prime), since the
196            // model requires a ≥ 1. Note: prime % prime = 0, so this is
197            // equivalent to forbidding residue 0.
198            pairs.push((prime, prime));
199            for residue in 3..prime {
200                pairs.push((residue, prime));
201            }
202        }
203
204        for clause in self.clauses() {
205            let (bad_residue, clause_modulus) = clause_bad_residue(clause, &variable_primes)
206                .map_err(|message| {
207                    crate::rules::ReductionError::invalid_target::<
208                        KSatisfiability<K3>,
209                        SimultaneousIncongruences,
210                    >(message)
211                })?;
212            // The model requires a >= 1. Use modulus instead of 0 since
213            // modulus % modulus = 0, achieving the same incongruence.
214            let a = if bad_residue == 0 {
215                clause_modulus
216            } else {
217                bad_residue
218            };
219            pairs.push((a, clause_modulus));
220        }
221
222        let pairs = pairs
223            .into_iter()
224            .map(|(residue, modulus)| {
225                Ok((
226                    i64::try_from(residue).map_err(|_| "residue exceeds i64")?,
227                    i64::try_from(modulus).map_err(|_| "modulus exceeds i64")?,
228                ))
229            })
230            .collect::<Result<Vec<_>, &str>>()
231            .map_err(|message| {
232                crate::rules::ReductionError::invalid_target::<
233                    KSatisfiability<K3>,
234                    SimultaneousIncongruences,
235                >(message)
236            })?;
237        let target = SimultaneousIncongruences::new(pairs).map_err(|message| {
238            crate::rules::ReductionError::construction::<
239                KSatisfiability<K3>,
240                SimultaneousIncongruences,
241            >(message)
242        })?;
243        Ok(Reduction3SATToSimultaneousIncongruences {
244            target,
245            variable_primes,
246        })
247    }
248}
249
250#[cfg(feature = "example-db")]
251pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
252    use crate::export::SolutionPair;
253
254    vec![crate::example_db::specs::RuleExampleSpec {
255        id: "ksatisfiability_to_simultaneous_incongruences",
256        build: || {
257            let source = KSatisfiability::<K3>::new(
258                2,
259                vec![
260                    CNFClause::new(vec![1, 2, 2]),
261                    CNFClause::new(vec![-1, 2, 2]),
262                ],
263            );
264            crate::example_db::specs::rule_example_with_witness::<_, SimultaneousIncongruences>(
265                source,
266                SolutionPair {
267                    source_config: serde_json::json!(vec![true, true]),
268                    target_config: serde_json::json!(1),
269                },
270            )
271        },
272    }]
273}
274
275#[cfg(test)]
276#[path = "../unit_tests/rules/ksatisfiability_simultaneousincongruences.rs"]
277mod tests;
problemreductions/rules/ksatisfiability_simultaneousincongruences.rs

problemreductions/rules/
ksatisfiability_simultaneousincongruences.rs
