problemreductions/rules/

factoring_circuit.rs

//! Reduction from Factoring to CircuitSAT.
//!
//! The reduction constructs a multiplier circuit that computes p × q
//! and constrains the output to equal the target number N.
//! A satisfying assignment to the circuit gives the factorization.
//!
//! The multiplier circuit uses an array multiplier structure with
//! carry propagation, building up partial products row by row.

use crate::models::formula::{Assignment, BooleanExpr, Circuit, CircuitSAT};
use crate::models::misc::Factoring;
use crate::reduction;
use crate::rules::traits::{ReduceTo, ReductionResult};
use num_bigint::BigUint;
use num_traits::{One, Zero};
/// Result of reducing Factoring to CircuitSAT.
///
/// This struct contains:
/// - The target CircuitSAT problem (the multiplier circuit)
/// - Variable indices for the first factor p (m bits)
/// - Variable indices for the second factor q (n bits)
/// - Variable indices for the product m (m+n bits)
#[derive(Debug, Clone)]
pub struct ReductionFactoringToCircuit {
    /// The target CircuitSAT problem.
    target: CircuitSAT,
    /// Variable names for the first factor p (bit positions).
    p_vars: Vec<String>,
    /// Variable names for the second factor q (bit positions).
    q_vars: Vec<String>,
    /// Variable names for the product (bit positions).
    m_vars: Vec<String>,
}

impl ReductionResult for ReductionFactoringToCircuit {
    type Source = Factoring;
    type Target = CircuitSAT;

    fn target_problem(&self) -> &Self::Target {
        &self.target
    }

    /// Extract a Factoring solution from a CircuitSAT solution.
    ///
    /// Returns the decoded factors in ascending order.
    fn extract_solution(
        &self,
        target_solution: &<Self::Target as crate::traits::Problem>::Solution,
    ) -> crate::rules::ExtractionResult<<Self::Source as crate::traits::Problem>::Solution> {
        crate::rules::traits::validate_target_witness(
            self.target_problem(),
            target_solution,
            |value| value.0,
            "target assignment does not satisfy the multiplication circuit",
        )?;

        Ok({
            let var_names = self.target.variable_names();

            // Build a map from variable name to its value
            let var_map: std::collections::HashMap<&str, bool> = var_names
                .iter()
                .enumerate()
                .map(|(i, name)| (name.as_str(), target_solution[i]))
                .collect();

            let decode = |names: &[String]| {
                names
                    .iter()
                    .enumerate()
                    .try_fold(BigUint::zero(), |value, (index, name)| {
                        let bit = var_map.get(name.as_str()).copied().ok_or_else(|| {
                            crate::rules::ExtractionError::invalid(format!(
                                "target circuit does not contain factor variable {name}"
                            ))
                        })?;
                        Ok::<BigUint, crate::rules::ExtractionError>(if bit {
                            value + (BigUint::one() << index)
                        } else {
                            value
                        })
                    })
            };
            let left = decode(&self.p_vars)?;
            let right = decode(&self.q_vars)?;
            if left <= right {
                (left, right)
            } else {
                (right, left)
            }
        })
    }
}

impl ReductionFactoringToCircuit {
    /// Product width and assignment capacity, checked before circuit allocation.
    fn dimensions(m: usize, n: usize) -> Result<(usize, usize), crate::rules::ReductionError> {
        let overflow = || {
            crate::rules::ReductionError::integer_overflow::<Factoring, CircuitSAT>(
                "computing multiplication circuit dimensions",
            )
        };
        let width = m.checked_add(n).ok_or_else(overflow)?;
        let capacity = m
            .checked_mul(n)
            .and_then(|v| v.checked_mul(6))
            .and_then(|v| width.checked_mul(2).and_then(|w| v.checked_add(w)))
            .and_then(|v| v.checked_add(2))
            .ok_or_else(overflow)?;
        Ok((width, capacity))
    }

    /// Get the variable names for the first factor.
    pub fn p_vars(&self) -> &[String] {
        &self.p_vars
    }

    /// Get the variable names for the second factor.
    pub fn q_vars(&self) -> &[String] {
        &self.q_vars
    }

    /// Get the variable names for the product.
    pub fn m_vars(&self) -> &[String] {
        &self.m_vars
    }
}

/// Read the i-th bit (1-indexed) of a number (little-endian).
fn read_bit(n: &BigUint, i: usize) -> bool {
    if i == 0 {
        false
    } else {
        n.bit(u64::try_from(i - 1).expect("bit index fits u64"))
    }
}

