pubsat 0.1.0

//! Varisat SAT solver implementation
//!
//! This module provides a production-ready SAT solver using the Varisat
//! library, which is a pure Rust implementation of a modern CDCL SAT solver.

use std::time::{Duration, Instant};

use async_trait::async_trait;
use varisat::{CnfFormula, ExtendFormula, Lit, Solver, Var};

use crate::error::{SatError, SatResult};
use crate::sat::{
    Clause, Literal, SatModel, SatProblem, SatSolution, SatSolver, SolverConfig, SolverStats,
};

/// Varisat-based SAT solver implementation.
///
/// Supports both one-shot solving via [`SatSolver::solve`] (the
/// common path) and incremental solving via [`SatSolver::add_clauses`]
/// followed by [`SatSolver::solve_under_assumptions`]. Incrementally
/// added clauses persist across calls until [`SatSolver::reset`].
#[allow(dead_code)] // Configuration field reserved for future use
pub struct VarisatSolver {
    config: SolverConfig,
    stats: SolverStats,
    variable_count: u32,
    incremental_clauses: Vec<Clause>,
}

impl VarisatSolver {
    /// Create a new Varisat solver instance
    pub fn new(config: SolverConfig) -> SatResult<Self> {
        if let Some(_seed) = config.random_seed {
            // Varisat's public API does not expose a seed setter; reproducibility
            // for assumption-based workflows comes from deterministic clause and
            // variable ordering on the caller side.
            tracing::warn!("Random seed configuration not supported by varisat backend");
        }

        Ok(Self {
            config,
            stats: SolverStats::default(),
            variable_count: 0,
            incremental_clauses: Vec::new(),
        })
    }

    /// Convert our Literal to Varisat's Lit format
    fn convert_literal(literal: &Literal) -> SatResult<Lit> {
        if literal.variable == 0 {
            return Err(SatError::encoding_failed(
                "Variable numbers must be >= 1 (DIMACS standard)".to_string(),
            ));
        }

        // Varisat uses 0-based variables internally, but we use 1-based (DIMACS)
        let var = Var::from_index((literal.variable - 1) as usize);
        Ok(Lit::from_var(var, !literal.negated)) // Note: Varisat uses !negated
        // for positive
    }

    /// Convert our Clause to Varisat's format
    fn convert_clause(clause: &Clause) -> SatResult<Vec<Lit>> {
        clause.literals.iter().map(Self::convert_literal).collect()
    }

    /// Convert Varisat's model to our SatModel format
    #[allow(dead_code)] // Helper method reserved for future use
    fn convert_model(&self, model: &[bool]) -> SatModel {
        let mut sat_model = SatModel::new();

        // Convert from 0-based to 1-based variable numbering
        for (i, &value) in model.iter().enumerate() {
            sat_model.assign((i + 1) as u32, value);
        }

        sat_model
    }

    /// Ensure we have enough variables allocated
    fn ensure_variables(&mut self, max_variable: u32) -> SatResult<()> {
        if max_variable > self.variable_count {
            // Varisat automatically allocates variables as needed
            // We just track the count for our purposes
            self.variable_count = max_variable;
        }
        Ok(())
    }

    /// Add statistics from the solving process
    fn update_stats(&mut self, solve_time: Duration) {
        self.stats.solve_time = solve_time;

        // Varisat doesn't expose detailed statistics in the current version
        // We'll add estimated values based on problem size
        self.stats.decisions = self.variable_count as u64;
        self.stats.conflicts = 0; // Would need solver instrumentation
        self.stats.restarts = 0;
        self.stats.memory_usage = 0;
        self.stats.learned_clauses = 0;
    }
}

