Export Solver and Theory Statistics

examples/sat/Cargo.toml

@@ -11,7 +11,7 @@ aries = { path = "../../solver" }
 varisat-dimacs = "0.2.2"
 varisat-formula = "0.2.2"
 zip = { default-features = false, features = ["deflate"], version = "2.1.3" }
-
+serde_json = "*"
 
 [[bin]]
 name = "aries-sat"

examples/sat/main.rs

@@ -8,6 +8,7 @@ use aries::solver::search::combinators::{RoundRobin, WithGeomRestart};
 use aries::solver::search::conflicts::{ConflictBasedBrancher, Params};
 use aries::solver::search::SearchControl;
 use aries::solver::Solver;
+use aries::utils::SnapshotStatistics;
 use std::collections::HashMap;
 use std::fs::File;
 use std::io::Read;
@@ -30,6 +31,10 @@ struct Opt {
     timeout: Option<u64>,
     #[structopt(long, short, default_value = "")]
     search: String,
+
+    /// File to write JSON-encoded solver statistics
+    #[structopt(long = "stats-file")]
+    stats_file: Option<PathBuf>,
 }
 
 enum Source {
@@ -168,6 +173,11 @@ fn solve_multi_threads(model: Model, opt: &Opt, deadline: Option<Instant>) -> Re
             }
         }
     }
+    if let Some(stats_path) = &opt.stats_file {
+        let stats = par_solver.snapshot_statistics();
+        let mut stats_file = std::fs::File::create(stats_path)?;
+        serde_json::to_writer(&mut stats_file, &stats)?;
+    }
     par_solver.print_stats();
 
     Ok(())

solver/Cargo.toml

@@ -8,6 +8,9 @@ edition = "2021"
 
 [features]
 
+# if enabled, solver and theory statistics may be exported and imported using serde
+export_stats = [ "dep:serde", "serde/serde_derive" ]
+
 # If enabled, will instruct the the solver to count cpu cycles at various point of its execution.
 # The implementation relies to time-stamp counter and intrinsic for the x86_64 platform.
 # If the target platform is not supported, activating this feature will have no effects.
@@ -30,6 +33,7 @@ lru = "0.12.3"
 rand = { workspace = true }
 num-rational = { workspace = true }
 hashbrown = "0.15"
+serde = { version = "1", optional = true }
 
 [dev-dependencies]
 rand = "0.8"

solver/src/reasoners/cp/mod.rs

@@ -19,6 +19,7 @@ use crate::model::lang::mul::NFEqVarMulLit;
 use crate::reasoners::cp::linear::{LinearSumLeq, SumElem};
 use crate::reasoners::cp::max::AtLeastOneGeq;
 use crate::reasoners::{Contradiction, ReasonerId, Theory};
+use crate::utils::SnapshotStatistics;
 use anyhow::Context;
 use mul::VarEqVarMulLit;
 use set::IterableRefSet;
@@ -235,6 +236,31 @@ impl Theory for Cp {
     }
 }
 
