sat_solvers/solvers/

minisat.rs

//! MiniSat SAT solver executor.
//!
//! This module provides the [`MiniSatExecutor`] for running the MiniSat SAT solver.
//! MiniSat is a minimalistic, open-source SAT solver that serves as a reference
//! implementation for CDCL solvers and is widely used in education and research.
//!
//! # Example
//!
//! ```no_run
//! use sat_solvers::solvers::minisat::MiniSatExecutor;
//! use sat_solvers::solvers::SolverExecutor;
//! use std::time::Duration;
//!
//! let executor = MiniSatExecutor;
//! let dimacs = "p cnf 3 2\n1 -2 0\n2 3 0\n";
//!
//! let result = executor.execute(dimacs, Some(Duration::from_secs(30))).unwrap();
//! println!("Result: {}", result);
//! ```

use log::warn;
use tempfile::NamedTempFile;

use std::{
    io::{Read, Write},
    path::{Path, PathBuf},
    time::Duration,
};

use crate::minisat_path;

use super::{SATResult, SATSolverError, SolverExecutor, execute_with_timeout};

/// 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
///
/// ```no_run
/// 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),
/// }
/// ```
pub struct MiniSatExecutor;

impl SolverExecutor for MiniSatExecutor {
    fn get_solver_path(&self) -> PathBuf {
        minisat_path()
    }

    fn execute(
        &self,
        dimacs: &str,
        timeout: Option<Duration>,
    ) -> Result<SATResult, SATSolverError> {
        let mut input_file = NamedTempFile::new()?;
        input_file.write_all(dimacs.as_bytes())?;
        input_file.flush()?;

        let output_file = NamedTempFile::new()?;

        let mut args = self.get_args(input_file.path());
        args.push(output_file.path().to_string_lossy().to_string());

        let (_, stderr) = execute_with_timeout(&self.get_solver_path(), &args, timeout)?;
        let mut stdout = String::new();
        output_file
            .into_file()
            .read_to_string(&mut stdout)
            .map_err(|e| {
                SATSolverError::OutputParseError(format!(
                    "Error reading minisat output file: {:?}",
                    e
                ))
            })?;
        self.parse_output(&stdout, &stderr)
    }

    fn get_args(&self, input_file: &Path) -> Vec<String> {
        vec![
            "-verb=0".to_string(), // Minimal verbosity for cleaner output
            input_file.to_string_lossy().to_string(), // Note: MiniSat outputs to stdout by default if no result file specified
        ]
    }

    fn parse_output(&self, stdout: &str, stderr: &str) -> Result<SATResult, SATSolverError> {
        let mut is_sat = None;
        let mut assignment = Vec::new();
        let mut found_assignment_line = false;

        for line in stdout.lines() {
            let line = line.trim();

            match line {
                "SAT" | "UNSAT" => {
                    if is_sat.is_some() {
                        return Err(SATSolverError::OutputParseError(
                            "Multiple satisfiability results found".to_string(),
                        ));
                    }
                    is_sat = Some(line == "SAT");
                }
                _ if !line.is_empty()
                    && !line.starts_with('c')
                    && is_sat == Some(true)
                    && !found_assignment_line =>
                {
                    // MiniSat outputs assignment as space-separated literals on next line after "SAT"
                    // No "v " prefix like other solvers
                    found_assignment_line = true;

                    let vars: Vec<i32> = line
                        .split_whitespace()
                        .filter_map(|s| s.parse().ok())
                        .filter(|&x| x != 0) // Remove terminating 0 if present
                        .collect();

                    for var in vars {
                        assignment.push(var);
                    }
                }
                _ => continue,
            }
        }

        // Process stderr for any warnings or errors
        for line in stderr.lines() {
            if line.trim().starts_with("c ") {
                continue;
            }

            warn!("{}", line.trim());
        }

        match is_sat {
            Some(true) => Ok(SATResult::Satisfiable(assignment)),
            Some(false) => Ok(SATResult::Unsatisfiable),
            None => Err(SATSolverError::OutputParseError(
                "No satisfiability result found".to_string(),
            )),
        }
    }
}

#[cfg(test)]
mod tests {
    use super::*;

    #[test]
    fn test_parse_output() {
        let executor = MiniSatExecutor;
        let stdout = "SAT\n1 -2 3 0\n";
        let stderr = "";

        let result = executor.parse_output(stdout, stderr).unwrap();
        match result {
            SATResult::Satisfiable(assignment) => {
                assert_eq!(assignment.len(), 3);
            }
            _ => panic!("Expected satisfiable result"),
        }
    }

    #[test]
    fn test_parse_unsat_output() {
        let executor = MiniSatExecutor;
        let stdout = "UNSAT\n";
        let stderr = "";

        let result = executor.parse_output(stdout, stderr).unwrap();
        assert!(matches!(result, SATResult::Unsatisfiable));
    }

    #[test]
    fn test_parse_invalid_output() {
        let executor = MiniSatExecutor;

        // Test multiple satisfiability results
        let stdout = "UNSAT\nSAT\n";
        let stderr = "";
        assert!(executor.parse_output(stdout, stderr).is_err());

        // Test assignment without satisfiability result
        let stdout = "v 1 -2 3 0\n";
        let stderr = "";
        assert!(executor.parse_output(stdout, stderr).is_err());

        // Test no result
        let stdout = "c This is just a comment\n";
        let stderr = "";
        assert!(executor.parse_output(stdout, stderr).is_err());
    }
}