#[async_trait]
impl SatSolver for VarisatSolver {
    async fn solve(&mut self, problem: &SatProblem) -> SatResult<SatSolution> {
        let start = Instant::now();

        // Ensure we have enough variables
        self.ensure_variables(problem.num_variables)?;

        // Build a new formula for this solve
        let mut formula = CnfFormula::new();

        for clause in &problem.clauses {
            let varisat_clause = Self::convert_clause(clause)?;

            if varisat_clause.is_empty() {
                // Empty clause means immediate unsatisfiability
                self.update_stats(start.elapsed());
                return Ok(SatSolution::Unsatisfiable);
            }

            formula.add_clause(&varisat_clause);
        }

        // Add assumptions if any
        let assumptions: SatResult<Vec<Lit>> = problem
            .assumptions
            .iter()
            .map(Self::convert_literal)
            .collect();
        let assumptions = assumptions?;

        // Run the solver
        tracing::debug!(
            "Solving SAT problem with {} variables, {} clauses",
            problem.num_variables,
            problem.clauses.len()
        );

        // Create new solver and solve
        let _num_variables = self.variable_count;
        let _variable_count = self.variable_count;
        let res = tokio::task::spawn_blocking(move || {
            let mut solver = Solver::new();
            solver.add_formula(&formula);

            if !assumptions.is_empty() {
                solver.assume(&assumptions);
            }

            // Solve and extract model if SAT
            match solver.solve() {
                Ok(true) => {
                    let model_lits = solver.model().unwrap_or_default();
                    Ok::<_, varisat::solver::SolverError>((true, Some(model_lits)))
                }
                Ok(false) => Ok((false, None)),
                Err(e) => Err(e),
            }
        })
        .await
        .map_err(|e| SatError::solver_failure(format!("Solver task failed: {}", e)))?;

        let solve_time = start.elapsed();
        self.update_stats(solve_time);

        match res {
            Ok((true, Some(model_lits))) => {
                // Convert Varisat model literals to our SatModel
                let mut sat_model = SatModel::new();
                for lit in model_lits {
                    let var = (lit.var().index() + 1) as u32; // convert 0-based to 1-based
                    let value = lit.is_positive();
                    sat_model.assign(var, value);
                }

                tracing::debug!(
                    "SAT problem solved as satisfiable in {:?} with {} assigned variables",
                    solve_time,
                    sat_model.assignments.len()
                );

                Ok(SatSolution::Satisfiable(sat_model))
            }
            Ok((false, _)) => {
                tracing::debug!("SAT problem is unsatisfiable (solved in {:?})", solve_time);
                Ok(SatSolution::Unsatisfiable)
            }
            Ok((true, None)) => {
                tracing::error!("Varisat returned SAT but no model available");
                Err(SatError::solver_failure(
                    "Varisat returned SAT without a model".to_string(),
                ))
            }
            Err(e) => {
                tracing::error!("Varisat solver error: {:?}", e);
                Err(SatError::solver_failure(format!("Varisat error: {:?}", e)))
            }
        }
    }

    async fn solve_with_timeout(
        &mut self,
        problem: &SatProblem,
        timeout: Duration,
    ) -> SatResult<SatSolution> {
        // Use tokio's timeout functionality
        match tokio::time::timeout(timeout, self.solve(problem)).await {
            Ok(result) => result,
            Err(_) => {
                tracing::warn!("SAT solver timed out after {:?}", timeout);
                Ok(SatSolution::Unknown)
            }
        }
    }

    async fn add_clauses(&mut self, clauses: &[Clause]) -> SatResult<()> {
        let max_var = clauses
            .iter()
            .flat_map(|clause| clause.literals.iter())
            .map(|lit| lit.variable)
            .max()
            .unwrap_or(0);

        self.ensure_variables(max_var)?;

        // Validate every literal up front so a malformed clause is rejected
        // before any state mutates.
        for clause in clauses {
            for literal in &clause.literals {
                if literal.variable == 0 {
                    return Err(SatError::encoding_failed(
                        "Variable numbers must be >= 1 (DIMACS standard)".to_string(),
                    ));
                }
            }
        }

        self.incremental_clauses.extend_from_slice(clauses);

        tracing::debug!(
            "Added {} clauses to Varisat solver (total stored: {})",
            clauses.len(),
            self.incremental_clauses.len()
        );
        Ok(())
    }

    async fn solve_under_assumptions(&mut self, assumptions: &[Literal]) -> SatResult<SatSolution> {
        let assumption_max_var = assumptions
            .iter()
            .map(|lit| lit.variable)
            .max()
            .unwrap_or(0);
        let num_vars = self.variable_count.max(assumption_max_var);

        let mut problem = SatProblem::new(num_vars);
        for clause in &self.incremental_clauses {
            problem.add_clause(clause.clone());
        }
        for &assumption in assumptions {
            problem.add_assumption(assumption);
        }

        self.solve(&problem).await
    }

