diff --git a/Cargo.toml b/Cargo.toml
index e30e0ca..739982c 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -8,3 +8,4 @@ unsafe_code = "forbid"
 [workspace.lints.clippy]
 mutable_key_type = "allow"
 module_inception = "allow"
+doc_markdown = "allow"
diff --git a/sddrs/Cargo.toml b/sddrs/Cargo.toml
index 0d87792..46ddde5 100644
--- a/sddrs/Cargo.toml
+++ b/sddrs/Cargo.toml
@@ -6,11 +6,11 @@ authors = ["Josef Podany"]
 repository = "https://github.com/jsfpdn/sdd-rs"
 description = "Bottom-up Sentential Decision Diagram compiler library."
 keywords = [
-    "knowledge-compilation",
+    "knowledge-base",
     "boolean-functions",
-    "sentential-decision-diagrams",
+    "decision-diagrams",
     "model-counting",
-    "satisfiability",
+    "sdd",
 ]
 categories = ["compilers", "data-structures", "mathematics"]
 license = "BSD-3-Clause"
diff --git a/sddrs/lib.rs b/sddrs/lib.rs
index 6942e68..69a2dc5 100644
--- a/sddrs/lib.rs
+++ b/sddrs/lib.rs
@@ -9,13 +9,7 @@
 //! * efficient querying of model count, model enumeration, and equivalence of SDDs,
 //! * dynamic minimization of SDDs via *vtree fragments*,
 //! * garbage collection of dead nodes,
-//! * SDD compilation from CNF in
-//!  [DIMACS](https://www21.in.tum.de/~lammich/2015_SS_Seminar_SAT/resources/dimacs-cnf.pdf) format.
-//!
-//!
-//!
-//!
-//!
+//! * SDD compilation from CNF in [DIMACS](https://www21.in.tum.de/~lammich/2015_SS_Seminar_SAT/resources/dimacs-cnf.pdf) format.
 //!
 //! The following snippet compiles the function `(A ∧ B) ∨ C` to SDD,
 //! computes number of its models, enumerates and prints them to the stdout,
@@ -26,47 +20,45 @@
 //! use sddrs::literal::literal::Polarity;
 //! use bon::arr;
 //!
-//! fn main() {
-//!    let options = options::SddOptions::builder()
-//!        // Create right-linear vtree.
-//!        .vtree_strategy(options::VTreeStragey::RightLinear)
-//!        // Initialize the manager with variables A, B, and C.
-//!        .variables(["A".to_string(), "B".to_string(), "C".to_string()])
-//!        .build();
-//!    let manager = SddManager::new(options);
-//!
-//!    // Retrieve SDDs for literals A, B, and C.
-//!    let a = manager.literal("A", Polarity::Positive).unwrap();
-//!    let b = manager.literal("B", Polarity::Positive).unwrap();
-//!    let c = manager.literal("C", Polarity::Positive).unwrap();
-//!
-//!    // Compute "A ∧ B"
-//!    let a_and_b = manager.conjoin(&a, &b);
-//!    // Compute "(A ∧ B) ∨ C"
-//!    let a_and_b_or_c = manager.disjoin(&a_and_b, &c);
-//!
-//!    let model_count = manager.model_count(&a_and_b_or_c);
-//!    let models = manager.model_enumeration(&a_and_b_or_c);
-//!
-//!    println!("'(A ∧ B) ∨ C' has {model_count} models.");
-//!    println!("They are:\n{models}");
-//!
-//!    let sdd_path = "my_formula.dot"
-//!    let f = File::create(sdd_path).unwrap();
-//!    let mut b = BufWriter::new(f);
-//!    manager
-//!        .draw_sdd(&mut b as &mut dyn std::io::Write, &sdd)
-//!        .unwrap();
-//!
-//!    let vtree_path = "my_vtree.dot"
-//!    let f = File::create(vtree_path).unwrap();
-//!    let mut b = BufWriter::new(f);
-//!    manager
-//!        .draw_vtree(&mut b as &mut dyn std::io::Write)
-//!        .unwrap();
-//!
-//!    println!("Rendered SDD to '{sdd_path}' and vtree to '{vtree_path}'");
-//! }
+//! let options = options::SddOptions::builder()
+//!     // Create right-linear vtree.
+//!     .vtree_strategy(options::VTreeStragey::RightLinear)
+//!     // Initialize the manager with variables A, B, and C.
+//!     .variables(["A".to_string(), "B".to_string(), "C".to_string()])
+//!     .build();
+//! let manager = SddManager::new(options);
+//!
+//! // Retrieve SDDs for literals A, B, and C.
+//! let a = manager.literal("A", Polarity::Positive).unwrap();
+//! let b = manager.literal("B", Polarity::Positive).unwrap();
+//! let c = manager.literal("C", Polarity::Positive).unwrap();
+//!
+//! // Compute "A ∧ B"
+//! let a_and_b = manager.conjoin(&a, &b);
+//! // Compute "(A ∧ B) ∨ C"
+//! let a_and_b_or_c = manager.disjoin(&a_and_b, &c);
+//!
+//! let model_count = manager.model_count(&a_and_b_or_c);
+//! let models = manager.model_enumeration(&a_and_b_or_c);
+//!
+//! println!("'(A ∧ B) ∨ C' has {model_count} models.");
+//! println!("They are:\n{models}");
+//!
+//! let sdd_path = "my_formula.dot"
+//! let f = File::create(sdd_path).unwrap();
+//! let mut b = BufWriter::new(f);
+//! manager
+//!     .draw_sdd(&mut b as &mut dyn std::io::Write, &sdd)
+//!      .unwrap();
+//!
+//! let vtree_path = "my_vtree.dot"
+//! let f = File::create(vtree_path).unwrap();
+//! let mut b = BufWriter::new(f);
+//! manager
+//!     .draw_vtree(&mut b as &mut dyn std::io::Write)
+//!     .unwrap();
+//!
+//! println!("Rendered SDD to '{sdd_path}' and vtree to '{vtree_path}'");
 //! ```
 //!
 //! ---