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

problemreductions/rules/
sat_circuitsat.rs
