diff --git a/Cargo.toml b/Cargo.toml
index b7d776f..ffc21ec 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -22,6 +22,7 @@ tabled = "0.15.0"
 csv = { version = "1.3.0", optional = true }
 tempfile = { version = "3.10.1", optional = true }
 num-bigint = "0.4.4"
+biodivine-lib-bdd = "0.5.16"
 
 pyo3 = { version = "0.21.2", features = ["abi3-py37", "extension-module", "num-bigint"], optional = true }
 
diff --git a/src/bdd/iterators/image.rs b/src/bdd/iterators/image.rs
new file mode 100644
index 0000000..2cc6879
--- /dev/null
+++ b/src/bdd/iterators/image.rs
@@ -0,0 +1,96 @@
+use crate::iterators::DomainIterator;
+use biodivine_lib_bdd::Bdd;
+use biodivine_lib_bdd::BddValuation;
+
+pub struct ImageIterator {
+    domain_iterator: Box<dyn Iterator<Item = Vec<bool>>>,
+    bdd: Bdd,
+}
+
+impl ImageIterator {
+    pub(crate) fn new(input_count: usize, bdd: &Bdd) -> Self {
+        Self {
+            domain_iterator: Box::new(DomainIterator::from_count(input_count)),
+            bdd: bdd.clone(),
+        }
+    }
+}
+
+impl Iterator for ImageIterator {
+    type Item = bool;
+
+    fn next(&mut self) -> Option<Self::Item> {
+        self.domain_iterator
+            .next()
+            .map(|it| self.bdd.eval_in(&BddValuation::new(it)))
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use crate::bdd::Bdd;
+    use crate::expressions::var;
+    use crate::traits::{BooleanFunction, Evaluate};
+    use std::collections::BTreeMap;
+
+    #[test]
+    fn test_image_ok() {
+        let input = Bdd::try_from(var("d") & var("b") | var("a")).expect("Should not panic");
+
+        let mut actual = input.image();
+        let expected = [
+            Some(input.evaluate(&BTreeMap::from([
+                ("a".to_string(), false),
+                ("b".to_string(), false),
+                ("d".to_string(), false),
+            ]))),
+            Some(input.evaluate(&BTreeMap::from([
+                ("a".to_string(), false),
+                ("b".to_string(), false),
+                ("d".to_string(), true),
+            ]))),
+            Some(input.evaluate(&BTreeMap::from([
+                ("a".to_string(), false),
+                ("b".to_string(), true),
+                ("d".to_string(), false),
+            ]))),
+            Some(input.evaluate(&BTreeMap::from([
+                ("a".to_string(), false),
+                ("b".to_string(), true),
+                ("d".to_string(), true),
+            ]))),
+            Some(input.evaluate(&BTreeMap::from([
+                ("a".to_string(), true),
+                ("b".to_string(), false),
+                ("d".to_string(), false),
+            ]))),
+            Some(input.evaluate(&BTreeMap::from([
+                ("a".to_string(), true),
+                ("b".to_string(), false),
+                ("d".to_string(), true),
+            ]))),
+            Some(input.evaluate(&BTreeMap::from([
+                ("a".to_string(), true),
+                ("b".to_string(), true),
+                ("d".to_string(), false),
+            ]))),
+            Some(input.evaluate(&BTreeMap::from([
+                ("a".to_string(), true),
+                ("b".to_string(), true),
+                ("d".to_string(), true),
+            ]))),
+        ];
+
+        assert_eq!(actual.next(), expected[0]);
+        assert_eq!(actual.next(), expected[1]);
+        assert_eq!(actual.next(), expected[2]);
+        assert_eq!(actual.next(), expected[3]);
+        assert_eq!(actual.next(), expected[4]);
+        assert_eq!(actual.next(), expected[5]);
+        assert_eq!(actual.next(), expected[6]);
+        assert_eq!(actual.next(), expected[7]);
+
+        assert_eq!(actual.next(), None);
+        assert_eq!(actual.next(), None);
+    }
+}
diff --git a/src/bdd/iterators/mod.rs b/src/bdd/iterators/mod.rs
new file mode 100644
index 0000000..af1b6a6
--- /dev/null
+++ b/src/bdd/iterators/mod.rs
@@ -0,0 +1,5 @@
+pub use image::ImageIterator;
+pub use support::SupportIterator;
+
+mod image;
+mod support;
diff --git a/src/bdd/iterators/support.rs b/src/bdd/iterators/support.rs
new file mode 100644
index 0000000..8263c11
--- /dev/null
+++ b/src/bdd/iterators/support.rs
@@ -0,0 +1,90 @@
+use biodivine_lib_bdd::{Bdd, OwnedBddSatisfyingValuations};
+
+pub struct SupportIterator {
+    iterator: OwnedBddSatisfyingValuations,
+}
+
+impl SupportIterator {
+    pub(crate) fn new(bdd: &Bdd) -> Self {
+        Self {
+            iterator: bdd.clone().into_sat_valuations(),
+        }
+    }
+}
+
+impl Iterator for SupportIterator {
+    type Item = Vec<bool>;
+
+    fn next(&mut self) -> Option<Self::Item> {
+        self.iterator.next().map(|it| it.vector())
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use crate::bdd::Bdd;
+    use crate::expressions::var;
+    use crate::traits::{BooleanFunction, Evaluate};
+    use std::collections::BTreeMap;
+
+    #[test]
+    fn test_image_ok() {
+        let input = Bdd::try_from(var("d") & var("b") | var("a")).expect("Should not panic here");
+
+        let mut actual = input.image();
+        let expected = [
+            Some(input.evaluate(&BTreeMap::from([
+                ("a".to_string(), false),
+                ("b".to_string(), false),
+                ("d".to_string(), false),
+            ]))),
+            Some(input.evaluate(&BTreeMap::from([
+                ("a".to_string(), false),
+                ("b".to_string(), false),
+                ("d".to_string(), true),
+            ]))),
+            Some(input.evaluate(&BTreeMap::from([
+                ("a".to_string(), false),
+                ("b".to_string(), true),
+                ("d".to_string(), false),
+            ]))),
+            Some(input.evaluate(&BTreeMap::from([
+                ("a".to_string(), false),
+                ("b".to_string(), true),
+                ("d".to_string(), true),
+            ]))),
+            Some(input.evaluate(&BTreeMap::from([
+                ("a".to_string(), true),
+                ("b".to_string(), false),
+                ("d".to_string(), false),
+            ]))),
+            Some(input.evaluate(&BTreeMap::from([
+                ("a".to_string(), true),
+                ("b".to_string(), false),
+                ("d".to_string(), true),
+            ]))),
+            Some(input.evaluate(&BTreeMap::from([
+                ("a".to_string(), true),
+                ("b".to_string(), true),
+                ("d".to_string(), false),
+            ]))),
+            Some(input.evaluate(&BTreeMap::from([
+                ("a".to_string(), true),
+                ("b".to_string(), true),
+                ("d".to_string(), true),
+            ]))),
+        ];
+
+        assert_eq!(actual.next(), expected[0]);
+        assert_eq!(actual.next(), expected[1]);
+        assert_eq!(actual.next(), expected[2]);
+        assert_eq!(actual.next(), expected[3]);
+        assert_eq!(actual.next(), expected[4]);
+        assert_eq!(actual.next(), expected[5]);
+        assert_eq!(actual.next(), expected[6]);
+        assert_eq!(actual.next(), expected[7]);
+
+        assert_eq!(actual.next(), None);
+        assert_eq!(actual.next(), None);
+    }
+}
diff --git a/src/bdd/mod.rs b/src/bdd/mod.rs
new file mode 100644
index 0000000..72c1701
--- /dev/null
+++ b/src/bdd/mod.rs
@@ -0,0 +1,150 @@
+mod iterators;
+mod traits;
+mod utils;
+
+use crate::bdd::utils::{extend_bdd_variables, prune_bdd_variables};
+use biodivine_lib_bdd::{Bdd as InnerBdd, BddVariable, BddVariableSet};
+use std::collections::{BTreeMap, BTreeSet};
+use std::fmt::Debug;
+use std::num::TryFromIntError;
+
+/*
+   Conversions:
+
+   Bdd -> Table: iterate support and use it to fill the table with ones.
+
+   Table -> Bdd: Build a `BddPartialValuation` for each one-row in the table and then
+   use `BddVariableSet::mk_dnf` to build `Bdd`.
+
+   Bdd -> Expression: `Bdd.to_optimized_dnf()` to convert to `Vec<BddPartialValuation>`, then
+   convert each partial valuation to one AND-clause and the whole vector to a disjunction.
+
+   Expression -> Bdd: Run gather literals, create a BddVariableSet, then recursively follow
+   the expression structure. Literal/Constant correspond to BddVariableSet.mk_literal/mk_constant,
+   not/and/or operators correspond to Bdd.not/and/or.
+
+*/
+
+#[derive(Debug, PartialEq, Eq, Clone)]
+pub struct Bdd<TLiteral>
+where
+    TLiteral: Debug + Clone + Eq + Ord,
+{
+    /// Always-sorted vector of no more than 65k variables (see `lib-bdd`).
+    inputs: Vec<TLiteral>,
+    /// Holds the `lib_bdd` representation.
+    bdd: InnerBdd,
+}
+
+impl<TLiteral: Debug + Clone + Eq + Ord> Bdd<TLiteral> {
+    pub(crate) fn new(inner: InnerBdd, inputs: Vec<TLiteral>) -> Self {
+        Self { bdd: inner, inputs }
+    }
+
+    /// Converts a literal representation as a generic user struct
+    /// into `BddVariable` used by `lib_bdd::Bdd`.
+    ///
+    /// If such a variable isn't used in this `Bdd`, the method returns `None`.
+    fn map_var_outer_to_inner(&self, variable: &TLiteral) -> Option<BddVariable> {
+        self.inputs
+            .binary_search(variable)
+            .ok()
+            .map(BddVariable::from_index)
+    }
+
+    /// Converts a `BddVariable` used by `lib_bdd::Bdd` into a literal representation
+    /// used by `self`.
+    ///
+    /// If such a variable isn't used in this `Bdd`, the method returns `None`.
+    pub(crate) fn map_var_inner_to_outer(&self, variable: BddVariable) -> Option<TLiteral> {
+        self.inputs.get(variable.to_index()).cloned()
+    }
+
+    /// Creates a `BddVariableSet` used by `lib_bdd::Bdd`.
+    ///
+    /// Since `lib_bdd` only supports up to 2<sup>16</sup> variables, this method returns an `Err` if
+    /// the number of `variables` is above that.
+    fn make_inner_variable_set(
+        variables: BTreeSet<TLiteral>,
+    ) -> Result<BddVariableSet, TryFromIntError> {
+        let num_vars = u16::try_from(variables.len())?;
+        Ok(BddVariableSet::new_anonymous(num_vars))
+    }
+
+    pub(crate) fn inner(&self) -> &InnerBdd {
+        &self.bdd
+    }
+
+    fn restrict_and_prune_map<TValue>(
+        &self,
+        valuation: &BTreeMap<TLiteral, TValue>,
+        new_bdd: &Bdd<TLiteral>,
+    ) -> Bdd<TLiteral> {
+        self.restrict_and_prune_common(valuation, new_bdd, |set, var| set.contains_key(var))
+    }
+
+    fn restrict_and_prune_set(
+        &self,
+        valuation: &BTreeSet<TLiteral>,
+        new_bdd: &Bdd<TLiteral>,
+    ) -> Bdd<TLiteral> {
+        self.restrict_and_prune_common(valuation, new_bdd, |set, var| set.contains(var))
+    }
+
+    fn restrict_and_prune_common<TCollection, P: Fn(&TCollection, &&TLiteral) -> bool>(
+        &self,
+        valuation: &TCollection,
+        new_bdd: &Bdd<TLiteral>,
+        contains: P,
+    ) -> Bdd<TLiteral> {
+        let restricted_inputs = self
+            .inputs
+            .iter()
+            .filter(|var| !contains(valuation, var))
+            .cloned()
+            .collect::<Vec<_>>();
+        prune_bdd_variables(new_bdd, &restricted_inputs)
+    }
+
+    fn union_and_extend(
+        &self,
+        other: &Bdd<TLiteral>,
+    ) -> (Bdd<TLiteral>, Bdd<TLiteral>, Vec<TLiteral>) {
+        let mut common_inputs = self.inputs.clone();
+        for other in &other.inputs {
+            if !common_inputs.contains(other) {
+                common_inputs.push(other.clone());
+            }
+        }
+        common_inputs.sort();
+
+        let self_lifted = extend_bdd_variables(self, &common_inputs);
+        let other_lifted = extend_bdd_variables(other, &common_inputs);
+
+        (self_lifted, other_lifted, common_inputs)
+    }
+
+    fn union_and_extend_n_ary(
+        &self,
+        others: &mut BTreeMap<TLiteral, Bdd<TLiteral>>,
+    ) -> (Bdd<TLiteral>, Vec<TLiteral>) {
+        let mut common_inputs = self.inputs.clone();
+
+        for other in others.values() {
+            for input in &other.inputs {
+                if !common_inputs.contains(input) {
+                    common_inputs.push(input.clone());
+                }
+            }
+        }
+
+        common_inputs.sort();
+
+        let self_lifted = extend_bdd_variables(self, &common_inputs);
+        for other in others.values_mut() {
+            *other = extend_bdd_variables(other, &common_inputs);
+        }
+
+        (self_lifted, common_inputs)
+    }
+}
diff --git a/src/bdd/traits/bit/and.rs b/src/bdd/traits/bit/and.rs
new file mode 100644
index 0000000..b270320
--- /dev/null
+++ b/src/bdd/traits/bit/and.rs
@@ -0,0 +1,90 @@
+use crate::bdd::traits::bit::bit_common;
+use crate::bdd::Bdd;
+use biodivine_lib_bdd::Bdd as InnerBdd;
+use std::fmt::Debug;
+use std::ops::BitAnd;
+
+impl<TLiteral: Debug + Clone + Eq + Ord + 'static> BitAnd for Bdd<TLiteral> {
+    type Output = Bdd<TLiteral>;
+
+    fn bitand(self, rhs: Self) -> Self::Output {
+        bit_common(self, rhs, InnerBdd::and)
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use crate::bdd::Bdd;
+    use crate::expressions::var;
+    use crate::table::TruthTable;
+    use crate::traits::{BooleanFunction, Implication};
+
+    #[test]
+    fn test_and_same_variables() {
+        let and = var("a") & var("b");
+        let imply = var("a").imply(var("b"));
+
+        let and_table = Bdd::try_from(and.clone()).expect("Should not panic here");
+        let imply_table = Bdd::try_from(imply.clone()).expect("Should not panic here");
+
+        let actual = and_table & imply_table;
+        let expected = Bdd::try_from(and & imply).expect("Should not panic here");
+
+        assert!(actual.is_equivalent(&expected));
+        assert_eq!(actual, expected);
+    }
+
+    #[test]
+    fn test_and_different_variables_1() {
+        let and = var("a") & var("b");
+        let imply = var("b").imply(var("c"));
+
+        let and_table = Bdd::try_from(and.clone()).expect("Should not panic here");
+        let imply_table = Bdd::try_from(imply.clone()).expect("Should not panic here");
+
+        let actual = and_table & imply_table;
+        let expected = Bdd::try_from(and & imply).expect("Should not panic here");
+
+        assert!(actual.is_equivalent(&expected));
+        assert_eq!(actual, expected);
+    }
+
+    #[test]
+    fn test_and_different_variables_2() {
+        let and = var("c") & var("b");
+        let imply = var("a").imply(var("d"));
+
+        let and_table = Bdd::try_from(and.clone()).expect("Should not panic here");
+        let imply_table = Bdd::try_from(imply.clone()).expect("Should not panic here");
+
+        let actual = and_table & imply_table;
+        let expected = Bdd::try_from(and & imply).expect("Should not panic here");
+
+        assert!(actual.is_equivalent(&expected));
+        assert_eq!(actual, expected);
+    }
+
+    #[test]
+    fn test_and_different_variables_3() {
+        let lhs = Bdd::try_from(TruthTable::new(
+            vec!["a", "b"],
+            vec![true, true, false, true],
+        ))
+        .expect("Should not panic here");
+        let rhs = Bdd::try_from(TruthTable::new(
+            vec!["a", "c"],
+            vec![false, true, false, true],
+        ))
+        .expect("Should not panic here");
+
+        let actual = lhs & rhs;
+        let expected = Bdd::try_from(TruthTable::new(
+            vec!["a", "b", "c"],
+            vec![false, true, false, true, false, false, false, true],
+        ))
+        .expect("Should not panic here");
+
+        assert!(actual.is_equivalent(&expected));
+        assert_eq!(actual, expected);
+    }
+}
diff --git a/src/bdd/traits/bit/mod.rs b/src/bdd/traits/bit/mod.rs
new file mode 100644
index 0000000..4be3959
--- /dev/null
+++ b/src/bdd/traits/bit/mod.rs
@@ -0,0 +1,21 @@
+use crate::bdd::Bdd;
+use biodivine_lib_bdd::Bdd as InnerBdd;
+use std::fmt::Debug;
+
+mod and;
+mod or;
+mod xor;
+
+fn bit_common<T: Debug + Clone + Ord, F: Fn(&InnerBdd, &InnerBdd) -> InnerBdd>(
+    me: Bdd<T>,
+    other: Bdd<T>,
+    op: F,
+) -> Bdd<T> {
+    if me.inputs == other.inputs {
+        Bdd::new(op(&me.bdd, &other.bdd), me.inputs.clone())
+    } else {
+        let (self_lifted, rhs_lifted, common_inputs) = me.union_and_extend(&other);
+
+        Bdd::new(op(&self_lifted.bdd, &rhs_lifted.bdd), common_inputs)
+    }
+}
diff --git a/src/bdd/traits/bit/or.rs b/src/bdd/traits/bit/or.rs
new file mode 100644
index 0000000..50d2513
--- /dev/null
+++ b/src/bdd/traits/bit/or.rs
@@ -0,0 +1,100 @@
+use crate::bdd::traits::bit::bit_common;
+use crate::bdd::Bdd;
+use biodivine_lib_bdd::Bdd as InnerBdd;
+use std::fmt::Debug;
+use std::ops::BitOr;
+
+impl<TLiteral: Debug + Clone + Eq + Ord + 'static> BitOr for Bdd<TLiteral> {
+    type Output = Bdd<TLiteral>;
+
+    fn bitor(self, rhs: Self) -> Self::Output {
+        bit_common(self, rhs, InnerBdd::or)
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use crate::bdd::Bdd;
+    use crate::expressions::{var, Expression};
+    use crate::table::TruthTable;
+    use crate::traits::{BooleanFunction, GatherLiterals, Implication};
+
+    #[test]
+    fn test_or_same_variables() {
+        let and = var("a") & var("b");
+        let imply = var("a").imply(var("b"));
+
+        let and_table = Bdd::try_from(and.clone()).expect("Should not panic here");
+        let imply_table = Bdd::try_from(imply.clone()).expect("Should not panic here");
+
+        let actual = and_table | imply_table;
+        let expected = Bdd::try_from(and | imply).expect("Should not panic here");
+
+        assert!(actual.is_equivalent(&expected));
+        assert_eq!(actual, expected);
+    }
+
+    #[test]
+    fn test_or_different_variables_1() {
+        let and = var("a") & var("b");
+        let imply = var("b").imply(var("c"));
+
+        let and_table = Bdd::try_from(and.clone()).expect("Should not panic here");
+        let imply_table = Bdd::try_from(imply.clone()).expect("Should not panic here");
+
+        let actual = and_table | imply_table;
+        let expected = Bdd::try_from(and | imply).expect("Should not panic here");
+
+        assert!(actual.is_equivalent(&expected));
+        assert_eq!(actual, expected);
+    }
+
+    #[test]
+    fn test_or_different_variables_2() {
+        let and = var("c") & var("b");
+        let imply = var("a").imply(var("d"));
+
+        let and_table = Bdd::try_from(and.clone()).expect("Should not panic here");
+        let imply_table = Bdd::try_from(imply.clone()).expect("Should not panic here");
+
+        let actual = and_table | imply_table;
+        let expected = Bdd::try_from(and | imply).expect("Should not panic here");
+
+        assert!(actual.is_equivalent(&expected));
+        assert_eq!(actual, expected);
+    }
+
+    #[test]
+    fn test_or_different_variables_3() {
+        let lhs = Bdd::try_from(TruthTable::new(
+            vec!["a", "b"],
+            vec![true, true, false, true],
+        ))
+        .expect("Should not panic here");
+        let rhs = Bdd::try_from(TruthTable::new(
+            vec!["a", "c"],
+            vec![false, true, false, false],
+        ))
+        .expect("Should not panic here");
+
+        let actual = lhs | rhs;
+        let expected = Bdd::try_from(TruthTable::new(
+            vec!["a", "b", "c"],
+            vec![true, true, true, true, false, true, true, true],
+        ))
+        .expect("Should not panic here");
+
+        println!(
+            "actual: {}",
+            actual.bdd.to_dot_string(
+                &Bdd::make_inner_variable_set(actual.gather_literals()).unwrap(),
+                true
+            )
+        );
+
+        println!("expr: {}", Expression::from(expected.clone()));
+
+        assert!(actual.is_equivalent(&expected));
+        assert_eq!(actual, expected);
+    }
+}
diff --git a/src/bdd/traits/bit/xor.rs b/src/bdd/traits/bit/xor.rs
new file mode 100644
index 0000000..c753a1b
--- /dev/null
+++ b/src/bdd/traits/bit/xor.rs
@@ -0,0 +1,90 @@
+use crate::bdd::traits::bit::bit_common;
+use crate::bdd::Bdd;
+use biodivine_lib_bdd::Bdd as InnerBdd;
+use std::fmt::Debug;
+use std::ops::BitXor;
+
+impl<TLiteral: Debug + Clone + Eq + Ord + 'static> BitXor for Bdd<TLiteral> {
+    type Output = Bdd<TLiteral>;
+
+    fn bitxor(self, rhs: Self) -> Self::Output {
+        bit_common(self, rhs, InnerBdd::xor)
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use crate::bdd::Bdd;
+    use crate::expressions::var;
+    use crate::table::TruthTable;
+    use crate::traits::{BooleanFunction, Implication};
+
+    #[test]
+    fn test_and_same_variables() {
+        let and = var("a") & var("b");
+        let imply = var("a").imply(var("b"));
+
+        let and_table = Bdd::try_from(and.clone()).expect("Should not panic here");
+        let imply_table = Bdd::try_from(imply.clone()).expect("Should not panic here");
+
+        let actual = and_table ^ imply_table;
+        let expected = Bdd::try_from(and ^ imply).expect("Should not panic here");
+
+        assert!(actual.is_equivalent(&expected));
+        assert_eq!(actual, expected);
+    }
+
+    #[test]
+    fn test_and_different_variables_1() {
+        let and = var("a") & var("b");
+        let imply = var("b").imply(var("c"));
+
+        let and_table = Bdd::try_from(and.clone()).expect("Should not panic here");
+        let imply_table = Bdd::try_from(imply.clone()).expect("Should not panic here");
+
+        let actual = and_table ^ imply_table;
+        let expected = Bdd::try_from(and ^ imply).expect("Should not panic here");
+
+        assert!(actual.is_equivalent(&expected));
+        assert_eq!(actual, expected);
+    }
+
+    #[test]
+    fn test_and_different_variables_2() {
+        let and = var("c") & var("b");
+        let imply = var("a").imply(var("d"));
+
+        let and_table = Bdd::try_from(and.clone()).expect("Should not panic here");
+        let imply_table = Bdd::try_from(imply.clone()).expect("Should not panic here");
+
+        let actual = and_table ^ imply_table;
+        let expected = Bdd::try_from(and ^ imply).expect("Should not panic here");
+
+        assert!(actual.is_equivalent(&expected));
+        assert_eq!(actual, expected);
+    }
+
+    #[test]
+    fn test_and_different_variables_3() {
+        let lhs = Bdd::try_from(TruthTable::new(
+            vec!["a", "b"],
+            vec![true, true, false, true],
+        ))
+        .expect("Should not panic here");
+        let rhs = Bdd::try_from(TruthTable::new(
+            vec!["a", "c"],
+            vec![false, true, false, true],
+        ))
+        .expect("Should not panic here");
+
+        let actual = lhs | rhs;
+        let expected = Bdd::try_from(TruthTable::new(
+            vec!["a", "b", "c"],
+            vec![true, false, true, false, false, true, true, false],
+        ))
+        .expect("Should not panic here");
+
+        assert!(actual.is_equivalent(&expected));
+        assert_eq!(actual, expected);
+    }
+}
diff --git a/src/bdd/traits/boolean_function.rs b/src/bdd/traits/boolean_function.rs
new file mode 100644
index 0000000..15cdf30
--- /dev/null
+++ b/src/bdd/traits/boolean_function.rs
@@ -0,0 +1,766 @@
+use crate::bdd::iterators::{ImageIterator, SupportIterator};
+use crate::bdd::Bdd;
+use crate::iterators::DomainIterator;
+use crate::traits::{BooleanFunction, BooleanPoint, BooleanValuation};
+use biodivine_lib_bdd::Bdd as InnerBdd;
+use biodivine_lib_bdd::BddVariable;
+use num_bigint::BigUint;
+use std::collections::{BTreeMap, BTreeSet, HashSet};
+use std::fmt::Debug;
+use std::iter::{zip, Zip};
+
+impl<T: Debug + Clone + Ord> BooleanFunction<T> for Bdd<T> {
+    type DomainIterator = DomainIterator;
+    type RangeIterator = ImageIterator;
+    type RelationIterator = Zip<DomainIterator, ImageIterator>;
+    type SupportIterator = SupportIterator;
+
+    fn inputs(&self) -> BTreeSet<T> {
+        self.inputs.iter().cloned().collect()
+    }
+
+    fn essential_inputs(&self) -> BTreeSet<T> {
+        self.bdd
+            .support_set()
+            .into_iter()
+            .map(|var| {
+                // This unwrap is safe unless the BDD has variables that we don't know about.
+                self.map_var_inner_to_outer(var).unwrap()
+            })
+            .collect()
+    }
+
+    fn essential_degree(&self) -> usize {
+        self.bdd.support_set().len()
+    }
+
+    fn domain(&self) -> Self::DomainIterator {
+        DomainIterator::from_count(self.inputs.len())
+    }
+
+    fn image(&self) -> Self::RangeIterator {
+        ImageIterator::new(self.inputs.len(), &self.bdd)
+    }
+
+    fn relation(&self) -> Self::RelationIterator {
+        // zip domain/range
+        zip(self.domain(), self.image())
+    }
+
+    fn support(&self) -> Self::SupportIterator {
+        SupportIterator::new(&self.bdd)
+    }
+
+    fn weight(&self) -> BigUint {
+        self.bdd.exact_cardinality().to_biguint().unwrap()
+    }
+
+    fn restrict(&self, valuation: &BooleanValuation<T>) -> Self {
+        let lib_bdd_valuation: Vec<(BddVariable, bool)> = valuation
+            .iter()
+            .filter_map(|(a, b)| self.map_var_outer_to_inner(a).map(|var| (var, *b)))
+            .collect::<Vec<_>>();
+        let new_bdd = Bdd::new(self.bdd.restrict(&lib_bdd_valuation), self.inputs.clone());
+
+        self.restrict_and_prune_map(valuation, &new_bdd)
+    }
+
+    fn substitute(&self, mapping: &BTreeMap<T, Self>) -> Self {
+        // Bdd.substitute exists, but assumes all BDDs share input variables (we need to extend)
+        // and does not eliminate the substituted variable from inputs afterward (we need to prune).
+
+        // Bdd.substitute currently assumes that the substituted functions does not depend on the
+        // substituted variables. This will be solved in lib-bdd, we can just panic for now.
+        if mapping
+            .iter()
+            .any(|(key, value_bdd)| value_bdd.inputs.contains(key))
+        {
+            panic!("Currently not allowed to have the substituted variable also appear in the substituting BDD value");
+        }
+
+        let mut extended_mapping = mapping.clone();
+        let (mut self_lifted, _common_inputs) = self.union_and_extend_n_ary(&mut extended_mapping);
+
+        for (k, v) in extended_mapping.iter() {
+            self_lifted.bdd = self_lifted
+                .bdd
+                .substitute(self_lifted.map_var_outer_to_inner(k).unwrap(), &v.bdd)
+        }
+
+        self_lifted.restrict_and_prune_map(&extended_mapping, &self_lifted)
+    }
+
+    fn sat_point(&self) -> Option<BooleanPoint> {
+        self.bdd.sat_witness().map(|it| it.vector())
+    }
+
+    fn existential_quantification(&self, variables: BTreeSet<T>) -> Self {
+        let lib_bdd_variables = variables
+            .iter()
+            .filter_map(|it| self.map_var_outer_to_inner(it))
+            .collect::<Vec<_>>();
+        let new_bdd = Bdd::new(self.bdd.exists(&lib_bdd_variables), self.inputs.clone());
+
+        self.restrict_and_prune_set(&variables, &new_bdd)
+    }
+
+    fn universal_quantification(&self, variables: BTreeSet<T>) -> Self {
+        let lib_bdd_variables = variables
+            .iter()
+            .filter_map(|it| self.map_var_outer_to_inner(it))
+            .collect::<Vec<_>>();
+        let new_bdd = Bdd::new(self.bdd.for_all(&lib_bdd_variables), self.inputs.clone());
+
+        self.restrict_and_prune_set(&variables, &new_bdd)
+    }
+
+    fn derivative(&self, variables: BTreeSet<T>) -> Self {
+        let lib_bdd_variables = variables
+            .iter()
+            .filter_map(|it| self.map_var_outer_to_inner(it))
+            .collect::<HashSet<_>>();
+        let trigger = |var: BddVariable| lib_bdd_variables.contains(&var);
+
+        let new_bdd = Bdd::new(
+            InnerBdd::binary_op_nested(
+                &self.bdd,
+                &self.bdd,
+                trigger,
+                biodivine_lib_bdd::op_function::and,
+                biodivine_lib_bdd::op_function::xor,
+            ),
+            self.inputs.clone(),
+        );
+
+        self.restrict_and_prune_set(&variables, &new_bdd)
+    }
+
+    fn is_equivalent(&self, other: &Self) -> bool {
+        let (self_lifted, other_lifted, _common_inputs) = self.union_and_extend(other);
+
+        self_lifted.bdd == other_lifted.bdd
+    }
+
+    fn is_implied_by(&self, other: &Self) -> bool {
+        let (self_lifted, other_lifted, _common_inputs) = self.union_and_extend(other);
+
+        other_lifted.bdd.imp(&self_lifted.bdd).is_true()
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+    use crate::expressions::{bool, var, Expression};
+    use crate::table::TruthTable;
+    use crate::traits::{Evaluate, GatherLiterals, Implication};
+    use crate::utils::btreeset_to_valuation;
+
+    #[test]
+    fn test_inputs_ok() {
+        for var_count in 0..100 {
+            let vars = (0..var_count).map(var).collect::<Vec<_>>();
+            let input = Bdd::try_from(Expression::n_ary_and(&vars)).expect("Should not panic here");
+
+            let expected = BTreeSet::from_iter((0..var_count).map(|c| c.to_string()));
+            let actual = input.inputs();
+
+            assert_eq!(actual, expected);
+        }
+    }
+
+    #[test]
+    fn test_essential_inputs_all_inputs_ok() {
+        let input = Bdd::try_from(var("a") & var("b")).expect("Should not panic here");
+
+        let actual = input.essential_inputs();
+        let expected = BTreeSet::from_iter(["a".to_string(), "b".to_string()]);
+        assert_eq!(actual, expected);
+
+        assert_eq!(input.essential_degree(), 2);
+    }
+
+    #[test]
+    fn test_essential_inputs_no_inputs_ok() {
+        let input = Bdd::try_from((var("a") & var("b")).imply(var("c") | !var("c")))
+            .expect("Should not panic here");
+
+        let actual = input.essential_inputs();
+        let expected = BTreeSet::new();
+
+        assert_eq!(actual, expected);
+        assert_eq!(input.essential_degree(), 0);
+    }
+
+    #[test]
+    fn test_essential_inputs_some_inputs_ok() {
+        // the boolean function doesn't depend on Z, but does on X and Y
+        // "x,y,z,output\n",
+        // "0,0,1,1\n",
+        // "0,0,0,1\n",
+        // "0,1,1,0\n",
+        // "0,1,0,0\n",
+        // "1,0,1,0\n",
+        // "1,0,0,0\n",
+        // "1,1,1,0\n",
+        // "1,1,0,0\n",
+
+        let input = Bdd::try_from(
+            TruthTable::new(
+                vec!["x", "y", "z"],
+                vec![false, false, true, true, true, true, true, true],
+            )
+            .to_expression_trivial(),
+        )
+        .expect("Should not panic here");
+
+        let actual = input.essential_inputs();
+        let expected = BTreeSet::from_iter(["x", "y"]);
+
+        assert_eq!(actual, expected);
+
+        assert_eq!(input.degree(), 3);
+        assert_eq!(input.essential_degree(), 2);
+    }
+
+    #[test]
+    fn test_essential_inputs_xor_all_inputs_ok() {
+        let input = Bdd::try_from(var("a") ^ var("b")).expect("Should not panic here");
+
+        let actual = input.essential_inputs();
+        let expected = BTreeSet::from_iter(["a".to_string(), "b".to_string()]);
+
+        assert_eq!(actual, expected);
+        assert_eq!(input.essential_degree(), 2);
+    }
+
+    #[test]
+    fn test_domain_ok() {
+        let input = Bdd::try_from(var("d") & var("b") | var("a")).expect("Should not panic here");
+
+        let actual = input.domain().collect::<Vec<_>>();
+
+        let expected = vec![
+            vec![false, false, false],
+            vec![false, false, true],
+            vec![false, true, false],
+            vec![false, true, true],
+            vec![true, false, false],
+            vec![true, false, true],
+            vec![true, true, false],
+            vec![true, true, true],
+        ];
+
+        assert_eq!(actual, expected);
+    }
+
+    #[test]
+    fn test_relation_ok() {
+        let input = Bdd::try_from(var("d") & var("b") | var("a")).expect("Should not panic here");
+
+        let mut actual = input.relation();
+        let expected = vec![
+            vec![false, false, false],
+            vec![false, false, true],
+            vec![false, true, false],
+            vec![false, true, true],
+            vec![true, false, false],
+            vec![true, false, true],
+            vec![true, true, false],
+            vec![true, true, true],
+        ]
+        .into_iter()
+        .map(|point| {
+            Some((
+                point.clone(),
+                input.evaluate(&BTreeMap::from_iter(vec![
+                    ("a".to_string(), point[0]),
+                    ("b".to_string(), point[1]),
+                    ("d".to_string(), point[2]),
+                ])),
+            ))
+        })
+        .collect::<Vec<_>>();
+
+        assert_eq!(actual.next(), expected[0]);
+        assert_eq!(actual.next(), expected[1]);
+        assert_eq!(actual.next(), expected[2]);
+        assert_eq!(actual.next(), expected[3]);
+        assert_eq!(actual.next(), expected[4]);
+        assert_eq!(actual.next(), expected[5]);
+        assert_eq!(actual.next(), expected[6]);
+        assert_eq!(actual.next(), expected[7]);
+
+        assert_eq!(actual.next(), None);
+        assert_eq!(actual.next(), None);
+    }
+
+    #[test]
+    fn test_support_ok() {
+        let input = Bdd::try_from(var("d") & var("b") | var("a")).expect("Should not panic here");
+
+        let actual = BTreeSet::from_iter(input.support());
+        let expected = BTreeSet::from([
+            vec![false, true, true],
+            vec![true, false, false],
+            vec![true, false, true],
+            vec![true, true, false],
+            vec![true, true, true],
+        ]);
+
+        assert_eq!(actual, expected);
+    }
+
+    #[test]
+    fn test_support_2_ok() {
+        let input = Bdd::try_from(var("d") & var("b") | var("c")).expect("Should not panic here");
+
+        let mut actual = input.support();
+        let expected = [
+            Some(vec![false, true, false]),
+            Some(vec![false, true, true]),
+            Some(vec![true, false, true]),
+            Some(vec![true, true, false]),
+            Some(vec![true, true, true]),
+        ];
+
+        assert_eq!(actual.next(), expected[0]);
+        assert_eq!(actual.next(), expected[1]);
+        assert_eq!(actual.next(), expected[2]);
+        assert_eq!(actual.next(), expected[3]);
+        assert_eq!(actual.next(), expected[4]);
+
+        assert_eq!(actual.next(), None);
+        assert_eq!(actual.next(), None);
+    }
+
+    #[test]
+    fn test_no_support_2_ok() {
+        let input = Bdd::try_from(var("a") & !var("a")).expect("Should not panic here");
+
+        let mut actual = input.support();
+
+        assert_eq!(actual.next(), None);
+        assert_eq!(actual.next(), None);
+    }
+
+    #[test]
+    fn test_saturating_point_some() {
+        let input = Bdd::try_from(var("0") & var("1") & var("2")).expect("Should not panic here");
+
+        let actual = input.sat_point();
+        let expected = Some(vec![true, true, true]);
+
+        assert_eq!(actual, expected);
+    }
+
+    #[test]
+    fn test_saturating_none() {
+        // (p ∨ q) ∧ (¬p) ∧ (¬q)
+        let input = Bdd::try_from(Expression::n_ary_and(&[
+            var("a") | var("b"),
+            !var("a"),
+            !var("b"),
+        ]))
+        .expect("Should not panic here");
+
+        let actual = input.sat_point();
+        let expected = None;
+
+        assert_eq!(actual, expected);
+    }
+
+    #[test]
+    fn test_weight_one() {
+        let input = Bdd::try_from(var("0") & var("1") & var("2")).expect("Should not panic here");
+
+        let actual = input.weight();
+        let expected = BigUint::from(1u8);
+
+        assert_eq!(actual, expected);
+    }
+
+    #[test]
+    fn test_weight_zero() {
+        let input = Bdd::try_from(Expression::n_ary_and(&[
+            var("a") | var("b"),
+            !var("a"),
+            !var("b"),
+        ]))
+        .expect("Should not panic here");
+
+        let actual = input.weight();
+        let expected = BigUint::from(0u8);
+
+        assert_eq!(actual, expected);
+    }
+
+    #[test]
+    fn test_weight_all() {
+        // tautology
+        let input = Bdd::try_from(
+            ((var("A").imply(var("B"))) & (!var("A").imply(!var("B")))).imply(var("A")),
+        )
+        .expect("Should not panic here");
+
+        // sanity
+        assert!(input.bdd.is_true());
+
+        let actual = input.weight();
+        let expected = 2usize.pow(input.gather_literals().len() as u32).into();
+
+        assert_eq!(actual, expected);
+    }
+
+    #[test]
+    fn test_restrict_ok() {
+        let input = Bdd::try_from((var("a") | var("b")) & var("c")).expect("Should not panic here");
+        let valuation = BTreeMap::from_iter([("a".to_string(), false), ("c".to_string(), true)]);
+
+        let expected =
+            Bdd::try_from((bool(false) | var("b")) & bool(true)).expect("Should not panic here");
+        let actual = input.restrict(&valuation);
+
+        assert_eq!(expected, actual);
+        assert!(expected.is_equivalent(&actual));
+
+        assert_eq!(actual.degree(), 1);
+    }
+
+    #[test]
+    fn test_restrict_too_many_variables_ok() {
+        let input = Bdd::try_from((var("a") | var("b")) & var("c")).expect("Should not panic here");
+        let valuation = BTreeMap::from_iter([
+            ("a".to_string(), false),
+            ("c".to_string(), true),
+            ("notinthere".to_string(), true),
+        ]);
+
+        let expected =
+            Bdd::try_from((bool(false) | var("b")) & bool(true)).expect("Should not panic here");
+        let actual = input.restrict(&valuation);
+
+        assert_eq!(expected, actual);
+        assert!(expected.is_equivalent(&actual));
+        assert_eq!(actual.degree(), 1);
+    }
+
+    #[test]
+    fn test_restrict_no_variables_ok() {
+        let input = Bdd::try_from((var("a") | var("b")) & var("c")).expect("Should not panic here");
+        let valuation = BTreeMap::new();
+
+        let expected = input.clone();
+        let actual = input.restrict(&valuation);
+
+        assert_eq!(expected, actual);
+        assert!(expected.is_equivalent(&actual));
+        assert_eq!(actual.degree(), expected.degree());
+    }
+
+    #[test]
+    fn test_substitute_no_variables() {
+        let input = Bdd::try_from((var("a") | var("b")) & var("c")).expect("Should not panic here");
+        let valuation = BTreeMap::new();
+
+        let expected = input.clone();
+        let actual = input.substitute(&valuation);
+
+        assert_eq!(expected, actual);
+        assert!(expected.is_equivalent(&actual));
+        assert_eq!(actual.degree(), expected.degree());
+    }
+
+    #[test]
+    #[should_panic]
+    fn test_substitute_variables_same_substituted_ok() {
+        let input = Bdd::try_from((var("a") | var("b")) & var("c") & !var("a") & bool(true))
+            .expect("Should not panic here");
+
+        let new_value = var("a") | !var("b");
+        let new_value_bdd = Bdd::try_from(new_value.clone()).expect("Should not panic here");
+        let mapping = BTreeMap::from_iter([("a".to_string(), new_value_bdd)]);
+
+        // cannot use `var("a") | !var("b") | var("b")` for defining expected here
+        // since that collapses Or(Or(a, !b), b), which substitute doesn't do
+        let expected = Bdd::try_from(
+            Expression::n_ary_or(&[new_value.clone(), var("b")])
+                & var("c")
+                & !new_value.clone()
+                & bool(true),
+        )
+        .expect("Should not panic here");
+        let actual = input.substitute(&mapping);
+
+        assert_eq!(expected, actual);
+        assert!(expected.is_equivalent(&actual));
+        assert_eq!(actual.degree(), expected.degree());
+    }
+
+    #[test]
+    fn test_substitute_variables_same_unsubstituted_ok() {
+        // (a | b) & c & !a & 1
+        let input = Bdd::try_from((var("a") | var("b")) & var("c") & !var("a") & bool(true))
+            .expect("Should not panic here");
+
+        // c | !b
+        let new_value = var("c") | !var("b");
+        let new_value_bdd = Bdd::try_from(new_value.clone()).expect("Should not panic here");
+        let mapping = BTreeMap::from_iter([("a".to_string(), new_value_bdd)]);
+
+        // cannot use `var("a") | !var("b") | var("b")` for defining expected here
+        // since that collapses Or(Or(a, !b), b), which substitute doesn't do
+        // ((c | !b) | b) & c & !(c | !b) & 1
+        let expected = Bdd::try_from(
+            Expression::n_ary_or(&[new_value.clone(), var("b")])
+                & var("c")
+                & !new_value.clone()
+                & bool(true),
+        )
+        .expect("Should not panic here");
+        let actual = input.substitute(&mapping);
+
+        assert_eq!(expected, actual);
+        assert!(expected.is_equivalent(&actual));
+        assert_eq!(actual.degree(), expected.degree());
+    }
+
+    #[test]
+    fn test_substitute_variables_added_only_ok() {
+        let input = Bdd::try_from((var("a") | var("b")) & var("c") & !var("a") & bool(true))
+            .expect("Should not panic here");
+
+        let new_value = var("ddd") & (bool(false));
+        let new_value_bdd = Bdd::try_from(new_value.clone()).expect("Should not panic here");
+        let mapping = BTreeMap::from_iter([("a".to_string(), new_value_bdd)]);
+
+        // cannot use bitwise operators for defining expected here
+        // since that collapses Or(Or(a, !b), b), which substitute doesn't do
+        let expected = Bdd::try_from(
+            Expression::n_ary_or(&[new_value.clone(), var("b")])
+                & var("c")
+                & !new_value.clone()
+                & bool(true),
+        )
+        .expect("Should not panic here");
+        let actual = input.substitute(&mapping);
+
+        assert_eq!(expected, actual);
+        assert!(expected.is_equivalent(&actual));
+
+        assert_eq!(input.degree(), 3);
+        assert_eq!(actual.degree(), 3);
+        assert_eq!(actual.degree(), expected.degree());
+    }
+
+    #[test]
+    #[should_panic]
+    fn test_substitute_variables_added_and_substituted_ok() {
+        let input = Bdd::try_from((var("a") | var("b")) & var("c") & !var("a") & bool(true))
+            .expect("Should not panic here");
+
+        let new_value = var("ddd") & (bool(false) | var("a"));
+        let new_value_bdd = Bdd::try_from(new_value.clone()).expect("Should not panic here");
+        let mapping = BTreeMap::from_iter([("a".to_string(), new_value_bdd)]);
+
+        // cannot use bitwise operators for defining expected here
+        // since that collapses Or(Or(a, !b), b), which substitute doesn't do
+        let expected = Bdd::try_from(
+            Expression::n_ary_or(&[new_value.clone(), var("b")])
+                & var("c")
+                & !new_value.clone()
+                & bool(true),
+        )
+        .expect("Should not panic here");
+        let actual = input.substitute(&mapping);
+
+        assert_eq!(expected, actual);
+        assert!(expected.is_equivalent(&actual));
+
+        assert_eq!(input.degree(), 3);
+        assert_eq!(actual.degree(), 4);
+        assert_eq!(expected.degree(), 4);
+    }
+
+    #[test]
+    fn test_substitute_variables_added_and_unsubstituted_ok() {
+        // (a | b) & c & !a & 1
+        let input = Bdd::try_from((var("a") | var("b")) & var("c") & !var("a") & bool(true))
+            .expect("Should not panic here");
+
+        // ddd & (0 | b)
+        let new_value = var("ddd") & (bool(false) | var("b"));
+        let new_value_bdd = Bdd::try_from(new_value.clone()).expect("Should not panic here");
+        let mapping = BTreeMap::from_iter([("a".to_string(), new_value_bdd)]);
+
+        // cannot use bitwise operators for defining expected here
+        // since that collapses Or(Or(a, !b), b), which substitute doesn't do
+        // ((ddd & (0 | b)) | b) & c & !(ddd & (0 | b)) & 1
+        let expected = Bdd::try_from(
+            Expression::n_ary_or(&[new_value.clone(), var("b")])
+                & var("c")
+                & !new_value.clone()
+                & bool(true),
+        )
+        .expect("Should not panic here");
+        let actual = input.substitute(&mapping);
+
+        assert_eq!(expected, actual);
+        assert!(expected.is_equivalent(&actual));
+
+        assert_eq!(input.degree(), 3);
+        assert_eq!(actual.degree(), 3);
+        assert_eq!(expected.degree(), 3);
+    }
+
+    #[test]
+    fn test_substitute_variables_removed_ok() {
+        let input = Bdd::try_from((var("a") | var("b")) & var("c") & !var("a") & bool(true))
+            .expect("Should not panic here");
+
+        let new_value = bool(false);
+        let new_value_bdd = Bdd::try_from(new_value.clone()).expect("Should not panic here");
+        let mapping = BTreeMap::from_iter([("a".to_string(), new_value_bdd)]);
+
+        // cannot use bitwise operators for defining expected here
+        // since that collapses Or(Or(a, !b), b), which substitute doesn't do
+        let expected = Bdd::try_from(
+            Expression::n_ary_or(&[new_value.clone(), var("b")])
+                & var("c")
+                & !new_value.clone()
+                & bool(true),
+        )
+        .expect("Should not panic here");
+        let actual = input.substitute(&mapping);
+
+        assert_eq!(expected, actual);
+        assert!(expected.is_equivalent(&actual));
+
+        assert_eq!(input.degree(), 3);
+        assert_eq!(actual.degree(), 2);
+        assert_eq!(actual.degree(), expected.degree());
+    }
+
+    #[test]
+    fn test_existential_and_ok() {
+        let target = "a".to_string();
+        let set = BTreeSet::from([target.clone()]);
+        let input = Bdd::try_from(var(target.clone()) & var("b")).expect("Should not panic here");
+
+        let actual = input.existential_quantification(set.clone());
+        assert!(!actual.inputs().contains(&target.clone()));
+
+        let evaluated_with_true = actual.evaluate(&btreeset_to_valuation(set.clone(), true));
+        let evaluated_with_false = actual.evaluate(&btreeset_to_valuation(set, false));
+
+        assert_eq!(evaluated_with_true, evaluated_with_false);
+        assert!(!evaluated_with_true)
+    }
+
+    #[test]
+    fn test_existential_or_ok() {
+        let target = "a".to_string();
+        let set = BTreeSet::from([target.clone()]);
+        let input = Bdd::try_from(var(target.clone()) | var("b")).expect("Should not panic here");
+
+        let actual = input.existential_quantification(set.clone());
+        assert!(!actual.inputs().contains(&target.clone()));
+
+        let evaluated_with_true = actual.evaluate(&btreeset_to_valuation(set.clone(), true));
+        let evaluated_with_false = actual.evaluate(&btreeset_to_valuation(set, false));
+
+        assert_eq!(evaluated_with_true, evaluated_with_false);
+        assert!(evaluated_with_true)
+    }
+
+    #[test]
+    fn test_universal_and_ok() {
+        let target = "a".to_string();
+        let set = BTreeSet::from([target.clone()]);
+        let input = Bdd::try_from(var(target.clone()) & var("b")).expect("Should not panic here");
+
+        let actual = input.universal_quantification(set.clone());
+        assert!(!actual.inputs().contains(&target.clone()));
+
+        let evaluated_with_true = actual.evaluate(&btreeset_to_valuation(set.clone(), true));
+        let evaluated_with_false = actual.evaluate(&btreeset_to_valuation(set, false));
+
+        assert_eq!(evaluated_with_true, evaluated_with_false);
+        assert!(!evaluated_with_true)
+    }
+
+    #[test]
+    fn test_universal_or_ok() {
+        let target = "a".to_string();
+        let set = BTreeSet::from([target.clone()]);
+        let input = Bdd::try_from(var(target.clone()) | var("b")).expect("Should not panic here");
+
+        let actual = input.universal_quantification(set.clone());
+        assert!(!actual.inputs().contains(&target.clone()));
+
+        let evaluated_with_true = actual.evaluate(&btreeset_to_valuation(set.clone(), true));
+        let evaluated_with_false = actual.evaluate(&btreeset_to_valuation(set, false));
+
+        assert_eq!(evaluated_with_true, evaluated_with_false);
+        assert!(!evaluated_with_true)
+    }
+
+    #[test]
+    fn test_derivative_and_ok() {
+        let target = "a".to_string();
+        let set = BTreeSet::from([target.clone()]);
+        let input = Bdd::try_from(var(target.clone()) & var("b")).expect("Should not panic here");
+
+        let actual = input.derivative(set.clone());
+        assert!(!actual.inputs().contains(&target.clone()));
+
+        let evaluated_with_true = actual.evaluate(&btreeset_to_valuation(set.clone(), true));
+        let evaluated_with_false = actual.evaluate(&btreeset_to_valuation(set, false));
+
+        assert_eq!(evaluated_with_true, evaluated_with_false);
+        assert!(!evaluated_with_true)
+    }
+
+    #[test]
+    fn test_derivative_or_ok() {
+        let target = "a".to_string();
+        let set = BTreeSet::from([target.clone()]);
+        let input = Bdd::try_from(var(target.clone()) | var("b")).expect("Should not panic here");
+
+        let actual = input.derivative(set.clone());
+        assert!(!actual.inputs().contains(&target.clone()));
+
+        let evaluated_with_true = actual.evaluate(&btreeset_to_valuation(set.clone(), true));
+        let evaluated_with_false = actual.evaluate(&btreeset_to_valuation(set, false));
+
+        assert_eq!(evaluated_with_true, evaluated_with_false);
+        assert!(evaluated_with_true)
+    }
+
+    #[test]
+    fn test_derivative_xor_ok() {
+        let target = "a".to_string();
+        let set = BTreeSet::from([target.clone()]);
+        let input = Bdd::try_from(var(target.clone()) ^ var("b")).expect("Should not panic here");
+
+        let actual = input.derivative(set.clone());
+        assert!(!actual.inputs().contains(&target.clone()));
+
+        let evaluated_with_true = actual.evaluate(&btreeset_to_valuation(set.clone(), true));
+        let evaluated_with_false = actual.evaluate(&btreeset_to_valuation(set, false));
+
+        assert_eq!(evaluated_with_true, evaluated_with_false);
+        assert!(evaluated_with_true)
+    }
+
+    #[test]
+    fn test_is_implied_by_unit_ok() {
+        let f = Bdd::try_from(bool(false)).expect("Should not panic here");
+        let t = Bdd::try_from(bool(true)).expect("Should not panic here");
+
+        assert!(f.is_implied_by(&f));
+        assert!(t.is_implied_by(&f));
+        assert!(!f.is_implied_by(&t));
+        assert!(t.is_implied_by(&t));
+    }
+}
diff --git a/src/bdd/traits/evaluate.rs b/src/bdd/traits/evaluate.rs
new file mode 100644
index 0000000..9716fdf
--- /dev/null
+++ b/src/bdd/traits/evaluate.rs
@@ -0,0 +1,174 @@
+use crate::traits::Evaluate;
+use std::collections::BTreeMap;
+use std::fmt::Debug;
+
+use crate::bdd::Bdd;
+use biodivine_lib_bdd::BddValuation;
+use itertools::Itertools;
+
+impl<TLiteral: Debug + Clone + Eq + Ord> Evaluate<TLiteral> for Bdd<TLiteral> {
+    fn evaluate_with_default(
+        &self,
+        literal_values: &BTreeMap<TLiteral, bool>,
+        default_value: bool,
+    ) -> bool {
+        let v = self
+            .inputs
+            .iter()
+            .map(|input| *literal_values.get(input).unwrap_or(&default_value))
+            .collect_vec();
+
+        self.bdd.eval_in(&BddValuation::new(v))
+    }
+
+    fn evaluate_checked(
+        &self,
+        literal_values: &BTreeMap<TLiteral, bool>,
+    ) -> Result<bool, Vec<TLiteral>> {
+        let (point, errors): (Vec<_>, Vec<_>) = self
+            .inputs
+            .iter()
+            .map(|input| literal_values.get(input).copied().ok_or(input.clone()))
+            .partition_result();
+
+        if !errors.is_empty() {
+            Err(errors)
+        } else {
+            Ok(self.bdd.eval_in(&BddValuation::new(point)))
+        }
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+    use crate::expressions::{bool as boolFn, var};
+
+    #[test]
+    fn test_evaluate_variables_match_and_ok() {
+        let input = Bdd::try_from(!(var("a") & var("b"))).expect("Should not panic here");
+
+        let pairs = [("a", true), ("b", true)];
+        let mapping = BTreeMap::<String, bool>::from_iter(
+            pairs.map(|(name, value)| (name.to_string(), value)),
+        );
+        let expected_base = false;
+
+        assert_eq!(input.evaluate(&mapping), expected_base);
+        assert_eq!(input.evaluate_with_default(&mapping, false), expected_base);
+        assert!(!input.evaluate_with_default(&mapping, true));
+        assert_eq!(input.evaluate_checked(&mapping), Ok(false));
+    }
+
+    #[test]
+    fn test_evaluate_too_many_variables_and_ok() {
+        let input = Bdd::try_from(!(var("a") & var("b"))).expect("Should not panic here");
+
+        let pairs = [("a", true), ("b", true), ("c", false)];
+        let mapping = BTreeMap::<String, bool>::from_iter(
+            pairs.map(|(name, value)| (name.to_string(), value)),
+        );
+        let expected_base = false;
+
+        assert_eq!(input.evaluate(&mapping), expected_base);
+        assert_eq!(input.evaluate_with_default(&mapping, false), expected_base);
+        assert!(!input.evaluate_with_default(&mapping, true));
+        assert_eq!(input.evaluate_checked(&mapping), Ok(false));
+    }
+
+    #[test]
+    fn test_evaluate_too_few_variables_and_ok() {
+        let input = Bdd::try_from(!(var("a") & var("b"))).expect("Should not panic here");
+
+        let pairs = [("a", true)];
+        let mapping = BTreeMap::<String, bool>::from_iter(
+            pairs.map(|(name, value)| (name.to_string(), value)),
+        );
+        let expected_base = true;
+
+        assert_eq!(input.evaluate(&mapping), expected_base);
+        assert_eq!(input.evaluate_with_default(&mapping, false), expected_base);
+        assert!(!input.evaluate_with_default(&mapping, true));
+        assert_eq!(input.evaluate_checked(&mapping), Err(vec!["b".to_string()]));
+    }
+
+    #[test]
+    fn test_evaluate_variables_match_or_ok() {
+        let input = Bdd::try_from(var("a") | var("b")).expect("Should not panic here");
+
+        let pairs = [("a", false), ("b", false)];
+        let mapping = BTreeMap::<String, bool>::from_iter(
+            pairs.map(|(name, value)| (name.to_string(), value)),
+        );
+        let expected_base = false;
+
+        assert_eq!(input.evaluate(&mapping), expected_base);
+        assert_eq!(input.evaluate_with_default(&mapping, false), expected_base);
+        assert!(!input.evaluate_with_default(&mapping, true));
+        assert_eq!(input.evaluate_checked(&mapping), Ok(false));
+    }
+
+    #[test]
+    fn test_evaluate_too_many_variables_or_ok() {
+        let input = Bdd::try_from(var("a") | var("b")).expect("Should not panic here");
+
+        let pairs = [("a", false), ("b", false), ("c", true)];
+        let mapping = BTreeMap::<String, bool>::from_iter(
+            pairs.map(|(name, value)| (name.to_string(), value)),
+        );
+        let expected_base = false;
+
+        assert_eq!(input.evaluate(&mapping), expected_base);
+        assert_eq!(input.evaluate_with_default(&mapping, false), expected_base);
+        assert!(!input.evaluate_with_default(&mapping, true));
+        assert_eq!(input.evaluate_checked(&mapping), Ok(false));
+    }
+
+    #[test]
+    fn test_evaluate_too_few_variables_or_ok() {
+        let input = Bdd::try_from(var("a") | var("b")).expect("Should not panic here");
+
+        let pairs = [("a", false)];
+        let mapping = BTreeMap::<String, bool>::from_iter(
+            pairs.map(|(name, value)| (name.to_string(), value)),
+        );
+        let expected_base = false;
+
+        assert_eq!(input.evaluate(&mapping), expected_base);
+        assert_eq!(input.evaluate_with_default(&mapping, false), expected_base);
+        assert!(input.evaluate_with_default(&mapping, true));
+        assert_eq!(input.evaluate_checked(&mapping), Err(vec!["b".to_string()]));
+    }
+
+    #[test]
+    fn test_evaluate_variables_match_const_ok() {
+        let input = Bdd::try_from(boolFn(true) | boolFn(false)).expect("Should not panic here");
+
+        let pairs: [(&str, bool); 0] = [];
+        let mapping = BTreeMap::<String, bool>::from_iter(
+            pairs.map(|(name, value)| (name.to_string(), value)),
+        );
+        let expected_base = true;
+
+        assert_eq!(input.evaluate(&mapping), expected_base);
+        assert_eq!(input.evaluate_with_default(&mapping, false), expected_base);
+        assert!(input.evaluate_with_default(&mapping, true));
+        assert_eq!(input.evaluate_checked(&mapping), Ok(true));
+    }
+
+    #[test]
+    fn test_evaluate_too_many_variables_const_ok() {
+        let input = Bdd::try_from(boolFn(true) | boolFn(false)).expect("Should not panic here");
+
+        let pairs = [("a", false), ("b", false), ("c", true)];
+        let mapping = BTreeMap::<String, bool>::from_iter(
+            pairs.map(|(name, value)| (name.to_string(), value)),
+        );
+        let expected_base = true;
+
+        assert_eq!(input.evaluate(&mapping), expected_base);
+        assert_eq!(input.evaluate_with_default(&mapping, false), expected_base);
+        assert!(input.evaluate_with_default(&mapping, true));
+        assert_eq!(input.evaluate_checked(&mapping), Ok(true));
+    }
+}
diff --git a/src/bdd/traits/from_expression.rs b/src/bdd/traits/from_expression.rs
new file mode 100644
index 0000000..aee524b
--- /dev/null
+++ b/src/bdd/traits/from_expression.rs
@@ -0,0 +1,112 @@
+use crate::bdd::Bdd;
+use crate::expressions::Expression;
+use crate::expressions::ExpressionNode::{And, Constant, Literal, Not, Or};
+use crate::traits::GatherLiterals;
+use biodivine_lib_bdd::{Bdd as InnerBdd, BddVariable, BddVariableSet};
+use std::collections::BTreeMap;
+use std::fmt::Debug;
+use std::num::TryFromIntError;
+
+impl<T: Debug + Clone + Ord> TryFrom<Expression<T>> for Bdd<T> {
+    type Error = TryFromIntError;
+
+    fn try_from(value: Expression<T>) -> Result<Self, Self::Error> {
+        let literals = value.gather_literals();
+        let mapping = BTreeMap::from_iter(
+            literals
+                .clone()
+                .into_iter()
+                .enumerate()
+                .map(|(index, var)| (var, index)),
+        );
+        let literal_set = Self::make_inner_variable_set(literals.clone())?;
+
+        Ok(Bdd::new(
+            try_from_rec(&value, &literal_set, &mapping),
+            mapping.into_keys().collect(),
+        ))
+    }
+}
+
+fn try_from_rec<T: Debug + Clone + Ord>(
+    expression: &Expression<T>,
+    literal_set: &BddVariableSet,
+    literal_index_map: &BTreeMap<T, usize>,
+) -> InnerBdd {
+    match expression.node() {
+        Literal(t) => {
+            literal_set.mk_var(BddVariable::from_index(*literal_index_map.get(t).expect(
+                "Literal index map should be created from literals occurring in expression",
+            )))
+        }
+        Constant(value) => {
+            if *value {
+                literal_set.mk_true()
+            } else {
+                literal_set.mk_false()
+            }
+        }
+
+        Not(x) => try_from_rec(x, literal_set, literal_index_map).not(),
+        And(values) => values
+            .iter()
+            .map(|e| try_from_rec(e, literal_set, literal_index_map))
+            .reduce(|current, next| current.and(&next))
+            .unwrap_or_else(|| literal_set.mk_true()),
+        Or(values) => values
+            .iter()
+            .map(|e| try_from_rec(e, literal_set, literal_index_map))
+            .reduce(|current, next| current.or(&next))
+            .unwrap_or_else(|| literal_set.mk_false()),
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+    use crate::traits::BooleanFunction;
+    use rstest::rstest;
+    use std::str::FromStr;
+
+    #[test]
+    fn test_bdd_from_expression() {
+        let exp_string = "(b | a & c & false) & !a | true".to_string();
+        let input = Expression::from_str(&exp_string).unwrap();
+        let actual = Bdd::try_from(input).unwrap();
+
+        let inputs = vec!["a".to_string(), "b".to_string(), "c".to_string()];
+        let var_set = BddVariableSet::from(inputs.clone());
+        let inner_bdd = var_set.eval_expression_string(&exp_string);
+        let expected = Bdd::new(inner_bdd, inputs);
+
+        assert!(actual.is_equivalent(&expected))
+    }
+
+    #[test]
+    fn test_bdd_from_expression_n_ary() {
+        let exp_string = "(a | b | c) | (!a & !b & !c)".to_string();
+        let input = Expression::from_str(&exp_string).unwrap();
+        let actual = Bdd::try_from(input).unwrap();
+
+        let inputs = vec!["a".to_string(), "b".to_string(), "c".to_string()];
+        let var_set = BddVariableSet::from(inputs.clone());
+        let inner_bdd = var_set.eval_expression_string(&exp_string);
+        let expected = Bdd::new(inner_bdd, inputs);
+
+        assert!(actual.is_equivalent(&expected))
+    }
+
+    #[rstest]
+    fn test_bdd_from_expression_const(#[values("true", "false")] exp_string: &str) {
+        let input = Expression::from_str(exp_string).unwrap();
+        let actual = Bdd::try_from(input).unwrap();
+
+        let inputs = vec![];
+        let var_set = BddVariableSet::from(inputs.clone());
+        let inner_bdd = var_set.eval_expression_string(exp_string);
+        let expected = Bdd::new(inner_bdd, inputs);
+
+        assert!(actual.is_equivalent(&expected));
+        assert_eq!(actual, expected);
+    }
+}
diff --git a/src/bdd/traits/from_table.rs b/src/bdd/traits/from_table.rs
new file mode 100644
index 0000000..6739e0a
--- /dev/null
+++ b/src/bdd/traits/from_table.rs
@@ -0,0 +1,66 @@
+use crate::bdd::Bdd;
+use crate::table::TruthTable;
+use crate::traits::{BooleanFunction, GatherLiterals};
+use biodivine_lib_bdd::{BddPartialValuation, BddVariable};
+use std::fmt::Debug;
+use std::num::TryFromIntError;
+
+impl<T: Debug + Clone + Ord> TryFrom<TruthTable<T>> for Bdd<T> {
+    type Error = TryFromIntError;
+
+    fn try_from(value: TruthTable<T>) -> Result<Self, Self::Error> {
+        let literals = value.gather_literals();
+        let literal_set = Self::make_inner_variable_set(literals.clone())?;
+
+        let valuations = value
+            .domain()
+            .map(|point| {
+                point
+                    .into_iter()
+                    .enumerate()
+                    .map(|(index, value)| (BddVariable::from_index(index), value))
+            })
+            .map(|point_with_index| {
+                BddPartialValuation::from_values(&point_with_index.collect::<Vec<_>>())
+            })
+            .collect::<Vec<_>>();
+
+        Ok(Bdd::new(
+            literal_set.mk_dnf(&valuations),
+            literals.into_iter().collect(),
+        ))
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+    use crate::expressions::Expression;
+    use itertools::Itertools;
+    use std::str::FromStr;
+
+    #[test]
+    fn test_bdd_from_table_too_many_variables_nok() {
+        let disallowed_count = u16::MAX as usize + 1;
+        let inputs = (0..disallowed_count).collect_vec();
+        // not accurate but doesn't effect test result
+        let outputs = vec![true; 2usize.pow(16)];
+
+        let table = TruthTable::new(inputs, outputs);
+        let bdd = Bdd::try_from(table);
+
+        assert!(bdd.is_err());
+    }
+
+    #[test]
+    fn test_bdd_from_table_ok() {
+        let exp_string = "(b | a & c & false) & !a | true".to_string();
+        let source = Expression::from_str(&exp_string).unwrap();
+        let expected = Bdd::try_from(source.clone()).unwrap();
+
+        let input = TruthTable::from(source);
+        let actual = Bdd::try_from(input).unwrap();
+
+        assert!(actual.is_equivalent(&expected));
+    }
+}
diff --git a/src/bdd/traits/gather_literals.rs b/src/bdd/traits/gather_literals.rs
new file mode 100644
index 0000000..1a4e787
--- /dev/null
+++ b/src/bdd/traits/gather_literals.rs
@@ -0,0 +1,11 @@
+use crate::bdd::Bdd;
+use std::collections::BTreeSet;
+use std::fmt::Debug;
+
+use crate::traits::GatherLiterals;
+
+impl<TLiteral: Debug + Clone + Eq + Ord> GatherLiterals<TLiteral> for Bdd<TLiteral> {
+    fn gather_literals_rec(&self, current: &mut BTreeSet<TLiteral>) {
+        current.extend(self.inputs.clone())
+    }
+}
diff --git a/src/bdd/traits/mod.rs b/src/bdd/traits/mod.rs
new file mode 100644
index 0000000..bb3dfbf
--- /dev/null
+++ b/src/bdd/traits/mod.rs
@@ -0,0 +1,6 @@
+mod bit;
+mod boolean_function;
+mod evaluate;
+mod from_expression;
+mod from_table;
+mod gather_literals;
diff --git a/src/bdd/utils/extend_variables.rs b/src/bdd/utils/extend_variables.rs
new file mode 100644
index 0000000..93d35c4
--- /dev/null
+++ b/src/bdd/utils/extend_variables.rs
@@ -0,0 +1,54 @@
+use crate::bdd::Bdd;
+use biodivine_lib_bdd::BddVariable;
+use std::collections::HashMap;
+use std::fmt::Debug;
+
+/// Takes a `Bdd` object and extends it to a new input domain described by `new_inputs`.
+///
+/// Here, extends means that the input variables of the new `Bdd` are exactly `new_inputs`, but
+/// the `Bdd` still represents the same function.
+///
+/// As such, it must hold that `new_inputs` is a superset of `bdd.inputs`. Currently, if this
+/// condition is not satisfied, the method will panic.
+pub fn extend_bdd_variables<TLiteral: Debug + Clone + Eq + Ord>(
+    bdd: &Bdd<TLiteral>,
+    new_inputs: &[TLiteral],
+) -> Bdd<TLiteral> {
+    if bdd.inputs == new_inputs {
+        return bdd.clone();
+    }
+
+    // Test pre-condition.
+    debug_assert!(bdd.inputs.iter().all(|it| new_inputs.contains(it)));
+
+    let mut permutation = HashMap::new();
+
+    // Since both vectors are sorted, we can advance through them simultaneously.
+    // Also, since `bdd.inputs` is a subset of `new_inputs`, we know that every
+    // `bdd.inputs[old_i]` must (eventually) appear in the `new_inputs` iterator, we just
+    // need to skip enough of the new variables.
+    for (old_i, var) in bdd.inputs.iter().enumerate() {
+        let new_i = new_inputs
+            .binary_search(var)
+            .expect("Collection `new_inputs` is not a superset of `bdd.inputs`.");
+
+        if new_i != old_i {
+            permutation.insert(
+                BddVariable::from_index(old_i),
+                BddVariable::from_index(new_i),
+            );
+        }
+    }
+
+    let mut new_bdd = bdd.bdd.clone();
+    unsafe {
+        // These operations are not memory-unsafe, they can just break the BDD
+        // in weird ways if you don't know what you are doing.
+        new_bdd.set_num_vars(u16::try_from(new_inputs.len()).unwrap());
+        if !permutation.is_empty() {
+            new_bdd.rename_variables(&permutation);
+        }
+    }
+
+    Bdd::new(new_bdd, new_inputs.to_owned())
+}
diff --git a/src/bdd/utils/mod.rs b/src/bdd/utils/mod.rs
new file mode 100644
index 0000000..100db23
--- /dev/null
+++ b/src/bdd/utils/mod.rs
@@ -0,0 +1,5 @@
+pub use extend_variables::extend_bdd_variables;
+pub use prune_variables::prune_bdd_variables;
+
+mod extend_variables;
+mod prune_variables;
diff --git a/src/bdd/utils/prune_variables.rs b/src/bdd/utils/prune_variables.rs
new file mode 100644
index 0000000..be738db
--- /dev/null
+++ b/src/bdd/utils/prune_variables.rs
@@ -0,0 +1,72 @@
+use crate::bdd::Bdd;
+use crate::traits::BooleanFunction;
+use biodivine_lib_bdd::BddVariable;
+use std::collections::HashMap;
+use std::fmt::Debug;
+
+/// Takes a `Bdd` object and only retains the variables given in `new_inputs`.
+///
+/// This expects the `Bdd` to only depend on the variables in `new_inputs`, meaning that
+/// `bdd.essential_inputs` is a subset of `new_inputs`. If this is not satisfied, panic.
+pub fn prune_bdd_variables<TLiteral: Debug + Clone + Eq + Ord>(
+    bdd: &Bdd<TLiteral>,
+    new_inputs: &[TLiteral],
+) -> Bdd<TLiteral> {
+    if bdd.inputs == new_inputs {
+        return bdd.clone();
+    }
+
+    // Test pre-condition.
+    debug_assert!(bdd
+        .essential_inputs()
+        .into_iter()
+        .all(|it| new_inputs.contains(&it)));
+
+    let mut permutation = HashMap::new();
+
+    // "Inverse" of `expand_bdd_variables`. This works because both input lists are sorted
+    // and the `new_inputs` is a subset of `bdd.inputs`.
+    for (new_i, var) in new_inputs.iter().enumerate() {
+        let old_i = bdd
+            .inputs
+            .binary_search(var)
+            .expect("Collection `new_inputs` is not a subset of `bdd.inputs`.");
+
+        if new_i != old_i {
+            permutation.insert(
+                BddVariable::from_index(old_i),
+                BddVariable::from_index(new_i),
+            );
+        }
+    }
+
+    let mut new_bdd = bdd.bdd.clone();
+    unsafe {
+        // These operations are not memory-unsafe, they can just break the BDD
+        // in weird ways if you don't know what you are doing.
+        if !permutation.is_empty() {
+            new_bdd.rename_variables(&permutation);
+        }
+        new_bdd.set_num_vars(u16::try_from(new_inputs.len()).unwrap());
+        // Also, notice that here, we are setting the variable count *after*
+        // the permutation, not before, because it is actually decreasing, not
+        // increasing.
+    }
+
+    Bdd::new(new_bdd, new_inputs.to_owned())
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+    use crate::expressions::var;
+
+    #[test]
+    #[should_panic]
+    fn test_prune_variables_nonsubset_nok() {
+        let input = Bdd::try_from(var("a") & var("b")).unwrap();
+        let new_vars = vec!["a".to_string(), "c".to_string()];
+
+        let _ = prune_bdd_variables(&input, &new_vars);
+    }
+}
diff --git a/src/expressions/traits/from_bdd.rs b/src/expressions/traits/from_bdd.rs
new file mode 100644
index 0000000..dd0bc5d
--- /dev/null
+++ b/src/expressions/traits/from_bdd.rs
@@ -0,0 +1,98 @@
+use crate::bdd::Bdd;
+use crate::expressions::{Expression, ExpressionNode};
+use std::fmt::Debug;
+
+impl<T: Debug + Clone + Ord> From<Bdd<T>> for Expression<T> {
+    fn from(value: Bdd<T>) -> Self {
+        if value.inner().is_true() {
+            return ExpressionNode::Constant(true).into();
+        } else if value.inner().is_false() {
+            return ExpressionNode::Constant(false).into();
+        }
+
+        let and_expressions = value
+            .inner()
+            .to_optimized_dnf()
+            .into_iter()
+            .map(|valuation| {
+                let and_inner = valuation
+                    .to_values()
+                    .into_iter()
+                    .map(|(literal, literal_value)| {
+                        let var = value
+                            .map_var_inner_to_outer(literal)
+                            .expect("Literal should come from bdd instance");
+
+                        if literal_value {
+                            ExpressionNode::Literal(var).into()
+                        } else {
+                            Expression::negate(&ExpressionNode::Literal(var).into())
+                        }
+                    })
+                    .collect::<Vec<_>>();
+
+                Expression::n_ary_and(&and_inner)
+            })
+            .collect::<Vec<_>>();
+
+        Expression::n_ary_or(&and_expressions)
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+    use crate::traits::{BooleanFunction, SemanticEq};
+    use biodivine_lib_bdd::BddVariableSet;
+    use rstest::rstest;
+    use std::str::FromStr;
+
+    #[test]
+    fn test_expression_from_bdd_standard() {
+        let exp_string = "(b | a & c) & !a".to_string();
+        let inputs = vec!["a".to_string(), "b".to_string(), "c".to_string()];
+        let var_set = BddVariableSet::from(inputs.clone());
+        let inner_bdd = var_set.eval_expression_string(&exp_string);
+        let bdd = Bdd::new(inner_bdd, inputs);
+
+        let expected = Expression::from_str(&exp_string).unwrap();
+        let actual = Expression::from(bdd);
+
+        assert!(
+            actual.semantic_eq(&expected),
+            "expected: `{expected}`,\nactual: `{actual}`"
+        );
+    }
+
+    #[test]
+    fn test_expression_from_bdd_n_ary() {
+        let exp_string = "(a | b | c) | (!a & !b & !c)".to_string();
+        let inputs = vec!["a".to_string(), "b".to_string(), "c".to_string()];
+        let var_set = BddVariableSet::from(inputs.clone());
+        let inner_bdd = var_set.eval_expression_string(&exp_string);
+        let bdd = Bdd::new(inner_bdd, inputs);
+
+        let expected = Expression::from_str(&exp_string).unwrap();
+        let actual = Expression::from(bdd);
+
+        assert!(
+            actual.semantic_eq(&expected),
+            "expected: `{expected}`,\nactual: `{actual}`"
+        );
+    }
+
+    #[rstest]
+    fn test_bdd_from_expression_const(#[values("true", "false")] exp_string: &str) {
+        let inputs = vec![];
+        let var_set = BddVariableSet::from(inputs.clone());
+        let inner_bdd = var_set.eval_expression_string(exp_string);
+        let bdd = Bdd::new(inner_bdd, inputs);
+
+        let expected = Expression::from_str(exp_string).unwrap();
+        let actual = Expression::from(bdd);
+
+        println!("{expected}, {actual}");
+        assert!(actual.is_equivalent(&expected));
+        assert_eq!(actual, expected);
+    }
+}
diff --git a/src/expressions/traits/mod.rs b/src/expressions/traits/mod.rs
index f758b34..21357a9 100644
--- a/src/expressions/traits/mod.rs
+++ b/src/expressions/traits/mod.rs
@@ -2,6 +2,7 @@ mod bit;
 mod boolean_function;
 mod display;
 mod evaluate;
+mod from_bdd;
 mod gather_literals;
 mod operations;
 mod parse;
diff --git a/src/lib.rs b/src/lib.rs
index 8aa505f..e169546 100644
--- a/src/lib.rs
+++ b/src/lib.rs
@@ -1,3 +1,4 @@
+pub mod bdd;
 #[cfg(feature = "python")]
 mod bindings;
 pub mod expressions;
diff --git a/src/table/traits/bit/or.rs b/src/table/traits/bit/or.rs
index d3cb69e..affc7b2 100644
--- a/src/table/traits/bit/or.rs
+++ b/src/table/traits/bit/or.rs
@@ -18,7 +18,7 @@ mod tests {
     use crate::traits::{Implication, SemanticEq};
 
     #[test]
-    fn test_and_same_variables() {
+    fn test_or_same_variables() {
         let and = var("a") & var("b");
         let imply = var("a").imply(var("b"));
 
@@ -33,7 +33,7 @@ mod tests {
     }
 
     #[test]
-    fn test_and_different_variables_1() {
+    fn test_or_different_variables_1() {
         let and = var("a") & var("b");
         let imply = var("b").imply(var("c"));
 
@@ -48,7 +48,7 @@ mod tests {
     }
 
     #[test]
-    fn test_and_different_variables_2() {
+    fn test_or_different_variables_2() {
         let and = var("c") & var("b");
         let imply = var("a").imply(var("d"));
 
@@ -63,7 +63,7 @@ mod tests {
     }
 
     #[test]
-    fn test_and_different_variables_3() {
+    fn test_or_different_variables_3() {
         let lhs = TruthTable::new(vec!["a", "b"], vec![true, true, false, true]);
         let rhs = TruthTable::new(vec!["a", "c"], vec![false, true, false, true]);
 
diff --git a/src/table/traits/bit/xor.rs b/src/table/traits/bit/xor.rs
index 0034494..639e877 100644
--- a/src/table/traits/bit/xor.rs
+++ b/src/table/traits/bit/xor.rs
@@ -18,7 +18,7 @@ mod tests {
     use crate::traits::{Implication, SemanticEq};
 
     #[test]
-    fn test_and_same_variables() {
+    fn test_xor_same_variables() {
         let and = var("a") & var("b");
         let imply = var("a").imply(var("b"));
 
@@ -33,7 +33,7 @@ mod tests {
     }
 
     #[test]
-    fn test_and_different_variables_1() {
+    fn test_xor_different_variables_1() {
         let and = var("a") & var("b");
         let imply = var("b").imply(var("c"));
 
@@ -48,7 +48,7 @@ mod tests {
     }
 
     #[test]
-    fn test_and_different_variables_2() {
+    fn test_xor_different_variables_2() {
         let and = var("c") & var("b");
         let imply = var("a").imply(var("d"));
 
@@ -63,7 +63,7 @@ mod tests {
     }
 
     #[test]
-    fn test_and_different_variables_3() {
+    fn test_xor_different_variables_3() {
         let lhs = TruthTable::new(vec!["a", "b"], vec![true, true, false, true]);
         let rhs = TruthTable::new(vec!["a", "c"], vec![false, true, false, true]);
 
diff --git a/src/table/traits/boolean_function.rs b/src/table/traits/boolean_function.rs
index bb1a58d..84f8d86 100644
--- a/src/table/traits/boolean_function.rs
+++ b/src/table/traits/boolean_function.rs
@@ -8,7 +8,7 @@ use crate::utils::{boolean_point_to_valuation, btreeset_to_valuation};
 use std::collections::{BTreeMap, BTreeSet};
 use std::fmt::Debug;
 
-impl<T: Debug + Clone + Ord + 'static> BooleanFunction<T> for TruthTable<T> {
+impl<T: Debug + Clone + Ord> BooleanFunction<T> for TruthTable<T> {
     type DomainIterator = DomainIterator;
     type RangeIterator = ImageIterator;
     type RelationIterator = RelationIterator;
diff --git a/src/table/traits/from_bdd.rs b/src/table/traits/from_bdd.rs
new file mode 100644
index 0000000..4ff7f14
--- /dev/null
+++ b/src/table/traits/from_bdd.rs
@@ -0,0 +1,61 @@
+use crate::bdd::Bdd;
+use crate::table::utils::boolean_point_to_row_index;
+use crate::table::TruthTable;
+use crate::traits::BooleanFunction;
+use std::fmt::Debug;
+
+impl<T: Debug + Clone + Ord> From<Bdd<T>> for TruthTable<T> {
+    fn from(value: Bdd<T>) -> Self {
+        let inputs = value.inputs();
+        let mut outputs = vec![false; 2usize.pow(value.inputs().len() as u32)];
+
+        value
+            .support()
+            .map(|point| boolean_point_to_row_index(&point))
+            .for_each(|index| outputs[index] = true);
+
+        TruthTable::new(inputs.into_iter().collect(), outputs)
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+    use crate::expressions::Expression;
+    use biodivine_lib_bdd::BddVariableSet;
+    use std::str::FromStr;
+
+    #[test]
+    fn test_table_from_bdd_standard() {
+        let exp_string = "(b | a & c) & !a | false".to_string();
+        let inputs = vec!["a".to_string(), "b".to_string(), "c".to_string()];
+        let var_set = BddVariableSet::from(inputs.clone());
+        let inner_bdd = var_set.eval_expression_string(&exp_string);
+        let bdd = Bdd::new(inner_bdd, inputs);
+
+        let expected = TruthTable::from(Expression::from_str(&exp_string).unwrap());
+        let actual = TruthTable::from(bdd);
+
+        assert!(
+            actual.is_equivalent(&expected),
+            "expected: `{expected}`,\nactual: `{actual}`"
+        );
+    }
+
+    #[test]
+    fn test_table_from_bdd_n_ary() {
+        let exp_string = "(a | b | c) | (!a & !b & !c)".to_string();
+        let inputs = vec!["a".to_string(), "b".to_string(), "c".to_string()];
+        let var_set = BddVariableSet::from(inputs.clone());
+        let inner_bdd = var_set.eval_expression_string(&exp_string);
+        let bdd = Bdd::new(inner_bdd, inputs);
+
+        let expected = TruthTable::from(Expression::from_str(&exp_string).unwrap());
+        let actual = TruthTable::from(bdd);
+
+        assert!(
+            actual.is_equivalent(&expected),
+            "expected: `{expected}`,\nactual: `{actual}`"
+        );
+    }
+}
diff --git a/src/table/traits/mod.rs b/src/table/traits/mod.rs
index f19b306..15cd81f 100644
--- a/src/table/traits/mod.rs
+++ b/src/table/traits/mod.rs
@@ -2,6 +2,7 @@ pub mod bit;
 mod boolean_function;
 pub mod display;
 pub mod evaluate;
+pub mod from_bdd;
 pub mod from_expression;
 pub mod gather_literals;
 pub mod power_set;
diff --git a/src/table/utils/bool_point_to_row_index.rs b/src/table/utils/bool_point_to_row_index.rs
new file mode 100644
index 0000000..d5cd0e7
--- /dev/null
+++ b/src/table/utils/bool_point_to_row_index.rs
@@ -0,0 +1,63 @@
+pub fn boolean_point_to_row_index(point: &[bool]) -> usize {
+    point
+        .iter()
+        .rev()
+        .enumerate()
+        .map(|(digit_index, var_is_true)| {
+            if *var_is_true {
+                2_usize.pow(digit_index as u32)
+            } else {
+                0
+            }
+        })
+        .sum()
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    #[test]
+    fn test() {
+        let inputs = [
+            vec![false, false, false, false, false],
+            vec![false, false, false, false, true],
+            vec![false, false, false, true, false],
+            vec![false, false, false, true, true],
+            vec![false, false, true, false, false],
+            vec![false, false, true, false, true],
+            vec![false, false, true, true, false],
+            vec![false, false, true, true, true],
+            vec![false, true, false, false, false],
+            vec![false, true, false, false, true],
+            vec![false, true, false, true, false],
+            vec![false, true, false, true, true],
+            vec![false, true, true, false, false],
+            vec![false, true, true, false, true],
+            vec![false, true, true, true, false],
+            vec![false, true, true, true, true],
+            vec![true, false, false, false, false],
+            vec![true, false, false, false, true],
+            vec![true, false, false, true, false],
+            vec![true, false, false, true, true],
+            vec![true, false, true, false, false],
+            vec![true, false, true, false, true],
+            vec![true, false, true, true, false],
+            vec![true, false, true, true, true],
+            vec![true, true, false, false, false],
+            vec![true, true, false, false, true],
+            vec![true, true, false, true, false],
+            vec![true, true, false, true, true],
+            vec![true, true, true, false, false],
+            vec![true, true, true, false, true],
+            vec![true, true, true, true, false],
+            vec![true, true, true, true, true],
+        ];
+
+        for (expected, input) in inputs.iter().enumerate() {
+            let actual = boolean_point_to_row_index(input);
+
+            assert_eq!(actual, expected);
+        }
+    }
+}
diff --git a/src/table/utils/mod.rs b/src/table/utils/mod.rs
index 1adeb0b..8dca2f0 100644
--- a/src/table/utils/mod.rs
+++ b/src/table/utils/mod.rs
@@ -1,5 +1,7 @@
+pub use bool_point_to_row_index::boolean_point_to_row_index;
 pub use valuation_to_row_index::{
     values_to_row_index, values_to_row_index_checked, values_to_row_index_with_default,
 };
 
+mod bool_point_to_row_index;
 mod valuation_to_row_index;