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

problemreductions/rules/
ksatisfiability_quadraticcongruences.rs
