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;
11use std::collections::HashSet;
12
13/// Result of reducing SAT to CircuitSAT.
14#[derive(Debug, Clone)]
15pub struct ReductionSATToCircuit {
16    target: CircuitSAT,
17    /// Indices of original SAT variables in the CircuitSAT variable list.
18    source_var_indices: Vec<usize>,
19}
20
21impl ReductionResult for ReductionSATToCircuit {
22    type Source = Satisfiability;
23    type Target = CircuitSAT;
24
25    fn target_problem(&self) -> &CircuitSAT {
26        &self.target
27    }
28
29    fn extract_solution(&self, target_solution: &[usize]) -> Vec<usize> {
30        self.source_var_indices
31            .iter()
32            .map(|&idx| target_solution[idx])
33            .collect()
34    }
35}
36
37#[reduction(
38    overhead = {
39        num_variables = "num_vars + num_clauses",
40        num_assignments = "num_vars + num_clauses",
41    }
42)]
43impl ReduceTo<CircuitSAT> for Satisfiability {
44    type Result = ReductionSATToCircuit;
45
46    fn reduce_to(&self) -> Self::Result {
47        let num_vars = self.num_variables();
48        let clauses = self.clauses();
49
50        let mut assignments = Vec::new();
51        let mut clause_outputs = Vec::new();
52
53        for (i, clause) in clauses.iter().enumerate() {
54            let clause_output = format!("__clause_{}", i);
55            let literal_exprs: Vec<BooleanExpr> = clause
56                .literals
57                .iter()
58                .map(|&lit| {
59                    let var_name = format!("x{}", lit.unsigned_abs());
60                    let var_expr = BooleanExpr::var(&var_name);
61                    if lit < 0 {
62                        BooleanExpr::not(var_expr)
63                    } else {
64                        var_expr
65                    }
66                })
67                .collect();
68
69            let clause_expr = if literal_exprs.len() == 1 {
70                literal_exprs.into_iter().next().unwrap()
71            } else {
72                BooleanExpr::or(literal_exprs)
73            };
74
75            assignments.push(Assignment::new(vec![clause_output.clone()], clause_expr));
76            clause_outputs.push(clause_output);
77        }
78
79        // Final AND gate
80        let final_output = "__out".to_string();
81        let and_expr = if clause_outputs.len() == 1 {
82            BooleanExpr::var(&clause_outputs[0])
83        } else {
84            BooleanExpr::and(
85                clause_outputs
86                    .iter()
87                    .map(|name| BooleanExpr::var(name))
88                    .collect(),
89            )
90        };
91        assignments.push(Assignment::new(vec![final_output.clone()], and_expr));
92
93        // Constrain the final output to be true
94        assignments.push(Assignment::new(
95            vec![final_output],
96            BooleanExpr::constant(true),
97        ));
98
99        // Add identity assignments for variables that don't appear in any clause,
100        // so they are present in Circuit::variables() for index mapping.
101        let used_vars: HashSet<usize> = clauses
102            .iter()
103            .flat_map(|c| c.literals.iter().map(|&lit| lit.unsigned_abs() as usize))
104            .collect();
105        for i in 1..=num_vars {
106            if !used_vars.contains(&i) {
107                let var_name = format!("x{}", i);
108                assignments.push(Assignment::new(
109                    vec![format!("__unused_{}", i)],
110                    BooleanExpr::var(&var_name),
111                ));
112            }
113        }
114
115        let circuit = Circuit::new(assignments);
116        let target = CircuitSAT::new(circuit);
117
118        // Map SAT variable indices to CircuitSAT variable indices
119        let var_names = target.variable_names();
120        let source_var_indices: Vec<usize> = (1..=num_vars)
121            .map(|i| {
122                let name = format!("x{}", i);
123                var_names
124                    .iter()
125                    .position(|n| n == &name)
126                    .unwrap_or_else(|| panic!("Variable {} not found in CircuitSAT", name))
127            })
128            .collect();
129
130        ReductionSATToCircuit {
131            target,
132            source_var_indices,
133        }
134    }
135}
136
137#[cfg(feature = "example-db")]
138pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
139    use crate::export::SolutionPair;
140    use crate::models::formula::CNFClause;
141
142    vec![crate::example_db::specs::RuleExampleSpec {
143        id: "satisfiability_to_circuitsat",
144        build: || {
145            let source = Satisfiability::new(
146                3,
147                vec![
148                    CNFClause::new(vec![1, -2, 3]),
149                    CNFClause::new(vec![-1, 2]),
150                    CNFClause::new(vec![2, 3]),
151                ],
152            );
153            crate::example_db::specs::rule_example_with_witness::<_, CircuitSAT>(
154                source,
155                SolutionPair {
156                    source_config: vec![1, 1, 1],
157                    target_config: vec![1, 1, 1, 1, 1, 1, 1],
158                },
159            )
160        },
161    }]
162}
163
164#[cfg(test)]
165#[path = "../unit_tests/rules/sat_circuitsat.rs"]
166mod tests;
problemreductions/rules/sat_circuitsat.rs

problemreductions/rules/
sat_circuitsat.rs
