1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16

use crate::formula::{Cnf, Model};

mod cdcl;
mod dpll;

pub use cdcl::CdclSolver;
pub use dpll::DpllSolver;

pub trait Solver {
    /// Creates a new solver instance.
    fn new(formula: Cnf) -> Self;

    /// Solves a CNF SAT problem with the solver.
    /// Returns `Some(Model)` if satisfiable, `None` otherwise.
    fn solve(self) -> Option<Model>;
}