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::{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        module_path: module_path!(),
18        description: "Find a falsifying assignment for a DNF formula (proving it is not a tautology)",
19        fields: &[
20            FieldInfo { name: "num_vars", type_name: "usize", description: "Number of Boolean variables" },
21            FieldInfo { name: "disjuncts", type_name: "Vec<Vec<i32>>", description: "Disjuncts (each a conjunction of literals) in disjunctive normal form" },
22        ],
23    }
24}
25
26/// Non-Tautology problem.
27///
28/// Given a Boolean formula in DNF (disjunctive normal form) with disjuncts
29/// D_1, ..., D_m, find a truth assignment that makes ALL disjuncts false
30/// (i.e., the formula is not a tautology).
31///
32/// A disjunct is a conjunction (AND) of literals. The DNF formula is the
33/// disjunction (OR) of all disjuncts. The formula is false when every
34/// disjunct is false, which happens when each disjunct has at least one
35/// false literal.
36///
37/// # Example
38///
39/// ```
40/// use problemreductions::models::formula::NonTautology;
41/// use problemreductions::{Problem, Solver, BruteForce};
42///
43/// // (x1 AND x2 AND x3) OR (NOT x1 AND NOT x2 AND NOT x3)
44/// let problem = NonTautology::new(
45///     3,
46///     vec![vec![1, 2, 3], vec![-1, -2, -3]],
47/// );
48///
49/// let solver = BruteForce::new();
50/// let solution = solver.find_witness(&problem);
51/// assert!(solution.is_some());
52/// ```
53#[derive(Debug, Clone, Serialize, Deserialize)]
54pub struct NonTautology {
55    /// Number of variables.
56    num_vars: usize,
57    /// Disjuncts in DNF. Each disjunct is a conjunction of literals
58    /// represented as signed integers (positive = variable, negative = negation).
59    disjuncts: Vec<Vec<i32>>,
60}
61
62impl NonTautology {
63    /// Create a new Non-Tautology problem.
64    ///
65    /// # Panics
66    /// Panics if any literal references a variable outside the range [1, num_vars].
67    pub fn new(num_vars: usize, disjuncts: Vec<Vec<i32>>) -> Self {
68        for (i, disjunct) in disjuncts.iter().enumerate() {
69            for &lit in disjunct {
70                let var = lit.unsigned_abs() as usize;
71                assert!(
72                    var >= 1 && var <= num_vars,
73                    "Disjunct {} contains literal {} referencing variable {} outside range [1, {}]",
74                    i,
75                    lit,
76                    var,
77                    num_vars
78                );
79            }
80        }
81        Self {
82            num_vars,
83            disjuncts,
84        }
85    }
86
87    /// Get the number of variables.
88    pub fn num_vars(&self) -> usize {
89        self.num_vars
90    }
91
92    /// Get the number of disjuncts.
93    pub fn num_disjuncts(&self) -> usize {
94        self.disjuncts.len()
95    }
96
97    /// Get the disjuncts.
98    pub fn disjuncts(&self) -> &[Vec<i32>] {
99        &self.disjuncts
100    }
101
102    /// Check if a literal is true under the given assignment.
103    fn literal_is_true(lit: i32, assignment: &[bool]) -> bool {
104        let var = lit.unsigned_abs() as usize - 1;
105        let value = assignment.get(var).copied().unwrap_or(false);
106        if lit > 0 {
107            value
108        } else {
109            !value
110        }
111    }
112
113    /// Check if all disjuncts are false (the formula evaluates to false).
114    ///
115    /// A disjunct (conjunction of literals) is true iff ALL its literals are true.
116    /// The DNF formula is false iff ALL disjuncts are false, i.e., each disjunct
117    /// has at least one false literal.
118    pub fn is_falsifying(&self, assignment: &[bool]) -> bool {
119        self.disjuncts.iter().all(|disjunct| {
120            // A disjunct is false if at least one literal is false
121            !disjunct
122                .iter()
123                .all(|&lit| Self::literal_is_true(lit, assignment))
124        })
125    }
126}
127
128impl Problem for NonTautology {
129    const NAME: &'static str = "NonTautology";
130    type Value = crate::types::Or;
131
132    fn dims(&self) -> Vec<usize> {
133        vec![2; self.num_vars]
134    }
135
136    fn evaluate(&self, config: &[usize]) -> crate::types::Or {
137        crate::types::Or({
138            let assignment = super::config_to_assignment(config);
139            self.is_falsifying(&assignment)
140        })
141    }
142
143    fn variant() -> Vec<(&'static str, &'static str)> {
144        crate::variant_params![]
145    }
146}
147
148crate::declare_variants! {
149    default NonTautology => "1.307^num_variables",
150}
151
152#[cfg(feature = "example-db")]
153pub(crate) fn canonical_model_example_specs() -> Vec<crate::example_db::specs::ModelExampleSpec> {
154    vec![crate::example_db::specs::ModelExampleSpec {
155        id: "non_tautology",
156        instance: Box::new(NonTautology::new(3, vec![vec![1, 2, 3], vec![-1, -2, -3]])),
157        optimal_config: vec![1, 0, 0],
158        optimal_value: serde_json::json!(true),
159    }]
160}
161
162#[cfg(test)]
163#[path = "../../unit_tests/models/formula/non_tautology.rs"]
164mod tests;
problemreductions/models/formula/non_tautology.rs

problemreductions/models/formula/
non_tautology.rs
