From 4d15c0f49ec255ecc0106b4c1dde257ec87c4068 Mon Sep 17 00:00:00 2001 From: Noah Bruns Date: Mon, 8 Jul 2024 09:59:41 +0300 Subject: [PATCH] feat: batsat solver interface interface to the [BatSat](https://github.com/c-cube/batsat) solver closes #84 Squashed commit of the following: commit 25bea4d13862e0d02e39861b467f1830529b58a1 Author: Noah Bruns <51422579+nfbruns@users.noreply.github.com> Date: Thu Jul 4 16:01:43 2024 +0200 refactor: reorder clippy valid idents list Co-authored-by: Christoph Jabs <98587286+chrjabs@users.noreply.github.com> commit adbe43efc18187df93c036003836f0f39e834d80 Author: Noah Bruns Date: Thu Jul 4 12:03:33 2024 +0200 lint: Batsat added as valid ident commit 80db5aab3e76beefdc2076393228735ca0c0c2ab Author: Noah Bruns Date: Thu Jul 4 09:42:01 2024 +0200 ci: run cargo rdme commit 3a3bd46ebf5fcc9bfec98d6409ad87629606e0c4 Author: Noah Bruns <51422579+nfbruns@users.noreply.github.com> Date: Thu Jul 4 09:41:02 2024 +0200 docu: remove code blocks for names Co-authored-by: Christoph Jabs <98587286+chrjabs@users.noreply.github.com> commit e0a9cd2c04b7248800f4cba8f610826576df6b2b Author: Noah Bruns Date: Wed Jul 3 11:03:56 2024 +0200 ci: run cargo rdme after comments changed commit 0aeac456fc5371417008d102953a88f109f00bcb Author: Noah Bruns Date: Mon Jul 1 18:09:57 2024 +0200 docu: more comments and restructuring commit a549dda76b99558347aaca5dde0dde2beb741aa2 Author: Noah Bruns Date: Mon Jul 1 17:51:42 2024 +0200 docu: cargo rdme run commit a1e44980b557544e72c2a7b205a61855811997ff Author: Noah Bruns Date: Mon Jul 1 17:48:15 2024 +0200 lint: clippy fixes and docu commit fcfa9dffed93f914dfa92181fe672c0c5a1e479f Author: Noah Bruns Date: Mon Jul 1 17:32:42 2024 +0200 PR: implemented suggestions and applied reviews commit 15449807c3923b9dd02ae09a958d7378011b142b Author: Noah Bruns Date: Wed Jun 26 11:17:22 2024 +0200 fix: clippy linting issues addressed commit 727e42c06b56159f9daad899a0c3cb914852514a Author: Noah Bruns <51422579+nfbruns@users.noreply.github.com> Date: Fri Jun 21 19:19:21 2024 +0200 fix: use workspace dependencies commit 707e2077fea92a5359bb3943d5059854a3f486bc Merge: 4649148 1e6aa6b Author: Noah Bruns Date: Wed Jun 26 11:08:55 2024 +0200 Merge branch 'feat-batsat-solver' of github.com:nfbruns/rustsat into feat-batsat-solver commit 464914895972d85863d582ff3fde8194142a9661 Author: Noah Bruns Date: Wed Jun 26 11:08:40 2024 +0200 compatability to 0.5.1 and solvertests implemented commit ed21c4f61c2d054ebe2e2f63c8780904a86a3e99 Author: Noah Bruns Date: Wed Jun 26 11:08:40 2024 +0200 test: cleanup and renaming commit 8ecd6ad406d6de7feade94bac6e85025709dcbe8 Author: Noah Bruns <51422579+nfbruns@users.noreply.github.com> Date: Wed Jun 26 11:08:40 2024 +0200 fix: return of ok if clause not added commit a0e84a1d286b8b31742bc2b65ba2ced2218bee82 Author: Noah Bruns <51422579+nfbruns@users.noreply.github.com> Date: Wed Jun 26 11:08:40 2024 +0200 docs: fixed comments commit 4acddcd783dcfe9f6511e3744b700fed26a920af Author: Noah Bruns Date: Wed Jun 26 11:08:40 2024 +0200 ci: running github workflows commit 2ccc905540fe14f0189caf89691f4036b60f71c2 Author: Noah Bruns Date: Wed Jun 26 11:08:40 2024 +0200 docs: changelog and readme added commit 9f59fdd724d660d54073df2985f7b41524114a38 Author: Noah Bruns Date: Wed Jun 26 11:08:40 2024 +0200 feat:implemented batsat api commit 1e6aa6b2fb2a52a18d87c3509bb658cfebb48c69 Author: Noah Bruns Date: Fri Jun 14 17:21:51 2024 +0200 compatability to 0.5.1 and solvertests implemented commit cf6dd71efef4a7449f22961b671e2e2f7f5dd421 Merge: 31d7e1c ff1a3d6 Author: Noah Bruns <51422579+nfbruns@users.noreply.github.com> Date: Fri Jun 14 16:48:35 2024 +0200 Merge branch 'main' into feat-batsat-solver commit 31d7e1c623f4682f2b65417f81882503c7121077 Author: Noah Bruns Date: Wed Apr 10 16:25:51 2024 +0200 test: cleanup and renaming commit 46b2c2724d41cd91fa029abb9fdf184d4a803bd8 Author: Noah Bruns <51422579+nfbruns@users.noreply.github.com> Date: Wed Apr 10 17:10:03 2024 +0200 fix: return of ok if clause not added commit 4b58cc80477944fd9188f02cf4b5dd02138974da Author: Noah Bruns <51422579+nfbruns@users.noreply.github.com> Date: Wed Apr 10 17:08:58 2024 +0200 docs: fixed comments commit ae01e17faee9988cea6f5d18ee3612a8df7edbd4 Author: Noah Bruns Date: Wed Apr 10 15:56:36 2024 +0200 ci: running github workflows commit b8326bea437248ab8f622519fd8cc5d56fa8a412 Author: Noah Bruns Date: Wed Apr 10 15:55:25 2024 +0200 docs: changelog and readme added commit 5b78bd22cb25cb8adb1763064fdb81637cf192e1 Author: Noah Bruns Date: Wed Apr 10 15:17:41 2024 +0200 feat:implemented batsat api --- .github/workflows/batsat.yml | 30 +++++++ .github/workflows/docs.yml | 2 +- .github/workflows/semver-checks.yml | 4 + Cargo.toml | 1 + batsat/.gitignore | 2 + batsat/CHANGELOG.md | 9 ++ batsat/Cargo.toml | 21 +++++ batsat/README.md | 18 ++++ batsat/data | 1 + batsat/src/lib.rs | 125 ++++++++++++++++++++++++++++ batsat/tests/incremental.rs | 1 + batsat/tests/small.rs | 3 + clippy.toml | 2 +- release-plz.toml | 5 ++ 14 files changed, 222 insertions(+), 2 deletions(-) create mode 100644 .github/workflows/batsat.yml create mode 100644 batsat/.gitignore create mode 100644 batsat/CHANGELOG.md create mode 100644 batsat/Cargo.toml create mode 100644 batsat/README.md create mode 120000 batsat/data create mode 100644 batsat/src/lib.rs create mode 100644 batsat/tests/incremental.rs create mode 100644 batsat/tests/small.rs diff --git a/.github/workflows/batsat.yml b/.github/workflows/batsat.yml new file mode 100644 index 00000000..cd5ef4df --- /dev/null +++ b/.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 diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml index 82831b8e..9a954b6c 100644 --- a/.github/workflows/docs.yml +++ b/.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}" diff --git a/.github/workflows/semver-checks.yml b/.github/workflows/semver-checks.yml index d756f6eb..3b073590 100644 --- a/.github/workflows/semver-checks.yml +++ b/.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 \ No newline at end of file diff --git a/Cargo.toml b/Cargo.toml index 0f250fa7..ff786a14 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -9,6 +9,7 @@ members = [ "solvertests", "capi", "pyapi", + "batsat", ] resolver = "2" diff --git a/batsat/.gitignore b/batsat/.gitignore new file mode 100644 index 00000000..2ebc5ea0 --- /dev/null +++ b/batsat/.gitignore @@ -0,0 +1,2 @@ +/target +/Cargo.lock \ No newline at end of file diff --git a/batsat/CHANGELOG.md b/batsat/CHANGELOG.md new file mode 100644 index 00000000..c582dab2 --- /dev/null +++ b/batsat/CHANGELOG.md @@ -0,0 +1,9 @@ +# Changelog + +All notable changes to this project will be documented in this file. + +## [0.1.0] - + +Initial Release + + diff --git a/batsat/Cargo.toml b/batsat/Cargo.toml new file mode 100644 index 00000000..d23d95bb --- /dev/null +++ b/batsat/Cargo.toml @@ -0,0 +1,21 @@ +[package] +name = "rustsat-batsat" +version = "0.1.0" +edition = "2021" +authors = ["Noah Bruns "] +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" } diff --git a/batsat/README.md b/batsat/README.md new file mode 100644 index 00000000..218809a9 --- /dev/null +++ b/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) + + + +# 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. + + diff --git a/batsat/data b/batsat/data new file mode 120000 index 00000000..4909e06e --- /dev/null +++ b/batsat/data @@ -0,0 +1 @@ +../data \ No newline at end of file diff --git a/batsat/src/lib.rs b/batsat/src/lib.rs new file mode 100644 index 00000000..5937ffd9 --- /dev/null +++ b/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 for BatsatBasicSolver { + fn extend>(&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>(&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 { + 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 { + 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 = clause + .iter() + .map(|l| batsat::Lit::new(self.0.var_of_int(l.vidx32() + 1), l.is_pos())) + .collect::>(); + + self.0.add_clause_reuse(&mut c); + + Ok(()) + } + + fn add_clause_ref(&mut self, clause: &Clause) -> anyhow::Result<()> { + let mut c: Vec = clause + .iter() + .map(|l| batsat::Lit::new(self.0.var_of_int(l.vidx32() + 1), l.is_pos())) + .collect::>(); + + self.0.add_clause_reuse(&mut c); + + Ok(()) + } +} + +impl SolveIncremental for BatsatBasicSolver { + fn solve_assumps(&mut self, assumps: &[Lit]) -> anyhow::Result { + let a = assumps + .iter() + .map(|l| batsat::Lit::new(self.0.var_of_int(l.vidx32() + 1), l.is_pos())) + .collect::>(); + + 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> { + Ok(self + .0 + .unsat_core() + .iter() + .map(|l| Lit::new(l.var().idx() - 1, !l.sign())) + .collect::>()) + } +} diff --git a/batsat/tests/incremental.rs b/batsat/tests/incremental.rs new file mode 100644 index 00000000..f76eb878 --- /dev/null +++ b/batsat/tests/incremental.rs @@ -0,0 +1 @@ +rustsat_solvertests::incremental_tests!(rustsat_batsat::BatsatBasicSolver); diff --git a/batsat/tests/small.rs b/batsat/tests/small.rs new file mode 100644 index 00000000..a6f444c0 --- /dev/null +++ b/batsat/tests/small.rs @@ -0,0 +1,3 @@ +mod base { + rustsat_solvertests::base_tests!(rustsat_batsat::BatsatBasicSolver, false, true); +} diff --git a/clippy.toml b/clippy.toml index eff43ef7..a9773d0a 100644 --- a/clippy.toml +++ b/clippy.toml @@ -1,2 +1,2 @@ -doc-valid-idents = ["RustSAT", "CaDiCaL", "MaxSAT", ".."] +doc-valid-idents = ["RustSAT", "CaDiCaL", "MaxSAT", "BatSat", ".."] avoid-breaking-exported-api = false diff --git a/release-plz.toml b/release-plz.toml index fe2e31a4..28ca80fb 100644 --- a/release-plz.toml +++ b/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