Struct MiniSatExecutor 

pub struct MiniSatExecutor;

Executor for the MiniSat SAT solver.

MiniSat is one of the most widely used and studied SAT solvers. It provides a clean, efficient implementation of the CDCL algorithm and serves as the foundation for many other solvers including Glucose.

Output Format

Unlike other solvers, MiniSat outputs results to a file rather than stdout. The executor handles this automatically by creating a temporary output file.

Example

use sat_solvers::solvers::minisat::MiniSatExecutor;
use sat_solvers::solvers::SolverExecutor;
use sat_solvers::SATResult;
use std::time::Duration;

let executor = MiniSatExecutor;

// Simple satisfiable formula: (x1 OR NOT x2) AND (x2 OR x3)
let dimacs = "p cnf 3 2\n1 -2 0\n2 3 0\n";

match executor.execute(dimacs, Some(Duration::from_secs(60))) {
    Ok(SATResult::Satisfiable(assignment)) => {
        println!("SAT! Assignment: {:?}", assignment);
    }
    Ok(SATResult::Unsatisfiable) => println!("UNSAT"),
    Ok(SATResult::Unknown) => println!("Unknown"),
    Err(e) => eprintln!("Error: {}", e),
}

Trait Implementations

impl SolverExecutor for MiniSatExecutor

fn get_solver_path(&self) -> PathBuf

Returns the path to the solver binary.

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

Executes the SAT solver with the given DIMACS input.

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

Returns solver-specific command-line arguments.

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

Parses the solver’s output to extract the result.