feat:implemented batsat api

Cargo.toml

@@ -7,6 +7,7 @@ members = [
   "glucose",
   "minisat",
   "ipasir",
+  "batsat",
 ]
 resolver = "2"
 

batsat/Cargo.toml

@@ -0,0 +1,22 @@
+[package]
+name = "rustsat-batsat"
+version = "0.2.4"
+edition = "2021"
+authors = ["Noah Bruns <nbruns@efs.at>"]
+license = "MIT"
+description = "Interface to the SAT solver BatSat for the RustSAT library. BatSat is fully implemented in Rust"
+keywords = ["sat-solver", "rustsat", "batsat"]
+repository = "https://github.com/chrjabs/rustsat"
+readme = "README.md"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[features]
+debug = []
+
+[dependencies]
+batsat = "0.5.0"
+rustsat = { version = "0.4.3", path = "../rustsat", default-features = false, features = [
+] }
+anyhow = { version = "1.0.80" }
+thiserror = { version = "1.0.57" }

batsat/data

@@ -0,0 +1 @@
+../data

batsat/src/lib.rs

@@ -0,0 +1,107 @@
+//! # Minisat Solver Interface Without Preprocessing (Core)
+//!
+//! Interface to the [Minisat](https://github.com/niklasso/minisat) incremental
+//! SAT solver.
+
+use batsat::{intmap::AsIndex, lbool, BasicSolver, SolverInterface};
+use rustsat::{
+    solvers::{Solve, SolveIncremental, SolverResult},
+    types::{Clause, Lit, TernaryVal},
+};
+use thiserror::Error;
+
+#[derive(Error, Clone, Copy, PartialEq, Eq, Debug)]
+#[error("BatSat returned an invalid value: {error}")]
+pub struct InvalidApiReturn {
+    error: &'static str,
+}
+
+pub struct BatsatBasicSolver(BasicSolver);
+
+impl Default for BatsatBasicSolver {
+    fn default() -> BatsatBasicSolver {
+        BatsatBasicSolver(BasicSolver::default())
+    }
+}
+
+impl Extend<Clause> for BatsatBasicSolver {
+    fn extend<T: IntoIterator<Item = Clause>>(&mut self, iter: T) {
+        iter.into_iter()
+            .for_each(|cl| self.add_clause(cl).expect("Error adding clause in extend"))
+    }
+}
+
+impl Solve for BatsatBasicSolver {
+    fn signature(&self) -> &'static str {
+        "BatSat 0.5.0"
+    }
+
+    fn solve(&mut self) -> anyhow::Result<SolverResult> {
+        match self.0.solve_limited(&[]) {
+            x if x == lbool::TRUE => Ok(SolverResult::Sat),
+            x if x == lbool::FALSE => Ok(SolverResult::Unsat),
+            x if x == lbool::UNDEF => Err(InvalidApiReturn {
+                error: "BatSat Solver is in an UNSAT state".into(),
+            }
+            .into()),
+
+            _ => unreachable!(),
+        }
+    }
+
+    fn lit_val(&self, lit: Lit) -> anyhow::Result<TernaryVal> {
+        let l = batsat::Lit::new(batsat::Var::from_index(lit.vidx() + 1), lit.is_pos());
+
+        match self.0.value_lit(l) {
+            x if x == lbool::TRUE => Ok(TernaryVal::True),
+            x if x == lbool::FALSE => Ok(TernaryVal::False),
+            x if x == lbool::UNDEF => Ok(TernaryVal::DontCare),
+            _ => unreachable!(),
+        }
+    }
+
+    fn add_clause(&mut self, clause: Clause) -> anyhow::Result<()> {
+        let mut c: Vec<batsat::Lit> = clause
+            .iter()
+            .map(|l| batsat::Lit::new(self.0.var_of_int(l.vidx32() + 1), l.is_pos()))
+            .collect::<Vec<batsat::Lit>>();
+
+        match self.0.add_clause_reuse(&mut c) {
+            true => Ok(()),
+            false => Ok(()), //Err(SolverError::Api("Currently in an UNSAT state".into())),
+        }
+    }
+}
+
+impl SolveIncremental for BatsatBasicSolver {
+    fn solve_assumps(&mut self, assumps: &[Lit]) -> anyhow::Result<SolverResult> {
+        let a = assumps
+            .iter()
+            .map(|l| {
+                batsat::Lit::new(
+                    self.0.var_of_int((l.vidx32() + 1).try_into().unwrap()),
+                    l.is_pos(),
+                )
+            })
+            .collect::<Vec<_>>();
+
+        match self.0.solve_limited(&a) {
+            x if x == lbool::TRUE => Ok(SolverResult::Sat),
+            x if x == lbool::FALSE => Ok(SolverResult::Unsat),
+            x if x == lbool::UNDEF => Err(InvalidApiReturn {
+                error: "BatSat Solver is in an UNSAT state".into(),
+            }
+            .into()),
+            _ => unreachable!(),
+        }
+    }
+
+    fn core(&mut self) -> anyhow::Result<Vec<Lit>> {
+        Ok(self
+            .0
+            .unsat_core()
+            .iter()
+            .map(|l| Lit::new(l.var().idx() - 1, !l.sign()))
+            .collect::<Vec<_>>())
+    }
+}

batsat/tests/incremental.rs