    fn get_stats(&self) -> SolverStats {
        self.stats.clone()
    }

    fn reset(&mut self) {
        self.stats = SolverStats::default();
        self.variable_count = 0;
        self.incremental_clauses.clear();

        tracing::debug!("Reset Varisat solver");
    }

    fn name(&self) -> &'static str {
        "Varisat"
    }
}

#[cfg(test)]
mod tests {
    use super::*;
    use crate::sat::{Clause, Literal, SatProblem};

    #[tokio::test]
    async fn test_varisat_simple_satisfiable() {
        let config = SolverConfig::default();
        let mut solver = VarisatSolver::new(config).unwrap();

        // Simple problem: (x1 ∨ x2) ∧ (¬x1 ∨ x2) ∧ (x1 ∨ ¬x2)
        // This should be satisfiable with x1=true, x2=true
        let mut problem = SatProblem::new(2);

        problem.add_clause(Clause::binary(Literal::positive(1), Literal::positive(2)));

        problem.add_clause(Clause::binary(Literal::negative(1), Literal::positive(2)));

        problem.add_clause(Clause::binary(Literal::positive(1), Literal::negative(2)));

        let result = solver.solve(&problem).await.unwrap();

        match result {
            SatSolution::Satisfiable(model) => {
                // Should have assignments for variables 1 and 2
                assert!(model.is_assigned(1));
                assert!(model.is_assigned(2));
                println!("Solution: x1={:?}, x2={:?}", model.get(1), model.get(2));
            }
            _ => panic!("Expected satisfiable solution"),
        }
    }

    #[tokio::test]
    async fn test_varisat_unsatisfiable() {
        let config = SolverConfig::default();
        let mut solver = VarisatSolver::new(config).unwrap();

        // Unsatisfiable problem: x1 ∧ ¬x1
        let mut problem = SatProblem::new(1);

        problem.add_clause(Clause::unit(Literal::positive(1)));
        problem.add_clause(Clause::unit(Literal::negative(1)));

        let result = solver.solve(&problem).await.unwrap();

        assert_eq!(result, SatSolution::Unsatisfiable);
    }

    #[tokio::test]
    async fn test_varisat_with_assumptions() {
        let config = SolverConfig::default();
        let mut solver = VarisatSolver::new(config).unwrap();

        // Add clauses first
        let clauses = vec![Clause::binary(Literal::positive(1), Literal::positive(2))];

        solver.add_clauses(&clauses).await.unwrap();

        // Test with assumption x1 = false
        let assumptions = vec![Literal::negative(1)];
        let result = solver.solve_under_assumptions(&assumptions).await.unwrap();

        match result {
            SatSolution::Satisfiable(model) => {
                // With x1 = false, we need x2 = true to satisfy the clause
                assert_eq!(model.get(1), Some(false));
                assert_eq!(model.get(2), Some(true));
            }
            _ => panic!("Expected satisfiable solution"),
        }
    }

    #[tokio::test]
    async fn test_varisat_performance() {
        let config = SolverConfig::default();
        let mut solver = VarisatSolver::new(config).unwrap();

        // Create a larger problem to test performance
        let num_vars = 100;
        let mut problem = SatProblem::new(num_vars);

        // Add some constraints: each pair of variables has at most one true
        for i in 1..=num_vars {
            for j in (i + 1)..=num_vars {
                problem.add_clause(Clause::binary(Literal::negative(i), Literal::negative(j)));
            }
        }

        // Force at least one variable to be true
        let mut at_least_one_literals = Vec::new();
        for i in 1..=num_vars {
            at_least_one_literals.push(Literal::positive(i));
        }
        problem.add_clause(Clause::new(at_least_one_literals));

        let start = std::time::Instant::now();
        let result = solver.solve(&problem).await.unwrap();
        let solve_time = start.elapsed();

        println!("Solved {}-variable problem in {:?}", num_vars, solve_time);

        match result {
            SatSolution::Satisfiable(model) => {
                let true_count = model.true_variables().len();
                assert_eq!(true_count, 1); // Exactly one should be true
                println!("Solution has {} true variables", true_count);
            }
            _ => panic!("Expected satisfiable solution"),
        }

        // Should solve reasonably quickly
        assert!(solve_time < Duration::from_secs(1));
    }
}