sat_solvers/solvers/
mod.rs

1//! SAT solver executors and utilities.
2//!
3//! This module provides the [`SolverExecutor`] trait and implementations for
4//! each supported SAT solver. It also includes utilities for executing solvers
5//! with timeout support.
6//!
7//! # Available Executors
8//!
9//! Each solver has its own executor type (enabled via feature flags):
10//!
11//! - [`cadical::CaDiCaLExecutor`] - CaDiCaL solver (feature: `cadical`)
12//! - [`minisat::MiniSatExecutor`] - MiniSat solver (feature: `minisat`)
13//! - [`glucose::GlucoseExecutor`] - Glucose solver (feature: `glucose`)
14//! - [`lingeling::LingelingExecutor`] - Lingeling solver (feature: `lingeling`)
15//! - [`kissat::KissatExecutor`] - Kissat solver (feature: `kissat`)
16//!
17//! # Example
18//!
19//! ```no_run
20//! use sat_solvers::solvers::SolverExecutor;
21//! use sat_solvers::SATResult;
22//! use std::time::Duration;
23//!
24//! # #[cfg(feature = "cadical")]
25//! # fn main() {
26//! use sat_solvers::solvers::cadical::CaDiCaLExecutor;
27//!
28//! let executor = CaDiCaLExecutor;
29//! let dimacs = "p cnf 2 1\n1 2 0\n";
30//!
31//! match executor.execute(dimacs, Some(Duration::from_secs(60))) {
32//!     Ok(SATResult::Satisfiable(assignment)) => {
33//!         println!("SAT: {:?}", assignment);
34//!     }
35//!     Ok(SATResult::Unsatisfiable) => println!("UNSAT"),
36//!     Ok(SATResult::Unknown) => println!("UNKNOWN"),
37//!     Err(e) => eprintln!("Error: {}", e),
38//! }
39//! # }
40//! # #[cfg(not(feature = "cadical"))]
41//! # fn main() {}
42//! ```
43
44use thiserror::Error;
45
46use std::{
47    path::{Path, PathBuf},
48    process::{Command, Stdio},
49    thread,
50    time::{Duration, Instant},
51};
52
53use super::SATResult;
54
55#[cfg(feature = "cadical")]
56pub mod cadical;
57#[cfg(feature = "glucose")]
58pub mod glucose;
59#[cfg(feature = "kissat")]
60pub mod kissat;
61#[cfg(feature = "lingeling")]
62pub mod lingeling;
63#[cfg(feature = "minisat")]
64pub mod minisat;
65
66/// Errors that can occur during SAT solver execution.
67///
68/// This error type covers all failure modes when running a SAT solver,
69/// including I/O errors, process failures, timeouts, and output parsing issues.
70#[derive(Error, Debug)]
71pub enum SATSolverError {
72    /// An I/O error occurred (e.g., failed to spawn process or write temp file).
73    #[error("I/O error: {0}")]
74    Io(#[from] std::io::Error),
75
76    /// The solver process crashed with a non-standard exit code.
77    ///
78    /// Standard exit codes (10 = SAT, 20 = UNSAT, 0 = success) are not errors.
79    #[error("Process crashed with exit code: {code:?}")]
80    ProcessCrashed {
81        /// The exit code, or `None` if the process was terminated by a signal.
82        code: Option<i32>,
83    },
84
85    /// The solver exceeded the specified timeout.
86    ///
87    /// When this occurs, the solver process is killed and this error is returned.
88    #[error("Solver timed out after {timeout:?}")]
89    Timeout {
90        /// The timeout duration that was exceeded.
91        timeout: Duration,
92    },
93
94    /// Failed to parse the solver's output.
95    ///
96    /// This can occur if the solver produces unexpected output format,
97    /// or if there are inconsistencies in the output.
98    #[error("Output parsing error: {0}")]
99    OutputParseError(String),
100}
101
102/// Trait for SAT solver execution.
103///
104/// This trait provides a unified interface for executing different SAT solvers.
105/// Each solver implementation handles its specific command-line interface and
106/// output format.
107///
108/// # Implementors
109///
110/// - [`cadical::CaDiCaLExecutor`] (requires `cadical` feature)
111/// - [`minisat::MiniSatExecutor`] (requires `minisat` feature)
112/// - [`glucose::GlucoseExecutor`] (requires `glucose` feature)
113/// - [`lingeling::LingelingExecutor`] (requires `lingeling` feature)
114/// - [`kissat::KissatExecutor`] (requires `kissat` feature)
115///
116/// # Example
117///
118/// ```no_run
119/// use sat_solvers::solvers::SolverExecutor;
120/// use std::time::Duration;
121///
122/// # #[cfg(feature = "cadical")]
123/// fn solve_with_any_executor(executor: &impl SolverExecutor, dimacs: &str) {
124///     let result = executor.execute(dimacs, Some(Duration::from_secs(30)));
125///     match result {
126///         Ok(r) => println!("Result: {}", r),
127///         Err(e) => eprintln!("Error: {}", e),
128///     }
129/// }
130/// ```
131pub trait SolverExecutor {
132    /// Returns the path to the solver binary.
133    ///
134    /// The path is typically determined at build time and embedded in the binary.
135    /// It can often be overridden via environment variables.
136    fn get_solver_path(&self) -> PathBuf;
137
138    /// Executes the SAT solver with the given DIMACS input.
139    ///
140    /// This is the main entry point for solving SAT problems. The input should
141    /// be a valid DIMACS CNF formula.
142    ///
143    /// # Arguments
144    ///
145    /// * `dimacs` - The SAT problem in DIMACS CNF format
146    /// * `timeout` - Optional timeout duration. If `None`, no timeout is applied.
147    ///
148    /// # Returns
149    ///
150    /// Returns a [`SATResult`] indicating whether the problem is satisfiable,
151    /// unsatisfiable, or unknown (e.g., due to timeout).
152    ///
153    /// # Errors
154    ///
155    /// Returns [`SATSolverError`] if:
156    /// - The solver process fails to start ([`SATSolverError::Io`])
157    /// - The solver crashes ([`SATSolverError::ProcessCrashed`])
158    /// - The timeout is exceeded ([`SATSolverError::Timeout`])
159    /// - The output cannot be parsed ([`SATSolverError::OutputParseError`])
160    fn execute(&self, dimacs: &str, timeout: Option<Duration>)
161    -> Result<SATResult, SATSolverError>;
162
163    /// Returns solver-specific command-line arguments.
164    ///
165    /// This method is used internally by [`execute`](SolverExecutor::execute)
166    /// to construct the command line for the solver.
167    ///
168    /// # Arguments
169    ///
170    /// * `input_file` - Path to the temporary file containing the DIMACS input
171    fn get_args(&self, input_file: &Path) -> Vec<String>;
172
173    /// Parses the solver's output to extract the result.
174    ///
175    /// Each solver has its own output format. This method handles the
176    /// solver-specific parsing logic.
177    ///
178    /// # Arguments
179    ///
180    /// * `stdout` - The solver's standard output
181    /// * `stderr` - The solver's standard error
182    ///
183    /// # Errors
184    ///
185    /// Returns [`SATSolverError::OutputParseError`] if the output cannot be parsed.
186    fn parse_output(&self, stdout: &str, stderr: &str) -> Result<SATResult, SATSolverError>;
187}
188
189/// Executes a command with an optional timeout.
190///
191/// This is a helper function used by solver executors to run the solver binary
192/// with timeout support.
193///
194/// # Arguments
195///
196/// * `solver_path` - Path to the solver binary
197/// * `args` - Command-line arguments for the solver
198/// * `timeout` - Optional timeout duration. If `None`, the maximum possible
199///   duration is used (effectively no timeout).
200///
201/// # Returns
202///
203/// Returns a tuple of `(stdout, stderr)` as strings.
204///
205/// # Errors
206///
207/// Returns [`SATSolverError`] if:
208/// - The process fails to spawn ([`SATSolverError::Io`])
209/// - The process crashes with a non-standard exit code ([`SATSolverError::ProcessCrashed`])
210/// - The timeout is exceeded ([`SATSolverError::Timeout`])
211///
212/// # Exit Code Handling
213///
214/// The following exit codes are considered successful:
215/// - `10`: SATISFIABLE (standard SAT solver convention)
216/// - `20`: UNSATISFIABLE (standard SAT solver convention)
217/// - `0`: General success
218///
219/// Any other exit code is treated as a crash.
220pub fn execute_with_timeout(
221    solver_path: &Path,
222    args: &[String],
223    timeout: Option<Duration>,
224) -> Result<(String, String), SATSolverError> {
225    let mut cmd = Command::new(solver_path);
226    cmd.args(args).stdout(Stdio::piped()).stderr(Stdio::piped());
227
228    let mut child = cmd.spawn()?;
229    let timeout = timeout.unwrap_or(Duration::from_secs(u64::MAX));
230    let start_time = Instant::now();
231
232    // Wait for completion or timeout
233    loop {
234        match child.try_wait()? {
235            Some(status) => {
236                if let Some(code) = status.code() {
237                    match code {
238                        10 => break, // SATISFIABLE
239                        20 => break, // UNSATISFIABLE
240                        0 => break,  // SUCCESS
241                        _ => {
242                            return Err(SATSolverError::ProcessCrashed { code: Some(code) });
243                        }
244                    }
245                }
246                break;
247            }
248            None => {
249                if start_time.elapsed() > timeout {
250                    let _ = child.kill();
251                    let _ = child.wait();
252                    return Err(SATSolverError::Timeout { timeout });
253                }
254                thread::sleep(Duration::from_millis(100));
255            }
256        }
257    }
258
259    let output = child.wait_with_output()?;
260    let stdout = String::from_utf8_lossy(&output.stdout).to_string();
261    let stderr = String::from_utf8_lossy(&output.stderr).to_string();
262
263    Ok((stdout, stderr))
264}
sat_solvers/solvers/mod.rs

sat_solvers/solvers/
mod.rs
