problemreductions/models/formula/
non_tautology.rs

1//! Non-Tautology problem implementation.
2//!
3//! Given a Boolean formula in disjunctive normal form (DNF), determine whether
4//! there exists a truth assignment that makes the formula false — i.e., the
5//! formula is not a tautology.
6
7use crate::registry::{ConstructionError, FieldInfo, ProblemSchemaEntry};
8use crate::traits::Problem;
9use serde::{Deserialize, Serialize};
10
11inventory::submit! {
12    ProblemSchemaEntry {
13        name: "NonTautology",
14        display_name: "Non-Tautology",
15        aliases: &[],
16        dimensions: &[],
17        category: crate::registry::ProblemCategory::Formula,
18        module_path: module_path!(),
19        description: "Find a falsifying assignment for a DNF formula (proving it is not a tautology)",
20        fields: &[
21            FieldInfo { name: "num_vars", type_name: "usize", description: "Number of Boolean variables" },
22            FieldInfo { name: "disjuncts", type_name: "Vec<Vec<i64>>", description: "Disjuncts (each a conjunction of literals) in disjunctive normal form" },
23        ],
24    }
25}
26
27/// Non-Tautology problem.
28///
29/// Given a Boolean formula in DNF (disjunctive normal form) with disjuncts
30/// D_1, ..., D_m, find a truth assignment that makes ALL disjuncts false
31/// (i.e., the formula is not a tautology).
32///
33/// A disjunct is a conjunction (AND) of literals. The DNF formula is the
34/// disjunction (OR) of all disjuncts. The formula is false when every
35/// disjunct is false, which happens when each disjunct has at least one
36/// false literal.
37///
38/// # Example
39///
40/// ```
41/// use problemreductions::models::formula::NonTautology;
42/// use problemreductions::{Problem, BruteForce};
43///
44/// // (x1 AND x2 AND x3) OR (NOT x1 AND NOT x2 AND NOT x3)
45/// let problem = NonTautology::new(
46///     3,
47///     vec![vec![1, 2, 3], vec![-1, -2, -3]],
48/// ).unwrap();
49///
50/// let solver = BruteForce::new();
51/// let solution = solver.solve(&problem).unwrap();
52/// assert!(solution.is_some());
53/// ```
54#[derive(Debug, Clone, Serialize)]
55pub struct NonTautology {
56    /// Number of variables.
57    num_vars: usize,
58    /// Disjuncts in DNF. Each disjunct is a conjunction of literals
59    /// represented as signed integers (positive = variable, negative = negation).
60    disjuncts: Vec<Vec<i64>>,
61}
62
63impl NonTautology {
64    /// Create a new Non-Tautology problem.
65    ///
66    pub fn new(num_vars: usize, disjuncts: Vec<Vec<i64>>) -> Result<Self, ConstructionError> {
67        if num_vars > i64::MAX as usize {
68            return Err(ConstructionError::IntegerOverflow(format!(
69                "num_vars {num_vars} exceeds the SAT literal limit {}",
70                i64::MAX
71            )));
72        }
73        for (i, disjunct) in disjuncts.iter().enumerate() {
74            for &lit in disjunct {
75                if lit == 0 || lit == i64::MIN {
76                    return Err(ConstructionError::Conversion(format!(
77                        "disjunct {i} contains invalid literal {lit}; allowed variable numbers are 1..={num_vars} with either sign"
78                    )));
79                }
80                let var = usize::try_from(lit.unsigned_abs()).map_err(|_| {
81                    ConstructionError::IntegerOverflow(format!(
82                        "literal {lit} magnitude does not fit usize"
83                    ))
84                })?;
85                if var > num_vars {
86                    return Err(ConstructionError::Conversion(format!(
87                        "disjunct {i} contains literal {lit} referencing variable {var} outside range [1, {num_vars}]"
88                    )));
89                }
90            }
91        }
92        Ok(Self {
93            num_vars,
94            disjuncts,
95        })
96    }
97
98    /// Get the number of variables.
99    pub fn num_vars(&self) -> usize {
100        self.num_vars
101    }
102
103    /// Get the number of disjuncts.
104    pub fn num_disjuncts(&self) -> usize {
105        self.disjuncts.len()
106    }
107
108    /// Get the disjuncts.
109    pub fn disjuncts(&self) -> &[Vec<i64>] {
110        &self.disjuncts
111    }
112
113    /// Check if a literal is true under the given assignment.
114    fn literal_is_true(lit: i64, assignment: &[bool]) -> bool {
115        let var = lit.unsigned_abs() as usize - 1;
116        let value = assignment.get(var).copied().unwrap_or(false);
117        if lit > 0 {
118            value
119        } else {
120            !value
121        }
122    }
123
124    /// Check if all disjuncts are false (the formula evaluates to false).
125    ///
126    /// A disjunct (conjunction of literals) is true iff ALL its literals are true.
127    /// The DNF formula is false iff ALL disjuncts are false, i.e., each disjunct
128    /// has at least one false literal.
129    pub fn is_falsifying(&self, assignment: &[bool]) -> bool {
130        self.disjuncts.iter().all(|disjunct| {
131            // A disjunct is false if at least one literal is false
132            !disjunct
133                .iter()
134                .all(|&lit| Self::literal_is_true(lit, assignment))
135        })
136    }
137}
138
139impl<'de> Deserialize<'de> for NonTautology {
140    fn deserialize<D>(deserializer: D) -> Result<Self, D::Error>
141    where
142        D: serde::Deserializer<'de>,
143    {
144        #[derive(Deserialize)]
145        struct Raw {
146            num_vars: usize,
147            disjuncts: Vec<Vec<i64>>,
148        }
149
150        let raw = Raw::deserialize(deserializer)?;
151        Self::new(raw.num_vars, raw.disjuncts).map_err(serde::de::Error::custom)
152    }
153}
154
155impl Problem for NonTautology {
156    const NAME: &'static str = "NonTautology";
157    type Solution = Vec<bool>;
158    type Value = crate::types::Or;
159
160    crate::problem_parameters![("num_disjuncts", num_disjuncts), ("num_vars", num_vars),];
161
162    fn evaluate(
163        &self,
164        config: &Self::Solution,
165    ) -> Result<crate::types::Or, crate::traits::EvaluationError> {
166        if config.len() != self.num_vars {
167            return Err(crate::traits::EvaluationError::InvalidConfiguration(
168                "assignment length does not match the formula variables".into(),
169            ));
170        }
171        Ok(crate::types::Or(self.is_falsifying(config)))
172    }
173
174    fn variant() -> Vec<(&'static str, &'static str)> {
175        crate::variant_params![]
176    }
177}
178
179impl crate::solvers::BruteForceProblem for NonTautology {
180    fn dimensions(&self) -> Vec<usize> {
181        vec![2; self.num_vars]
182    }
183}
184
185crate::declare_variants! {
186    default NonTautology => "1.307^num_vars",
187}
188
189crate::register_brute_force! {
190    NonTautology decode |_, indices: Vec<usize>| crate::config::config_to_bits(&indices),
191}
192
193#[cfg(feature = "example-db")]
194pub(crate) fn canonical_model_example_specs() -> Vec<crate::example_db::specs::ModelExampleSpec> {
195    vec![crate::example_db::specs::ModelExampleSpec {
196        id: "non_tautology",
197        instance: Box::new(
198            NonTautology::new(3, vec![vec![1, 2, 3], vec![-1, -2, -3]])
199                .expect("canonical non-tautology instance must be valid"),
200        ),
201        optimal_config: serde_json::json!(vec![true, false, false]),
202        optimal_value: serde_json::json!(true),
203    }]
204}
205
206#[cfg(test)]
207#[path = "../../unit_tests/models/formula/non_tautology.rs"]
208mod tests;
problemreductions/models/formula/non_tautology.rs

problemreductions/models/formula/
non_tautology.rs
