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(
25        &self,
26        target_solution: &<Self::Target as crate::traits::Problem>::Solution,
27    ) -> crate::rules::ExtractionResult<<Self::Source as crate::traits::Problem>::Solution> {
28        crate::rules::traits::validate_target_solution(self.target_problem(), target_solution)?;
29
30        Ok(target_solution.to_vec())
31    }
32}
33
34#[reduction(
35    transform = exact {
36        num_vars = "num_vars",
37        num_disjuncts = "num_clauses",
38    })]
39impl ReduceTo<NonTautology> for Satisfiability {
40    type Result = ReductionSATToNonTautology;
41
42    fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
43        let disjuncts = self
44            .clauses()
45            .iter()
46            .map(|clause| clause.literals.iter().map(|&lit| -lit).collect())
47            .collect();
48
49        Ok(ReductionSATToNonTautology {
50            target: NonTautology::new(self.num_vars(), disjuncts).map_err(|error| {
51                crate::rules::ReductionError::construction::<Satisfiability, NonTautology>(error)
52            })?,
53        })
54    }
55}
56
57#[cfg(feature = "example-db")]
58pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
59    use crate::export::SolutionPair;
60    use crate::models::formula::CNFClause;
61
62    vec![crate::example_db::specs::RuleExampleSpec {
63        id: "satisfiability_to_nontautology",
64        build: || {
65            crate::example_db::specs::rule_example_with_witness::<_, NonTautology>(
66                Satisfiability::new(
67                    3,
68                    vec![
69                        CNFClause::new(vec![1, 2]),
70                        CNFClause::new(vec![-1, 3]),
71                        CNFClause::new(vec![-2, -3]),
72                    ],
73                ),
74                SolutionPair {
75                    source_config: serde_json::json!(vec![true, false, true]),
76                    target_config: serde_json::json!(vec![true, false, true]),
77                },
78            )
79        },
80    }]
81}
82
83#[cfg(test)]
84#[path = "../unit_tests/rules/satisfiability_nontautology.rs"]
85mod tests;
problemreductions/rules/satisfiability_nontautology.rs

problemreductions/rules/
satisfiability_nontautology.rs
