diff --git a/Cargo.lock b/Cargo.lock
index f2a49c8..26c6ef4 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -613,6 +613,7 @@ name = "oxidd-ffi-python"
 version = "0.8.1"
 dependencies = [
  "anyhow",
+ "num-bigint",
  "oxidd",
  "oxidd-core",
  "oxidd-dump",
@@ -796,6 +797,7 @@ dependencies = [
  "indoc",
  "libc",
  "memoffset",
+ "num-bigint",
  "once_cell",
  "portable-atomic",
  "pyo3-build-config",
diff --git a/bindings/python/oxidd/protocols.py b/bindings/python/oxidd/protocols.py
index 7f4badf..7d5b06b 100644
--- a/bindings/python/oxidd/protocols.py
+++ b/bindings/python/oxidd/protocols.py
@@ -367,9 +367,24 @@ def valid(self, /) -> bool:
         """
         raise NotImplementedError
 
+    @abstractmethod
+    def sat_count(self, /, vars: int) -> int:
+        """Count the exact number of satisfying assignments.
+
+        Uses arbitrary precision integers.
+
+        Locking behavior: acquires the manager's lock for shared access.
+
+        Args:
+            vars: Assume that the function's domain has this many variables.
+        """
+        raise NotImplementedError
+
     @abstractmethod
     def sat_count_float(self, /, vars: int) -> float:
-        """Count the number of satisfying assignments.
+        """Count the (approximate) number of satisfying assignments.
+
+        Uses floating point numbers.
 
         Locking behavior: acquires the manager's lock for shared access.
 
diff --git a/crates/oxidd-ffi-python/Cargo.toml b/crates/oxidd-ffi-python/Cargo.toml
index b4f69d2..6582025 100644
--- a/crates/oxidd-ffi-python/Cargo.toml
+++ b/crates/oxidd-ffi-python/Cargo.toml
@@ -23,7 +23,10 @@ oxidd-core = { workspace = true }
 oxidd-dump = { workspace = true, features = ["dddmp", "dot"] }
 oxidd = { workspace = true, features = ["bdd", "bcdd", "zbdd"] }
 
-pyo3 = { version = "0.23.1", features = ["extension-module", "abi3-py39"] }
+pyo3 = { version = "0.23.1", features = ["extension-module", "abi3-py39", "num-bigint"] }
+
+# big integers
+num-bigint = "0.4"
 
 # fast hash function
 #
diff --git a/crates/oxidd-ffi-python/src/bcdd.rs b/crates/oxidd-ffi-python/src/bcdd.rs
index ea331fc..42ee291 100644
--- a/crates/oxidd-ffi-python/src/bcdd.rs
+++ b/crates/oxidd-ffi-python/src/bcdd.rs
@@ -3,6 +3,7 @@
 use std::hash::BuildHasherDefault;
 use std::path::PathBuf;
 
+use num_bigint::BigUint;
 use pyo3::prelude::*;
 use pyo3::types::{PyBool, PyList, PyNone, PyTuple, PyType};
 use rustc_hash::FxHasher;
@@ -695,6 +696,23 @@ impl BCDDFunction {
         self.0.valid()
     }
 
+    /// Count the number of satisfying assignments.
+    ///
+    /// Locking behavior: acquires the manager's lock for shared access.
+    ///
+    /// Args:
+    ///     vars (int): Assume that the function's domain has this many
+    ///         variables.
+    ///
+    /// Returns:
+    ///     int: The exact number of satisfying assignments
+    fn sat_count(&self, py: Python, vars: LevelNo) -> BigUint {
+        py.allow_threads(move || {
+            self.0
+                .sat_count::<BigUint, BuildHasherDefault<FxHasher>>(vars, &mut Default::default())
+        })
+    }
+
     /// Count the number of satisfying assignments.
     ///
     /// Locking behavior: acquires the manager's lock for shared access.
diff --git a/crates/oxidd-ffi-python/src/bdd.rs b/crates/oxidd-ffi-python/src/bdd.rs
index a65d5f1..697873d 100644
--- a/crates/oxidd-ffi-python/src/bdd.rs
+++ b/crates/oxidd-ffi-python/src/bdd.rs
@@ -3,6 +3,7 @@
 use std::hash::BuildHasherDefault;
 use std::path::PathBuf;
 
+use num_bigint::BigUint;
 use pyo3::prelude::*;
 use pyo3::types::{PyBool, PyList, PyNone, PyTuple, PyType};
 use rustc_hash::FxHasher;
@@ -693,6 +694,23 @@ impl BDDFunction {
         self.0.valid()
     }
 
+    /// Count the number of satisfying assignments.
+    ///
+    /// Locking behavior: acquires the manager's lock for shared access.
+    ///
+    /// Args:
+    ///     vars (int): Assume that the function's domain has this many
+    ///         variables.
+    ///
+    /// Returns:
+    ///     int: The exact number of satisfying assignments
+    fn sat_count(&self, py: Python, vars: LevelNo) -> BigUint {
+        py.allow_threads(move || {
+            self.0
+                .sat_count::<BigUint, BuildHasherDefault<FxHasher>>(vars, &mut Default::default())
+        })
+    }
+
     /// Count the number of satisfying assignments.
     ///
     /// Locking behavior: acquires the manager's lock for shared access.
diff --git a/crates/oxidd-ffi-python/src/zbdd.rs b/crates/oxidd-ffi-python/src/zbdd.rs
index ea21a9b..64fffd0 100644
--- a/crates/oxidd-ffi-python/src/zbdd.rs
+++ b/crates/oxidd-ffi-python/src/zbdd.rs
@@ -3,6 +3,7 @@
 use std::hash::BuildHasherDefault;
 use std::path::PathBuf;
 
+use num_bigint::BigUint;
 use pyo3::prelude::*;
 use pyo3::types::{PyBool, PyList, PyNone, PyTuple};
 use rustc_hash::FxHasher;
@@ -580,6 +581,23 @@ impl ZBDDFunction {
         self.0.valid()
     }
 
+    /// Count the number of satisfying assignments.
+    ///
+    /// Locking behavior: acquires the manager's lock for shared access.
+    ///
+    /// Args:
+    ///     vars (int): Assume that the function's domain has this many
+    ///         variables.
+    ///
+    /// Returns:
+    ///     int: The exact number of satisfying assignments
+    fn sat_count(&self, py: Python, vars: LevelNo) -> BigUint {
+        py.allow_threads(move || {
+            self.0
+                .sat_count::<BigUint, BuildHasherDefault<FxHasher>>(vars, &mut Default::default())
+        })
+    }
+
     /// Count the number of satisfying assignments.
     ///
     /// Locking behavior: acquires the manager's lock for shared access.