stalmarck_sat/core/
stalmarck.rs

1use crate::core::formula::Formula;
2use crate::parser::dimacs::Parser;
3use crate::solver::solver::{Dilemma, SimpleRuleStrategy, Solver};
4use crate::Result;
5
6/// Main solver class for Stålmarck's method
7#[derive(Debug, Default)]
8pub struct StalmarckSolver {
9    solver: Solver,
10    parser: Parser,
11    is_tautology_result: bool,
12    timeout: f64,
13    verbosity: i32,
14}
15
16impl StalmarckSolver {
17    /// Create a new Stalmarck solver
18    pub fn new() -> Self {
19        Self::default()
20    }
21
22    /// Solve from a file path
23    pub fn solve_from_file(&mut self, filename: &str) -> Result<bool> {
24        // Parse the DIMACS file
25        let parse_start = std::time::Instant::now();
26        let mut formula = self.parser.parse_dimacs(filename)?;
27        self.solver.statistics.parse_time = parse_start.elapsed();
28
29        // Solve the formula
30        self.solve(&mut formula)
31    }
32
33    /// Solve from a formula
34    pub fn solve(&mut self, formula: &mut Formula) -> Result<bool> {
35        // Set verbosity in the solver
36        self.solver.set_verbosity(self.verbosity);
37
38        // Set timeout in the solver
39        self.solver.set_timeout(self.timeout);
40
41        // Use the solver to determine if -F is a tautology
42        let is_negated_tautology = self.solver.solve(&mut formula.clone());
43
44        // Check if a timeout occurred
45        if self.solver.timeout_occurred() {
46            println!("UNKNOWN (Timeout)");
47            // Exit or handle the timeout case appropriately
48            // For now, we'll exit the process
49            std::process::exit(1);
50        }
51
52        // Store the result
53        self.is_tautology_result = is_negated_tautology;
54
55        // Return true if the original formula is satisfiable
56        let is_satisfiable = !is_negated_tautology;
57        if is_satisfiable {
58            let assignments = self.solver.get_assignments();
59            let num_vars = self.solver.get_num_original_variables();
60            let mut output = String::from("v");
61            for i in 1..=num_vars {
62                let var = i as i32;
63                if let Some(val) = assignments.get(&var) {
64                    if *val {
65                        output.push_str(&format!(" {}", var));
66                    } else {
67                        output.push_str(&format!(" -{}", var));
68                    }
69                } else {
70                    // If a variable is not in the assignments, it can be either true or false.
71                    // We'll default to false for this case.
72                    output.push_str(&format!(" -{}", var));
73                }
74            }
75            output.push_str(" 0");
76            println!("{}", output);
77        }
78
79        Ok(is_satisfiable)
80    }
81
82    /// Check if the formula is a tautology
83    pub fn is_tautology(&self) -> bool {
84        self.is_tautology_result
85    }
86
87    /// Set the timeout value in seconds
88    pub fn set_timeout(&mut self, seconds: f64) {
89        self.timeout = seconds;
90        self.solver.set_timeout(seconds);
91    }
92
93    /// Set the verbosity level
94    pub fn set_verbosity(&mut self, level: i32) {
95        self.verbosity = level;
96    }
97
98    /// Set the dilemma strategy
99    pub fn set_dilemma_strategy(&mut self, strategy: Dilemma) {
100        self.solver.set_dilemma_strategy(strategy);
101    }
102
103    /// Set the simple rule strategy
104    pub fn set_simple_rule_strategy(&mut self, strategy: SimpleRuleStrategy) {
105        self.solver.set_simple_rule_strategy(strategy);
106    }
107}
stalmarck_sat/core/stalmarck.rs

stalmarck_sat/core/
stalmarck.rs
