problemreductions/models/misc/
minimum_disjunctive_normal_form.rs

1//! Minimum Disjunctive Normal Form (DNF) problem implementation.
2//!
3//! Given a Boolean function specified by its truth table, find a DNF formula
4//! with the minimum number of terms (prime implicants) equivalent to the function.
5//! NP-hard (Masek 1979, via reduction from Minimum Cover).
6
7use crate::registry::{FieldInfo, ProblemSchemaEntry};
8use crate::traits::Problem;
9use crate::types::Min;
10use serde::{Deserialize, Serialize};
11
12inventory::submit! {
13    ProblemSchemaEntry {
14        name: "MinimumDisjunctiveNormalForm",
15        display_name: "Minimum Disjunctive Normal Form",
16        aliases: &["MinDNF"],
17        dimensions: &[],
18        category: crate::registry::ProblemCategory::Misc,
19        module_path: module_path!(),
20        description: "Find minimum-term DNF formula equivalent to a Boolean function",
21        fields: &[
22            FieldInfo { name: "num_variables", type_name: "usize", description: "Number of Boolean variables" },
23            FieldInfo { name: "truth_table", type_name: "Vec<bool>", description: "Truth table of length 2^n" },
24        ],
25    }
26}
27
28/// A prime implicant, represented as a pattern over n variables.
29/// Each entry is `Some(true)` (positive literal), `Some(false)` (negative literal),
30/// or `None` (don't care).
31#[derive(Debug, Clone, PartialEq, Eq, Hash, Serialize, Deserialize)]
32pub struct PrimeImplicant {
33    /// Pattern: one entry per variable.
34    pub pattern: Vec<Option<bool>>,
35}
36
37impl PrimeImplicant {
38    /// Check if this prime implicant covers a given minterm (as a bit pattern).
39    pub fn covers(&self, minterm: usize) -> bool {
40        for (i, &p) in self.pattern.iter().enumerate() {
41            if let Some(val) = p {
42                let bit = ((minterm >> (self.pattern.len() - 1 - i)) & 1) == 1;
43                if bit != val {
44                    return false;
45                }
46            }
47        }
48        true
49    }
50}
51
52/// Minimum Disjunctive Normal Form problem.
53///
54/// Given a Boolean function by its truth table, find the minimum number of
55/// prime implicants whose disjunction (OR) is equivalent to the function.
56///
57/// The constructor computes all prime implicants via Quine-McCluskey.
58/// The configuration is a binary selection over prime implicants.
59///
60/// # Example
61///
62/// ```
63/// use problemreductions::models::misc::MinimumDisjunctiveNormalForm;
64/// use problemreductions::{Problem, BruteForce};
65///
66/// // f(x1,x2,x3) = 1 when exactly 1 or 2 variables are true
67/// let truth_table = vec![false, true, true, true, true, true, true, false];
68/// let problem = MinimumDisjunctiveNormalForm::new(3, truth_table);
69/// let solver = BruteForce::new();
70/// let value = solver.solve(&problem).unwrap();
71/// ```
72#[derive(Debug, Clone, Serialize, Deserialize)]
73#[serde(try_from = "MinimumDisjunctiveNormalFormData")]
74pub struct MinimumDisjunctiveNormalForm {
75    /// Number of Boolean variables.
76    num_variables: usize,
77    /// Truth table of length 2^n.
78    truth_table: Vec<bool>,
79    /// Precomputed prime implicants.
80    prime_implicants: Vec<PrimeImplicant>,
81    /// Minterms (indices where truth table is true).
82    minterms: Vec<usize>,
83}
84
85#[derive(Deserialize)]
86struct MinimumDisjunctiveNormalFormData {
87    num_variables: usize,
88    truth_table: Vec<bool>,
89}
90
91impl TryFrom<MinimumDisjunctiveNormalFormData> for MinimumDisjunctiveNormalForm {
92    type Error = crate::registry::ConstructionError;
93    fn try_from(data: MinimumDisjunctiveNormalFormData) -> Result<Self, Self::Error> {
94        Self::try_new(data.num_variables, data.truth_table)
95    }
96}
97
98impl MinimumDisjunctiveNormalForm {
99    /// Create a new MinimumDisjunctiveNormalForm problem.
100    ///
101    /// # Panics
102    /// - If truth_table length != 2^num_variables
103    /// - If the function is identically false (no minterms)
104    pub fn new(num_variables: usize, truth_table: Vec<bool>) -> Self {
105        Self::try_new(num_variables, truth_table).unwrap_or_else(|error| panic!("{error}"))
106    }
107
108    fn try_new(
109        num_variables: usize,
110        truth_table: Vec<bool>,
111    ) -> Result<Self, crate::registry::ConstructionError> {
112        if num_variables == 0 {
113            return Err("Need at least 1 variable".into());
114        }
115        if truth_table.len()
116            != 1usize
117                .checked_shl(
118                    u32::try_from(num_variables).map_err(|_| "truth table size overflows usize")?,
119                )
120                .ok_or("truth table size overflows usize")?
121        {
122            return Err("Truth table must have 2^n entries".into());
123        }
124
125        let minterms: Vec<usize> = truth_table
126            .iter()
127            .enumerate()
128            .filter_map(|(i, &v)| if v { Some(i) } else { None })
129            .collect();
130        if minterms.is_empty() {
131            return Err("Function must have at least one minterm".into());
132        }
133
134        let prime_implicants = compute_prime_implicants(num_variables, &minterms);
135
136        Ok(Self {
137            num_variables,
138            truth_table,
139            prime_implicants,
140            minterms,
141        })
142    }
143
144    /// Get the number of variables.
145    pub fn num_variables(&self) -> usize {
146        self.num_variables
147    }
148
149    /// Get the truth table.
150    pub fn truth_table(&self) -> &[bool] {
151        &self.truth_table
152    }
153
154    /// Get the prime implicants.
155    pub fn prime_implicants(&self) -> &[PrimeImplicant] {
156        &self.prime_implicants
157    }
158
159    /// Get the number of prime implicants.
160    pub fn num_prime_implicants(&self) -> usize {
161        self.prime_implicants.len()
162    }
163
164    /// Get the minterms.
165    pub fn minterms(&self) -> &[usize] {
166        &self.minterms
167    }
168}
169
170impl Problem for MinimumDisjunctiveNormalForm {
171    const NAME: &'static str = "MinimumDisjunctiveNormalForm";
172    type Solution = Vec<bool>;
173    type Value = Min<i64>;
174
175    crate::problem_parameters![
176        ("num_variables", num_variables),
177        ("num_prime_implicants", num_prime_implicants),
178    ];
179
180    fn evaluate(
181        &self,
182        config: &Self::Solution,
183    ) -> Result<Min<i64>, crate::traits::EvaluationError> {
184        Ok({
185            if config.len() != self.prime_implicants.len() {
186                return Err(crate::traits::EvaluationError::InvalidConfiguration(
187                    "implicant-selection length does not match the instance".into(),
188                ));
189            }
190
191            // Collect selected prime implicants
192            let selected: Vec<usize> = config
193                .iter()
194                .enumerate()
195                .filter_map(|(i, &v)| if v { Some(i) } else { None })
196                .collect();
197
198            if selected.is_empty() {
199                return Ok(Min(None));
200            }
201
202            // Check that all minterms are covered
203            for &mt in &self.minterms {
204                let covered = selected
205                    .iter()
206                    .any(|&pi_idx| self.prime_implicants[pi_idx].covers(mt));
207                if !covered {
208                    return Ok(Min(None));
209                }
210            }
211
212            Min(Some(i64::try_from(selected.len()).map_err(|_| {
213                crate::traits::EvaluationError::IntegerOverflow(
214                    "converting DNF term count to i64".into(),
215                )
216            })?))
217        })
218    }
219
220    fn variant() -> Vec<(&'static str, &'static str)> {
221        crate::variant_params![]
222    }
223}
224
225impl crate::solvers::BruteForceProblem for MinimumDisjunctiveNormalForm {
226    fn dimensions(&self) -> Vec<usize> {
227        vec![2; self.prime_implicants.len()]
228    }
229}
230
231crate::declare_variants! {
232    default MinimumDisjunctiveNormalForm => "2^(3^num_variables)",
233}
234
235crate::register_brute_force! {
236    MinimumDisjunctiveNormalForm decode |_, indices: Vec<usize>| crate::config::config_to_bits(&indices),
237}
238
239/// Compute all prime implicants of a Boolean function using Quine-McCluskey.
240///
241/// Each implicant is represented as a Vec<Option<bool>> of length num_variables.
242fn compute_prime_implicants(num_vars: usize, minterms: &[usize]) -> Vec<PrimeImplicant> {
243    use std::collections::HashSet;
244
245    if minterms.is_empty() {
246        return vec![];
247    }
248
249    type Pattern = Vec<Option<bool>>;
250
251    let mut current: Vec<Pattern> = minterms
252        .iter()
253        .map(|&mt| {
254            (0..num_vars)
255                .map(|i| Some(((mt >> (num_vars - 1 - i)) & 1) == 1))
256                .collect()
257        })
258        .collect();
259
260    let mut all_prime: HashSet<Pattern> = HashSet::new();
261
262    loop {
263        let mut next_set: HashSet<Pattern> = HashSet::new();
264        let mut used = vec![false; current.len()];
265
266        for i in 0..current.len() {
267            for j in (i + 1)..current.len() {
268                if let Some(merged) = try_merge(&current[i], &current[j]) {
269                    next_set.insert(merged);
270                    used[i] = true;
271                    used[j] = true;
272                }
273            }
274        }
275
276        for (i, &was_used) in used.iter().enumerate() {
277            if !was_used {
278                all_prime.insert(current[i].clone());
279            }
280        }
281
282        if next_set.is_empty() {
283            break;
284        }
285        current = next_set.into_iter().collect();
286    }
287
288    let mut result: Vec<PrimeImplicant> = all_prime
289        .into_iter()
290        .map(|pattern| PrimeImplicant { pattern })
291        .collect();
292    // Sort for deterministic output (HashSet iteration order is non-deterministic)
293    result.sort_by(|a, b| a.pattern.cmp(&b.pattern));
294    result
295}
296
297/// Try to merge two implicant patterns that differ in exactly one position.
298/// Returns the merged pattern (with that position set to None) or None if they can't merge.
299fn try_merge(a: &[Option<bool>], b: &[Option<bool>]) -> Option<Vec<Option<bool>>> {
300    if a.len() != b.len() {
301        return None;
302    }
303
304    let mut diff_count = 0;
305    let mut diff_pos = 0;
306
307    for (i, (va, vb)) in a.iter().zip(b.iter()).enumerate() {
308        if va != vb {
309            diff_count += 1;
310            diff_pos = i;
311            if diff_count > 1 {
312                return None;
313            }
314        }
315    }
316
317    if diff_count == 1 {
318        let mut merged = a.to_vec();
319        merged[diff_pos] = None;
320        Some(merged)
321    } else {
322        None
323    }
324}
325
326#[cfg(feature = "example-db")]
327pub(crate) fn canonical_model_example_specs() -> Vec<crate::example_db::specs::ModelExampleSpec> {
328    vec![crate::example_db::specs::ModelExampleSpec {
329        id: "minimum_disjunctive_normal_form",
330        instance: Box::new(MinimumDisjunctiveNormalForm::new(
331            3,
332            vec![false, true, true, true, true, true, true, false],
333        )),
334        // Select prime implicants: p1(¬x1∧x2), p4(x1∧¬x3), p5(¬x2∧x3)
335        // The order of PIs depends on the QMC algorithm output.
336        // We'll verify this in tests.
337        optimal_config: serde_json::json!(vec![true, false, false, true, true, false]),
338        optimal_value: serde_json::json!(3),
339    }]
340}
341
342#[cfg(test)]
343#[path = "../../unit_tests/models/misc/minimum_disjunctive_normal_form.rs"]
344mod tests;
problemreductions/models/misc/minimum_disjunctive_normal_form.rs

problemreductions/models/misc/
minimum_disjunctive_normal_form.rs
