problemreductions/rules/
ksatisfiability_quadraticcongruences.rs

1//! Reduction from 3-SAT to bounded quadratic congruences.
2//!
3//! Manders and Adleman (ERL-M615, 1976), Section 2: an odd signed-knapsack
4//! target and prime-power CRT encode the clauses. Only the actual normalized
5//! clauses need base-eight positions; widths zero through three use the same
6//! slack equation. Squaring uses twice the linear modulus, and extraction
7//! orients every sign by the distinguished odd coordinate.
8
9use std::collections::{BTreeMap, BTreeSet};
10
11use crate::models::algebraic::QuadraticCongruences;
12use crate::models::formula::KSatisfiability;
13use crate::reduction;
14use crate::rules::traits::{ReduceTo, ReductionResult};
15use crate::variant::K3;
16use num_bigint::{BigInt, BigUint};
17#[cfg(any(test, feature = "example-db"))]
18use num_traits::Signed;
19use num_traits::{One, Zero};
20
21#[derive(Debug, Clone)]
22pub struct Reduction3SATToQuadraticCongruences {
23    target: QuadraticCongruences,
24    source_num_vars: usize,
25    active_to_source: Vec<usize>,
26    clause_count: usize,
27    h: BigUint,
28    prime_powers: Vec<BigUint>,
29}
30
31impl ReductionResult for Reduction3SATToQuadraticCongruences {
32    type Source = KSatisfiability<K3>;
33    type Target = QuadraticCongruences;
34
35    fn target_problem(&self) -> &Self::Target {
36        &self.target
37    }
38
39    fn extract_solution(
40        &self,
41        target_solution: &<Self::Target as crate::traits::Problem>::Solution,
42    ) -> crate::rules::ExtractionResult<<Self::Source as crate::traits::Problem>::Solution> {
43        let value =
44            crate::rules::traits::validate_target_solution(self.target_problem(), target_solution)?;
45        if !value.0 {
46            return Err(crate::rules::ExtractionError::invalid(
47                "target integer does not satisfy the bounded quadratic congruence",
48            ));
49        }
50        // Validation gives 0 < x <= H. Each prime power divides exactly one
51        // of H-x and H+x. The coordinate zero sign chooses x or -x so that
52        // the odd linear target, rather than its negative, is recovered.
53        let h_minus_x = &self.h - target_solution;
54        let positive_orientation = (&h_minus_x % &self.prime_powers[0]).is_zero();
55        let mut assignment = vec![false; self.source_num_vars];
56        for (active, &original) in self.active_to_source.iter().enumerate() {
57            let coordinate = 2 * self.clause_count + active + 1;
58            let positive = (&h_minus_x % &self.prime_powers[coordinate]).is_zero();
59            assignment[original] = positive != positive_orientation;
60        }
61        Ok(assignment)
62    }
63}
64
65#[cfg_attr(not(any(test, feature = "example-db")), allow(dead_code))]
66#[derive(Debug, Clone)]
67struct MandersAdlemanConstruction {
68    target: QuadraticCongruences,
69    source_num_vars: usize,
70    active_to_source: Vec<usize>,
71    clauses: Vec<Vec<i64>>,
72    #[cfg_attr(not(test), allow(dead_code))]
73    coefficients: Vec<BigInt>,
74    #[cfg_attr(not(test), allow(dead_code))]
75    tau: BigInt,
76    thetas: Vec<BigUint>,
77    h: BigUint,
78    prime_powers: Vec<BigUint>,
79}
80
81fn is_prime(candidate: u64) -> bool {
82    if candidate < 2 {
83        return false;
84    }
85    if candidate == 2 {
86        return true;
87    }
88    if candidate.is_multiple_of(2) {
89        return false;
90    }
91    let mut divisor = 3u64;
92    while divisor <= candidate / divisor {
93        if candidate.is_multiple_of(divisor) {
94            return false;
95        }
96        divisor += 2;
97    }
98    true
99}
100
101fn admissible_primes(count: usize) -> Result<Vec<u64>, crate::rules::ReductionError> {
102    let mut primes = Vec::with_capacity(count);
103    let mut candidate = 13u64;
104    while primes.len() < count {
105        if is_prime(candidate) {
106            primes.push(candidate);
107        }
108        candidate = candidate.checked_add(1).ok_or_else(|| {
109            crate::rules::ReductionError::integer_overflow::<
110                KSatisfiability<K3>,
111                QuadraticCongruences,
112            >("enumerating CRT primes")
113        })?;
114    }
115    Ok(primes)
116}
117
118fn bigint_mod_to_biguint(value: &BigInt, modulus: &BigUint) -> BigUint {
119    let modulus_bigint = BigInt::from(modulus.clone());
120    let reduced = ((value % &modulus_bigint) + &modulus_bigint) % &modulus_bigint;
121    reduced
122        .to_biguint()
123        .expect("Euclidean residue is nonnegative")
124}
125
126fn normalize_clause(clause: &[i64]) -> Option<Vec<i64>> {
127    let mut literals = BTreeSet::new();
128    for &literal in clause {
129        if literals.contains(&-literal) {
130            return None;
131        }
132        literals.insert(literal);
133    }
134    Some(literals.into_iter().collect())
135}
136
137fn build_construction(
138    source: &KSatisfiability<K3>,
139) -> Result<MandersAdlemanConstruction, crate::rules::ReductionError> {
140    let clauses: BTreeSet<_> = source
141        .clauses()
142        .iter()
143        .filter_map(|clause| normalize_clause(&clause.literals))
144        .collect();
145    let active_vars: Vec<_> = clauses
146        .iter()
147        .flatten()
148        .map(|literal| {
149            usize::try_from(literal.unsigned_abs()).expect("native SAT indices fit usize")
150        })
151        .collect::<BTreeSet<_>>()
152        .into_iter()
153        .collect();
154    let var_map: BTreeMap<_, _> = active_vars
155        .iter()
156        .enumerate()
157        .map(|(compact, &original)| (original, compact + 1))
158        .collect();
159    let clauses: Vec<Vec<i64>> = clauses
160        .into_iter()
161        .map(|clause| {
162            clause
163                .into_iter()
164                .map(|literal| {
165                    let original = usize::try_from(literal.unsigned_abs())
166                        .expect("native SAT indices fit usize");
167                    let variable =
168                        i64::try_from(var_map[&original]).expect("compact SAT indices fit i64");
169                    if literal > 0 {
170                        variable
171                    } else {
172                        -variable
173                    }
174                })
175                .collect()
176        })
177        .collect();
178    let m = clauses.len();
179    let coordinate_count = m
180        .checked_mul(2)
181        .and_then(|aux| aux.checked_add(active_vars.len()))
182        .and_then(|count| count.checked_add(1))
183        .ok_or_else(|| {
184            crate::rules::ReductionError::integer_overflow::<
185                KSatisfiability<K3>,
186                QuadraticCongruences,
187            >("counting signed-knapsack coordinates")
188        })?;
189    let mut coefficients = vec![BigInt::zero(); coordinate_count];
190    coefficients[0] = BigInt::one();
191    let mut tau = BigInt::one();
192    let mut weight = BigUint::one();
193    for (j, clause) in clauses.iter().enumerate() {
194        weight *= 8u32;
195        let half_weight = BigInt::from(&weight / 2u32);
196        coefficients[2 * j + 1] = -&half_weight;
197        coefficients[2 * j + 2] = -BigInt::from(weight.clone());
198        let width =
199            i64::try_from(clause.len()).expect("native K3 clauses have at most three literals");
200        tau += (width - 5) * &half_weight;
201        for &literal in clause {
202            let variable =
203                usize::try_from(literal.unsigned_abs()).expect("compact SAT indices fit usize");
204            if literal > 0 {
205                coefficients[2 * m + variable] += &half_weight;
206            } else {
207                coefficients[2 * m + variable] -= &half_weight;
208            }
209        }
210    }
211    // c.alpha - tau = alpha_0 - 1 + sum_j (y_j - true_literals_j + 1) 8^j.
212    // tau is odd; coefficient doubling would invalidate the square-root lemma.
213    let linear_modulus = weight * 8u32;
214    let primes = admissible_primes(coordinate_count)?;
215    let prime_powers: Vec<_> = primes
216        .iter()
217        .map(|&prime| num_traits::Pow::pow(BigUint::from(prime), coordinate_count))
218        .collect();
219    let k: BigUint = prime_powers.iter().product();
220    let mut thetas = Vec::with_capacity(coordinate_count);
221    for ((coefficient, prime_power), prime) in coefficients.iter().zip(&prime_powers).zip(&primes) {
222        let other = &k / prime_power;
223        let step = &other * &linear_modulus;
224        let residue = bigint_mod_to_biguint(coefficient, &linear_modulus);
225        let inverse = other
226            .modinv(&linear_modulus)
227            .expect("an odd prime-power product is coprime to a power of two");
228        let mut theta = &other * ((residue * inverse) % &linear_modulus);
229        if theta.is_zero() {
230            theta += &step;
231        }
232        if (&theta % BigUint::from(*prime)).is_zero() {
233            theta += &step;
234        }
235        thetas.push(theta);
236    }
237    let h: BigUint = thetas.iter().sum();
238    // With N=2m+l+1, 13^N > 4N*8^(m+1) for m>=1, hence 2H<K.
239    // For the empty formula N=1, theta_0=1 and K=13 give the same strict bound.
240    let square_modulus = &linear_modulus * 2u32;
241    let b = &square_modulus * &k;
242    let inverse = (&square_modulus + &k)
243        .modinv(&b)
244        .expect("the two CRT moduli are coprime");
245    let tau_squared = (&tau * &tau).to_biguint().expect("a square is nonnegative");
246    let a = (inverse * (&k * tau_squared + &square_modulus * &h * &h)) % &b;
247    let target = QuadraticCongruences::try_new(a, b, &h + BigUint::one()).map_err(
248        crate::rules::ReductionError::construction::<KSatisfiability<K3>, QuadraticCongruences>,
249    )?;
250    Ok(MandersAdlemanConstruction {
251        target,
252        source_num_vars: source.num_vars(),
253        active_to_source: active_vars
254            .into_iter()
255            .map(|variable| variable - 1)
256            .collect(),
257        clauses,
258        coefficients,
259        tau,
260        thetas,
261        h,
262        prime_powers,
263    })
264}
265
266#[cfg(any(test, feature = "example-db"))]
267fn build_alphas(construction: &MandersAdlemanConstruction, assignment: &[bool]) -> Option<Vec<i8>> {
268    if assignment.len() != construction.source_num_vars {
269        return None;
270    }
271    let m = construction.clauses.len();
272    let mut alphas = vec![1; construction.thetas.len()];
273    for (i, &original) in construction.active_to_source.iter().enumerate() {
274        alphas[2 * m + i + 1] = 1 - 2 * i8::from(assignment[original]);
275    }
276    for (j, clause) in construction.clauses.iter().enumerate() {
277        let mut y = -1i8;
278        for &literal in clause {
279            let variable =
280                usize::try_from(literal.unsigned_abs()).expect("compact SAT indices fit usize") - 1;
281            let truth = assignment[construction.active_to_source[variable]];
282            y += i8::from(truth == (literal > 0));
283        }
284        let (first, second) = match y {
285            0 => (1, 1),
286            1 => (-1, 1),
287            2 => (1, -1),
288            _ => return None,
289        };
290        alphas[2 * j + 1] = first;
291        alphas[2 * j + 2] = second;
292    }
293    Some(alphas)
294}
295
296#[cfg(any(test, feature = "example-db"))]
297fn witness_value_from_alphas(alphas: &[i8], thetas: &[BigUint]) -> BigUint {
298    alphas
299        .iter()
300        .zip(thetas)
301        .map(|(&alpha, theta)| BigInt::from(alpha) * BigInt::from(theta.clone()))
302        .sum::<BigInt>()
303        .abs()
304        .to_biguint()
305        .expect("absolute witness is nonnegative")
306}
307
308#[cfg(any(test, feature = "example-db"))]
309fn witness_config_for_assignment(
310    source: &KSatisfiability<K3>,
311    assignment: &[bool],
312) -> Option<BigUint> {
313    let construction = build_construction(source).expect("example or test source must reduce");
314    let alphas = build_alphas(&construction, assignment)?;
315    Some(witness_value_from_alphas(&alphas, &construction.thetas))
316}
317
318#[reduction(
319    transform = upper_bound {
320        bit_length_a = "64 * (2 * num_clauses + num_vars + 1)^2 + 3 * num_clauses + 4",
321        bit_length_b = "64 * (2 * num_clauses + num_vars + 1)^2 + 3 * num_clauses + 4",
322        bit_length_c = "64 * (2 * num_clauses + num_vars + 1)^2 + 3 * num_clauses + 4",
323    }
324)]
325impl ReduceTo<QuadraticCongruences> for KSatisfiability<K3> {
326    type Result = Reduction3SATToQuadraticCongruences;
327
328    fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
329        let construction = build_construction(self)?;
330        Ok(Reduction3SATToQuadraticCongruences {
331            target: construction.target,
332            source_num_vars: construction.source_num_vars,
333            active_to_source: construction.active_to_source,
334            clause_count: construction.clauses.len(),
335            h: construction.h,
336            prime_powers: construction.prime_powers,
337        })
338    }
339}
340
341#[cfg(feature = "example-db")]
342pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
343    use crate::export::SolutionPair;
344
345    vec![crate::example_db::specs::RuleExampleSpec {
346        id: "ksatisfiability_to_quadraticcongruences",
347        build: || {
348            let source = KSatisfiability::<K3>::new(
349                3,
350                vec![crate::models::formula::CNFClause::new(vec![1, 2, 3])],
351            );
352            let target_config = witness_config_for_assignment(&source, &[true, false, false])
353                .expect("canonical satisfying assignment should lift to a QC witness");
354            crate::example_db::specs::rule_example_with_witness::<_, QuadraticCongruences>(
355                source,
356                SolutionPair {
357                    source_config: serde_json::json!(vec![true, false, false]),
358                    target_config: serde_json::to_value(target_config)
359                        .expect("solution serialization must succeed"),
360                },
361            )
362        },
363    }]
364}
365
366#[cfg(test)]
367#[path = "../unit_tests/rules/ksatisfiability_quadraticcongruences.rs"]
368mod tests;
problemreductions/rules/ksatisfiability_quadraticcongruences.rs

problemreductions/rules/
ksatisfiability_quadraticcongruences.rs