+#[cfg_attr(feature = "export_stats", derive(serde::Serialize, serde::Deserialize))]
+#[derive(Debug, PartialEq, Eq, Clone)]
+pub struct CpStatsSnapshot {
+    pub num_constraints: usize,
+    pub num_propagations: u64,
+}
+
+impl std::fmt::Display for CpStatsSnapshot {
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+        writeln!(f, "# constraints: {}", self.num_constraints)?;
+        writeln!(f, "# propagations: {}", self.num_propagations)
+    }
+}
+
+impl SnapshotStatistics for Cp {
+    type Stats = CpStatsSnapshot;
+
+    fn snapshot_statistics(&self) -> Self::Stats {
+        Self::Stats {
+            num_constraints: self.constraints.len(),
+            num_propagations: self.stats.num_propagations,
+        }
+    }
+}
+
 impl Backtrack for Cp {
     fn save_state(&mut self) -> DecLvl {
         self.saved += 1;

solver/src/reasoners/eq/dense.rs

@@ -6,6 +6,7 @@ use crate::model::{Label, Model};
 use crate::reasoners::eq::domain;
 use crate::reasoners::{Contradiction, ReasonerId, Theory};
 use crate::reif::ReifExpr;
+use crate::utils::SnapshotStatistics;
 use itertools::Itertools;
 use std::collections::{HashMap, HashSet};
 use std::fmt::{Debug, Formatter};
@@ -875,6 +876,58 @@ impl Theory for DenseEqTheory {
     }
 }
 
+#[cfg_attr(feature = "export_stats", derive(serde::Serialize, serde::Deserialize))]
+#[derive(Debug, Clone, PartialEq, Eq, Default)]
+pub struct EqTheoryStatsSnapshot {
+    pub num_nodes: usize,
+    pub num_edge_propagations: usize,
+    pub num_edge_propagations_pos: usize,
+    pub num_edge_propagations_neg: usize,
+    pub num_edge_propagation1_pos_pos: usize,
+    pub num_edge_propagation1_pos_neg: usize,
+    pub num_edge_propagation1_neg_pos: usize,
+    pub num_edge_propagation1_effective: usize,
+    pub num_edge_propagation2_pos_pos: usize,
+    pub num_edge_propagation2_pos_neg: usize,
+    pub num_edge_propagation2_neg_pos: usize,
+}
+
+impl std::fmt::Display for EqTheoryStatsSnapshot {
+    fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result {
+        writeln!(f, "num nodes: {}", self.num_nodes)?;
+        writeln!(f, "num edge props1 {}", self.num_edge_propagations)?;
+        writeln!(f, "num edge props+ {}", self.num_edge_propagations_pos)?;
+        writeln!(f, "num edge props- {}", self.num_edge_propagations_neg)?;
+        writeln!(f, "num edge props1 ++  {}", self.num_edge_propagation1_pos_pos)?;
+        writeln!(f, "num edge props1 +-  {}", self.num_edge_propagation1_pos_neg)?;
+        writeln!(f, "num edge props1 -+  {}", self.num_edge_propagation1_neg_pos)?;
+        writeln!(f, "num edge props1 eff  {}", self.num_edge_propagation1_effective)?;
+        writeln!(f, "num edge props2 ++  {}", self.num_edge_propagation2_pos_pos)?;
+        writeln!(f, "num edge props2 +-  {}", self.num_edge_propagation2_pos_neg)?;
+        writeln!(f, "num edge props2 -+  {}", self.num_edge_propagation2_neg_pos)
+    }
+}
+
+impl SnapshotStatistics for DenseEqTheory {
+    type Stats = EqTheoryStatsSnapshot;
+
+    fn snapshot_statistics(&self) -> Self::Stats {
+        Self::Stats {
+            num_nodes: self.graph.nodes_ordered.len(),
+            num_edge_propagations: self.stats.num_edge_propagations,
+            num_edge_propagations_pos: self.stats.num_edge_propagations_pos,
+            num_edge_propagations_neg: self.stats.num_edge_propagations_neg,
+            num_edge_propagation1_pos_pos: self.stats.num_edge_propagation1_pos_pos,
+            num_edge_propagation1_pos_neg: self.stats.num_edge_propagation1_pos_neg,
+            num_edge_propagation1_neg_pos: self.stats.num_edge_propagation1_neg_pos,
+            num_edge_propagation1_effective: self.stats.num_edge_propagation1_effective,
+            num_edge_propagation2_pos_pos: self.stats.num_edge_propagation2_pos_pos,
+            num_edge_propagation2_pos_neg: self.stats.num_edge_propagation2_pos_neg,
+            num_edge_propagation2_neg_pos: self.stats.num_edge_propagation2_neg_pos,
+        }
+    }
+}
+
 pub trait ReifyEq {
     fn domains(&self) -> &Domains;
     fn domain(&self, a: Node) -> (IntCst, IntCst);

solver/src/reasoners/eq/split.rs

@@ -1,8 +1,9 @@
 use crate::backtrack::{Backtrack, DecLvl, DecisionLevelTracker};
 use crate::core::state::{Domains, DomainsSnapshot, Explanation, InferenceCause};
 use crate::core::{IntCst, Lit, VarRef};
-use crate::reasoners::eq::{DenseEqTheory, Node, ReifyEq};
+use crate::reasoners::eq::{DenseEqTheory, EqTheoryStatsSnapshot, Node, ReifyEq};
 use crate::reasoners::{Contradiction, ReasonerId, Theory};
+use crate::utils::SnapshotStatistics;
 use itertools::Itertools;
 use std::collections::HashMap;
 
@@ -17,6 +18,30 @@ pub struct SplitEqTheory {
     lvl: DecisionLevelTracker,
 }
 
+impl SnapshotStatistics for SplitEqTheory {
+    type Stats = EqTheoryStatsSnapshot;
+
+    fn snapshot_statistics(&self) -> Self::Stats {
+        self.parts()
+            .map(|part| part.snapshot_statistics())
+            .reduce(|sum, next| EqTheoryStatsSnapshot {
+                num_nodes: sum.num_nodes + next.num_nodes,
+                num_edge_propagations: sum.num_edge_propagations + next.num_edge_propagations,
+                num_edge_propagations_pos: sum.num_edge_propagations_pos + next.num_edge_propagations_pos,
+                num_edge_propagations_neg: sum.num_edge_propagations_neg + next.num_edge_propagations_neg,
+                num_edge_propagation1_pos_pos: sum.num_edge_propagation1_pos_pos + next.num_edge_propagation1_pos_pos,
+                num_edge_propagation1_pos_neg: sum.num_edge_propagation1_pos_neg + next.num_edge_propagation1_pos_neg,
+                num_edge_propagation1_neg_pos: sum.num_edge_propagation1_neg_pos + next.num_edge_propagation1_neg_pos,
+                num_edge_propagation1_effective: sum.num_edge_propagation1_effective
+                    + next.num_edge_propagation1_effective,
+                num_edge_propagation2_pos_pos: sum.num_edge_propagation2_pos_pos + next.num_edge_propagation2_pos_pos,
+                num_edge_propagation2_pos_neg: sum.num_edge_propagation2_pos_neg + next.num_edge_propagation2_pos_neg,
+                num_edge_propagation2_neg_pos: sum.num_edge_propagation2_neg_pos + next.num_edge_propagation2_neg_pos,
+            })
+            .unwrap_or_default()
+    }
+}
+
 impl SplitEqTheory {
     pub fn add_edge(&mut self, a: VarRef, b: VarRef, model: &mut impl ReifyEq) -> Lit {
         debug_assert_eq!(self.lvl.num_saved(), 0, "Adding an edge but not at the root");

solver/src/reasoners/sat/sat_solver.rs

@@ -6,6 +6,7 @@ use crate::core::*;
 use crate::model::extensions::DisjunctionExt;
 use crate::reasoners::sat::clauses::*;
 use crate::reasoners::{Contradiction, ReasonerId, Theory};
+use crate::utils::SnapshotStatistics;
 use itertools::Itertools;
 use smallvec::alloc::collections::VecDeque;
 
@@ -721,6 +722,31 @@ impl Backtrack for SatSolver {
     }
 }
 
+#[cfg_attr(feature = "export_stats", derive(serde::Serialize, serde::Deserialize))]
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub struct SatSolverStatsSnapshot {
+    pub num_clauses: usize,
+    pub propagations: u64,
+}
+
+impl std::fmt::Display for SatSolverStatsSnapshot {
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+        writeln!(f, "DB size              : {}", self.num_clauses)?;
+        writeln!(f, "Num unit propagations: {}", self.propagations)
+    }
+}
+
+impl SnapshotStatistics for SatSolver {
+    type Stats = SatSolverStatsSnapshot;
+
+    fn snapshot_statistics(&self) -> Self::Stats {
+        SatSolverStatsSnapshot {
+            num_clauses: self.clauses.num_clauses(),
+            propagations: self.stats.propagations,
+        }
+    }
+}
+
 impl Theory for SatSolver {
     fn identity(&self) -> ReasonerId {
         self.identity

solver/src/reasoners/stn/theory.rs

@@ -10,6 +10,7 @@ use crate::core::state::*;
 use crate::core::*;
 use crate::reasoners::stn::theory::Event::EdgeActivated;
 use crate::reasoners::{Contradiction, ReasonerId, Theory};
+use crate::utils::SnapshotStatistics;
 use contraint_db::*;
 use distances::{Graph, StnGraph};
 use edges::*;
@@ -114,6 +115,30 @@ struct Stats {
     num_theory_deactivations: u64,
 }
 
+#[cfg_attr(feature = "export_stats", derive(serde::Serialize, serde::Deserialize))]
+#[derive(Clone, Debug, PartialEq, Eq)]
+pub struct StnStatSnapshot {
+    pub num_nodes: u32,
+    pub num_propagator_groups: usize,
+    pub num_propagations: u64,
+    pub bound_updates: u64,
+    pub num_bound_edge_deactivation: u64,
+    pub num_theory_propagations: u64,
+    pub num_theory_deactivations: u64,
+}
+
+impl std::fmt::Display for StnStatSnapshot {
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+        writeln!(f, "# nodes: {}", self.num_nodes)?;
+        writeln!(f, "# propagators: {}", self.num_propagator_groups)?;
+        writeln!(f, "# propagations: {}", self.num_propagations)?;
+        writeln!(f, "# domain updates: {}", self.bound_updates)?;
+        writeln!(f, "# bounds deactivations: {}", self.num_bound_edge_deactivation)?;
+        writeln!(f, "# theory propagations: {}", self.num_theory_propagations)?;
+        writeln!(f, "# theory deactivations: {}", self.num_theory_deactivations)
+    }
+}
+
 #[derive(Debug, Clone, Copy)]
 pub(crate) struct Identity<Cause>
 where
@@ -963,6 +988,22 @@ impl Backtrack for StnTheory {
     }
 }
 
+impl SnapshotStatistics for StnTheory {
+    type Stats = StnStatSnapshot;
+
+    fn snapshot_statistics(&self) -> Self::Stats {
+        StnStatSnapshot {
+            num_nodes: self.num_nodes(),
+            num_propagator_groups: self.constraints.num_propagator_groups(),
+            num_propagations: self.stats.num_propagations,
+            bound_updates: self.stats.bound_updates,
+            num_bound_edge_deactivation: self.stats.num_bound_edge_deactivation,
+            num_theory_propagations: self.stats.num_theory_propagations,
+            num_theory_deactivations: self.stats.num_theory_deactivations,
+        }
+    }
+}
+
 #[allow(clippy::let_unit_value)]
 #[cfg(test)]
 mod tests {

solver/src/reasoners/tautologies.rs

@@ -2,6 +2,7 @@ use crate::backtrack::{Backtrack, DecLvl};
 use crate::core::state::{Cause, Domains, DomainsSnapshot, Explanation, InferenceCause};
 use crate::core::Lit;
 use crate::reasoners::{Contradiction, ReasonerId, Theory};
+use crate::utils::SnapshotStatistics;
 
 /// A reasoner that holds a set of tautologies (single literals that are known to be true)
 /// and propagates them at every decision level.
@@ -77,3 +78,21 @@ impl Theory for Tautologies {
         Box::new(self.clone())
     }
 }
+
+#[cfg_attr(feature = "export_stats", derive(serde::Serialize, serde::Deserialize))]
+#[derive(Debug, Clone)]
+pub struct TautologiesStatSnapshot;
+
+impl std::fmt::Display for TautologiesStatSnapshot {
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+        write!(f, "{}", std::any::type_name::<Self>())
+    }
+}
+
+impl SnapshotStatistics for Tautologies {
+    type Stats = TautologiesStatSnapshot;
+
+    fn snapshot_statistics(&self) -> Self::Stats {
+        TautologiesStatSnapshot
+    }
+}