problemreductions/rules/
ksatisfiability_quadraticdiophantineequations.rs

1//! Reduction from KSatisfiability (3-SAT) to Quadratic Diophantine Equations.
2//!
3//! This reuses the existing Manders-Adleman 3-SAT -> QuadraticCongruences
4//! construction, then converts the bounded congruence witness into an equation
5//! of the form x^2 + by = c.
6
7use crate::models::algebraic::{QuadraticCongruences, QuadraticDiophantineEquations};
8use crate::models::formula::KSatisfiability;
9use crate::reduction;
10use crate::rules::ksatisfiability_quadraticcongruences::Reduction3SATToQuadraticCongruences;
11use crate::rules::traits::{ReduceTo, ReductionResult};
12use crate::variant::K3;
13use num_bigint::BigUint;
14use num_traits::One;
15
16/// Result of reducing 3-SAT to Quadratic Diophantine Equations.
17#[derive(Debug, Clone)]
18pub struct Reduction3SATToQuadraticDiophantineEquations {
19    target: QuadraticDiophantineEquations,
20    congruence_reduction: Reduction3SATToQuadraticCongruences,
21}
22
23impl ReductionResult for Reduction3SATToQuadraticDiophantineEquations {
24    type Source = KSatisfiability<K3>;
25    type Target = QuadraticDiophantineEquations;
26
27    fn target_problem(&self) -> &Self::Target {
28        &self.target
29    }
30
31    fn extract_solution(&self, target_solution: &[usize]) -> Vec<usize> {
32        let Some(x) = self.target.decode_witness(target_solution) else {
33            return self.congruence_reduction.extract_solution(&[]);
34        };
35
36        let Some(congruence_config) = self
37            .congruence_reduction
38            .target_problem()
39            .encode_witness(&x)
40        else {
41            return self.congruence_reduction.extract_solution(&[]);
42        };
43
44        self.congruence_reduction
45            .extract_solution(&congruence_config)
46    }
47}
48
49fn no_instance() -> QuadraticDiophantineEquations {
50    QuadraticDiophantineEquations::new(1u32, 1u32, 1u32)
51}
52
53fn translate_congruence(source: &QuadraticCongruences) -> QuadraticDiophantineEquations {
54    if source.c() <= &BigUint::one() {
55        return no_instance();
56    }
57
58    let h = source.c().clone() - BigUint::one();
59    let h_squared = &h * &h;
60    if h_squared < *source.a() {
61        return no_instance();
62    }
63
64    let padding = ((&h_squared - source.a()) / source.b()) + BigUint::one();
65    let c = source.a() + (source.b() * &padding);
66
67    QuadraticDiophantineEquations::new(BigUint::one(), source.b().clone(), c)
68}
69
70#[reduction(overhead = {
71    bit_length_a = "1",
72    bit_length_b = "(num_vars + num_clauses)^2 * log(num_vars + num_clauses + 1)",
73    bit_length_c = "(num_vars + num_clauses)^2 * log(num_vars + num_clauses + 1)",
74})]
75impl ReduceTo<QuadraticDiophantineEquations> for KSatisfiability<K3> {
76    type Result = Reduction3SATToQuadraticDiophantineEquations;
77
78    fn reduce_to(&self) -> Self::Result {
79        let congruence_reduction = ReduceTo::<QuadraticCongruences>::reduce_to(self);
80        let target = translate_congruence(congruence_reduction.target_problem());
81
82        Reduction3SATToQuadraticDiophantineEquations {
83            target,
84            congruence_reduction,
85        }
86    }
87}
88
89#[cfg(any(test, feature = "example-db"))]
90fn canonical_source() -> KSatisfiability<K3> {
91    use crate::models::formula::CNFClause;
92
93    KSatisfiability::<K3>::new(3, vec![CNFClause::new(vec![1, 2, 3])])
94}
95
96#[cfg(any(test, feature = "example-db"))]
97fn canonical_witness() -> BigUint {
98    BigUint::parse_bytes(
99        b"1751451122102119958305507786775835374858648979796949071929887579732578264063983923970828608254544727567945005331103265320267846420581308180536461678218456421163010842022583797942541569366464959069523226763069748653830351684499364645098951736761394790343553460544021210289436100818494593367113721596780252083857888675004881955664228675079663569835052161564690932502575257394108174870151908279593037426404556490332761276593006398441245490978500647642893471046425509487910796951416870024826654351366508266859321005453091128123256128675758429165869380881549388896022325625404673271432251145796159394173120179999131480837018022329857587128653018300402",
100        10,
101    )
102    .expect("reference witness must parse")
103}
104
105#[cfg(feature = "example-db")]
106pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
107    use crate::example_db::specs::assemble_rule_example;
108    use crate::export::SolutionPair;
109
110    vec![crate::example_db::specs::RuleExampleSpec {
111        id: "ksatisfiability_to_quadraticdiophantineequations",
112        build: || {
113            let source = canonical_source();
114            let reduction = ReduceTo::<QuadraticDiophantineEquations>::reduce_to(&source);
115            let target_config = reduction
116                .target_problem()
117                .encode_witness(&canonical_witness())
118                .expect("reference witness must fit QDE encoding");
119
120            assemble_rule_example(
121                &source,
122                reduction.target_problem(),
123                vec![SolutionPair {
124                    source_config: vec![1, 0, 0],
125                    target_config,
126                }],
127            )
128        },
129    }]
130}
131
132#[cfg(test)]
133#[path = "../unit_tests/rules/ksatisfiability_quadraticdiophantineequations.rs"]
134mod tests;
problemreductions/rules/ksatisfiability_quadraticdiophantineequations.rs

problemreductions/rules/
ksatisfiability_quadraticdiophantineequations.rs
