Optional serde support

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"]

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. |
 

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>,

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>,

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>,

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>,

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>,

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>,

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,

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 {

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,

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,13 +499,15 @@ impl Node {
 }
 
 #[derive(Debug, Clone, Copy)]
+#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
 enum Connection {
     Input(Lit),
     Sum(usize),
     Carry(usize),
 }
 
 #[derive(Debug, Clone, Copy)]
+#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
 struct Output {
     bit: Lit,
     enc_if: bool,

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>,

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.

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 {

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,

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>,

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>,

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,

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>,