diff --git a/.github/workflows/rust-compile.yml b/.github/workflows/rust-compile.yml
index 32a5342..3426cf1 100644
--- a/.github/workflows/rust-compile.yml
+++ b/.github/workflows/rust-compile.yml
@@ -40,7 +40,7 @@ jobs:
       - name: Run rustfmt
         uses: actions-rust-lang/rustfmt@559aa3035a47390ba96088dffa783b5d26da9326 # v1
       - name: Run clippy
-        run: cargo clippy --workspace
+        run: cargo clippy --workspace --all-features
 
   test:
     name: Test
@@ -54,6 +54,6 @@ jobs:
         with:
           components: rustfmt
       - name: Build
-        run: cargo build 
+        run: cargo build --all-features
       - name: Run tests
-        run: cargo test --workspace -- --nocapture
+        run: cargo test --workspace --all-features -- --nocapture
diff --git a/Cargo.lock b/Cargo.lock
index fda3b2b..10dbca6 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -381,7 +381,7 @@ dependencies = [
  "encode_unicode",
  "libc",
  "once_cell",
- "unicode-width",
+ "unicode-width 0.2.0",
  "windows-sys",
 ]
 
@@ -627,6 +627,12 @@ version = "0.4.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "fbf6a919d6cf397374f7dfeeea91d974c7c0a7221d0d0f4f20d859d329e53fcc"
 
+[[package]]
+name = "human_bytes"
+version = "0.4.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "91f255a4535024abf7640cb288260811fc14794f62b063652ed349f9a6c2348e"
+
 [[package]]
 name = "indexmap"
 version = "2.7.0"