/// Build a single multiplier cell that computes:
/// s + 2*c = p*q + s_pre + c_pre
///
/// This is a full adder that adds three bits: (p AND q), s_pre, and c_pre.
/// Returns the assignments needed and the list of ancilla variable names.
fn build_multiplier_cell(
    s_name: &str,
    c_name: &str,
    p_name: &str,
    q_name: &str,
    s_pre: &BooleanExpr,
    c_pre: &BooleanExpr,
    cell_id: &str,
) -> (Vec<Assignment>, Vec<String>) {
    // Create unique ancilla variable names
    let a_name = format!("a_{}", cell_id);
    let a_xor_s_name = format!("axs_{}", cell_id);
    let a_xor_s_and_c_name = format!("axsc_{}", cell_id);
    let a_and_s_name = format!("as_{}", cell_id);

    let p = BooleanExpr::var(p_name);
    let q = BooleanExpr::var(q_name);
    let a = BooleanExpr::var(&a_name);
    let a_xor_s = BooleanExpr::var(&a_xor_s_name);

    // Build the assignments:
    // a = p & q (AND of the two factor bits)
    let assign_a = Assignment::new(vec![a_name.clone()], BooleanExpr::and(vec![p, q]));

    // a_xor_s = a XOR s_pre
    let assign_a_xor_s = Assignment::new(
        vec![a_xor_s_name.clone()],
        BooleanExpr::xor(vec![a.clone(), s_pre.clone()]),
    );

    // s = a_xor_s XOR c_pre (sum output)
    let assign_s = Assignment::new(
        vec![s_name.to_string()],
        BooleanExpr::xor(vec![a_xor_s.clone(), c_pre.clone()]),
    );

    // a_xor_s_and_c = a_xor_s & c_pre
    let assign_a_xor_s_and_c = Assignment::new(
        vec![a_xor_s_and_c_name.clone()],
        BooleanExpr::and(vec![a_xor_s, c_pre.clone()]),
    );

    // a_and_s = a & s_pre
    let assign_a_and_s = Assignment::new(
        vec![a_and_s_name.clone()],
        BooleanExpr::and(vec![a, s_pre.clone()]),
    );

    // c = a_xor_s_and_c | a_and_s (carry output)
    let assign_c = Assignment::new(
        vec![c_name.to_string()],
        BooleanExpr::or(vec![
            BooleanExpr::var(&a_xor_s_and_c_name),
            BooleanExpr::var(&a_and_s_name),
        ]),
    );

    let assignments = vec![
        assign_a,
        assign_a_xor_s,
        assign_s,
        assign_a_xor_s_and_c,
        assign_a_and_s,
        assign_c,
    ];

    let ancillas = vec![a_name, a_xor_s_name, a_xor_s_and_c_name, a_and_s_name];

    (assignments, ancillas)
}

#[crate::aggregate_reduction(identity)]
impl crate::rules::AggregateReductionResult for ReductionFactoringToCircuit {}

#[reduction(transform = upper_bound {
    num_variables = "6 * num_bits_first * num_bits_second + 2 * (num_bits_first + num_bits_second) + 1",
    num_assignments = "6 * num_bits_first * num_bits_second + 2 * (num_bits_first + num_bits_second) + 2",
    num_assignment_outputs = "6 * num_bits_first * num_bits_second + 2 * (num_bits_first + num_bits_second) + 2",
    num_expression_nodes = "5 * (6 * num_bits_first * num_bits_second + 2 * (num_bits_first + num_bits_second) + 2)",
})]
impl ReduceTo<CircuitSAT> for Factoring {
    type Result = ReductionFactoringToCircuit;

    fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
        let n1 = self.m(); // bits for first factor
        let n2 = self.n(); // bits for second factor
        let target = self.target();
        let (width, capacity) = ReductionFactoringToCircuit::dimensions(n1, n2)?;

        // Create input variables for the two factors
        let p_vars: Vec<String> = (1..=n1).map(|i| format!("p{}", i)).collect();
        let q_vars: Vec<String> = (1..=n2).map(|i| format!("q{}", i)).collect();

        // Accumulate assignments and product bits
        let mut assignments = Vec::with_capacity(capacity);
        let mut product_bits = Vec::with_capacity(width);

