problemreductions/rules/
sat_circuitsat.rs

1//! Reduction from Satisfiability to CircuitSAT.
2//!
3//! Converts a CNF formula into a boolean circuit by creating
4//! an OR gate for each clause and a final AND gate.
5
6use crate::models::formula::Satisfiability;
7use crate::models::formula::{Assignment, BooleanExpr, Circuit, CircuitSAT};
8use crate::reduction;
9use crate::rules::traits::{ReduceTo, ReductionResult};
10use crate::traits::Problem;
11
12/// Result of reducing SAT to CircuitSAT.
13#[derive(Debug, Clone)]
14pub struct ReductionSATToCircuit {
15    target: CircuitSAT,
16    /// Indices of original SAT variables in the CircuitSAT variable list.
17    source_var_indices: Vec<usize>,
18}
19
20impl ReductionResult for ReductionSATToCircuit {
21    type Source = Satisfiability;
22    type Target = CircuitSAT;
23
24    fn target_problem(&self) -> &CircuitSAT {
25        &self.target
26    }
27
28    fn extract_solution(&self, target_solution: &[usize]) -> Vec<usize> {
29        self.source_var_indices
30            .iter()
31            .map(|&idx| target_solution[idx])
32            .collect()
33    }
34}
35
36#[reduction(
37    overhead = {
38        num_variables = "num_vars + num_clauses + 1",
39        num_assignments = "num_clauses + 2",
40    }
41)]
42impl ReduceTo<CircuitSAT> for Satisfiability {
43    type Result = ReductionSATToCircuit;
44
45    fn reduce_to(&self) -> Self::Result {
46        let num_vars = self.num_variables();
47        let clauses = self.clauses();
48
49        let mut assignments = Vec::new();
50        let mut clause_outputs = Vec::new();
51
52        for (i, clause) in clauses.iter().enumerate() {
53            let clause_output = format!("__clause_{}", i);
54            let literal_exprs: Vec<BooleanExpr> = clause
55                .literals
56                .iter()
57                .map(|&lit| {
58                    let var_name = format!("x{}", lit.unsigned_abs());
59                    let var_expr = BooleanExpr::var(&var_name);
60                    if lit < 0 {
61                        BooleanExpr::not(var_expr)
62                    } else {
63                        var_expr
64                    }
65                })
66                .collect();
67
68            let clause_expr = if literal_exprs.len() == 1 {
69                literal_exprs.into_iter().next().unwrap()
70            } else {
71                BooleanExpr::or(literal_exprs)
72            };
73
74            assignments.push(Assignment::new(vec![clause_output.clone()], clause_expr));
75            clause_outputs.push(clause_output);
76        }
77
78        // Final AND gate
79        let final_output = "__out".to_string();
80        let and_expr = if clause_outputs.len() == 1 {
81            BooleanExpr::var(&clause_outputs[0])
82        } else {
83            BooleanExpr::and(
84                clause_outputs
85                    .iter()
86                    .map(|name| BooleanExpr::var(name))
87                    .collect(),
88            )
89        };
90        assignments.push(Assignment::new(vec![final_output.clone()], and_expr));
91
92        // Constrain the final output to be true
93        assignments.push(Assignment::new(
94            vec![final_output],
95            BooleanExpr::constant(true),
96        ));
97
98        let circuit = Circuit::new(assignments);
99        let target = CircuitSAT::new(circuit);
100
101        // Map SAT variable indices to CircuitSAT variable indices
102        let var_names = target.variable_names();
103        let source_var_indices: Vec<usize> = (1..=num_vars)
104            .map(|i| {
105                let name = format!("x{}", i);
106                var_names
107                    .iter()
108                    .position(|n| n == &name)
109                    .unwrap_or_else(|| panic!("Variable {} not found in CircuitSAT", name))
110            })
111            .collect();
112
113        ReductionSATToCircuit {
114            target,
115            source_var_indices,
116        }
117    }
118}
119
120#[cfg(test)]
121#[path = "../unit_tests/rules/sat_circuitsat.rs"]
122mod tests;
problemreductions/rules/sat_circuitsat.rs

problemreductions/rules/
sat_circuitsat.rs
