satellite_format/
snapshot.rs

1//! Solver state snapshots for reproducibility.
2
3use serde::{Deserialize, Serialize};
4
5/// A snapshot of solver state for reproducibility.
6#[derive(Debug, Clone, Serialize, Deserialize)]
7pub struct Snapshot {
8    /// SHA256 hash of the problem.
9    pub problem_hash: String,
10    /// Branch tree structure.
11    pub branch_tree: BranchTree,
12    /// Learned clauses.
13    pub learned_clauses: Vec<Vec<i64>>,
14    /// PRNG state.
15    pub prng_state: PrngState,
16    /// Solver configuration.
17    pub solver_config: SolverConfig,
18}
19
20/// Branch tree structure in snapshot.
21#[derive(Debug, Clone, Serialize, Deserialize)]
22pub struct BranchTree {
23    /// All branches.
24    pub branches: Vec<BranchInfo>,
25}
26
27/// Information about a single branch.
28#[derive(Debug, Clone, Serialize, Deserialize)]
29pub struct BranchInfo {
30    /// Branch ID.
31    pub id: String,
32    /// Parent branch ID (None for root).
33    pub parent_id: Option<String>,
34    /// Depth in the tree.
35    pub depth: u32,
36    /// Current status.
37    pub status: BranchStatus,
38}
39
40/// Branch status.
41#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
42#[serde(rename_all = "lowercase")]
43pub enum BranchStatus {
44    Active,
45    Failed,
46    Solved,
47}
48
49/// PRNG state for reproducibility.
50#[derive(Debug, Clone, Serialize, Deserialize)]
51pub struct PrngState {
52    /// XorShift64 state.
53    pub xorshift_state: u64,
54}
55
56/// Solver configuration.
57#[derive(Debug, Clone, Serialize, Deserialize)]
58pub struct SolverConfig {
59    /// Number of CPU workers.
60    pub cpu_workers: usize,
61    /// Number of GPU workers (warps).
62    pub gpu_workers: usize,
63    /// Decision heuristic weights.
64    pub heuristic_weights: HeuristicWeights,
65}
66
67/// Weights for decision heuristics.
68#[derive(Debug, Clone, Serialize, Deserialize)]
69pub struct HeuristicWeights {
70    /// VSIDS weight.
71    pub vsids: f64,
72    /// EVSIDS weight.
73    pub evsids: f64,
74    /// LRB weight.
75    pub lrb: f64,
76}
77
78impl Default for HeuristicWeights {
79    fn default() -> Self {
80        Self {
81            vsids: 0.4,
82            evsids: 0.3,
83            lrb: 0.3,
84        }
85    }
86}
87
88impl Snapshot {
89    /// Serializes to JSON.
90    pub fn to_json(&self) -> Result<String, serde_json::Error> {
91        serde_json::to_string_pretty(self)
92    }
93
94    /// Deserializes from JSON.
95    pub fn from_json(json: &str) -> Result<Self, serde_json::Error> {
96        serde_json::from_str(json)
97    }
98}
satellite_format/snapshot.rs

satellite_format/
snapshot.rs
