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(
32        &self,
33        target_solution: &<Self::Target as crate::traits::Problem>::Solution,
34    ) -> crate::rules::ExtractionResult<<Self::Source as crate::traits::Problem>::Solution> {
35        crate::rules::traits::validate_target_solution(self.target_problem(), target_solution)?;
36
37        Ok({
38            self.congruence_reduction
39                .extract_solution(target_solution)?
40        })
41    }
42}
43
44fn no_instance() -> QuadraticDiophantineEquations {
45    QuadraticDiophantineEquations::new(1u32, 1u32, 1u32)
46}
47
48fn translate_congruence(source: &QuadraticCongruences) -> QuadraticDiophantineEquations {
49    if source.c() <= &BigUint::one() {
50        return no_instance();
51    }
52
53    let h = source.c().clone() - BigUint::one();
54    let h_squared = &h * &h;
55    if h_squared < *source.a() {
56        return no_instance();
57    }
58
59    let padding = ((&h_squared - source.a()) / source.b()) + BigUint::one();
60    let c = source.a() + (source.b() * &padding);
61
62    QuadraticDiophantineEquations::new(BigUint::one(), source.b().clone(), c)
63}
64
65#[reduction(
66    transform = upper_bound {
67        bit_length_a = "1",
68        bit_length_b = "64 * (2 * num_clauses + num_vars + 1)^2 + 3 * num_clauses + 4",
69        bit_length_c = "128 * (2 * num_clauses + num_vars + 1)^2 + 6 * num_clauses + 9",
70    }
71)]
72impl ReduceTo<QuadraticDiophantineEquations> for KSatisfiability<K3> {
73    type Result = Reduction3SATToQuadraticDiophantineEquations;
74
75    fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
76        let congruence_reduction = ReduceTo::<QuadraticCongruences>::reduce_to(self)?;
77        let target = translate_congruence(congruence_reduction.target_problem());
78
79        Ok(Reduction3SATToQuadraticDiophantineEquations {
80            target,
81            congruence_reduction,
82        })
83    }
84}
85
86#[cfg(any(test, feature = "example-db"))]
87fn canonical_source() -> KSatisfiability<K3> {
88    use crate::models::formula::CNFClause;
89
90    KSatisfiability::<K3>::new(3, vec![CNFClause::new(vec![1, 2, 3])])
91}
92
93#[cfg(any(test, feature = "example-db"))]
94fn canonical_witness() -> BigUint {
95    BigUint::parse_bytes(b"3851422232510508672725868082377332726402809", 10)
96        .expect("canonical CRT witness must parse")
97}
98
99#[cfg(feature = "example-db")]
100pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
101    use crate::example_db::specs::assemble_rule_example;
102    use crate::export::SolutionPair;
103
104    vec![crate::example_db::specs::RuleExampleSpec {
105        id: "ksatisfiability_to_quadraticdiophantineequations",
106        build: || {
107            let source = canonical_source();
108            let reduction = ReduceTo::<QuadraticDiophantineEquations>::reduce_to(&source)
109                .expect("reduction should succeed");
110            let target_config = canonical_witness();
111
112            assemble_rule_example(
113                &source,
114                reduction.target_problem(),
115                vec![SolutionPair {
116                    source_config: serde_json::json!(vec![true, false, false]),
117                    target_config: serde_json::to_value(target_config)
118                        .expect("solution serialization must succeed"),
119                }],
120            )
121        },
122    }]
123}
124
125#[cfg(test)]
126#[path = "../unit_tests/rules/ksatisfiability_quadraticdiophantineequations.rs"]
127mod tests;
problemreductions/rules/ksatisfiability_quadraticdiophantineequations.rs

problemreductions/rules/
ksatisfiability_quadraticdiophantineequations.rs
