stalmarck_sat/solver/
statistics.rs

1use std::time::{Duration, Instant};
2
3/// Statistics for tracking solver performance and progress
4#[derive(Debug, Default, Clone)]
5pub struct SolverStatistics {
6    /// Number of times solve_recursive has been called
7    pub recursive_calls: usize,
8    /// Number of times simple rules have been applied
9    pub simple_rule_applications: usize,
10    /// Number of subproblems created in the search tree
11    pub subproblems_explored: usize,
12    /// Maximum depth reached during recursive solving
13    pub max_depth: usize,
14    /// Number of times dilemma rule was applied (branching)
15    pub dilemma_rule_applications: usize,
16    /// Total time spent in parsing
17    pub parse_time: Duration,
18    /// Total time spent in translation
19    pub translate_time: Duration,
20    /// Total time spent in search
21    pub search_time: Duration,
22    /// Start time for the solver
23    start_time: Option<Instant>,
24}
25
26impl SolverStatistics {
27    /// Create a new instance of `SolverStatistics`
28    pub fn new() -> Self {
29        Self::default()
30    }
31
32    /// Reset all statistics to zero
33    pub fn reset(&mut self) {
34        self.recursive_calls = 0;
35        self.simple_rule_applications = 0;
36        self.subproblems_explored = 0;
37        self.max_depth = 0;
38        self.dilemma_rule_applications = 0;
39        self.parse_time = Duration::default();
40        self.translate_time = Duration::default();
41        self.search_time = Duration::default();
42        self.start_time = Some(Instant::now());
43    }
44
45    /// Increment the recursive calls counter
46    pub fn increment_recursive_calls(&mut self) {
47        self.recursive_calls += 1;
48    }
49
50    /// Increment the simple rule applications counter
51    pub fn increment_simple_rule_applications(&mut self) {
52        self.simple_rule_applications += 1;
53    }
54
55    /// Increment the subproblems explored counter
56    pub fn increment_subproblems_explored(&mut self) {
57        self.subproblems_explored += 1;
58    }
59
60    /// Update the maximum depth if current depth is greater
61    pub fn update_max_depth(&mut self, depth: usize) {
62        if depth > self.max_depth {
63            self.max_depth = depth;
64        }
65    }
66
67    /// Increment the dilemma rule applications counter
68    pub fn increment_dilemma_rule_applications(&mut self) {
69        self.dilemma_rule_applications += 1;
70    }
71
72    /// Print final statistics summary
73    pub fn print_summary(&self, verbosity: i32) {
74        if verbosity > 0 {
75            println!("\n=== Search Statistics ===");
76            println!("Total iterations: {}", self.recursive_calls);
77            println!(
78                "Total simple rule applications: {}",
79                self.simple_rule_applications
80            );
81            println!(
82                "Total dilemma rule applications: {}",
83                self.dilemma_rule_applications
84            );
85            println!("Total subproblems explored: {}", self.subproblems_explored);
86            println!("Maximum depth reached: {}", self.max_depth);
87            println!("=========================");
88
89            if verbosity >= 1 {
90                println!("\n--- [ run-time profiling ] -------------------------------------------------");
91                let total_solve_time = self.parse_time + self.translate_time + self.search_time;
92                if total_solve_time.as_secs_f64() > 0.0 {
93                    let parse_percent =
94                        (self.parse_time.as_secs_f64() / total_solve_time.as_secs_f64()) * 100.0;
95                    let translate_percent = (self.translate_time.as_secs_f64()
96                        / total_solve_time.as_secs_f64())
97                        * 100.0;
98                    let search_percent =
99                        (self.search_time.as_secs_f64() / total_solve_time.as_secs_f64()) * 100.0;
100
101                    println!(
102                        "{:10.2}s {:8.2}% parse",
103                        self.parse_time.as_secs_f64(),
104                        parse_percent
105                    );
106                    println!(
107                        "{:10.2}s {:8.2}% translate",
108                        self.translate_time.as_secs_f64(),
109                        translate_percent
110                    );
111                    println!(
112                        "{:10.2}s {:8.2}% search",
113                        self.search_time.as_secs_f64(),
114                        search_percent
115                    );
116                }
117                println!(
118                    "--------------------------------------------------------------------------"
119                );
120            }
121        }
122    }
123
124    /// Print progress information with specified verbosity level
125    pub fn print_progress(&self, _depth: usize, verbosity: i32) {
126        if verbosity >= 2 {
127            println!("Iteration number: {}", self.recursive_calls);
128            println!(
129                "Simple Rule Applications: {}, Dilemma Rule Applications: {}, Subproblems Explored: {}\n",
130                self.simple_rule_applications, self.dilemma_rule_applications, self.subproblems_explored
131            );
132            println!("=========================\n");
133        }
134    }
135}
stalmarck_sat/solver/statistics.rs

stalmarck_sat/solver/
statistics.rs
