problemreductions/rules/
satisfiability_nontautology.rs

1//! Reduction from Satisfiability to NonTautology via negation.
2//!
3//! Negating a CNF formula with De Morgan's law turns each clause into a DNF
4//! disjunct whose literals all have their signs flipped.
5
6use crate::models::formula::{NonTautology, Satisfiability};
7use crate::reduction;
8use crate::rules::traits::{ReduceTo, ReductionResult};
9
10/// Result of reducing SAT to NonTautology.
11#[derive(Debug, Clone)]
12pub struct ReductionSATToNonTautology {
13    target: NonTautology,
14}
15
16impl ReductionResult for ReductionSATToNonTautology {
17    type Source = Satisfiability;
18    type Target = NonTautology;
19
20    fn target_problem(&self) -> &Self::Target {
21        &self.target
22    }
23
24    fn extract_solution(&self, target_solution: &[usize]) -> Vec<usize> {
25        target_solution.to_vec()
26    }
27}
28
29#[reduction(overhead = {
30    num_vars = "num_vars",
31    num_disjuncts = "num_clauses",
32})]
33impl ReduceTo<NonTautology> for Satisfiability {
34    type Result = ReductionSATToNonTautology;
35
36    fn reduce_to(&self) -> Self::Result {
37        let disjuncts = self
38            .clauses()
39            .iter()
40            .map(|clause| clause.literals.iter().map(|&lit| -lit).collect())
41            .collect();
42
43        ReductionSATToNonTautology {
44            target: NonTautology::new(self.num_vars(), disjuncts),
45        }
46    }
47}
48
49#[cfg(feature = "example-db")]
50pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
51    use crate::export::SolutionPair;
52    use crate::models::formula::CNFClause;
53
54    vec![crate::example_db::specs::RuleExampleSpec {
55        id: "satisfiability_to_nontautology",
56        build: || {
57            crate::example_db::specs::rule_example_with_witness::<_, NonTautology>(
58                Satisfiability::new(
59                    3,
60                    vec![
61                        CNFClause::new(vec![1, 2]),
62                        CNFClause::new(vec![-1, 3]),
63                        CNFClause::new(vec![-2, -3]),
64                    ],
65                ),
66                SolutionPair {
67                    source_config: vec![1, 0, 1],
68                    target_config: vec![1, 0, 1],
69                },
70            )
71        },
72    }]
73}
74
75#[cfg(test)]
76#[path = "../unit_tests/rules/satisfiability_nontautology.rs"]
77mod tests;
problemreductions/rules/satisfiability_nontautology.rs

problemreductions/rules/
satisfiability_nontautology.rs
