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::solvers::BruteForceProblem as _;
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(
30        &self,
31        target_solution: &<Self::Target as crate::traits::Problem>::Solution,
32    ) -> crate::rules::ExtractionResult<<Self::Source as crate::traits::Problem>::Solution> {
33        crate::rules::traits::validate_target_solution(self.target_problem(), target_solution)?;
34
35        Ok({
36            self.source_var_indices
37                .iter()
38                .map(|&idx| target_solution[idx])
39                .collect()
40        })
41    }
42}
43
44#[reduction(
45    transform = upper_bound {
46        num_variables = "2 * num_vars + num_clauses + 1",
47        num_assignments = "num_vars + num_clauses + 2",
48    },
49    unavailable = {
50        num_assignment_outputs = "the exact target parameter is not represented by this reduction's symbolic transform",
51        num_expression_nodes = "the exact target parameter is not represented by this reduction's symbolic transform",
52    }
53)]
54impl ReduceTo<CircuitSAT> for Satisfiability {
55    type Result = ReductionSATToCircuit;
56
57    fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
58        let num_vars = self.num_variables();
59        let clauses = self.clauses();
60
61        let mut assignments = Vec::new();
62        let mut clause_outputs = Vec::new();
63
64        for (i, clause) in clauses.iter().enumerate() {
65            let clause_output = format!("__clause_{}", i);
66            let mut literal_exprs: Vec<BooleanExpr> = clause
67                .literals
68                .iter()
69                .map(|&lit| {
70                    let var_name = format!("x{}", lit.unsigned_abs());
71                    let var_expr = BooleanExpr::var(&var_name);
72                    if lit < 0 {
73                        BooleanExpr::not(var_expr)
74                    } else {
75                        var_expr
76                    }
77                })
78                .collect();
79
80            let clause_expr = if literal_exprs.len() == 1 {
81                literal_exprs.remove(0)
82            } else {
83                BooleanExpr::or(literal_exprs)
84            };
85
86            assignments.push(Assignment::new(vec![clause_output.clone()], clause_expr));
87            clause_outputs.push(clause_output);
88        }
89
90        // Final AND gate
91        let final_output = "__out".to_string();
92        let and_expr = if clause_outputs.len() == 1 {
93            BooleanExpr::var(&clause_outputs[0])
94        } else {
95            BooleanExpr::and(
96                clause_outputs
97                    .iter()
98                    .map(|name| BooleanExpr::var(name))
99                    .collect(),
100            )
101        };
102        assignments.push(Assignment::new(vec![final_output.clone()], and_expr));
103
104        // Constrain the final output to be true
105        assignments.push(Assignment::new(
106            vec![final_output],
107            BooleanExpr::constant(true),
108        ));
109
110        // Add identity assignments for variables that don't appear in any clause,
111        // so they are present in Circuit::variables() for index mapping.
112        let used_vars: HashSet<usize> = clauses
113            .iter()
114            .flat_map(|c| c.literals.iter().map(|&lit| lit.unsigned_abs() as usize))
115            .collect();
116        for i in 1..=num_vars {
117            if !used_vars.contains(&i) {
118                let var_name = format!("x{}", i);
119                assignments.push(Assignment::new(
120                    vec![format!("__unused_{}", i)],
121                    BooleanExpr::var(&var_name),
122                ));
123            }
124        }
125
126        let circuit = Circuit::new(assignments);
127        let target = CircuitSAT::new(circuit);
128
129        // Map SAT variable indices to CircuitSAT variable indices
130        let var_names = target.variable_names();
131        let source_var_indices: Vec<usize> = (1..=num_vars)
132            .map(|i| {
133                let name = format!("x{}", i);
134                var_names.iter().position(|n| n == &name).ok_or_else(|| {
135                    crate::rules::ReductionError::invalid_target::<Satisfiability, CircuitSAT>(
136                        format!("target circuit is missing source variable `{name}`"),
137                    )
138                })
139            })
140            .collect::<Result<_, _>>()?;
141
142        Ok(ReductionSATToCircuit {
143            target,
144            source_var_indices,
145        })
146    }
147}
148
149#[cfg(feature = "example-db")]
150pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
151    use crate::export::SolutionPair;
152    use crate::models::formula::CNFClause;
153
154    vec![crate::example_db::specs::RuleExampleSpec {
155        id: "satisfiability_to_circuitsat",
156        build: || {
157            let source = Satisfiability::new(
158                3,
159                vec![
160                    CNFClause::new(vec![1, -2, 3]),
161                    CNFClause::new(vec![-1, 2]),
162                    CNFClause::new(vec![2, 3]),
163                ],
164            );
165            crate::example_db::specs::rule_example_with_witness::<_, CircuitSAT>(
166                source,
167                SolutionPair {
168                    source_config: serde_json::json!(vec![true, true, true]),
169                    target_config: serde_json::json!(vec![
170                        true, true, true, true, true, true, true
171                    ]),
172                },
173            )
174        },
175    }]
176}
177
178#[cfg(test)]
179#[path = "../unit_tests/rules/sat_circuitsat.rs"]
180mod tests;
problemreductions/rules/sat_circuitsat.rs

problemreductions/rules/
sat_circuitsat.rs