@@ -992,6 +998,7 @@ dependencies = [
  "elsa",
  "event-listener 5.4.0",
  "futures",
+ "human_bytes",
  "indexmap",
  "insta",
  "itertools",
@@ -1000,6 +1007,7 @@ dependencies = [
  "resolvo",
  "serde",
  "serde_json",
+ "tabwriter",
  "tokio",
  "tracing",
  "tracing-test",
@@ -1160,6 +1168,15 @@ dependencies = [
  "unicode-ident",
 ]
 
+[[package]]
+name = "tabwriter"
+version = "1.4.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "a327282c4f64f6dc37e3bba4c2b6842cc3a992f204fa58d917696a89f691e5f6"
+dependencies = [
+ "unicode-width 0.1.14",
+]
+
 [[package]]
 name = "tap"
 version = "1.0.1"
@@ -1328,6 +1345,12 @@ version = "1.0.14"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "adb9e6ca4f869e1180728b7950e35922a7fc6397f7b641499e8f3ef06e50dc83"
 
+[[package]]
+name = "unicode-width"
+version = "0.1.14"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "7dd6e30e90baa6f72411720665d41d89b9a3d039dc45b8faea1ddd07f617f6af"
+
 [[package]]
 name = "unicode-width"
 version = "0.2.0"
diff --git a/Cargo.toml b/Cargo.toml
index 2b9587e..bd8d3e8 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -4,20 +4,24 @@ resolver = "2"
 
 [workspace.package]
 version = "0.9.0"
-authors = ["Adolfo Ochagavía <github@adolfo.ochagavia.nl>", "Bas Zalmstra <zalmstra.bas@gmail.com>", "Tim de Jager <tdejager89@gmail.com>"]
+authors = [
+    "Adolfo Ochagavía <github@adolfo.ochagavia.nl>",
+    "Bas Zalmstra <zalmstra.bas@gmail.com>",
+    "Tim de Jager <tdejager89@gmail.com>",
+]
 homepage = "https://github.com/mamba-org/resolvo"
 repository = "https://github.com/mamba-org/resolvo"
 license = "BSD-3-Clause"
 edition = "2024"
 readme = "README.md"
 keywords = ["dependency", "solver", "version"]
-categories= ["algorithms"]
+categories = ["algorithms"]
 
 [package]
 name = "resolvo"
 version.workspace = true
 authors.workspace = true
-description= "Fast package resolver written in Rust (CDCL based SAT solving)"
+description = "Fast package resolver written in Rust (CDCL based SAT solving)"
 keywords.workspace = true
 categories.workspace = true
 homepage.workspace = true
@@ -26,6 +30,9 @@ license.workspace = true
 edition.workspace = true
 readme.workspace = true
 
+[features]
+diagnostics = ["tabwriter", "human_bytes"]
+
 [dependencies]
 ahash = "0.8.11"
 itertools = "0.14"
@@ -38,8 +45,14 @@ futures = { version = "0.3", default-features = false, features = ["alloc"] }
 event-listener = "5.4"
 indexmap = "2"
 tokio = { version = "1.42", features = ["rt"], optional = true }
-async-std = { version = "1.13", default-features = false, features = ["alloc", "default"], optional = true }
+async-std = { version = "1.13", default-features = false, features = [
+    "alloc",
+    "default",
+], optional = true }
 version-ranges = { version = "0.1.1", optional = true }
+# Dependencies for the diagnostics feature
+tabwriter = { version = "1.4.0", optional = true }
+human_bytes = { version = "0.4.3", optional = true }
 
 [dev-dependencies]
 insta = "1.42.0"
diff --git a/src/conflict.rs b/src/conflict.rs
index bfa20fd..42b11c6 100644
--- a/src/conflict.rs
+++ b/src/conflict.rs
@@ -631,42 +631,6 @@ impl Indenter {
     }
 }
 
-#[cfg(test)]
-mod tests {
-    use super::*;
-
-    #[test]
-    fn test_indenter_without_top_level_indent() {
-        let indenter = Indenter::new(false);
-
-        let indenter = indenter.push_level_with_order(ChildOrder::Last);
-        assert_eq!(indenter.get_indent(), "");
-
-        let indenter = indenter.push_level_with_order(ChildOrder::Last);
-        assert_eq!(indenter.get_indent(), "└─ ");
-    }
-
-    #[test]
-    fn test_indenter_with_multiple_siblings() {
-        let indenter = Indenter::new(true);
-
-        let indenter = indenter.push_level_with_order(ChildOrder::Last);
-        assert_eq!(indenter.get_indent(), "└─ ");
-
-        let indenter = indenter.push_level_with_order(ChildOrder::HasRemainingSiblings);
-        assert_eq!(indenter.get_indent(), "   ├─ ");
-
-        let indenter = indenter.push_level_with_order(ChildOrder::Last);
-        assert_eq!(indenter.get_indent(), "   │  └─ ");
-
-        let indenter = indenter.push_level_with_order(ChildOrder::Last);
-        assert_eq!(indenter.get_indent(), "   │     └─ ");
-
-        let indenter = indenter.push_level_with_order(ChildOrder::HasRemainingSiblings);
-        assert_eq!(indenter.get_indent(), "   │        ├─ ");
-    }
-}
-
 /// A struct implementing [`fmt::Display`] that generates a user-friendly
 /// representation of a conflict graph
 pub struct DisplayUnsat<'i, I: Interner> {
@@ -1063,3 +1027,39 @@ impl<I: Interner> fmt::Display for DisplayUnsat<'_, I> {
         Ok(())
     }
 }
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    #[test]
+    fn test_indenter_without_top_level_indent() {
+        let indenter = Indenter::new(false);
+
+        let indenter = indenter.push_level_with_order(ChildOrder::Last);
+        assert_eq!(indenter.get_indent(), "");
+
+        let indenter = indenter.push_level_with_order(ChildOrder::Last);
+        assert_eq!(indenter.get_indent(), "└─ ");
+    }
+
+    #[test]
+    fn test_indenter_with_multiple_siblings() {
+        let indenter = Indenter::new(true);
+
+        let indenter = indenter.push_level_with_order(ChildOrder::Last);
+        assert_eq!(indenter.get_indent(), "└─ ");
+
+        let indenter = indenter.push_level_with_order(ChildOrder::HasRemainingSiblings);
+        assert_eq!(indenter.get_indent(), "   ├─ ");
+
+        let indenter = indenter.push_level_with_order(ChildOrder::Last);
+        assert_eq!(indenter.get_indent(), "   │  └─ ");
+
+        let indenter = indenter.push_level_with_order(ChildOrder::Last);
+        assert_eq!(indenter.get_indent(), "   │     └─ ");
+
+        let indenter = indenter.push_level_with_order(ChildOrder::HasRemainingSiblings);
+        assert_eq!(indenter.get_indent(), "   │        ├─ ");
+    }
+}
diff --git a/src/internal/mapping.rs b/src/internal/mapping.rs
index e668ad8..fac003c 100644
--- a/src/internal/mapping.rs
+++ b/src/internal/mapping.rs
@@ -27,6 +27,16 @@ impl<TId: ArenaId, TValue> Mapping<TId, TValue> {
         Self::with_capacity(1)
     }
 
