Implemented an interface to BatSat

.github/workflows/batsat.yml

@@ -0,0 +1,30 @@
+name: BatSat
+
+on:
+  push:
+    branches: [ "main", "next-major" ]
+  pull_request:
+    branches: [ "main", "next-major" ]
+
+env:
+  CARGO_TERM_COLOR: always
+
+jobs:
+  build-test:
+    name: Build and test
+    strategy:
+      matrix:
+        os: [ubuntu-latest, macos-latest, windows-latest]
+    runs-on: ${{ matrix.os }}
+    steps:
+      - name: Checkout sources
+        uses: actions/checkout@v4
+      - name: Install stable toolchain
+        uses: dtolnay/rust-toolchain@stable
+      - uses: Swatinem/rust-cache@v2
+        with:
+          shared-key: "build-test"
+      - name: Cargo build
+        run: cargo build -p rustsat-batsat --verbose
+      - name: Cargo test
+        run: cargo test -p rustsat-batsat --verbose

.github/workflows/docs.yml

@@ -32,7 +32,7 @@ jobs:
             echo "failed for main crate"
             return=false
           fi
-          for dir in tools cadical kissat minisat glucose ipasir capi pyapi; do
+          for dir in tools cadical kissat minisat glucose batsat ipasir capi pyapi; do
             cd ${dir}
             if ! cargo rdme --check; then
               echo "failed for ${dir}"

.github/workflows/semver-checks.yml

@@ -43,3 +43,7 @@ jobs:
         uses: obi1kenobi/cargo-semver-checks-action@v2
         with:
           package: rustsat-ipasir
+      - name: BatSat
+        uses: obi1kenobi/cargo-semver-checks-action@v2
+        with:
+          package: rustsat-batsat

Cargo.toml

@@ -9,6 +9,7 @@ members = [
   "solvertests",
   "capi",
   "pyapi",
+  "batsat",
 ]
 resolver = "2"
 

batsat/.gitignore

@@ -0,0 +1,2 @@
+/target
+/Cargo.lock

batsat/CHANGELOG.md

@@ -0,0 +1,9 @@
+# Changelog
+
+All notable changes to this project will be documented in this file.
+
+## [0.1.0] - <Set Date When Releasing>
+
+Initial Release
+
+<!-- generated by git-cliff -->

batsat/Cargo.toml

@@ -0,0 +1,21 @@
+[package]
+name = "rustsat-batsat"
+version = "0.1.0"
+edition = "2021"
+authors = ["Noah Bruns <[email protected]>"]
+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
+
+[dependencies]
+batsat = "0.5.0"           # when changing this version, do not forget to update signature
+anyhow.workspace = true
+thiserror.workspace = true
+rustsat.workspace = true
+
+[dev-dependencies]
+rustsat-solvertests = { path = "../solvertests" }

batsat/README.md

@@ -0,0 +1,18 @@
+[![Check & Test](https://github.com/chrjabs/rustsat/actions/workflows/batsat.yml/badge.svg)](https://github.com/chrjabs/rustsat/actions/workflows/batsat.yml)
+[![crates.io](https://img.shields.io/crates/v/rustsat-batsat)](https://crates.io/crates/rustsat-batsat)
+[![docs.rs](https://img.shields.io/docsrs/rustsat-batsat)](https://docs.rs/rustsat-batsat)
+[![License](https://img.shields.io/crates/l/rustsat-batsat)](../LICENSE)
+
+<!-- cargo-rdme start -->
+
+# rustsat-batsat - Interface to the BatSat SAT Solver for RustSAT
+
+Interface to the [BatSat](https://github.com/c-cube/batsat) incremental SAT-Solver to be used with the [RustSAT](https://github.com/chrjabs/rustsat) library.
+
+BatSat is fully implemented in Rust which has advantages in restricted compilation scenarios like WebAssembly.
+
+# BatSat Version
+
+The version of BatSat in this crate is Version 0.5.0.
+
+<!-- cargo-rdme end -->

batsat/data

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

batsat/src/lib.rs

@@ -0,0 +1,125 @@
+//! # rustsat-batsat - Interface to the BatSat SAT Solver for RustSAT
+//!
+//! Interface to the [BatSat](https://github.com/c-cube/batsat) incremental SAT-Solver to be used with the [RustSAT](https://github.com/chrjabs/rustsat) library.
+//!
+//! BatSat is fully implemented in Rust which has advantages in restricted compilation scenarios like WebAssembly.
+//!
+//! # BatSat Version
+//!
+//! The version of BatSat in this crate is Version 0.5.0.
+
+#![warn(clippy::pedantic)]
+#![warn(missing_docs)]
+
+use batsat::{intmap::AsIndex, lbool, BasicSolver, SolverInterface};
+use rustsat::{
+    solvers::{Solve, SolveIncremental, SolverResult},
+    types::{Clause, Lit, TernaryVal},
+};
+use thiserror::Error;
+
+/// API Error from the BatSat library (for example if the solver is in an UNSAT state)
+#[derive(Error, Clone, Copy, PartialEq, Eq, Debug)]
+#[error("BatSat returned an invalid value: {error}")]
+pub struct InvalidApiReturn {
+    error: &'static str,
+}
+
+/// RustSAT wrapper for the [`BasicSolver`] Solver from BatSat
+#[derive(Default)]
+pub struct BatsatBasicSolver(BasicSolver);
+
+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<'a> Extend<&'a Clause> for BatsatBasicSolver {
+    fn extend<T: IntoIterator<Item = &'a Clause>>(&mut self, iter: T) {
+        iter.into_iter().for_each(|cl| {
+            self.add_clause_ref(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()),
+            _ => 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>>();
+
+        self.0.add_clause_reuse(&mut c);
+
+        Ok(())
+    }
+
+    fn add_clause_ref(&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>>();
+
+        self.0.add_clause_reuse(&mut c);
+
+        Ok(())
+    }
+}
+
+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), 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()),
+            _ => 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 @@
+rustsat_solvertests::incremental_tests!(rustsat_batsat::BatsatBasicSolver);

batsat/tests/small.rs

@@ -0,0 +1,3 @@
+mod base {
+    rustsat_solvertests::base_tests!(rustsat_batsat::BatsatBasicSolver, false, true);
+}

clippy.toml

@@ -1,2 +1,2 @@
-doc-valid-idents = ["RustSAT", "CaDiCaL", "MaxSAT", ".."]
+doc-valid-idents = ["RustSAT", "CaDiCaL", "MaxSAT", "BatSat", ".."]
 avoid-breaking-exported-api = false

release-plz.toml

@@ -40,3 +40,8 @@ git_release_enable = false
 name = "rustsat-pyapi"
 release = false
 git_release_enable = false
+
+[[package]]
+name = "rustsat-batsat"
+release = false
+git_release_enable = false