1use crate::models::formula::{
4 Assignment, BooleanExpr, BooleanOp, CNFClause, CircuitSAT, Satisfiability,
5};
6use crate::reduction;
7use crate::rules::sat_helpers::SatVariableAllocator;
8use crate::rules::traits::{ReduceTo, ReductionResult};
9use std::collections::HashMap;
10
11#[derive(Debug, Clone, PartialEq, Eq)]
12enum NormalizedExpr {
13 Var(String),
14 Const(bool),
15 Not(Box<NormalizedExpr>),
16 And(Box<NormalizedExpr>, Box<NormalizedExpr>),
17 Or(Box<NormalizedExpr>, Box<NormalizedExpr>),
18 Xor(Box<NormalizedExpr>, Box<NormalizedExpr>),
19}
20
21#[derive(Debug, Clone, Copy, PartialEq, Eq)]
22enum EncodedTerm {
23 Const(bool),
24 Var(i64),
25}
26
27#[derive(Debug, Clone)]
28struct TseitinEncoding {
29 num_vars: usize,
30 clauses: Vec<CNFClause>,
31}
32
33#[derive(Debug)]
34struct TseitinEncoder {
35 source_var_ids: HashMap<String, i64>,
36 clauses: Vec<CNFClause>,
37 variables: SatVariableAllocator,
38}
39
40impl TseitinEncoder {
41 fn new(source: &CircuitSAT) -> Self {
42 let mut variables = SatVariableAllocator::new("CircuitSAT -> Satisfiability", 0)
43 .unwrap_or_else(|message| panic!("{message}"));
44 let source_ids = variables
45 .allocate_many(source.num_variables())
46 .unwrap_or_else(|message| panic!("{message}"));
47 let source_var_ids = source
48 .variable_names()
49 .iter()
50 .zip(source_ids)
51 .map(|(name, variable)| (name.clone(), variable))
52 .collect();
53 Self {
54 source_var_ids,
55 clauses: Vec::new(),
56 variables,
57 }
58 }
59
60 fn encode_problem(mut self, source: &CircuitSAT) -> TseitinEncoding {
61 for assignment in &source.circuit().assignments {
62 self.encode_assignment(assignment);
63 }
64
65 TseitinEncoding {
66 num_vars: self.variables.num_vars(),
67 clauses: self.clauses,
68 }
69 }
70
71 fn encode_assignment(&mut self, assignment: &Assignment) {
72 if assignment.outputs.is_empty() {
73 return;
74 }
75
76 let root = self.encode_expr(&normalize_expr(&assignment.expr));
77 match root {
78 EncodedTerm::Const(value) => {
79 let literal_sign = if value { 1 } else { -1 };
80 for output in &assignment.outputs {
81 let output_var = self.source_var(output);
82 self.push_clause(vec![literal_sign * output_var]);
83 }
84 }
85 EncodedTerm::Var(root_var) => {
86 for output in &assignment.outputs {
87 let output_var = self.source_var(output);
88 self.push_equivalence(output_var, root_var);
89 }
90 }
91 }
92 }
93
94 fn encode_expr(&mut self, expr: &NormalizedExpr) -> EncodedTerm {
95 match expr {
96 NormalizedExpr::Var(name) => EncodedTerm::Var(self.source_var(name)),
97 NormalizedExpr::Const(value) => EncodedTerm::Const(*value),
98 NormalizedExpr::Not(inner) => match self.encode_expr(inner) {
99 EncodedTerm::Const(value) => EncodedTerm::Const(!value),
100 EncodedTerm::Var(child_var) => {
101 let gate_var = self.allocate_auxiliary_var();
102 self.push_clause(vec![-gate_var, -child_var]);
103 self.push_clause(vec![gate_var, child_var]);
104 EncodedTerm::Var(gate_var)
105 }
106 },
107 NormalizedExpr::And(left, right) => {
108 let left_term = self.encode_expr(left);
109 let right_term = self.encode_expr(right);
110 let left_var = self.expect_var(left_term, "AND left input");
111 let right_var = self.expect_var(right_term, "AND right input");
112 let gate_var = self.allocate_auxiliary_var();
113 self.push_clause(vec![-gate_var, left_var]);
114 self.push_clause(vec![-gate_var, right_var]);
115 self.push_clause(vec![gate_var, -left_var, -right_var]);
116 EncodedTerm::Var(gate_var)
117 }
118 NormalizedExpr::Or(left, right) => {
119 let left_term = self.encode_expr(left);
120 let right_term = self.encode_expr(right);
121 let left_var = self.expect_var(left_term, "OR left input");
122 let right_var = self.expect_var(right_term, "OR right input");
123 let gate_var = self.allocate_auxiliary_var();
124 self.push_clause(vec![gate_var, -left_var]);
125 self.push_clause(vec![gate_var, -right_var]);
126 self.push_clause(vec![-gate_var, left_var, right_var]);
127 EncodedTerm::Var(gate_var)
128 }
129 NormalizedExpr::Xor(left, right) => {
130 let left_term = self.encode_expr(left);
131 let right_term = self.encode_expr(right);
132 let left_var = self.expect_var(left_term, "XOR left input");
133 let right_var = self.expect_var(right_term, "XOR right input");
134 let gate_var = self.allocate_auxiliary_var();
135 self.push_clause(vec![-left_var, -right_var, -gate_var]);
136 self.push_clause(vec![left_var, right_var, -gate_var]);
137 self.push_clause(vec![left_var, -right_var, gate_var]);
138 self.push_clause(vec![-left_var, right_var, gate_var]);
139 EncodedTerm::Var(gate_var)
140 }
141 }
142 }
143
144 fn expect_var(&self, term: EncodedTerm, context: &str) -> i64 {
145 match term {
146 EncodedTerm::Var(var) => var,
147 EncodedTerm::Const(_) => {
148 panic!("normalized Tseitin encoding produced a constant for {context}")
149 }
150 }
151 }
152
153 fn source_var(&self, name: &str) -> i64 {
154 *self
155 .source_var_ids
156 .get(name)
157 .unwrap_or_else(|| panic!("CircuitSAT variable {name:?} missing from source ordering"))
158 }
159
160 fn allocate_auxiliary_var(&mut self) -> i64 {
161 self.variables
162 .allocate()
163 .unwrap_or_else(|message| panic!("{message}"))
164 }
165
166 fn push_equivalence(&mut self, left: i64, right: i64) {
167 self.push_clause(vec![-left, right]);
168 self.push_clause(vec![left, -right]);
169 }
170
171 fn push_clause(&mut self, literals: Vec<i64>) {
172 self.clauses.push(CNFClause::new(literals));
173 }
174}
175
176fn make_and(left: NormalizedExpr, right: NormalizedExpr) -> NormalizedExpr {
177 NormalizedExpr::And(Box::new(left), Box::new(right))
178}
179
180fn make_or(left: NormalizedExpr, right: NormalizedExpr) -> NormalizedExpr {
181 NormalizedExpr::Or(Box::new(left), Box::new(right))
182}
183
184fn make_xor(left: NormalizedExpr, right: NormalizedExpr) -> NormalizedExpr {
185 NormalizedExpr::Xor(Box::new(left), Box::new(right))
186}
187
188fn build_balanced_expr(
189 mut items: Vec<NormalizedExpr>,
190 combine: fn(NormalizedExpr, NormalizedExpr) -> NormalizedExpr,
191) -> NormalizedExpr {
192 if items.len() == 1 {
193 return items.pop().expect("single item exists");
194 }
195
196 let right = items.split_off(items.len() / 2);
197 combine(
198 build_balanced_expr(items, combine),
199 build_balanced_expr(right, combine),
200 )
201}
202
203fn normalize_expr(expr: &BooleanExpr) -> NormalizedExpr {
204 match &expr.op {
205 BooleanOp::Var(name) => NormalizedExpr::Var(name.clone()),
206 BooleanOp::Const(value) => NormalizedExpr::Const(*value),
207 BooleanOp::Not(inner) => match normalize_expr(inner) {
208 NormalizedExpr::Const(value) => NormalizedExpr::Const(!value),
209 NormalizedExpr::Not(grandchild) => *grandchild,
210 normalized => NormalizedExpr::Not(Box::new(normalized)),
211 },
212 BooleanOp::And(args) => normalize_nary_gate(args, false, true, make_and),
213 BooleanOp::Or(args) => normalize_nary_gate(args, true, false, make_or),
214 BooleanOp::Xor(args) => {
215 let mut parity = false;
216 let mut normalized_args = Vec::new();
217
218 for arg in args {
219 match normalize_expr(arg) {
220 NormalizedExpr::Const(value) => parity ^= value,
221 normalized => normalized_args.push(normalized),
222 }
223 }
224
225 match normalized_args.len() {
226 0 => NormalizedExpr::Const(parity),
227 1 => {
228 let base = normalized_args.pop().expect("single item exists");
229 if parity {
230 NormalizedExpr::Not(Box::new(base))
231 } else {
232 base
233 }
234 }
235 _ => {
236 let base = build_balanced_expr(normalized_args, make_xor);
237 if parity {
238 NormalizedExpr::Not(Box::new(base))
239 } else {
240 base
241 }
242 }
243 }
244 }
245 }
246}
247
248fn normalize_nary_gate(
249 args: &[BooleanExpr],
250 absorbing_value: bool,
251 identity_value: bool,
252 combine: fn(NormalizedExpr, NormalizedExpr) -> NormalizedExpr,
253) -> NormalizedExpr {
254 let mut normalized_args = Vec::new();
255
256 for arg in args {
257 match normalize_expr(arg) {
258 NormalizedExpr::Const(value) if value == absorbing_value => {
259 return NormalizedExpr::Const(absorbing_value)
260 }
261 NormalizedExpr::Const(value) if value == identity_value => {}
262 normalized => normalized_args.push(normalized),
263 }
264 }
265
266 match normalized_args.len() {
267 0 => NormalizedExpr::Const(identity_value),
268 1 => normalized_args.pop().expect("single item exists"),
269 _ => build_balanced_expr(normalized_args, combine),
270 }
271}
272
273fn build_tseitin_encoding(source: &CircuitSAT) -> TseitinEncoding {
274 TseitinEncoder::new(source).encode_problem(source)
275}
276
277#[derive(Debug, Clone)]
279pub struct ReductionCircuitSATToSAT {
280 target: Satisfiability,
281 source_var_count: usize,
282}
283
284impl ReductionResult for ReductionCircuitSATToSAT {
285 type Source = CircuitSAT;
286 type Target = Satisfiability;
287
288 fn target_problem(&self) -> &Self::Target {
289 &self.target
290 }
291
292 fn extract_solution(
293 &self,
294 target_solution: &<Self::Target as crate::traits::Problem>::Solution,
295 ) -> crate::rules::ExtractionResult<<Self::Source as crate::traits::Problem>::Solution> {
296 crate::rules::traits::validate_target_witness(
297 self.target_problem(),
298 target_solution,
299 |value| value.0,
300 "target witness is not satisfying",
301 )?;
302
303 Ok(target_solution[..self.source_var_count].to_vec())
304 }
305}
306
307#[crate::aggregate_reduction(identity)]
308impl crate::rules::AggregateReductionResult for ReductionCircuitSATToSAT {}
309
310#[reduction(transform = upper_bound {
311 num_vars = "num_variables + 2 * num_expression_nodes",
312 num_clauses = "8 * num_expression_nodes + 2 * num_assignment_outputs",
313 num_literals = "24 * num_expression_nodes + 4 * num_assignment_outputs",
314})]
315impl ReduceTo<Satisfiability> for CircuitSAT {
316 type Result = ReductionCircuitSATToSAT;
317
318 fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
319 let encoding = build_tseitin_encoding(self);
320 Ok(ReductionCircuitSATToSAT {
321 target: Satisfiability::new(encoding.num_vars, encoding.clauses),
322 source_var_count: self.num_variables(),
323 })
324 }
325}
326
327#[cfg(any(test, feature = "example-db"))]
328fn issue_example_source() -> CircuitSAT {
329 use crate::models::formula::Circuit;
330
331 CircuitSAT::new(Circuit::new(vec![Assignment::new(
332 vec!["r".to_string()],
333 BooleanExpr::or(vec![
334 BooleanExpr::and(vec![BooleanExpr::var("x1"), BooleanExpr::var("x2")]),
335 BooleanExpr::and(vec![
336 BooleanExpr::not(BooleanExpr::var("x3")),
337 BooleanExpr::var("x4"),
338 ]),
339 ]),
340 )]))
341}
342
343#[cfg(feature = "example-db")]
344pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
345 use crate::export::SolutionPair;
346 use crate::solvers::BruteForce;
347
348 vec![crate::example_db::specs::RuleExampleSpec {
349 id: "circuitsat_to_satisfiability",
350 build: || {
351 let source = issue_example_source();
352 let source_config = vec![true, true, true, false, true];
353 let reduction =
354 ReduceTo::<Satisfiability>::reduce_to(&source).expect("reduction should succeed");
355 let target_config = BruteForce::new()
356 .find_all_witnesses(reduction.target_problem())
357 .expect("canonical target evaluation must succeed")
358 .into_iter()
359 .find(|candidate| reduction.extract_solution(candidate).unwrap() == source_config)
360 .expect("canonical CircuitSAT -> Satisfiability example must be satisfiable");
361
362 crate::example_db::specs::assemble_rule_example(
363 &source,
364 reduction.target_problem(),
365 vec![SolutionPair {
366 source_config: serde_json::to_value(source_config)
367 .expect("solution serialization must succeed"),
368 target_config: serde_json::to_value(target_config)
369 .expect("solution serialization must succeed"),
370 }],
371 )
372 },
373 }]
374}
375
376#[cfg(test)]
377#[path = "../unit_tests/rules/circuit_sat.rs"]
378mod tests;