refactor: remove boolean nodes, introduce flag for special cases

As boolean nodes are removed as a node type.
Instead, the attribute `kind` specifies whether the d-DNNF is a normal one without boolean nodes or a special case.
A special d-DNNF is either a tautology (true root node) or contradiction (false root node).

Author: uulm-janbaudisch

bindings/kotlin/src/test/java/de/softvare/ddnnife/JavaTest.java

@@ -90,4 +90,15 @@ void cnf() {
     void toUIntTest() {
         assertEquals(1, toUInt(1));
     }
+
+    @Test
+    fun trivial() {
+      Ddnnf trivialDdnnf = ddnnfFromFile("../../ddnnife/tests/data/stub_true.nnf", null);
+      assert(trivialDdnnf.isTrivial());
+    }
+
+    @Test
+    fun nonTrivial() {
+      assert(!ddnnf.isTrivial());
+    }
 }

bindings/kotlin/src/test/kotlin/de/softvare/ddnnife/DdnnfTest.kt

@@ -86,4 +86,15 @@ internal class DdnnfTest {
         assertEquals(7481, cnf.clauses().size)
         assertEquals(110642, serialized.length)
     }
+
+    @Test
+    fun trivial() {
+      val trivialDdnnf = Ddnnf.fromFile("../../ddnnife/tests/data/stub_true.nnf", null)
+      assert(trivialDdnnf.isTrivial())
+    }
+
+    @Test
+    fun nonTrivial() {
+      assert(!ddnnf.isTrivial())
+    }
 }

ddnnife/src/cnf/into.rs

@@ -1,4 +1,4 @@
-use crate::{Ddnnf, NodeType};
+use crate::{Ddnnf, DdnnfKind, NodeType};
 use ddnnife_cnf::{Clause, Cnf, Literal};
 use std::collections::HashMap;
 
