sat_solvers/solvers/

cadical.rs

//! CaDiCaL SAT solver executor.
//!
//! This module provides the [`CaDiCaLExecutor`] for running the CaDiCaL SAT solver.
//! CaDiCaL is a state-of-the-art CDCL (Conflict-Driven Clause Learning) SAT solver
//! developed by Armin Biere, winner of multiple SAT Competitions.
//!
//! # Example
//!
//! ```no_run
//! use sat_solvers::solvers::cadical::CaDiCaLExecutor;
//! use sat_solvers::solvers::SolverExecutor;
//! use std::time::Duration;
//!
//! let executor = CaDiCaLExecutor;
//! 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::Write,
    path::{Path, PathBuf},
    time::Duration,
};

use crate::cadical_path;

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

/// Executor for the CaDiCaL SAT solver.
///
/// CaDiCaL is a high-performance CDCL SAT solver known for its excellent
/// performance on industrial SAT instances. It has won multiple tracks
/// in SAT Competitions.
///
/// # Features
///
/// - State-of-the-art CDCL algorithm
/// - Efficient clause learning and deletion strategies
/// - Inprocessing techniques
///
/// # Example
///
/// ```no_run
/// use sat_solvers::solvers::cadical::CaDiCaLExecutor;
/// use sat_solvers::solvers::SolverExecutor;
/// use sat_solvers::SATResult;
/// use std::time::Duration;
///
/// let executor = CaDiCaLExecutor;
///
/// // 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 CaDiCaLExecutor;

impl SolverExecutor for CaDiCaLExecutor {
    fn get_solver_path(&self) -> PathBuf {
        cadical_path()
    }

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

        let args = self.get_args(temp_file.path());
        let (stdout, stderr) = execute_with_timeout(&self.get_solver_path(), &args, timeout)?;
        self.parse_output(&stdout, &stderr)
    }

    fn get_args(&self, input_file: &Path) -> Vec<String> {
        // Note: CaDiCaL prints witness by default, and uses "s SATISFIABLE"/"s UNSATISFIABLE" format
        vec![input_file.to_string_lossy().to_string()]
    }

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

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

            match line {
                "s SATISFIABLE" | "s UNSATISFIABLE" => {
                    if is_sat.is_some() {
                        return Err(SATSolverError::OutputParseError(
                            "Multiple satisfiability results found".to_string(),
                        ));
                    }

                    is_sat = Some(line == "s SATISFIABLE");
                }
                _ if line.starts_with("v ") => {
                    if let Some(false) = is_sat {
                        return Err(SATSolverError::OutputParseError(
                            "Variable assignment found before satisfiability result".to_string(),
                        ));
                    }

                    if is_sat.is_none() {
                        return Err(SATSolverError::OutputParseError(
                            "Variable assignment found without satisfiability result".to_string(),
                        ));
                    }

                    let vars: Vec<i32> = line[2..]
                        .split_whitespace()
                        .filter_map(|s| s.parse().ok())
                        .filter(|&x| x != 0) // Remove terminating 0
                        .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 = CaDiCaLExecutor;
        let stdout = "s SATISFIABLE\nv 1 -2 3 0\n";
        let stderr = "";

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

    #[test]
    fn test_parse_unsat_output() {
        let executor = CaDiCaLExecutor;
        let stdout = "s UNSATISFIABLE\n";
        let stderr = "";

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

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

        // Test multiple satisfiability results
        let stdout = "s SATISFIABLE\ns UNSATISFIABLE\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());
    }
}