        // Initialize s_pre (previous sum signals) with false constants
        // s_pre has n2+1 elements to handle the carry propagation
        let mut s_pre = Vec::with_capacity(n2 + 1);
        s_pre.push(BooleanExpr::constant(false));
        // The zero accumulator is expressed as Q AND zero. This also keeps
        // every Q input in the circuit when no multiplier rows are present.
        s_pre.extend(q_vars.iter().map(|name| {
            BooleanExpr::and(vec![BooleanExpr::var(name), BooleanExpr::constant(false)])
        }));

        // Build the array multiplier row by row
        for i in 1..=n1 {
            // c_pre is the carry from the previous cell in this row
            let mut c_pre = BooleanExpr::constant(false);

            for j in 1..=n2 {
                // Create signal names for this cell
                let c_name = format!("c{}_{}", i, j);
                let s_name = format!("s{}_{}", i, j);

                // Build the multiplier cell
                let cell_id = format!("{}_{}", i, j);
                let (cell_assignments, _ancillas) = build_multiplier_cell(
                    &s_name,
                    &c_name,
                    &p_vars[i - 1],
                    &q_vars[j - 1],
                    &s_pre[j], // s_pre[j+1] in 0-indexed Julia becomes s_pre[j] in 1-indexed
                    &c_pre,
                    &cell_id,
                );

                assignments.extend(cell_assignments);

                // Update c_pre for the next cell
                c_pre = BooleanExpr::var(&c_name);

                // Update s_pre for the next row
                // s_pre[j-1] (0-indexed) = s (the sum from this cell)
                s_pre[j - 1] = BooleanExpr::var(&s_name);
            }

            // The final carry becomes the last element of s_pre
            s_pre[n2] = c_pre;

            // The first element of s_pre is the i-th bit of the product
            product_bits.push(s_pre[0].clone());
        }

        // After all rows, the residual accumulator supplies the remaining
        // high bits. With zero rows these are the actual zero expressions,
        // not names of multiplier cells that were never constructed.
        product_bits.extend(s_pre.into_iter().skip(1));
        let m_vars: Vec<_> = (0..width).map(|i| format!("product_{i}")).collect();
        for (name, expr) in m_vars.iter().zip(product_bits) {
            assignments.push(Assignment::new(vec![name.clone()], expr));
        }

        // Constrain the output bits to match the target number
        for (i, m_var) in m_vars.iter().enumerate() {
            let target_bit = read_bit(target, i + 1);
            assignments.push(Assignment::new(
                vec![m_var.clone()],
                BooleanExpr::constant(target_bit),
            ));
        }

        // An m-bit by n-bit product cannot contain a set bit above position m+n-1.
        // Encode an explicit contradiction instead of truncating an oversized target.
        if target.bits() > u64::try_from(m_vars.len()).expect("product width fits u64") {
            let overflow = "target_overflow".to_string();
            assignments.push(Assignment::new(
                vec![overflow.clone()],
                BooleanExpr::constant(false),
            ));
            assignments.push(Assignment::new(vec![overflow], BooleanExpr::constant(true)));
        }

        // Build the circuit
        let circuit = Circuit::new(assignments);
        let circuit_sat = CircuitSAT::new(circuit);

        Ok(ReductionFactoringToCircuit {
            target: circuit_sat,
            p_vars,
            q_vars,
            m_vars,
        })
    }
}

#[cfg(feature = "example-db")]
pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
    use crate::export::SolutionPair;

    vec![crate::example_db::specs::RuleExampleSpec {
        id: "factoring_to_circuitsat",
        build: || {
            crate::example_db::specs::rule_example_with_witness::<_, CircuitSAT>(
                Factoring::with_factor_bits(35, 3, 3),
                SolutionPair {
                    source_config: serde_json::to_value((BigUint::from(5u32), BigUint::from(7u32)))
                        .expect("solution serialization must succeed"),
                    target_config: serde_json::json!(vec![
                        true, true, true, false, false, false, true, true, true, false, false,
                        false, false, false, false, true, false, false, true, true, true, true,
                        true, false, false, true, true, false, false, false, false, false, false,
                        false, true, true, false, false, false, false, false, false, true, true,
                        true, true, false, true, true, true, false, false, false, true, true, true,
                        true, true, true, true, true, true, false, false, false, false
                    ]),
                },
            )
        },
    }]
}

#[cfg(test)]
#[path = "../unit_tests/rules/factoring_circuit.rs"]
mod tests;