@@ -0,0 +1,89 @@
+use rustsat::{
+    instances::{BasicVarManager, SatInstance},
+    lit,
+    solvers::{SolveIncremental, SolverResult},
+};
+use rustsat_batsat::BatsatBasicSolver;
+
+fn test_assumption_sequence<S: SolveIncremental>(mut solver: S) {
+    let inst: SatInstance<BasicVarManager> =
+        SatInstance::from_dimacs_path("./data/small.cnf").unwrap();
+    solver.add_cnf(inst.as_cnf().0).unwrap();
+    let res = solver.solve().unwrap();
+    assert_eq!(res, SolverResult::Sat);
+    let res = solver.solve_assumps(&[!lit![0], !lit![1]]).unwrap();
+    assert_eq!(res, SolverResult::Unsat);
+    let res = solver
+        .solve_assumps(&[lit![0], lit![1], lit![2], lit![3]])
+        .unwrap();
+    assert_eq!(res, SolverResult::Unsat);
+    let res = solver
+        .solve_assumps(&[lit![0], lit![1], lit![2], !lit![3]])
+        .unwrap();
+    assert_eq!(res, SolverResult::Unsat);
+    let res = solver
+        .solve_assumps(&[lit![0], lit![1], !lit![2], lit![3]])
+        .unwrap();
+    assert_eq!(res, SolverResult::Unsat);
+    let res = solver
+        .solve_assumps(&[lit![0], lit![1], !lit![2], !lit![3]])
+        .unwrap();
+    assert_eq!(res, SolverResult::Sat);
+    let res = solver
+        .solve_assumps(&[lit![0], !lit![1], lit![2], lit![3]])
+        .unwrap();
+    assert_eq!(res, SolverResult::Unsat);
+    let res = solver
+        .solve_assumps(&[lit![0], !lit![1], lit![2], !lit![3]])
+        .unwrap();
+    assert_eq!(res, SolverResult::Sat);
+    let res = solver
+        .solve_assumps(&[lit![0], !lit![1], !lit![2], lit![3]])
+        .unwrap();
+    assert_eq!(res, SolverResult::Unsat);
+    let res = solver
+        .solve_assumps(&[lit![0], !lit![1], !lit![2], !lit![3]])
+        .unwrap();
+    assert_eq!(res, SolverResult::Unsat);
+    let res = solver
+        .solve_assumps(&[!lit![0], lit![1], lit![2], lit![3]])
+        .unwrap();
+    assert_eq!(res, SolverResult::Unsat);
+    let res = solver
+        .solve_assumps(&[!lit![0], lit![1], lit![2], !lit![3]])
+        .unwrap();
+    assert_eq!(res, SolverResult::Unsat);
+    let res = solver
+        .solve_assumps(&[!lit![0], lit![1], !lit![2], lit![3]])
+        .unwrap();
+    assert_eq!(res, SolverResult::Sat);
+    let res = solver
+        .solve_assumps(&[!lit![0], lit![1], !lit![2], !lit![3]])
+        .unwrap();
+    assert_eq!(res, SolverResult::Sat);
+    let res = solver
+        .solve_assumps(&[!lit![0], !lit![1], lit![2], lit![3]])
+        .unwrap();
+    assert_eq!(res, SolverResult::Unsat);
+    let res = solver
+        .solve_assumps(&[!lit![0], !lit![1], lit![2], !lit![3]])
+        .unwrap();
+    assert_eq!(res, SolverResult::Unsat);
+    let res = solver
+        .solve_assumps(&[!lit![0], !lit![1], !lit![2], lit![3]])
+        .unwrap();
+    assert_eq!(res, SolverResult::Unsat);
+    let res = solver
+        .solve_assumps(&[!lit![0], !lit![1], !lit![2], !lit![3]])
+        .unwrap();
+    assert_eq!(res, SolverResult::Unsat);
+}
+
+#[test]
+fn assumption_sequence() {
+    let solver = BatsatBasicSolver::default();
+    test_assumption_sequence(solver);
+}
+
+// Note: Cannot test prepro version of minisat with this small example because
+// the variable are eliminated by preprocessing

batsat/tests/small.rs

@@ -0,0 +1,38 @@
+use rustsat::{
+    instances::{BasicVarManager, SatInstance},
+    solvers::{Solve, SolverResult},
+};
+use rustsat_batsat::BatsatBasicSolver;
+
+#[test]
+fn core_ms_segfault() {
+    let mut solver = BatsatBasicSolver::default();
+    let inst: SatInstance<BasicVarManager> =
+        SatInstance::from_dimacs_path("./data/minisat-segfault.cnf").unwrap();
+    solver.add_cnf(inst.as_cnf().0).unwrap();
+    let res = solver.solve().unwrap();
+    assert_eq!(res, SolverResult::Unsat);
+}
+
+#[test]
+fn simp_small_sat() {
+    let mut solver = BatsatBasicSolver::default();
+    let inst: SatInstance<BasicVarManager> =
+        SatInstance::from_dimacs_path("./data/AProVE11-12.cnf").unwrap();
+    solver.add_cnf(inst.as_cnf().0).unwrap();
+    let res = solver.solve().unwrap();
+    assert_eq!(res, SolverResult::Sat);
+}
+
+// Note: this instance seems too hard for minisat to solve
+#[test]
+#[ignore]
+fn simp_small_unsat() {
+    let mut solver = BatsatBasicSolver::default();
+    let inst: SatInstance<BasicVarManager> =
+        SatInstance::from_dimacs_path("./data/smtlib-qfbv-aigs-ext_con_032_008_0256-tseitin.cnf")
+            .unwrap();
+    solver.add_cnf(inst.as_cnf().0).unwrap();
+    let res = solver.solve().unwrap();
+    assert_eq!(res, SolverResult::Unsat);
+}