+    /// Returns the total number of values that can be stored in the mapping without reallocating.
+    pub fn capacity(&self) -> usize {
+        self.chunks.len() * VALUES_PER_CHUNK
+    }
+
+    /// Returns the total number of bytes allocated by this instance.
+    pub fn size_in_bytes(&self) -> usize {
+        self.capacity() * std::mem::size_of::<Option<TValue>>()
+    }
+
     /// Constructs a new arena with a capacity for `n` values pre-allocated.
     pub fn with_capacity(n: usize) -> Self {
         let n = cmp::max(1, n);
@@ -60,7 +70,9 @@ impl<TId: ArenaId, TValue> Mapping<TId, TValue> {
                 .resize_with(chunk + 1, || std::array::from_fn(|_| None));
         }
         let previous_value = self.chunks[chunk][offset].replace(value);
-        self.len += 1;
+        if previous_value.is_none() {
+            self.len += 1;
+        }
         self.max = self.max.max(idx);
         previous_value
     }
diff --git a/src/solver/decision_map.rs b/src/solver/decision_map.rs
index b8004a8..6f6cc2e 100644
--- a/src/solver/decision_map.rs
+++ b/src/solver/decision_map.rs
@@ -43,6 +43,11 @@ pub(crate) struct DecisionMap {
 }
 
 impl DecisionMap {
+    #[cfg(feature = "diagnostics")]
+    pub fn len(&self) -> usize {
+        self.map.len()
+    }
+
     pub fn reset(&mut self, variable_id: VariableId) {
         let variable_id = variable_id.to_usize();
         if variable_id < self.map.len() {
diff --git a/src/solver/decision_tracker.rs b/src/solver/decision_tracker.rs
index 1a23eac..116738d 100644
--- a/src/solver/decision_tracker.rs
+++ b/src/solver/decision_tracker.rs
@@ -15,6 +15,11 @@ impl DecisionTracker {
         *self = Default::default();
     }
 
+    #[cfg(feature = "diagnostics")]
+    pub(crate) fn len(&self) -> usize {
+        self.map.len()
+    }
+
     #[inline(always)]
     pub(crate) fn assigned_value(&self, variable_id: VariableId) -> Option<bool> {
         self.map.value(variable_id)
diff --git a/src/solver/diagnostics.rs b/src/solver/diagnostics.rs
new file mode 100644
index 0000000..4efb9a3
--- /dev/null
+++ b/src/solver/diagnostics.rs
@@ -0,0 +1,106 @@
+use std::io::Write;
+
+use ahash::HashMap;
+use itertools::Itertools;
+
+use crate::{
+    DependencyProvider, Solver,
+    runtime::AsyncRuntime,
+    solver::clause::{Clause, WatchedLiterals},
+};
+
+impl<D: DependencyProvider, RT: AsyncRuntime> Solver<D, RT> {
+    /// Reports diagnostics about the current state of the solver.
+    pub(crate) fn report_diagnostics(&self) {
+        let mut forbid_clauses_by_name = HashMap::default();
+        let mut forbid_clauses = 0usize;
+        let mut requires_clauses = 0usize;
+        let mut locked_clauses = 0usize;
+        let mut learned_clauses = 0usize;
+        let mut constrains_clauses = 0usize;
+        let clauses = &self.state.clauses.kinds;
+        for clause in clauses.iter() {
+            match clause {
+                Clause::ForbidMultipleInstances(_a, _b, name_id) => {
+                    let count = forbid_clauses_by_name.entry(name_id).or_insert(0usize);
+                    *count += 1;
+                    forbid_clauses += 1;
+                }
+                Clause::Requires(..) => {
+                    requires_clauses += 1;
+                }
+                Clause::Lock(..) => {
+                    locked_clauses += 1;
+                }
+                Clause::Learnt(..) => {
+                    learned_clauses += 1;
+                }
+                Clause::Constrains(..) => {
+                    constrains_clauses += 1;
+                }
+                _ => {}
+            }
+        }
+
+        let mut writer = tabwriter::TabWriter::new(Vec::new());
+        writeln!(
+            writer,
+            "Total number of solvables:\t{}",
+            self.state.decision_tracker.len()
+        )
+        .unwrap();
+        writeln!(
+            writer,
+            "Total number of watches:\t{} ({})",
+            self.state.watches.len(),
+            human_bytes::human_bytes(self.state.watches.size_in_bytes() as f64)
+        )
+        .unwrap();
+        writeln!(
+            writer,
+            "Total number of variables:\t{} ({})",
+            self.state.variable_map.count(),
+            human_bytes::human_bytes(self.state.variable_map.size_in_bytes() as f64)
+        )
+        .unwrap();
+        writeln!(
+            writer,
+            "Total number of clauses:\t{} ({})",
+            clauses.len(),
+            human_bytes::human_bytes(
+                (clauses.len()
+                    * (std::mem::size_of::<Clause>() + std::mem::size_of::<WatchedLiterals>()))
+                    as f64
+            )
+        )
+        .unwrap();
+        writeln!(writer, "- Requires:\t{}", requires_clauses).unwrap();
+        writeln!(writer, "- Constrains:\t{}", constrains_clauses).unwrap();
+        writeln!(writer, "- Lock:\t{}", locked_clauses).unwrap();
+        writeln!(writer, "- Learned:\t{}", learned_clauses).unwrap();
+        writeln!(writer, "- ForbidMultiple:\t{}", forbid_clauses).unwrap();
+
+        for (name_id, count) in forbid_clauses_by_name
+            .iter()
+            .sorted_by_key(|(_, count)| **count)
+            .rev()
+            .take(5)
+        {
+            writeln!(
+                writer,
+                "  - {}:\t{}",
+                self.provider().display_name(**name_id),
+                count
+            )
+            .unwrap();
+        }
+
+        if forbid_clauses_by_name.len() > 5 {
+            writeln!(writer, "  ...").unwrap();
+        }
+
+        let report = String::from_utf8(writer.into_inner().unwrap()).unwrap();
+
+        tracing::info!("Solver diagnostics:\n{}", report);
+    }
+}
diff --git a/src/solver/mod.rs b/src/solver/mod.rs
index 65ab2c3..d40dcf2 100644
--- a/src/solver/mod.rs
+++ b/src/solver/mod.rs
@@ -29,6 +29,8 @@ pub(crate) mod clause;
 mod decision;
 mod decision_map;
 mod decision_tracker;
+#[cfg(feature = "diagnostics")]
+mod diagnostics;
 mod encoding;
 pub(crate) mod variable_map;
 mod watch_map;
@@ -340,6 +342,8 @@ impl<D: DependencyProvider, RT: AsyncRuntime> Solver<D, RT> {
             }
         }
 
+        #[cfg(feature = "diagnostics")]
+        self.report_diagnostics();
         Ok(self.state.chosen_solvables().collect())
     }
 
@@ -622,7 +626,7 @@ impl<D: DependencyProvider, RT: AsyncRuntime> Solver<D, RT> {
                 break;
             };
 
-            tracing::info!(
+            tracing::debug!(
                 "╒══ Install {} at level {level} (derived from {})",
                 candidate.display(&self.state.variable_map, self.provider()),
                 self.state.clauses.kinds[clause_id.to_usize()]
@@ -633,14 +637,14 @@ impl<D: DependencyProvider, RT: AsyncRuntime> Solver<D, RT> {
             match self.set_propagate_learn(level, candidate, required_by, clause_id) {
                 Ok(new_level) => {
                     level = new_level;
-                    tracing::info!("╘══ Propagation completed");
+                    tracing::debug!("╘══ Propagation completed");
                 }
                 Err(UnsolvableOrCancelled::Cancelled(value)) => {
-                    tracing::info!("╘══ Propagation cancelled");
+                    tracing::debug!("╘══ Propagation cancelled");
                     return Err(UnsolvableOrCancelled::Cancelled(value));
                 }
                 Err(UnsolvableOrCancelled::Unsolvable(conflict)) => {
-                    tracing::info!("╘══ Propagation resulted in a conflict");
+                    tracing::debug!("╘══ Propagation resulted in a conflict");
                     return Err(UnsolvableOrCancelled::Unsolvable(conflict));
                 }
             }
@@ -930,17 +934,17 @@ impl<D: DependencyProvider, RT: AsyncRuntime> Solver<D, RT> {
         conflicting_clause: ClauseId,
     ) -> Result<u32, Conflict> {
         {
-            tracing::info!(
+            tracing::debug!(
                 "├┬ Propagation conflicted: could not set {solvable} to {attempted_value}",
                 solvable = conflicting_solvable.display(&self.state.variable_map, self.provider()),
             );
-            tracing::info!(
+            tracing::debug!(
                 "││ During unit propagation for clause: {}",
                 self.state.clauses.kinds[conflicting_clause.to_usize()]
                     .display(&self.state.variable_map, self.provider())
             );
 
-            tracing::info!(
+            tracing::debug!(
                 "││ Previously decided value: {}. Derived from: {}",
                 !attempted_value,
                 self.state.clauses.kinds[self
@@ -965,7 +969,7 @@ impl<D: DependencyProvider, RT: AsyncRuntime> Solver<D, RT> {
                     continue;
                 }
 
-                tracing::info!(
+                tracing::debug!(
                     "* ({level}) {action} {}. Reason: {}",
                     decision
                         .variable
@@ -993,14 +997,14 @@ impl<D: DependencyProvider, RT: AsyncRuntime> Solver<D, RT> {
                 level,
             )
             .expect("bug: solvable was already decided!");
-        tracing::debug!(
+        tracing::trace!(
             "│├ Propagate after learn: {} = {decision}",
             literal
                 .variable()
                 .display(&self.state.variable_map, self.provider()),
         );
 
-        tracing::info!("│└ Backtracked from {old_level} -> {level}");
+        tracing::debug!("│└ Backtracked from {old_level} -> {level}");
 
         Ok(level)
     }
@@ -1185,6 +1189,7 @@ impl<D: DependencyProvider, RT: AsyncRuntime> Solver<D, RT> {
                 );
             }
         }
+
         Ok(())
     }
 
@@ -1193,7 +1198,7 @@ impl<D: DependencyProvider, RT: AsyncRuntime> Solver<D, RT> {
     /// Because learnt clauses are not relevant for the user, they are not added
     /// to the [`Conflict`]. Instead, we report the clauses that caused them.
     fn analyze_unsolvable_clause(
-        clauses: &[Clause],
+        clauses: &Vec<Clause>,
         learnt_why: &Mapping<LearntClauseId, Vec<ClauseId>>,
         clause_id: ClauseId,
         conflict: &mut Conflict,
@@ -1226,7 +1231,7 @@ impl<D: DependencyProvider, RT: AsyncRuntime> Solver<D, RT> {
 
         let mut conflict = Conflict::default();
 
-        tracing::info!("=== ANALYZE UNSOLVABLE");
+        tracing::debug!("=== ANALYZE UNSOLVABLE");
 
         let mut involved = HashSet::default();
         self.state.clauses.kinds[clause_id.to_usize()].visit_literals(
diff --git a/src/solver/variable_map.rs b/src/solver/variable_map.rs
index e65280a..d21bffe 100644
--- a/src/solver/variable_map.rs
+++ b/src/solver/variable_map.rs
@@ -70,6 +70,17 @@ impl VariableMap {
         }
     }
 
+    #[cfg(feature = "diagnostics")]
+    pub fn count(&self) -> usize {
+        self.next_id
+    }
+
+    #[cfg(feature = "diagnostics")]
+    pub fn size_in_bytes(&self) -> usize {
+        self.origins.capacity() * std::mem::size_of::<(VariableId, VariableOrigin)>()
+            + self.solvable_to_variable.capacity() * std::mem::size_of::<(SolvableId, VariableId)>()
+    }
+
     /// Allocate a variable for a solvable or the root.
     pub fn intern_solvable_or_root(&mut self, solvable_or_root_id: SolvableOrRootId) -> VariableId {
         match solvable_or_root_id.solvable() {
diff --git a/src/solver/watch_map.rs b/src/solver/watch_map.rs
index cbc8300..49b7c64 100644
--- a/src/solver/watch_map.rs
+++ b/src/solver/watch_map.rs
@@ -13,6 +13,16 @@ pub(crate) struct WatchMap {
 }
 
 impl WatchMap {
+    #[cfg(feature = "diagnostics")]
+    pub fn len(&self) -> usize {
+        self.map.len()
+    }
+
+    #[cfg(feature = "diagnostics")]
+    pub fn size_in_bytes(&self) -> usize {
+        self.map.size_in_bytes()
+    }
+
     /// Add the clause to the linked list of the literals that the clause is
     /// watching.
     pub(crate) fn start_watching(&mut self, clause: &mut WatchedLiterals, clause_id: ClauseId) {
diff --git a/tests/solver.rs b/tests/solver.rs
index aea71d1..31fb257 100644
--- a/tests/solver.rs
+++ b/tests/solver.rs
@@ -123,9 +123,7 @@ impl Spec {
     pub fn parse_union(
         spec: &str,
     ) -> impl Iterator<Item = Result<Self, <Self as FromStr>::Err>> + '_ {
-        spec.split('|')
-            .map(str::trim)
-            .map(|dep| Spec::from_str(dep))
+        spec.split('|').map(str::trim).map(Spec::from_str)
     }
 }
 
@@ -386,7 +384,7 @@ impl DependencyProvider for BundleBoxProvider {
         candidates
             .iter()
             .copied()
-            .filter(|s| range.contains(&self.pool.resolve_solvable(*s).record) == !inverse)
+            .filter(|s| range.contains(&self.pool.resolve_solvable(*s).record) != inverse)
             .collect()
     }
 
@@ -538,7 +536,7 @@ impl DependencyProvider for BundleBoxProvider {
 }
 
 /// Create a string from a [`Transaction`]
-fn transaction_to_string(interner: &impl Interner, solvables: &Vec<SolvableId>) -> String {
+fn transaction_to_string(interner: &impl Interner, solvables: &[SolvableId]) -> String {
     use std::fmt::Write;
     let mut buf = String::new();
     for solvable in solvables