diff --git a/Cargo.lock b/Cargo.lock
index add7ffd4..8e0e9cb4 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -1258,6 +1258,7 @@ dependencies = [
  "rustsat-minisat",
  "rustsat-solvertests",
  "rustsat-tools",
+ "serde",
  "tempfile",
  "thiserror",
  "visibility",
@@ -1428,18 +1429,18 @@ dependencies = [
 
 [[package]]
 name = "serde"
-version = "1.0.216"
+version = "1.0.217"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "0b9781016e935a97e8beecf0c933758c97a5520d32930e460142b4cd80c6338e"
+checksum = "02fc4265df13d6fa1d00ecff087228cc0a2b5f3c0e87e258d8b94a156e984c70"
 dependencies = [
  "serde_derive",
 ]
 
 [[package]]
 name = "serde_derive"
-version = "1.0.216"
+version = "1.0.217"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "46f859dbbf73865c6627ed570e78961cd3ac92407a2d117204c49232485da55e"
+checksum = "5a9bf7cf98d04a2b28aead066b7496853d4779c9cc183c440dbac457641e19a0"
 dependencies = [
  "proc-macro2",
  "quote",
diff --git a/Cargo.toml b/Cargo.toml
index ad6e1c8c..2625ccbb 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -44,6 +44,7 @@ rustsat = { version = "0.6.3", path = "./", default-features = false }
 rustsat-cadical = { version = "0.4.3", path = "./cadical" }
 rustsat-minisat = { version = "0.4.3", path = "./minisat" }
 rustsat-solvertests = { path = "./solvertests" }
+serde = { version = "1.0.217", features = ["derive"] }
 signal-hook = "0.3.17"
 tempfile = "3.17.1"
 visibility = "0.1.1"
@@ -80,6 +81,7 @@ flate2 = { workspace = true, optional = true }
 itertools.workspace = true
 rand = { workspace = true, optional = true }
 rustc-hash = { workspace = true, optional = true }
+serde = { workspace = true, optional = true }
 tempfile.workspace = true
 xz2 = { workspace = true, optional = true }
 
@@ -98,7 +100,8 @@ compression = ["dep:bzip2", "dep:flate2", "dep:xz2"]
 rand = ["dep:rand"]
 bench = []
 ipasir-display = []
-all = ["multiopt", "compression", "rand", "fxhash"]
+serde = ["dep:serde"]
+all = ["multiopt", "compression", "rand", "fxhash", "serde"]
 
 [package.metadata.docs.rs]
 features = ["all", "internals"]
diff --git a/README.md b/README.md
index fa37e8ef..96bbb086 100644
--- a/README.md
+++ b/README.md
@@ -60,6 +60,7 @@ To install the binary tools in `rustsat-tools` run `cargo install rustsat-tools`
 | `fxhash` | Use the faster firefox hash function from `rustc-hash` in RustSAT. |
 | `rand` | Enable randomization features. (Shuffling clauses etc.) |
 | `ipasir-display` | Changes `Display` trait for `Lit` and `Var` types to follow IPASIR variables indexing. |
+| `serde` | Add implementations for [`serde::Serialize`](https://docs.rs/serde/latest/serde/trait.Serialize.html) and [`serde::Deserialize`](https://docs.rs/serde/latest/serde/trait.Deserialize.html) for many library types |
 | `bench` | Enable benchmark tests. Behind feature flag since it requires unstable Rust. |
 | `internals` | Make some internal data structures for e.g. encodings public. This is useful when basing a more complex encoding on the RustSAT implementation of another encoding. Note that the internal API might change between releases. |
 
diff --git a/src/encodings/am1/bimander.rs b/src/encodings/am1/bimander.rs
index 3a0c61dd..c6a9fd2e 100644
--- a/src/encodings/am1/bimander.rs
+++ b/src/encodings/am1/bimander.rs
@@ -27,6 +27,7 @@ use crate::{
 /// - Van-Hau Nguyen and Son Thay Mai: _A New Method to Encode the At-Most-One Constraint into SAT,
 ///   SOICT 2015.
 #[derive(Default)]
+#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
 pub struct Bimander<const N: usize = 4, Sub = super::Pairwise> {
     /// Input literals
     in_lits: Vec<Lit>,
diff --git a/src/encodings/am1/bitwise.rs b/src/encodings/am1/bitwise.rs
index cbf51c68..f8480a71 100644
--- a/src/encodings/am1/bitwise.rs
+++ b/src/encodings/am1/bitwise.rs
@@ -20,6 +20,7 @@ use crate::{
 /// - Steven D. Prestwich: _Negative Effects of Modeling Techniques on Search Performance_, in
 ///   Trends in Constraint Programming 2007.
 #[derive(Default)]
+#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
 pub struct Bitwise {
     /// Input literals
     in_lits: Vec<Lit>,
diff --git a/src/encodings/am1/commander.rs b/src/encodings/am1/commander.rs
index 62d4ad90..68a7e49c 100644
--- a/src/encodings/am1/commander.rs
+++ b/src/encodings/am1/commander.rs
@@ -26,6 +26,7 @@ use crate::{
 /// - Will Klieber and Gihwon Kwon: _Efficient CNF Encoding for Selecting 1 from N Objects, CFV
 ///   2007.
 #[derive(Default)]
+#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
 pub struct Commander<const N: usize = 4, Sub = super::Pairwise> {
     /// Input literals
     in_lits: Vec<Lit>,
diff --git a/src/encodings/am1/ladder.rs b/src/encodings/am1/ladder.rs
index 28ab45ff..356e8ae3 100644
--- a/src/encodings/am1/ladder.rs
+++ b/src/encodings/am1/ladder.rs
@@ -18,6 +18,7 @@ use crate::{
 ///
 /// - Ian P. Gent and Peter Nightingale: _A new Encoding of AllDifferent into SAT_, CP 2004.
 #[derive(Default)]
+#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
 pub struct Ladder {
     /// Input literals
     in_lits: Vec<Lit>,
diff --git a/src/encodings/am1/pairwise.rs b/src/encodings/am1/pairwise.rs
index 8f19960d..d71a30e0 100644
--- a/src/encodings/am1/pairwise.rs
+++ b/src/encodings/am1/pairwise.rs
@@ -18,6 +18,7 @@ use crate::{
 ///
 /// - Steven D. Prestwich: _CNF Encodings_, in Handbook of Satisfiability 2021.
 #[derive(Default)]
+#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
 pub struct Pairwise {
     /// Input literals
     in_lits: Vec<Lit>,
diff --git a/src/encodings/card/dbtotalizer.rs b/src/encodings/card/dbtotalizer.rs
index 474ef336..6c04d4eb 100644
--- a/src/encodings/card/dbtotalizer.rs
+++ b/src/encodings/card/dbtotalizer.rs
@@ -35,6 +35,7 @@ use super::{BoundUpper, BoundUpperIncremental, Encode, EncodeIncremental};
 /// - \[2\] Ruben Martins and Saurabh Joshi and Vasco Manquinho and Ines Lynce: _Incremental
 ///     Cardinality Constraints for MaxSAT_, CP 2014.
 #[derive(Default)]
+#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
 pub struct DbTotalizer {
     /// Literals added but not yet in the encoding
     lit_buffer: Vec<Lit>,
@@ -218,6 +219,7 @@ impl Extend<Lit> for DbTotalizer {
 
 /// A totalizer adder node
 #[derive(Debug, Clone, PartialEq, Eq)]
+#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
 #[repr(transparent)]
 #[cfg(not(feature = "internals"))]
 pub struct Node(pub(in crate::encodings) INode);
@@ -226,6 +228,7 @@ pub struct Node(pub(in crate::encodings) INode);
 ///
 /// The internal node [`INode`] representation is only accessible on crate feature `internals`.
 #[derive(Debug, Clone, PartialEq, Eq)]
+#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
 #[repr(transparent)]
 #[cfg(feature = "internals")]
 pub struct Node(pub INode);
@@ -239,6 +242,7 @@ impl From<INode> for Node {
 /// The internal totalizer node type
 #[derive(Debug, Clone, PartialEq, Eq)]
 #[cfg_attr(feature = "internals", visibility::make(pub))]
+#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
 pub(in crate::encodings) enum INode {
     /// An input literal, i.e., a leaf of the tree
     Leaf(Lit),
@@ -468,6 +472,7 @@ impl Index<usize> for Node {
 
 /// An internal node of the totalizer
 #[derive(Debug, Clone, PartialEq, Eq)]
+#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
 pub struct UnitNode {
     pub(crate) lits: Vec<LitData>,
     pub(crate) depth: usize,
@@ -514,6 +519,7 @@ impl Index<usize> for UnitNode {
 
 /// An internal _general_ (weighted) node
 #[derive(Debug, Clone, PartialEq, Eq)]
+#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
 pub struct GeneralNode {
     pub(crate) lits: BTreeMap<usize, LitData>,
     pub(crate) depth: usize,
@@ -563,6 +569,7 @@ impl GeneralNode {
 
 /// Data associated with an output literal in a [`Node`]
 #[derive(Debug, Default, Clone, PartialEq, Eq)]
+#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
 pub(crate) enum LitData {
     #[default]
     None,
@@ -603,6 +610,7 @@ impl LitData {
 #[derive(Default, Clone)]
 #[cfg_attr(feature = "internals", visibility::make(pub))]
 #[cfg_attr(docsrs, doc(cfg(feature = "internals")))]
+#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
 pub(in crate::encodings) struct TotDb {
     /// The node database of the totalizer
     nodes: Vec<Node>,
diff --git a/src/encodings/card/simulators.rs b/src/encodings/card/simulators.rs
index fea7cf6c..6b04c60f 100644
--- a/src/encodings/card/simulators.rs
+++ b/src/encodings/card/simulators.rs
@@ -18,6 +18,7 @@ use crate::{
 
 /// Simulator type that builds a cardinality encoding of type `CE` over the
 /// negated input literals in order to simulate the other bound type
+#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
 pub struct Inverted<CE>
 where
     CE: Encode + 'static,
@@ -241,6 +242,7 @@ type InvertedIter<ICE> = std::iter::Map<ICE, fn(Lit) -> Lit>;
 /// Simulator type that builds a combined cardinality encoding supporting both
 /// bounds from two individual cardinality encodings supporting each bound
 /// separately
+#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
 pub struct Double<UBE, LBE>
 where
     UBE: BoundUpper + 'static,
diff --git a/src/encodings/card/totalizer.rs b/src/encodings/card/totalizer.rs
index c5ba8727..4cd38f68 100644
--- a/src/encodings/card/totalizer.rs
+++ b/src/encodings/card/totalizer.rs
@@ -36,6 +36,7 @@ use std::{
 /// - \[1\] Olivier Bailleux and Yacine Boufkhad: _Efficient CNF Encoding of Boolean Cardinality Constraints_, CP 2003.
 /// - \[2\] Ruben Martins and Saurabh Joshi and Vasco Manquinho and Ines Lynce: _Incremental Cardinality Constraints for MaxSAT_, CP 2014.
 #[derive(Default)]
+#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
 pub struct Totalizer {
     /// Input literals to the totalizer
     in_lits: Vec<Lit>,
@@ -343,6 +344,7 @@ pub(super) type TotIter<'a> = std::iter::Copied<std::slice::Iter<'a, Lit>>;
 /// accessed but only through [`Totalizer`].
 #[cfg_attr(feature = "internals", visibility::make(pub))]
 #[cfg_attr(docsrs, doc(cfg(feature = "internals")))]
+#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
 enum Node {
     /// An input literal, i.e., a leaf node of the tree
     Leaf {
diff --git a/src/encodings/nodedb.rs b/src/encodings/nodedb.rs
index be6b6598..4e0b0b21 100644
--- a/src/encodings/nodedb.rs
+++ b/src/encodings/nodedb.rs
@@ -18,6 +18,7 @@ use crate::{types::Lit, utils::unreachable_none};
 /// An ID of a [`NodeLike`] in a database. The [`usize`] is typically the index in a
 /// vector of nodes.
 #[derive(Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Debug, Hash)]
+#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
 #[repr(transparent)]
 pub struct NodeId(pub usize);
 
@@ -149,6 +150,7 @@ pub trait NodeLike {
 
 /// A connection to another node.
 #[derive(Debug, Clone, Copy, PartialEq, Eq)]
+#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
 pub struct NodeCon {
     /// The child node
     pub id: NodeId,
diff --git a/src/encodings/pb/adder.rs b/src/encodings/pb/adder.rs
index f113bc76..82674bd5 100644
--- a/src/encodings/pb/adder.rs
+++ b/src/encodings/pb/adder.rs
@@ -39,6 +39,7 @@ use super::{
 /// - \[2\] Niklas Eén and Niklas Sörensson: _Translating Pseudo-Boolean Constraints into SAT_,
 ///     JSAT 2006.
 #[derive(Default, Debug)]
+#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
 pub struct BinaryAdder {
     /// Input literals and weights for the encoding
     lit_buffer: RsHashMap<Lit, usize>,
@@ -57,6 +58,7 @@ pub struct BinaryAdder {
 /// The structure of a binary adder encoding
 #[cfg_attr(feature = "internals", visibility::make(pub))]
 #[cfg_attr(docsrs, doc(cfg(feature = "internals")))]
+#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
 #[derive(Debug, Clone)]
 struct Structure {
     /// The output bits of the structure
@@ -437,6 +439,7 @@ impl Extend<(Lit, usize)> for BinaryAdder {
 }
 
 #[derive(Debug, Clone, Copy)]
+#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
 enum Node {
     Full {
         a: Connection,
@@ -496,6 +499,7 @@ impl Node {
 }
 
 #[derive(Debug, Clone, Copy)]
+#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
 enum Connection {
     Input(Lit),
     Sum(usize),
@@ -503,6 +507,7 @@ enum Connection {
 }
 
 #[derive(Debug, Clone, Copy)]
+#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
 struct Output {
     bit: Lit,
     enc_if: bool,
diff --git a/src/encodings/pb/dbgte.rs b/src/encodings/pb/dbgte.rs
index 01d33e1f..b1c7d23f 100644
--- a/src/encodings/pb/dbgte.rs
+++ b/src/encodings/pb/dbgte.rs
@@ -29,6 +29,7 @@ use super::{BoundUpper, BoundUpperIncremental, Encode, EncodeIncremental};
 /// - \[1\] Saurabh Joshi and Ruben Martins and Vasco Manquinho: _Generalized
 ///     Totalizer Encoding for Pseudo-Boolean Constraints_, CP 2015.
 #[derive(Default)]
+#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
 pub struct DbGte {
     /// Input literals and weights not yet in the tree
     lit_buffer: RsHashMap<Lit, usize>,
diff --git a/src/encodings/pb/dpw.rs b/src/encodings/pb/dpw.rs
index c31467ce..d5e2a909 100644
--- a/src/encodings/pb/dpw.rs
+++ b/src/encodings/pb/dpw.rs
@@ -62,6 +62,7 @@ pub enum PrecisionError {
 /// - \[1\] Tobias Paxian and Sven Reimer and Bernd Becker: _Dynamic Polynomial
 ///     Watchdog Encoding for Solving Weighted MaxSAT_, SAT 2018.
 #[derive(Default)]
+#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
 pub struct DynamicPolyWatchdog {
     /// Input literals and weights for the encoding
     in_lits: RsHashMap<Lit, usize>,
@@ -227,6 +228,7 @@ impl DynamicPolyWatchdog {
 /// Type containing information about the DPW encoding structure
 #[cfg_attr(feature = "internals", visibility::make(pub))]
 #[cfg_attr(docsrs, doc(cfg(feature = "internals")))]
+#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
 #[derive(Clone)]
 pub(crate) struct Structure {
     /// The bottom buckets of the encoding. The first one of them is the root of the encoding.
diff --git a/src/encodings/pb/gte.rs b/src/encodings/pb/gte.rs
index ef962114..7b27f330 100644
--- a/src/encodings/pb/gte.rs
+++ b/src/encodings/pb/gte.rs
@@ -31,6 +31,7 @@ use std::{
 /// - \[1\] Saurabh Joshi and Ruben Martins and Vasco Manquinho: _Generalized
 ///     Totalizer Encoding for Pseudo-Boolean Constraints_, CP 2015.
 #[derive(Default)]
+#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
 pub struct GeneralizedTotalizer {
     /// Input literals and weights for the encoding
     in_lits: RsHashMap<Lit, usize>,
@@ -342,6 +343,7 @@ impl Extend<(Lit, usize)> for GeneralizedTotalizer {
 /// [`super::InvertedGeneralizedTotalizer`] structs.
 #[cfg_attr(feature = "internals", visibility::make(pub))]
 #[cfg_attr(docsrs, doc(cfg(feature = "internals")))]
+#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
 enum Node {
     /// A weighted input literal, i.e., a leaf node of the tree
     Leaf {
diff --git a/src/encodings/pb/simulators.rs b/src/encodings/pb/simulators.rs
index 139d2550..988339a6 100644
--- a/src/encodings/pb/simulators.rs
+++ b/src/encodings/pb/simulators.rs
@@ -20,6 +20,7 @@ use crate::{
 
 /// Simulator type that builds a pseudo-boolean encoding of type `PBE` over the
 /// negated input literals in order to simulate the other bound type
+#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
 pub struct Inverted<PBE>
 where
     PBE: Encode + 'static,
@@ -255,6 +256,7 @@ type InvertedIter<IPBE> = std::iter::Map<IPBE, fn((Lit, usize)) -> (Lit, usize)>
 /// Simulator type that builds a combined pseudo-boolean encoding supporting
 /// both bounds from two individual pseudo-boolean encodings supporting each
 /// bound separately
+#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
 pub struct Double<UBE, LBE>
 where
     UBE: BoundUpper + 'static,
@@ -454,6 +456,7 @@ where
 
 /// Simulator type that mimics a pseudo-boolean encoding based on a cardinality
 /// encoding that literals are added to multiple times
+#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
 pub struct Card<CE>
 where
     CE: card::Encode + 'static,
diff --git a/src/instances.rs b/src/instances.rs
index b38687d5..8dff5dd0 100644
--- a/src/instances.rs
+++ b/src/instances.rs
@@ -88,6 +88,7 @@ pub trait ReindexVars: ManageVars {
 
 /// Simple counting variable manager
 #[derive(Debug, PartialEq, Eq, Clone)]
+#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
 pub struct BasicVarManager {
     next_var: Var,
 }
@@ -148,6 +149,7 @@ impl Default for BasicVarManager {
 
 /// Manager for re-indexing an existing instance
 #[derive(PartialEq, Eq)]
+#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
 pub struct ReindexingVarManager {
     next_var: Var,
     in_map: RsHashMap<Var, Var>,
@@ -320,6 +322,7 @@ impl ManageVars for ObjectVarManager {
 #[cfg(feature = "rand")]
 /// Manager for randomly re-indexing an instance
 #[derive(PartialEq, Eq)]
+#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
 pub struct RandReindVarManager {
     next_var: Var,
     in_map: Vec<Var>,
diff --git a/src/instances/multiopt.rs b/src/instances/multiopt.rs
index 1999a2b3..9084ae16 100644
--- a/src/instances/multiopt.rs
+++ b/src/instances/multiopt.rs
@@ -19,6 +19,7 @@ use super::{
 /// Type representing a multi-objective optimization instance.
 /// The constraints are represented as a [`SatInstance`] struct.
 #[derive(Clone, Debug, PartialEq, Eq, Default)]
+#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
 pub struct MultiOptInstance<VM: ManageVars = BasicVarManager> {
     pub(super) constrs: SatInstance<VM>,
     pub(super) objs: Vec<Objective>,
diff --git a/src/instances/opt.rs b/src/instances/opt.rs
index 4d6765ea..6d65875c 100644
--- a/src/instances/opt.rs
+++ b/src/instances/opt.rs
@@ -21,6 +21,7 @@ use crate::{
 
 /// Internal objective type for not exposing variants
 #[derive(Clone, Debug, PartialEq, Eq)]
+#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
 enum IntObj {
     Weighted {
         offset: isize,
@@ -44,6 +45,7 @@ use super::{
 /// This type currently supports soft clauses and soft literals.
 /// All objectives are considered minimization objectives.
 #[derive(Clone, Debug, PartialEq, Eq)]
+#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
 pub struct Objective(IntObj);
 
 impl From<IntObj> for Objective {
@@ -1090,6 +1092,7 @@ impl FromIterator<(Clause, usize)> for Objective {
 /// Type representing an optimization instance.
 /// The constraints are represented as a [`SatInstance`] struct.
 #[derive(Clone, Debug, PartialEq, Eq, Default)]
+#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
 pub struct Instance<VM: ManageVars = BasicVarManager> {
     pub(super) constrs: SatInstance<VM>,
     pub(super) obj: Objective,
diff --git a/src/instances/sat.rs b/src/instances/sat.rs
index 08cb6590..48ec205d 100644
--- a/src/instances/sat.rs
+++ b/src/instances/sat.rs
@@ -30,6 +30,7 @@ use super::{
 /// Simple type representing a CNF formula. Other than [`Instance<VM>`], this
 /// type only supports clauses and does have an internal variable manager.
 #[derive(Clone, PartialEq, Eq, Default)]
+#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
 pub struct Cnf {
     pub(super) clauses: Vec<Clause>,
 }
@@ -365,6 +366,7 @@ impl Index<usize> for Cnf {
 /// Type representing a satisfiability instance. Supported constraints are
 /// clauses, cardinality constraints and pseudo-boolean constraints.
 #[derive(Clone, Debug, PartialEq, Eq)]
+#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
 pub struct Instance<VM: ManageVars = BasicVarManager> {
     pub(super) cnf: Cnf,
     pub(super) cards: Vec<CardConstraint>,
diff --git a/src/lib.rs b/src/lib.rs
index b3d7dd10..25ff651b 100644
--- a/src/lib.rs
+++ b/src/lib.rs
@@ -53,6 +53,7 @@
 //! | `fxhash` | Use the faster firefox hash function from `rustc-hash` in RustSAT. |
 //! | `rand` | Enable randomization features. (Shuffling clauses etc.) |
 //! | `ipasir-display` | Changes `Display` trait for `Lit` and `Var` types to follow IPASIR variables indexing. |
+//! | `serde` | Add implementations for [`serde::Serialize`](https://docs.rs/serde/latest/serde/trait.Serialize.html) and [`serde::Deserialize`](https://docs.rs/serde/latest/serde/trait.Deserialize.html) for many library types |
 //! | `bench` | Enable benchmark tests. Behind feature flag since it requires unstable Rust. |
 //! | `internals` | Make some internal data structures for e.g. encodings public. This is useful when basing a more complex encoding on the RustSAT implementation of another encoding. Note that the internal API might change between releases. |
 //!
diff --git a/src/types.rs b/src/types.rs
index 810ab766..f7dcfbe7 100644
--- a/src/types.rs
+++ b/src/types.rs
@@ -43,6 +43,7 @@ pub type RsHasher = std::collections::hash_map::DefaultHasher;
 /// because literals are represented as a single `u32` as well. The memory
 /// representation of variables is `u32`.
 #[derive(Hash, Eq, PartialEq, PartialOrd, Clone, Copy, Ord)]
+#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
 #[repr(transparent)]
 pub struct Var {
     idx: u32,
@@ -293,6 +294,7 @@ macro_rules! var {
 /// be used to index data structures with the two literals of a variable
 /// being close together.
 #[derive(Hash, Eq, PartialEq, PartialOrd, Ord, Clone, Copy)]
+#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
 #[repr(transparent)]
 pub struct Lit {
     lidx: u32,
@@ -628,6 +630,7 @@ macro_rules! ipasir_lit {
 
 /// Ternary value assigned to a literal or variable, including possible "don't care"
 #[derive(Clone, Copy, PartialEq, Eq, Default)]
+#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
 #[repr(u8)]
 pub enum TernaryVal {
     /// Positive assignment.
@@ -749,6 +752,7 @@ enum VLineFormat {
 
 /// Type representing an assignment of variables.
 #[derive(Clone, PartialEq, Eq, Default)]
+#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
 #[repr(transparent)]
 pub struct Assignment {
     assignment: Vec<TernaryVal>,
diff --git a/src/types/constraints.rs b/src/types/constraints.rs
index fe1a9aa6..3c74df06 100644
--- a/src/types/constraints.rs
+++ b/src/types/constraints.rs
@@ -43,6 +43,7 @@ impl fmt::Display for ConstraintRef<'_> {
 /// Wrapper around a std collection to allow for changing the data structure.
 /// Optional clauses as sets will be included in the future.
 #[derive(PartialEq, Eq, PartialOrd, Ord, Clone, Default)]
+#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
 pub struct Clause {
     lits: Vec<Lit>,
 }
@@ -526,6 +527,7 @@ impl AsMut<Cl> for [Lit] {
 
 /// Type representing a cardinality constraint.
 #[derive(Hash, Eq, PartialEq, Clone, Debug)]
+#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
 pub enum CardConstraint {
     /// An upper bound cardinality constraint
     Ub(CardUbConstr),
@@ -817,6 +819,7 @@ impl From<Clause> for CardConstraint {
 
 /// An upper bound cardinality constraint (`sum of lits <= b`)
 #[derive(Hash, Eq, PartialEq, Clone, Debug)]
+#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
 pub struct CardUbConstr {
     lits: Vec<Lit>,
     b: usize,
@@ -868,6 +871,7 @@ impl CardUbConstr {
 
 /// A lower bound cardinality constraint (`sum of lits >= b`)
 #[derive(Hash, Eq, PartialEq, Clone, Debug)]
+#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
 pub struct CardLbConstr {
     lits: Vec<Lit>,
     b: usize,
@@ -925,6 +929,7 @@ impl CardLbConstr {
 
 /// An equality cardinality constraint (`sum of lits = b`)
 #[derive(Hash, Eq, PartialEq, Clone, Debug)]
+#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
 pub struct CardEqConstr {
     lits: Vec<Lit>,
     b: usize,
@@ -998,6 +1003,7 @@ pub use PbToCardError as PBToCardError;
 /// constraint, the constraint is transformed so that all coefficients are
 /// positive.
 #[derive(Eq, PartialEq, Clone, Debug)]
+#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
 pub enum PbConstraint {
     /// An upper bound pseudo-boolean constraint
     Ub(PbUbConstr),
@@ -1462,6 +1468,7 @@ impl From<CardConstraint> for PbConstraint {
 
 /// An upper bound pseudo-boolean constraint (`weighted sum of lits <= b`)
 #[derive(Eq, PartialEq, Clone, Debug)]
+#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
 pub struct PbUbConstr {
     lits: Vec<(Lit, usize)>,
     weight_sum: usize,
@@ -1559,6 +1566,7 @@ impl PbUbConstr {
 
 /// A lower bound pseudo-boolean constraint (`weighted sum of lits >= b`)
 #[derive(Eq, PartialEq, Clone, Debug)]
+#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
 pub struct PbLbConstr {
     lits: Vec<(Lit, usize)>,
     weight_sum: usize,
@@ -1655,6 +1663,7 @@ impl PbLbConstr {
 
 /// An equality pseudo-boolean constraint (`weighted sum of lits = b`)
 #[derive(Eq, PartialEq, Clone, Debug)]
+#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
 pub struct PbEqConstr {
     lits: Vec<(Lit, usize)>,
     weight_sum: usize,