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

problemreductions/rules/
satisfiability_nontautology.rs
