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_witness(
36            self.target_problem(),
37            target_solution,
38            |value| value.0,
39            "target witness does not satisfy the target problem",
40        )?;
41
42        Ok({
43            self.congruence_reduction
44                .extract_solution(target_solution)?
45        })
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#[crate::aggregate_reduction(identity)]
71impl crate::rules::AggregateReductionResult for Reduction3SATToQuadraticDiophantineEquations {}
72
73#[reduction(
74    transform = upper_bound {
75        bit_length_a = "1",
76        bit_length_b = "64 * (2 * num_clauses + num_vars + 1)^2 + 3 * num_clauses + 4",
77        bit_length_c = "128 * (2 * num_clauses + num_vars + 1)^2 + 6 * num_clauses + 9",
78    }
79)]
80impl ReduceTo<QuadraticDiophantineEquations> for KSatisfiability<K3> {
81    type Result = Reduction3SATToQuadraticDiophantineEquations;
82
83    fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
84        let congruence_reduction = ReduceTo::<QuadraticCongruences>::reduce_to(self)?;
85        let target = translate_congruence(congruence_reduction.target_problem());
86
87        Ok(Reduction3SATToQuadraticDiophantineEquations {
88            target,
89            congruence_reduction,
90        })
91    }
92}
93
94#[cfg(any(test, feature = "example-db"))]
95fn canonical_source() -> KSatisfiability<K3> {
96    use crate::models::formula::CNFClause;
97
98    KSatisfiability::<K3>::new(3, vec![CNFClause::new(vec![1, 2, 3])])
99}
100
101#[cfg(any(test, feature = "example-db"))]
102fn canonical_witness() -> BigUint {
103    BigUint::parse_bytes(b"3851422232510508672725868082377332726402809", 10)
104        .expect("canonical CRT witness must parse")
105}
106
107#[cfg(feature = "example-db")]
108pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
109    use crate::example_db::specs::assemble_rule_example;
110    use crate::export::SolutionPair;
111
112    vec![crate::example_db::specs::RuleExampleSpec {
113        id: "ksatisfiability_to_quadraticdiophantineequations",
114        build: || {
115            let source = canonical_source();
116            let reduction = ReduceTo::<QuadraticDiophantineEquations>::reduce_to(&source)
117                .expect("reduction should succeed");
118            let target_config = canonical_witness();
119
120            assemble_rule_example(
121                &source,
122                reduction.target_problem(),
123                vec![SolutionPair {
124                    source_config: serde_json::json!(vec![true, false, false]),
125                    target_config: serde_json::to_value(target_config)
126                        .expect("solution serialization must succeed"),
127                }],
128            )
129        },
130    }]
131}
132
133#[cfg(test)]
134#[path = "../unit_tests/rules/ksatisfiability_quadraticdiophantineequations.rs"]
135mod tests;
problemreductions/rules/ksatisfiability_quadraticdiophantineequations.rs

problemreductions/rules/
ksatisfiability_quadraticdiophantineequations.rs
