Skip to main content

SolverExecutor

sat_solvers::solvers

Trait SolverExecutor 

Source 
pub trait SolverExecutor {
    // Required methods
    fn get_solver_path(&self) -> PathBuf;
    fn execute(
        &self,
        dimacs: &str,
        timeout: Option<Duration>,
    ) -> Result<SATResult, SATSolverError>;
    fn get_args(&self, input_file: &Path) -> Vec<String>;
    fn parse_output(
        &self,
        stdout: &str,
        stderr: &str,
    ) -> Result<SATResult, SATSolverError>;
}
Expand description

Trait for SAT solver execution.

This trait provides a unified interface for executing different SAT solvers. Each solver implementation handles its specific command-line interface and output format.

§Implementors

  • cadical::CaDiCaLExecutor (requires cadical feature)
  • minisat::MiniSatExecutor (requires minisat feature)
  • [glucose::GlucoseExecutor] (requires glucose feature)
  • [lingeling::LingelingExecutor] (requires lingeling feature)
  • [kissat::KissatExecutor] (requires kissat feature)

§Example

use sat_solvers::solvers::SolverExecutor;
use std::time::Duration;

fn solve_with_any_executor(executor: &impl SolverExecutor, dimacs: &str) {
    let result = executor.execute(dimacs, Some(Duration::from_secs(30)));
    match result {
        Ok(r) => println!("Result: {}", r),
        Err(e) => eprintln!("Error: {}", e),
    }
}

Required Methods§

Source

fn get_solver_path(&self) -> PathBuf

Returns the path to the solver binary.

The path is typically determined at build time and embedded in the binary. It can often be overridden via environment variables.

Source

fn execute( &self, dimacs: &str, timeout: Option<Duration>, ) -> Result<SATResult, SATSolverError>

Executes the SAT solver with the given DIMACS input.

This is the main entry point for solving SAT problems. The input should be a valid DIMACS CNF formula.

§Arguments
  • dimacs - The SAT problem in DIMACS CNF format
  • timeout - Optional timeout duration. If None, no timeout is applied.
§Returns

Returns a SATResult indicating whether the problem is satisfiable, unsatisfiable, or unknown (e.g., due to timeout).

§Errors

Returns SATSolverError if:

Source

fn get_args(&self, input_file: &Path) -> Vec<String>

Returns solver-specific command-line arguments.

This method is used internally by execute to construct the command line for the solver.

§Arguments
  • input_file - Path to the temporary file containing the DIMACS input
Source

fn parse_output( &self, stdout: &str, stderr: &str, ) -> Result<SATResult, SATSolverError>

Parses the solver’s output to extract the result.

Each solver has its own output format. This method handles the solver-specific parsing logic.

§Arguments
  • stdout - The solver’s standard output
  • stderr - The solver’s standard error
§Errors

Returns SATSolverError::OutputParseError if the output cannot be parsed.

Implementors§