@@ -91,22 +91,12 @@ impl From<Biconditional> for Clauses {
 
 impl From<&Ddnnf> for Cnf {
     /// Generates an equi-countable CNF representation via Tseitin transformation.
-    ///
-    /// **Note:** The d-DNNF is not allowed to contain boolean nodes in positions other than the root
-    /// node.
     fn from(ddnnf: &Ddnnf) -> Self {
         // Check for special case of boolean root nodes.
-        let root_index = ddnnf.nodes.len() - 1;
-        let root = &ddnnf.nodes[root_index];
-
-        // A `true` root node implicates a model count of `1`.
-        if root.ntype == NodeType::True {
-            return Cnf::with_count_1();
-        }
-
-        // A `false` root node implicates a model count of `0`.
-        if root.ntype == NodeType::False {
-            return Cnf::with_count_0();
+        match ddnnf.kind {
+            DdnnfKind::Tautology => return Cnf::with_count_1(),
+            DdnnfKind::Contradiction => return Cnf::with_count_0(),
+            _ => {}
         }
 
         // Index to keep track of the last variable introduced to reference a Tseitin transformation.
@@ -143,8 +133,6 @@ impl From<&Ddnnf> for Cnf {
                     &mut tseitin_index,
                 ),
                 NodeType::Literal { literal } => *literal as Literal,
-                NodeType::True => unreachable!("Boolean nodes are only allowed as a root node."),
-                NodeType::False => unreachable!("Boolean nodes are only allowed as a root node."),
             };
 
             node_literals[index] = literal;

ddnnife/src/ddnnf.rs

@@ -6,21 +6,35 @@ pub mod node;
 pub mod statistics;
 
 use self::node::Node;
+use crate::NodeType;
 use crate::parser::graph::{DdnnfGraph, rebuild_graph};
 use num::BigInt;
 use petgraph::stable_graph::NodeIndex;
 use std::collections::{HashMap, HashSet};
 use std::fmt::{Display, Formatter};
 use std::path::Path;
 
+/// Value for indicating whether the d-DNNF is a special case: tautology or contradiction.
+/// If it is neither a tautology nor a contradiction, it is non-trivial.
+#[derive(Debug, Default, Copy, Clone, Eq, PartialEq)]
+pub enum DdnnfKind {
+    #[default]
+    NonTrivial,
+    Tautology,
+    Contradiction,
+}
+
 /// A Ddnnf holds all the nodes as a vector, also includes meta data and further information that is used for optimations
 #[derive(Clone, Debug)]
 pub struct Ddnnf {
+    /// Flag indicating whether the d-DNNF is a special case: tautology or contradiction.
+    ///
+    /// **Note:** A d-DNNF representing a tautology or contradiction contains no nodes.
+    pub kind: DdnnfKind,
     /// The actual nodes of the d-DNNF in postorder
     pub nodes: Vec<Node>,
     /// Literals for upwards propagation
     pub literals: HashMap<i32, usize>, // <var_number of the Literal, and the corresponding indize>
-    pub true_nodes: Vec<usize>, // Indices of true nodes. In some cases those nodes needed to have special treatment
     /// The core/dead features of the model corresponding with this ddnnf
     pub core: HashSet<i32>,
     /// An interim save for the marking algorithm
@@ -33,9 +47,9 @@ pub struct Ddnnf {
 impl Default for Ddnnf {
     fn default() -> Self {
         Ddnnf {
+            kind: DdnnfKind::default(),
             nodes: Vec::new(),
             literals: HashMap::new(),
-            true_nodes: Vec::new(),
             core: HashSet::new(),
             md: Vec::new(),
             number_of_variables: 0,
@@ -47,12 +61,12 @@ impl Default for Ddnnf {
 impl Ddnnf {
     /// Creates a new ddnnf including dead and core features
     pub fn new(graph: DdnnfGraph, root: NodeIndex, number_of_variables: u32) -> Ddnnf {
-        let dfs_ig = rebuild_graph(graph, root);
+        let (kind, nodes, literals) = rebuild_graph(graph, root);
 
         let mut ddnnf = Ddnnf {
-            nodes: dfs_ig.0,
-            literals: dfs_ig.1,
-            true_nodes: dfs_ig.2,
+            kind,
+            nodes,
+            literals,
             core: HashSet::new(),
             md: Vec::new(),
             number_of_variables,
@@ -64,6 +78,15 @@ impl Ddnnf {
         ddnnf
     }
 
+    /// Checks whether this d-DNNF is trivial. A trivial d-DNNF is either a tautology or a
+    /// contradiction.
+    pub fn is_trivial(&self) -> bool {
+        match self.kind {
+            DdnnfKind::Tautology | DdnnfKind::Contradiction => true,
+            DdnnfKind::NonTrivial => false,
+        }
+    }
+
     /// Loads a d-DNNF from file.
     pub fn from_file(path: &Path, features: Option<u32>) -> Self {
         crate::parser::build_ddnnf(path, features)
@@ -73,7 +96,11 @@ impl Ddnnf {
     ///
     /// This value is the same during all computations.
     pub fn rc(&self) -> BigInt {
-        self.nodes[self.nodes.len() - 1].count.clone()
+        match self.kind {
+            DdnnfKind::NonTrivial => self.nodes[self.nodes.len() - 1].count.clone(),
+            DdnnfKind::Tautology => BigInt::from(2).pow(self.number_of_variables),
+            DdnnfKind::Contradiction => BigInt::ZERO,
+        }
     }
 
     /// Returns the core features of this d-DNNF.
@@ -96,12 +123,11 @@ impl Ddnnf {
 
     /// Computes the total number of edges in the dDNNF
     pub fn edge_count(&self) -> usize {
-        use crate::NodeType::*;
         let mut total_edges = 0;
 
         for node in self.nodes.iter() {
             match &node.ntype {
-                And { children } | Or { children } => {
+                NodeType::And { children } | NodeType::Or { children } => {
                     total_edges += children.len();
                 }
                 _ => (),

ddnnife/src/ddnnf/anomalies/config_creation.rs

@@ -20,14 +20,19 @@ static ENUMERATION_CACHE: Lazy<Arc<Mutex<HashMap<Vec<i32>, usize>>>> =
     Lazy::new(|| Arc::new(Mutex::new(HashMap::new())));
 
 impl Ddnnf {
-    /// Creates satisfiable complete configurations for a ddnnf and given assumptions
-    /// If the ddnnf on itself or in combination with the assumption is unsatisfiable,
-    /// then we can not create any satisfiable configuration and simply return None.
+    /// Creates satisfiable complete configurations for a d-DNNF and given assumptions.
+    ///
+    /// Returns `None` if the d-DNNF itself or with the assumptions represents a tautology or
+    /// contradiction.
     pub fn enumerate(
         &mut self,
         assumptions: &mut Vec<i32>,
         amount: usize,
     ) -> Option<Vec<Vec<i32>>> {
+        if self.is_trivial() {
+            return None;
+        }
+
         if amount == 0 {
             return Some(Vec::new());
         }
@@ -66,14 +71,21 @@ impl Ddnnf {
     }
 
     /// Generates amount many uniform random samples under a given set of assumptions and a seed.
-    /// Each sample is sorted by the number of the features. Each sample is a complete configuration with #SAT of 1.
-    /// If the ddnnf itself or in combination with the assumptions is unsatisfiable, None is returned.
+    /// Each sample is sorted by the number of the features. Each sample is a complete configuration
+    /// with #SAT of 1.
+    ///
+    /// Returns `None` if the d-DNNF itself or with the assumptions represents a tautology or
+    /// contradiction.
     pub fn uniform_random_sampling(
         &mut self,
         assumptions: &[i32],
         amount: usize,
         seed: u64,
     ) -> Option<Vec<Vec<i32>>> {
+        if self.is_trivial() {
+            return None;
+        }
+
         if !self.preprocess_config_creation(assumptions) {
             return None;
         }
@@ -114,11 +126,6 @@ impl Ddnnf {
             }
         }
 
-        // We can't create a config that contains a true node.
-        // Hence, we have to hide the true node by changing its count to 0
-        for &index in self.true_nodes.iter() {
-            self.nodes[index].temp.set_zero();
-        }
         true
     }
 
@@ -146,11 +153,6 @@ impl Ddnnf {
                 let mut enumeration_child_lists = Vec::new();
 
                 for &child in children {
-                    // skip the true nodes
-                    if self.true_nodes.contains(&child) {
-                        continue;
-                    }
-
                     if &acc_amount < range.1 {
                         let change = (&BigInt::ZERO, min(range.1, &self.nodes[child].temp));
                         enumeration_child_lists.push(self.enumerate_node(change, child));
@@ -215,7 +217,6 @@ impl Ddnnf {
             Literal { literal } => {
                 enumeration_list.push(vec![*literal]);
             }
-            _ => (),
         }
         enumeration_list
     }
@@ -304,7 +305,6 @@ impl Ddnnf {
                     sample_list.push(vec![*literal]);
                 }
             }
-            _ => (),
         }
         sample_list
     }

ddnnife/src/ddnnf/anomalies/sat.rs

@@ -1,4 +1,4 @@
-use crate::{Ddnnf, NodeType::*};
+use crate::{Ddnnf, DdnnfKind, NodeType::*};
 use num::Zero;
 
 impl Ddnnf {
@@ -33,6 +33,12 @@ impl Ddnnf {
         mark: &mut Vec<bool>,
         root_index: Option<usize>,
     ) -> bool {
+        match self.kind {
+            DdnnfKind::Tautology => return true,
+            DdnnfKind::Contradiction => return false,
+            _ => {}
+        }
+
         let root_index = root_index.unwrap_or(self.nodes.len() - 1);
 
         if features.iter().any(|f| self.makes_query_unsat(f)) {

ddnnife/src/ddnnf/anomalies/t_wise_sampling.rs

@@ -7,9 +7,9 @@ mod sat_wrapper;
 mod t_iterator;
 mod t_wise_sampler;
 
-use crate::Ddnnf;
 use crate::ddnnf::extended_ddnnf::ExtendedDdnnf;
 use crate::ddnnf::extended_ddnnf::objective_function::FloatOrd;
+use crate::{Ddnnf, DdnnfKind};
 use SamplingResult::ResultWithSample;
 pub use config::Config;
 use covering_strategies::cover_with_caching_sorted;
@@ -45,6 +45,12 @@ impl Ddnnf {
 
 impl ExtendedDdnnf {
     pub fn sample_t_wise(&self, t: usize) -> SamplingResult {
+        match self.ddnnf.kind {
+            DdnnfKind::Tautology => return SamplingResult::Empty,
+            DdnnfKind::Contradiction => return SamplingResult::Void,
+            _ => {}
+        }
+
         let sat_solver = SatWrapper::new(&self.ddnnf);
         let and_merger = AttributeZippingMerger {
             t,

ddnnife/src/ddnnf/anomalies/t_wise_sampling/t_wise_sampler.rs

@@ -2,10 +2,10 @@ use super::covering_strategies::cover_with_caching;
 use super::sample_merger::{AndMerger, OrMerger, SampleMerger};
 use super::t_iterator::TInteractionIter;
 use super::{Sample, SamplingResult, SatWrapper};
-use crate::Ddnnf;
 use crate::NodeType;
 use crate::ddnnf::extended_ddnnf::ExtendedDdnnf;
 use crate::util::rng;
+use crate::{Ddnnf, DdnnfKind};
 use itertools::Itertools;
 use rand::prelude::SliceRandom;
 use std::cmp::min;
@@ -35,6 +35,12 @@ impl<'a, A: AndMerger, O: OrMerger> TWiseSampler<'a, A, O> {
     }
 
     pub fn sample(&mut self, t: usize) -> SamplingResult {
+        match self.ddnnf.kind {
+            DdnnfKind::Tautology => return SamplingResult::Empty,
+            DdnnfKind::Contradiction => return SamplingResult::Void,
+            _ => {}
+        }
+
         let sat_solver = SatWrapper::new(self.ddnnf);
 
         // Sample each node and keep the result as a partial sample.
@@ -81,6 +87,12 @@ impl<'a, A: AndMerger, O: OrMerger> TWiseSampler<'a, A, O> {
     /// # Panics
     /// Panics if one child does not have a [SamplingResult] in [TWiseSampler::partial_samples].
     pub(crate) fn partial_sample(&mut self, node_id: usize) -> SamplingResult {
+        match self.ddnnf.kind {
+            DdnnfKind::Tautology => return SamplingResult::Empty,
+            DdnnfKind::Contradiction => return SamplingResult::Void,
+            _ => {}
+        }
+
         let node = self.ddnnf.nodes.get(node_id).expect("Node does not exist!");
 
         match &node.ntype {
@@ -97,8 +109,6 @@ impl<'a, A: AndMerger, O: OrMerger> TWiseSampler<'a, A, O> {
                 self.remove_unneeded(node_id, children);
                 sample
             }
-            NodeType::True => SamplingResult::Empty,
-            NodeType::False => SamplingResult::Void,
         }
     }
 

ddnnife/src/ddnnf/counting/default_count.rs

@@ -19,7 +19,6 @@ impl Ddnnf {
                     .map(|&indice| &self.nodes[indice].temp)
                     .sum()
             }
-            False => self.nodes[i].temp.set_zero(),
             _ => self.nodes[i].temp.set_one(), // True and Literal
         }
     }