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(feature = "example-db")]
271pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
272    use crate::export::SolutionPair;
273
274    vec![crate::example_db::specs::RuleExampleSpec {
275        id: "factoring_to_circuitsat",
276        build: || {
277            crate::example_db::specs::rule_example_with_witness::<_, CircuitSAT>(
278                Factoring::new(3, 3, 35),
279                SolutionPair {
280                    source_config: vec![1, 0, 1, 1, 1, 1],
281                    target_config: vec![
282                        1, 1, 1, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 0, 0, 1, 1, 1, 1, 1, 0, 0,
283                        1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 1, 1, 0, 1, 1, 1,
284                        1, 1, 1, 1, 1, 1, 0, 0, 0, 0,
285                    ],
286                },
287            )
288        },
289    }]
290}
291
292#[cfg(test)]
293#[path = "../unit_tests/rules/factoring_circuit.rs"]
294mod tests;
problemreductions/rules/factoring_circuit.rs

problemreductions/rules/
factoring_circuit.rs
