problemreductions/rules/
factoring_circuit.rs

1//! Reduction from Factoring to CircuitSAT.
2//!
3//! The reduction constructs a multiplier circuit that computes p × q
4//! and constrains the output to equal the target number N.
5//! A satisfying assignment to the circuit gives the factorization.
6//!
7//! The multiplier circuit uses an array multiplier structure with
8//! carry propagation, building up partial products row by row.
9
10use crate::models::formula::{Assignment, BooleanExpr, Circuit, CircuitSAT};
11use crate::models::misc::Factoring;
12use crate::reduction;
13use crate::rules::traits::{ReduceTo, ReductionResult};
14/// Result of reducing Factoring to CircuitSAT.
15///
16/// This struct contains:
17/// - The target CircuitSAT problem (the multiplier circuit)
18/// - Variable indices for the first factor p (m bits)
19/// - Variable indices for the second factor q (n bits)
20/// - Variable indices for the product m (m+n bits)
21#[derive(Debug, Clone)]
22pub struct ReductionFactoringToCircuit {
23    /// The target CircuitSAT problem.
24    target: CircuitSAT,
25    /// Variable names for the first factor p (bit positions).
26    p_vars: Vec<String>,
27    /// Variable names for the second factor q (bit positions).
28    q_vars: Vec<String>,
29    /// Variable names for the product (bit positions).
30    m_vars: Vec<String>,
31}
32
33impl ReductionResult for ReductionFactoringToCircuit {
34    type Source = Factoring;
35    type Target = CircuitSAT;
36
37    fn target_problem(&self) -> &Self::Target {
38        &self.target
39    }
40
41    /// Extract a Factoring solution from a CircuitSAT solution.
42    ///
43    /// Returns a configuration where the first m bits are the first factor p,
44    /// and the next n bits are the second factor q.
45    fn extract_solution(&self, target_solution: &[usize]) -> Vec<usize> {
46        let var_names = self.target.variable_names();
47
48        // Build a map from variable name to its value
49        let var_map: std::collections::HashMap<&str, usize> = var_names
50            .iter()
51            .enumerate()
52            .map(|(i, name)| (name.as_str(), target_solution.get(i).copied().unwrap_or(0)))
53            .collect();
54
55        // Extract p bits
56        let p_bits: Vec<usize> = self
57            .p_vars
58            .iter()
59            .map(|name| *var_map.get(name.as_str()).unwrap_or(&0))
60            .collect();
61
62        // Extract q bits
63        let q_bits: Vec<usize> = self
64            .q_vars
65            .iter()
66            .map(|name| *var_map.get(name.as_str()).unwrap_or(&0))
67            .collect();
68
69        // Concatenate p and q bits
70        let mut result = p_bits;
71        result.extend(q_bits);
72        result
73    }
74}
75
76impl ReductionFactoringToCircuit {
77    /// Get the variable names for the first factor.
78    pub fn p_vars(&self) -> &[String] {
79        &self.p_vars
80    }
81
82    /// Get the variable names for the second factor.
83    pub fn q_vars(&self) -> &[String] {
84        &self.q_vars
85    }
86
87    /// Get the variable names for the product.
88    pub fn m_vars(&self) -> &[String] {
89        &self.m_vars
90    }
91}
92
93/// Read the i-th bit (1-indexed) of a number (little-endian).
94fn read_bit(n: u64, i: usize) -> bool {
95    if i == 0 || i > 64 {
96        false
97    } else {
98        ((n >> (i - 1)) & 1) == 1
99    }
100}
101
102/// Build a single multiplier cell that computes:
103/// s + 2*c = p*q + s_pre + c_pre
104///
105/// This is a full adder that adds three bits: (p AND q), s_pre, and c_pre.
106/// Returns the assignments needed and the list of ancilla variable names.
107fn build_multiplier_cell(
108    s_name: &str,
109    c_name: &str,
110    p_name: &str,
111    q_name: &str,
112    s_pre: &BooleanExpr,
113    c_pre: &BooleanExpr,
114    cell_id: &str,
115) -> (Vec<Assignment>, Vec<String>) {
116    // Create unique ancilla variable names
117    let a_name = format!("a_{}", cell_id);
118    let a_xor_s_name = format!("axs_{}", cell_id);
119    let a_xor_s_and_c_name = format!("axsc_{}", cell_id);
120    let a_and_s_name = format!("as_{}", cell_id);
121
122    let p = BooleanExpr::var(p_name);
123    let q = BooleanExpr::var(q_name);
124    let a = BooleanExpr::var(&a_name);
125    let a_xor_s = BooleanExpr::var(&a_xor_s_name);
126
127    // Build the assignments:
128    // a = p & q (AND of the two factor bits)
129    let assign_a = Assignment::new(vec![a_name.clone()], BooleanExpr::and(vec![p, q]));
130
131    // a_xor_s = a XOR s_pre
132    let assign_a_xor_s = Assignment::new(
133        vec![a_xor_s_name.clone()],
134        BooleanExpr::xor(vec![a.clone(), s_pre.clone()]),
135    );
136
137    // s = a_xor_s XOR c_pre (sum output)
138    let assign_s = Assignment::new(
139        vec![s_name.to_string()],
140        BooleanExpr::xor(vec![a_xor_s.clone(), c_pre.clone()]),
141    );
142
143    // a_xor_s_and_c = a_xor_s & c_pre
144    let assign_a_xor_s_and_c = Assignment::new(
145        vec![a_xor_s_and_c_name.clone()],
146        BooleanExpr::and(vec![a_xor_s, c_pre.clone()]),
147    );
148
149    // a_and_s = a & s_pre
150    let assign_a_and_s = Assignment::new(
151        vec![a_and_s_name.clone()],
152        BooleanExpr::and(vec![a, s_pre.clone()]),
153    );
154
155    // c = a_xor_s_and_c | a_and_s (carry output)
156    let assign_c = Assignment::new(
157        vec![c_name.to_string()],
158        BooleanExpr::or(vec![
159            BooleanExpr::var(&a_xor_s_and_c_name),
160            BooleanExpr::var(&a_and_s_name),
161        ]),
162    );
163
164    let assignments = vec![
165        assign_a,
166        assign_a_xor_s,
167        assign_s,
168        assign_a_xor_s_and_c,
169        assign_a_and_s,
170        assign_c,
171    ];
172
173    let ancillas = vec![a_name, a_xor_s_name, a_xor_s_and_c_name, a_and_s_name];
174
175    (assignments, ancillas)
176}
177
178#[reduction(overhead = {
179    num_variables = "6 * num_bits_first * num_bits_second + num_bits_first + num_bits_second",
180    num_assignments = "6 * num_bits_first * num_bits_second + num_bits_first + num_bits_second",
181})]
182impl ReduceTo<CircuitSAT> for Factoring {
183    type Result = ReductionFactoringToCircuit;
184
185    fn reduce_to(&self) -> Self::Result {
186        let n1 = self.m(); // bits for first factor
187        let n2 = self.n(); // bits for second factor
188        let target = self.target();
189
190        // Create input variables for the two factors
191        let p_vars: Vec<String> = (1..=n1).map(|i| format!("p{}", i)).collect();
192        let q_vars: Vec<String> = (1..=n2).map(|i| format!("q{}", i)).collect();
193
194        // Accumulate assignments and product bits
195        let mut assignments = Vec::new();
196        let mut m_vars = Vec::new();
197
198        // Initialize s_pre (previous sum signals) with false constants
199        // s_pre has n2+1 elements to handle the carry propagation
200        let mut s_pre: Vec<BooleanExpr> = (0..=n2).map(|_| BooleanExpr::constant(false)).collect();
201
202        // Build the array multiplier row by row
203        for i in 1..=n1 {
204            // c_pre is the carry from the previous cell in this row
205            let mut c_pre = BooleanExpr::constant(false);
206
207            for j in 1..=n2 {
208                // Create signal names for this cell
209                let c_name = format!("c{}_{}", i, j);
210                let s_name = format!("s{}_{}", i, j);
211
212                // Build the multiplier cell
213                let cell_id = format!("{}_{}", i, j);
214                let (cell_assignments, _ancillas) = build_multiplier_cell(
215                    &s_name,
216                    &c_name,
217                    &p_vars[i - 1],
218                    &q_vars[j - 1],
219                    &s_pre[j], // s_pre[j+1] in 0-indexed Julia becomes s_pre[j] in 1-indexed
220                    &c_pre,
221                    &cell_id,
222                );
223
224                assignments.extend(cell_assignments);
225
226                // Update c_pre for the next cell
227                c_pre = BooleanExpr::var(&c_name);
228
229                // Update s_pre for the next row
230                // s_pre[j-1] (0-indexed) = s (the sum from this cell)
231                s_pre[j - 1] = BooleanExpr::var(&s_name);
232            }
233
234            // The final carry becomes the last element of s_pre
235            s_pre[n2] = c_pre;
236
237            // The first element of s_pre is the i-th bit of the product
238            m_vars.push(format!("s{}_{}", i, 1));
239        }
240
241        // The remaining bits of the product come from s_pre[1..=n2]
242        for j in 2..=n2 {
243            m_vars.push(format!("s{}_{}", n1, j));
244        }
245        // The final carry is the last bit
246        m_vars.push(format!("c{}_{}", n1, n2));
247
248        // Constrain the output bits to match the target number
249        for (i, m_var) in m_vars.iter().enumerate() {
250            let target_bit = read_bit(target, i + 1);
251            assignments.push(Assignment::new(
252                vec![m_var.clone()],
253                BooleanExpr::constant(target_bit),
254            ));
255        }
256
257        // Build the circuit
258        let circuit = Circuit::new(assignments);
259        let circuit_sat = CircuitSAT::new(circuit);
260
261        ReductionFactoringToCircuit {
262            target: circuit_sat,
263            p_vars,
264            q_vars,
265            m_vars,
266        }
267    }
268}
269
270#[cfg(test)]
271#[path = "../unit_tests/rules/factoring_circuit.rs"]
272mod tests;
problemreductions/rules/factoring_circuit.rs

problemreductions/rules/
factoring_circuit.rs
