Repository: chrjabs/rustsat (language: python)

Issue:
Factoring out solver interfaces into separate crates
Factoring out the solver interfaces into separate crates should improve build performance as the solvers can be built in parallel and enable building of the documentation on docs.rs as the downloading of the solver code happens only in the solver interface crates.


Discussion / hints:

Fix patch:
diff --git a/Cargo.toml b/Cargo.toml
index 0cec6008..c6f9e7a9 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -1,107 +1,9 @@
-[package]
-name = "rustsat"
-version = "0.1.2"
-edition = "2021"
-authors = ["Christoph Jabs <christoph.jabs@helsinki.fi>"]
-license = "MIT"
-description = "This library aims to provide implementations of elements commonly used in the development on software in the area of satisfiability solving. The focus of the library is to provide as much ease of use without giving up on performance."
-keywords = ["sat", "satisfiability", "encodings"]
-repository = "https://github.com/chrjabs/rustsat"
-readme = "README.md"
-
-build = "build.rs"
-
-# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
-
-[dependencies]
-nom = "7.1.1"
-bzip2 = { version = "0.4.4", optional = true }
-flate2 = { version = "1.0.25", optional = true, features = ["zlib-ng"], default-features = false }
-xz2 = { version = "0.1.7", optional = true }
-rustc-hash = { version = "1.1.0", optional = true }
-cpu-time = "1.0.0"
-rand = { version = "0.8.5", optional = true }
-clap = { optional = true, version = "4.2.4", features = ["derive", "cargo"] }
-concolor-clap = { optional = true, version = "0.1.0" }
-termcolor = { optional = true, version = "1.2.0" }
-atty = { optional = true, version = "0.2.14" }
-visibility = { version = "0.0.1" }
-
-[build-dependencies]
-cc = { version = "1.0.79", features = ["parallel"] }
-git2 = "0.17.1"
-glob = "0.3.1"
-chrono = "0.4.24"
-cmake = "0.1.50"
-
-[features]
-default-but-solvers = [
-  "optimization",
-  "fxhash"
-]
-default = [
-  "default-but-solvers",
-  "cadical",
-  "kissat",
-  "glucose4",
-  "minisat",
-]
-internals = []
-fxhash = ["dep:rustc-hash"]
-ipasir = []
-cadical = []
-kissat = []
-glucose4 = []
-minisat = []
-optimization = []
-multiopt = ["optimization"]
-compression = ["dep:bzip2", "dep:flate2", "dep:xz2"]
-rand = ["dep:rand"]
-all-non-conflicting = [
+[workspace]
+members = [
+  "rustsat",
+  "tools",
   "cadical",
   "kissat",
-  "glucose4",
-  "minisat",
-  "optimization",
-  "multiopt",
-  "compression",
-  "rand",
-  "fxhash"
+  "glucose",
+  "minisat"
 ]
-cli = ["dep:clap", "dep:concolor-clap", "dep:termcolor", "dep:atty"]
-
-[[example]]
-name = "enumerator"
-required-features = ["compression"]
-
-[[example]]
-name = "cnf2opb"
-required-features = ["compression", "cli"]
-
-[[example]]
-name = "opb2cnf"
-required-features = ["compression", "cli"]
-
-[[example]]
-name = "wcnf2opb"
-required-features = ["compression", "optimization", "cli"]
-
-[[example]]
-name = "opb2wcnf"
-required-features = ["compression", "optimization", "cli"]
-
-[[example]]
-name = "mcnf2opb"
-required-features = ["compression", "multiopt", "cli"]
-
-[[example]]
-name = "opb2mcnf"
-required-features = ["compression", "multiopt", "cli"]
-
-[[example]]
-name = "shuffledimacs"
-required-features = ["compression", "rand", "cli"]
-
-[[example]]
-name = "gbmosplit"
-required-features = ["compression", "multiopt", "cli"]
diff --git a/cadical/.gitignore b/cadical/.gitignore
new file mode 100644
index 00000000..a255f58c
--- /dev/null
+++ b/cadical/.gitignore
@@ -0,0 +1,3 @@
+/target
+/Cargo.lock
+*.log
diff --git a/cadical/Cargo.toml b/cadical/Cargo.toml
new file mode 100644
index 00000000..63c1d151
--- /dev/null
+++ b/cadical/Cargo.toml
@@ -0,0 +1,34 @@
+[package]
+name = "rustsat-cadical"
+version = "0.1.0"
+edition = "2021"
+authors = ["Christoph Jabs <christoph.jabs@helsinki.fi>"]
+license = "MIT"
+description = "Interface to the SAT solver CaDiCaL for the RustSAT library."
+keywords = ["sat solver", "rustsat"]
+readme = "README.md"
+
+build = "build.rs"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[features]
+v1-5-0 = []
+v1-5-1 = []
+v1-5-2 = []
+v1-5-3 = []
+v1-5-4 = []
+v1-5-5 = []
+v1-5-6 = []
+v1-6-0 = []
+v1-7-0 = []
+
+[dependencies]
+cpu-time = "1.0.0"
+rustsat = { version = ">= 0.2.0", path = "../rustsat", default-features = false }
+
+[build-dependencies]
+cc = { version = "1.0.79", features = ["parallel"] }
+git2 = "0.17.1"
+glob = "0.3.1"
+chrono = "0.4.24"
diff --git a/cadical/README.md b/cadical/README.md
new file mode 100644
index 00000000..2fa7d797
--- /dev/null
+++ b/cadical/README.md
@@ -0,0 +1,20 @@
+# rustsat-cadical - Interface to the CaDiCaL SAT Solver for RustSAT
+
+Armin Biere's SAT solver [CaDiCaL](https://github.com/arminbiere/cadical) be used with the [RustSAT](https://github.com/chrjabs/rustsat) library.
+
+## CaDiCaL Versions
+
+CaDiCaL versions can be selected via cargo crate features.
+The following CaDiCaL versions are available:
+- `v1-7-0`: [Version 1.7.0](https://github.com/arminbiere/cadical/releases/tag/rel-1.7.0)
+- `v1-6-0`: [Version 1.6.0](https://github.com/arminbiere/cadical/releases/tag/rel-1.6.0)
+- `v1-5-6`: [Version 1.5.6](https://github.com/arminbiere/cadical/releases/tag/rel-1.5.6)
+- `v1-5-5`: [Version 1.5.5](https://github.com/arminbiere/cadical/releases/tag/rel-1.5.5)
+- `v1-5-4`: [Version 1.5.4](https://github.com/arminbiere/cadical/releases/tag/rel-1.5.4)
+- `v1-5-3`: [Version 1.5.3](https://github.com/arminbiere/cadical/releases/tag/rel-1.5.3)
+- `v1-5-2`: [Version 1.5.2](https://github.com/arminbiere/cadical/releases/tag/rel-1.5.2)
+- `v1-5-1`: [Version 1.5.1](https://github.com/arminbiere/cadical/releases/tag/rel-1.5.1)
+- `v1-5-0`: [Version 1.5.0](https://github.com/arminbiere/cadical/releases/tag/rel-1.5.0)
+
+Without any features selected, the newest version will be used.
+If conflicting CaDiCaL versions are requested, the newest requested version will be selected.
\ No newline at end of file
diff --git a/cadical/build-all.sh b/cadical/build-all.sh
new file mode 100755
index 00000000..943e1132
--- /dev/null
+++ b/cadical/build-all.sh
@@ -0,0 +1,51 @@
+#!/usr/bin/bash
+
+echo "Building default (newest) version"
+if [ "$1" == "--clean" ]; then cargo clean -p rustsat-cadical > /dev/null; fi
+cargo build &> def-build.log
+echo "Default (newest) build returned: $?"
+
+echo "Building v1.5.0"
+if [ "$1" == "--clean" ]; then cargo clean -p rustsat-cadical > /dev/null; fi
+cargo build --features=v1-5-0 &> v150-build.log
+echo "v1.5.0 build returned: $?"
+
+echo "Building v1.5.1"
+if [ "$1" == "--clean" ]; then cargo clean -p rustsat-cadical > /dev/null; fi
+cargo build --features=v1-5-1 &> v151-build.log
+echo "v1.5.1 build returned: $?"
+
+echo "Building v1.5.2"
+if [ "$1" == "--clean" ]; then cargo clean -p rustsat-cadical > /dev/null; fi
+cargo build --features=v1-5-2 &> v152-build.log
+echo "v1.5.2 build returned: $?"
+
+echo "Building v1.5.3"
+if [ "$1" == "--clean" ]; then cargo clean -p rustsat-cadical > /dev/null; fi
+cargo build --features=v1-5-3 &> v153-build.log
+echo "v1.5.3 build returned: $?"
+
+echo "Building v1.5.4"
+if [ "$1" == "--clean" ]; then cargo clean -p rustsat-cadical > /dev/null; fi
+cargo build --features=v1-5-4 &> v154-build.log
+echo "v1.5.4 build returned: $?"
+
+echo "Building v1.5.5"
+if [ "$1" == "--clean" ]; then cargo clean -p rustsat-cadical > /dev/null; fi
+cargo build --features=v1-5-5 &> v155-build.log
+echo "v1.5.5 build returned: $?"
+
+echo "Building v1.5.6"
+if [ "$1" == "--clean" ]; then cargo clean -p rustsat-cadical > /dev/null; fi
+cargo build --features=v1-5-6 &> v156-build.log
+echo "v1.5.6 build returned: $?"
+
+echo "Building v1.6.0"
+if [ "$1" == "--clean" ]; then cargo clean -p rustsat-cadical > /dev/null; fi
+cargo build --features=v1-6-0 &> v160-build.log
+echo "v1.6.0 build returned: $?"
+
+echo "Building v1.7.0"
+if [ "$1" == "--clean" ]; then cargo clean -p rustsat-cadical > /dev/null; fi
+cargo build --features=v1-7-0 &> v170-build.log
+echo "v1.7.0 build returned: $?"
\ No newline at end of file
diff --git a/cadical/build.rs b/cadical/build.rs
new file mode 100644
index 00000000..b3b206be
--- /dev/null
+++ b/cadical/build.rs
@@ -0,0 +1,212 @@
+use git2::Repository;
+use glob::glob;
+use std::{
+    env,
+    fs::{self, File},
+    io::{Read, Write},
+    path::Path,
+    process::Command,
+    str,
+};
+
+fn main() {
+    // Select commit based on features. If conflict, always choose newest release
+    let (tag, patch) = if cfg!(feature = "v1-7-0") {
+        ("refs/tags/rel-1.7.0", "patches/v170.patch")
+    } else if cfg!(feature = "v1-6-0") {
+        ("refs/tags/rel-1.6.0", "patches/v160.patch")
+    } else if cfg!(feature = "v1-5-6") {
+        ("refs/tags/rel-1.5.6", "patches/v156.patch")
+    } else if cfg!(feature = "v1-5-5") {
+        ("refs/tags/rel-1.5.5", "patches/v154.patch")
+    } else if cfg!(feature = "v1-5-4") {
+        ("refs/tags/rel-1.5.4", "patches/v154.patch")
+    } else if cfg!(feature = "v1-5-3") {
+        ("refs/tags/rel-1.5.3", "patches/v150.patch")
+    } else if cfg!(feature = "v1-5-2") {
+        ("refs/tags/rel-1.5.2", "patches/v150.patch")
+    } else if cfg!(feature = "v1-5-1") {
+        ("refs/tags/rel-1.5.1", "patches/v150.patch")
+    } else if cfg!(feature = "v1-5-0") {
+        ("refs/tags/rel-1.5.0", "patches/v150.patch")
+    } else {
+        // default to newest version
+        ("refs/tags/rel-1.7.0", "patches/v170.patch")
+    };
+
+    // Build C++ library
+    build(
+        "https://github.com/arminbiere/cadical.git",
+        "master",
+        tag,
+        patch,
+    );
+
+    let out_dir = env::var("OUT_DIR").unwrap();
+
+    // Built solver is in out_dir
+    println!("cargo:rustc-link-search={}", out_dir);
+    println!("cargo:rustc-link-search={}/lib", out_dir);
+}
+
+fn build(repo: &str, branch: &str, reference: &str, patch: &str) {
+    let out_dir = env::var("OUT_DIR").unwrap();
+    let mut cadical_dir_str = out_dir.clone();
+    cadical_dir_str.push_str("/cadical");
+    let cadical_dir = Path::new(&cadical_dir_str);
+    if update_repo(cadical_dir, repo, branch, reference, patch)
+        || !Path::new(&out_dir).join("libcadical.a").exists()
+    {
+        // Repo changed, rebuild
+        // We specify the build manually here instead of calling make for better portability
+        let src_files = glob(&format!("{}/src/*.cpp", cadical_dir_str))
+            .unwrap()
+            .filter_map(|res| {
+                if let Ok(p) = res {
+                    if let Some(name) = p.file_name() {
+                        if name == "cadical.cpp" || name == "mobical.cpp" {
+                            return None; // Filter out application files
+                        }
+                    };
+                    Some(p)
+                } else {
+                    None
+                }
+            });
+        // Setup build configuration
+        let mut cadical_build = cc::Build::new();
+        cadical_build.cpp(true);
+        if env::var("PROFILE").unwrap() == "debug" {
+            cadical_build
+                .opt_level(0)
+                .define("DEBUG", None)
+                .warnings(true)
+                .debug(true);
+        } else {
+            cadical_build
+                .opt_level(3)
+                .define("NDEBUG", None)
+                .warnings(false);
+        }
+        // Generate build header
+        let mut build_header = File::create(cadical_dir.join("src").join("build.hpp"))
+            .expect("Could not create kissat CaDiCaL header");
+        let mut cadical_version =
+            fs::read_to_string(cadical_dir.join("VERSION")).expect("Cannot read CaDiCaL version");
+        cadical_version.retain(|c| c != '\n');
+        let (compiler_desc, compiler_flags) =
+            get_compiler_description(cadical_build.get_compiler());
+        write!(
+                build_header,
+                "#define VERSION \"{}\"\n#define IDENTIFIER \"{}\"\n#define COMPILER \"{}\"\n#define FLAGS \"{}\"\n#define DATE \"{}\"",
+                cadical_version, reference, compiler_desc, compiler_flags, chrono::Utc::now()
+            ).expect("Failed to write CaDiCaL build.hpp");
+        // Build CaDiCaL
+        cadical_build
+            .include(cadical_dir.join("src"))
+            .warnings(false)
+            .files(src_files)
+            .compile("cadical");
+    };
+
+    println!("cargo:rustc-link-lib=static=cadical");
+
+    #[cfg(target_os = "macos")]
+    println!("cargo:rustc-flags=-l dylib=c++");
+
+    #[cfg(not(target_os = "macos"))]
+    println!("cargo:rustc-flags=-l dylib=stdc++");
+}
+
+/// Returns true if there were changes, false if not
+fn update_repo(path: &Path, url: &str, branch: &str, reference: &str, patch: &str) -> bool {
+    let mut changed = false;
+    let repo = match git2::Repository::open(path) {
+        Ok(repo) => {
+            if repo.find_reference(reference).is_err() {
+                // Fetch repo
+                let mut remote = repo.find_remote("origin").unwrap_or_else(|e| {
+                    panic!("Expected remote \"origin\" in git repo {:?}: {}", path, e)
+                });
+                remote.fetch(&[branch], None, None).unwrap_or_else(|e| {
+                    panic!(
+                        "Could not fetch \"origin/{}\" for git repo {:?}: {}",
+                        branch, path, e
+                    )
+                });
+                drop(remote);
+                changed = true;
+            }
+            repo
+        }
+        Err(_) => {
+            if path.exists() {
+                fs::remove_dir_all(path).unwrap_or_else(|e| {
+                    panic!(
+                        "Could not delete directory {}: {}",
+                        path.to_str().unwrap(),
+                        e
+                    )
+                });
+            };
+            changed = true;
+            git2::Repository::clone(url, path)
+                .unwrap_or_else(|e| panic!("Could not clone repository {}: {}", url, e))
+        }
+    };
+    let target_commit = repo
+        .find_reference(reference)
+        .expect("could not find specified reference")
+        .peel_to_commit()
+        .expect("could not peel to commit");
+    repo.checkout_tree(
+        target_commit.as_object(),
+        Some(git2::build::CheckoutBuilder::new().force()),
+    )
+    .expect("could not checkout commit");
+    repo.set_head_detached(target_commit.id())
+        .expect("could not detach head");
+
+    apply_patch(&repo, patch);
+
+    changed
+}
+
+/// Applies a patch to the repo
+fn apply_patch(repo: &Repository, patch: &str) {
+    let mut f = File::open(patch).unwrap();
+    let mut buffer = Vec::new();
+    f.read_to_end(&mut buffer).unwrap();
+    let patch = git2::Diff::from_buffer(&buffer).unwrap();
+    repo.apply(&patch, git2::ApplyLocation::WorkDir, None)
+        .unwrap();
+}
+
+/// Gets a description of the C(++) compiler used and the used flags
+fn get_compiler_description(compiler: cc::Tool) -> (String, String) {
+    let compiler_command = compiler.to_command();
+    let mut first_line = true;
+    let compiler_version = match Command::new(compiler_command.get_program())
+        .arg("--version")
+        .output()
+    {
+        Ok(output) => {
+            let mut version = String::from_utf8(output.stdout).unwrap();
+            version.retain(|c| {
+                if first_line && c == '\n' {
+                    first_line = false;
+                    false
+                } else {
+                    first_line
+                }
+            });
+            version
+        }
+        Err(_) => String::from(compiler_command.get_program().to_str().unwrap()),
+    };
+    let compiler_flags = compiler.cflags_env();
+    (
+        compiler_version,
+        String::from(compiler_flags.to_str().unwrap()),
+    )
+}
diff --git a/cadical/data b/cadical/data
new file mode 120000
index 00000000..4909e06e
--- /dev/null
+++ b/cadical/data
@@ -0,0 +1,1 @@
+../data
\ No newline at end of file
diff --git a/cadical/patches/v150.patch b/cadical/patches/v150.patch
new file mode 100644
index 00000000..9d228f7a
--- /dev/null
+++ b/cadical/patches/v150.patch
@@ -0,0 +1,158 @@
+From d153963a145ae94c0f3ce695ec1dc89fe73a9815 Mon Sep 17 00:00:00 2001
+From: Christoph Jabs <christoph.jabs@helsinki.fi>
+Date: Wed, 23 Aug 2023 11:30:43 +0300
+Subject: [PATCH] extend C api
+
+---
+ src/cadical.hpp  |  6 ++++++
+ src/ccadical.cpp | 54 ++++++++++++++++++++++++++++++++++++++++++++++++
+ src/ccadical.h   | 17 +++++++++++++++
+ src/solver.cpp   | 24 +++++++++++++++++++++
+ 4 files changed, 101 insertions(+)
+
+diff --git a/src/cadical.hpp b/src/cadical.hpp
+index cbe476d..e5e8a9f 100644
+--- a/src/cadical.hpp
++++ b/src/cadical.hpp
+@@ -589,6 +589,12 @@ public:
+   void phase (int lit);
+   void unphase (int lit);
+ 
++  //------------------------------------------------------------------------
++  // Get some selected statistics
++  int64_t propagations () const;
++  int64_t decisions () const;
++  int64_t conflicts () const;
++
+   //------------------------------------------------------------------------
+ 
+   // Enables clausal proof tracing in DRAT format and returns 'true' if
+diff --git a/src/ccadical.cpp b/src/ccadical.cpp
+index e6e7d28..7fabb24 100644
+--- a/src/ccadical.cpp
++++ b/src/ccadical.cpp
+@@ -177,4 +177,58 @@ int ccadical_frozen (CCaDiCaL * ptr, int lit) {
+   return ((Wrapper*) ptr)->solver->frozen (lit);
+ }
+ 
++/*------------------------------------------------------------------------*/
++
++// Extending C API (Christoph Jabs)
++
++bool ccadical_configure (CCaDiCaL *ptr, const char *name) {
++  return ((Wrapper *) ptr)->solver->configure (name);
++}
++
++void ccadical_phase (CCaDiCaL *ptr, int lit) {
++  ((Wrapper *) ptr)->solver->phase (lit);
++}
++
++void ccadical_unphase (CCaDiCaL *ptr, int lit) {
++  ((Wrapper *) ptr)->solver->unphase (lit);
++}
++
++int ccadical_vars (CCaDiCaL *ptr) {
++  return ((Wrapper *) ptr)->solver->vars ();
++}
++
++bool ccadical_set_option_ret (CCaDiCaL *wrapper, const char *name,
++                              int val) {
++  return ((Wrapper *) wrapper)->solver->set (name, val);
++}
++
++bool ccadical_limit_ret (CCaDiCaL *wrapper, const char *name, int val) {
++  return ((Wrapper *) wrapper)->solver->limit (name, val);
++}
++
++int64_t ccadical_redundant (CCaDiCaL *wrapper) {
++  return ((Wrapper *) wrapper)->solver->redundant ();
++}
++
++int ccadical_simplify_rounds (CCaDiCaL *wrapper, int rounds) {
++  return ((Wrapper *) wrapper)->solver->simplify (rounds);
++}
++
++void ccadical_reserve (CCaDiCaL *wrapper, int min_max_var) {
++  return ((Wrapper *) wrapper)->solver->reserve (min_max_var);
++}
++
++int64_t ccadical_propagations (CCaDiCaL *wrapper) {
++  return ((Wrapper *) wrapper)->solver->propagations ();
++}
++
++int64_t ccadical_decisions (CCaDiCaL *wrapper) {
++  return ((Wrapper *) wrapper)->solver->decisions ();
++}
++
++int64_t ccadical_conflicts (CCaDiCaL *wrapper) {
++  return ((Wrapper *) wrapper)->solver->conflicts ();
++}
++
++/*------------------------------------------------------------------------*/
+ }
+diff --git a/src/ccadical.h b/src/ccadical.h
+index 332f842..1a141f4 100644
+--- a/src/ccadical.h
++++ b/src/ccadical.h
+@@ -50,6 +50,23 @@ int ccadical_simplify (CCaDiCaL *);
+ 
+ /*------------------------------------------------------------------------*/
+ 
++// Extending C API (Christoph Jabs)
++
++bool ccadical_configure (CCaDiCaL *, const char *);
++void ccadical_phase (CCaDiCaL *, int lit);
++void ccadical_unphase (CCaDiCaL *, int lit);
++int ccadical_vars (CCaDiCaL *);
++bool ccadical_set_option_ret (CCaDiCaL *, const char *name, int val);
++bool ccadical_limit_ret (CCaDiCaL *, const char *name, int val);
++int64_t ccadical_redundant (CCaDiCaL *);
++int ccadical_simplify_rounds (CCaDiCaL *, int rounds);
++void ccadical_reserve (CCaDiCaL *, int min_max_var);
++int64_t ccadical_propagations (CCaDiCaL *);
++int64_t ccadical_decisions (CCaDiCaL *);
++int64_t ccadical_conflicts (CCaDiCaL *);
++
++/*------------------------------------------------------------------------*/
++
+ // Support legacy names used before moving to more IPASIR conforming names.
+ 
+ #define ccadical_reset ccadical_release
+diff --git a/src/solver.cpp b/src/solver.cpp
+index 31b1610..a079861 100644
+--- a/src/solver.cpp
++++ b/src/solver.cpp
+@@ -796,6 +796,30 @@ int64_t Solver::irredundant () const {
+   return res;
+ }
+ 
++int64_t Solver::propagations () const {
++  TRACE ("propagations");
++  REQUIRE_VALID_STATE ();
++  int64_t res = internal->stats.propagations.search;
++  LOG_API_CALL_RETURNS ("propagations", res);
++  return res;
++}
++
++int64_t Solver::decisions () const {
++  TRACE ("decisions");
++  REQUIRE_VALID_STATE ();
++  int64_t res = internal->stats.decisions;
++  LOG_API_CALL_RETURNS ("decisions", res);
++  return res;
++}
++
++int64_t Solver::conflicts () const {
++  TRACE ("conflicts");
++  REQUIRE_VALID_STATE ();
++  int64_t res = internal->stats.conflicts;
++  LOG_API_CALL_RETURNS ("conflicts", res);
++  return res;
++}
++
+ /*------------------------------------------------------------------------*/
+ 
+ void Solver::freeze (int lit) {
+-- 
+2.41.0
+
diff --git a/cadical/patches/v154.patch b/cadical/patches/v154.patch
new file mode 100644
index 00000000..88f6f5a8
--- /dev/null
+++ b/cadical/patches/v154.patch
@@ -0,0 +1,168 @@
+From 0a29abb1115e1bf09819f27fb3fb2db09f0b6759 Mon Sep 17 00:00:00 2001
+From: Christoph Jabs <christoph.jabs@helsinki.fi>
+Date: Wed, 23 Aug 2023 11:30:43 +0300
+Subject: [PATCH] extend C api
+
+---
+ src/cadical.hpp  |  6 +++++
+ src/ccadical.cpp | 62 ++++++++++++++++++++++++++++++++++++++++++++++++
+ src/ccadical.h   | 19 +++++++++++++++
+ src/solver.cpp   | 24 +++++++++++++++++++
+ 4 files changed, 111 insertions(+)
+
+diff --git a/src/cadical.hpp b/src/cadical.hpp
+index 066c94b..fa252af 100644
+--- a/src/cadical.hpp
++++ b/src/cadical.hpp
+@@ -624,6 +624,12 @@ public:
+   void phase (int lit);
+   void unphase (int lit);
+ 
++  //------------------------------------------------------------------------
++  // Get some selected statistics
++  int64_t propagations () const;
++  int64_t decisions () const;
++  int64_t conflicts () const;
++
+   //------------------------------------------------------------------------
+ 
+   // Enables clausal proof tracing in DRAT format and returns 'true' if
+diff --git a/src/ccadical.cpp b/src/ccadical.cpp
+index e6e7d28..0d1ebad 100644
+--- a/src/ccadical.cpp
++++ b/src/ccadical.cpp
+@@ -177,4 +177,66 @@ int ccadical_frozen (CCaDiCaL * ptr, int lit) {
+   return ((Wrapper*) ptr)->solver->frozen (lit);
+ }
+ 
++/*------------------------------------------------------------------------*/
++
++// Extending C API (Christoph Jabs)
++
++bool ccadical_configure (CCaDiCaL *ptr, const char *name) {
++  return ((Wrapper *) ptr)->solver->configure (name);
++}
++
++void ccadical_phase (CCaDiCaL *ptr, int lit) {
++  ((Wrapper *) ptr)->solver->phase (lit);
++}
++
++void ccadical_unphase (CCaDiCaL *ptr, int lit) {
++  ((Wrapper *) ptr)->solver->unphase (lit);
++}
++
++int ccadical_vars (CCaDiCaL *ptr) {
++  return ((Wrapper *) ptr)->solver->vars ();
++}
++
++bool ccadical_set_option_ret (CCaDiCaL *wrapper, const char *name,
++                              int val) {
++  return ((Wrapper *) wrapper)->solver->set (name, val);
++}
++
++bool ccadical_limit_ret (CCaDiCaL *wrapper, const char *name, int val) {
++  return ((Wrapper *) wrapper)->solver->limit (name, val);
++}
++
++int64_t ccadical_redundant (CCaDiCaL *wrapper) {
++  return ((Wrapper *) wrapper)->solver->redundant ();
++}
++
++int ccadical_simplify_rounds (CCaDiCaL *wrapper, int rounds) {
++  return ((Wrapper *) wrapper)->solver->simplify (rounds);
++}
++
++void ccadical_reserve (CCaDiCaL *wrapper, int min_max_var) {
++  return ((Wrapper *) wrapper)->solver->reserve (min_max_var);
++}
++
++int64_t ccadical_propagations (CCaDiCaL *wrapper) {
++  return ((Wrapper *) wrapper)->solver->propagations ();
++}
++
++int64_t ccadical_decisions (CCaDiCaL *wrapper) {
++  return ((Wrapper *) wrapper)->solver->decisions ();
++}
++
++int64_t ccadical_conflicts (CCaDiCaL *wrapper) {
++  return ((Wrapper *) wrapper)->solver->conflicts ();
++}
++
++bool ccadical_flip (CCaDiCaL *wrapper, int lit) {
++  return ((Wrapper *) wrapper)->solver->flip (lit);
++}
++
++bool ccadical_flippable (CCaDiCaL *wrapper, int lit) {
++  return ((Wrapper *) wrapper)->solver->flippable (lit);
++}
++
++/*------------------------------------------------------------------------*/
+ }
+diff --git a/src/ccadical.h b/src/ccadical.h
+index 332f842..4c75ce4 100644
+--- a/src/ccadical.h
++++ b/src/ccadical.h
+@@ -50,6 +50,25 @@ int ccadical_simplify (CCaDiCaL *);
+ 
+ /*------------------------------------------------------------------------*/
+ 
++// Extending C API (Christoph Jabs)
++
++bool ccadical_configure (CCaDiCaL *, const char *);
++void ccadical_phase (CCaDiCaL *, int lit);
++void ccadical_unphase (CCaDiCaL *, int lit);
++int ccadical_vars (CCaDiCaL *);
++bool ccadical_set_option_ret (CCaDiCaL *, const char *name, int val);
++bool ccadical_limit_ret (CCaDiCaL *, const char *name, int val);
++int64_t ccadical_redundant (CCaDiCaL *);
++int ccadical_simplify_rounds (CCaDiCaL *, int rounds);
++void ccadical_reserve (CCaDiCaL *, int min_max_var);
++int64_t ccadical_propagations (CCaDiCaL *);
++int64_t ccadical_decisions (CCaDiCaL *);
++int64_t ccadical_conflicts (CCaDiCaL *);
++bool ccadical_flip (CCaDiCaL *, int lit);
++bool ccadical_flippable (CCaDiCaL *, int lit);
++
++/*------------------------------------------------------------------------*/
++
+ // Support legacy names used before moving to more IPASIR conforming names.
+ 
+ #define ccadical_reset ccadical_release
+diff --git a/src/solver.cpp b/src/solver.cpp
+index 5648101..f7e7a34 100644
+--- a/src/solver.cpp
++++ b/src/solver.cpp
+@@ -832,6 +832,30 @@ int64_t Solver::irredundant () const {
+   return res;
+ }
+ 
++int64_t Solver::propagations () const {
++  TRACE ("propagations");
++  REQUIRE_VALID_STATE ();
++  int64_t res = internal->stats.propagations.search;
++  LOG_API_CALL_RETURNS ("propagations", res);
++  return res;
++}
++
++int64_t Solver::decisions () const {
++  TRACE ("decisions");
++  REQUIRE_VALID_STATE ();
++  int64_t res = internal->stats.decisions;
++  LOG_API_CALL_RETURNS ("decisions", res);
++  return res;
++}
++
++int64_t Solver::conflicts () const {
++  TRACE ("conflicts");
++  REQUIRE_VALID_STATE ();
++  int64_t res = internal->stats.conflicts;
++  LOG_API_CALL_RETURNS ("conflicts", res);
++  return res;
++}
++
+ /*------------------------------------------------------------------------*/
+ 
+ void Solver::freeze (int lit) {
+-- 
+2.41.0
+
diff --git a/cadical/patches/v156.patch b/cadical/patches/v156.patch
new file mode 100644
index 00000000..2ff822e0
--- /dev/null
+++ b/cadical/patches/v156.patch
@@ -0,0 +1,169 @@
+From bbbb4a0392a79340f407e816d4b368468203a052 Mon Sep 17 00:00:00 2001
+From: Christoph Jabs <christoph.jabs@helsinki.fi>
+Date: Wed, 23 Aug 2023 11:30:43 +0300
+Subject: [PATCH] extend C api
+
+---
+ src/cadical.hpp  |  6 +++++
+ src/ccadical.cpp | 63 ++++++++++++++++++++++++++++++++++++++++++++++++
+ src/ccadical.h   | 19 +++++++++++++++
+ src/solver.cpp   | 24 ++++++++++++++++++
+ 4 files changed, 112 insertions(+)
+
+diff --git a/src/cadical.hpp b/src/cadical.hpp
+index 49310c7..7e40f1d 100644
+--- a/src/cadical.hpp
++++ b/src/cadical.hpp
+@@ -627,6 +627,12 @@ public:
+   void phase (int lit);
+   void unphase (int lit);
+ 
++  //------------------------------------------------------------------------
++  // Get some selected statistics
++  int64_t propagations () const;
++  int64_t decisions () const;
++  int64_t conflicts () const;
++
+   //------------------------------------------------------------------------
+ 
+   // Enables clausal proof tracing in DRAT format and returns 'true' if
+diff --git a/src/ccadical.cpp b/src/ccadical.cpp
+index ac11e44..9f7c943 100644
+--- a/src/ccadical.cpp
++++ b/src/ccadical.cpp
+@@ -173,4 +173,67 @@ void ccadical_melt (CCaDiCaL *ptr, int lit) {
+ int ccadical_frozen (CCaDiCaL *ptr, int lit) {
+   return ((Wrapper *) ptr)->solver->frozen (lit);
+ }
++
++/*------------------------------------------------------------------------*/
++
++// Extending C API (Christoph Jabs)
++
++bool ccadical_configure (CCaDiCaL *ptr, const char *name) {
++  return ((Wrapper *) ptr)->solver->configure (name);
++}
++
++void ccadical_phase (CCaDiCaL *ptr, int lit) {
++  ((Wrapper *) ptr)->solver->phase (lit);
++}
++
++void ccadical_unphase (CCaDiCaL *ptr, int lit) {
++  ((Wrapper *) ptr)->solver->unphase (lit);
++}
++
++int ccadical_vars (CCaDiCaL *ptr) {
++  return ((Wrapper *) ptr)->solver->vars ();
++}
++
++bool ccadical_set_option_ret (CCaDiCaL *wrapper, const char *name,
++                              int val) {
++  return ((Wrapper *) wrapper)->solver->set (name, val);
++}
++
++bool ccadical_limit_ret (CCaDiCaL *wrapper, const char *name, int val) {
++  return ((Wrapper *) wrapper)->solver->limit (name, val);
++}
++
++int64_t ccadical_redundant (CCaDiCaL *wrapper) {
++  return ((Wrapper *) wrapper)->solver->redundant ();
++}
++
++int ccadical_simplify_rounds (CCaDiCaL *wrapper, int rounds) {
++  return ((Wrapper *) wrapper)->solver->simplify (rounds);
++}
++
++void ccadical_reserve (CCaDiCaL *wrapper, int min_max_var) {
++  return ((Wrapper *) wrapper)->solver->reserve (min_max_var);
++}
++
++int64_t ccadical_propagations (CCaDiCaL *wrapper) {
++  return ((Wrapper *) wrapper)->solver->propagations ();
++}
++
++int64_t ccadical_decisions (CCaDiCaL *wrapper) {
++  return ((Wrapper *) wrapper)->solver->decisions ();
++}
++
++int64_t ccadical_conflicts (CCaDiCaL *wrapper) {
++  return ((Wrapper *) wrapper)->solver->conflicts ();
++}
++
++bool ccadical_flip (CCaDiCaL *wrapper, int lit) {
++  return ((Wrapper *) wrapper)->solver->flip (lit);
++}
++
++bool ccadical_flippable (CCaDiCaL *wrapper, int lit) {
++  return ((Wrapper *) wrapper)->solver->flippable (lit);
++}
++
++/*------------------------------------------------------------------------*/
+ }
+diff --git a/src/ccadical.h b/src/ccadical.h
+index 30a79b3..56fb16b 100644
+--- a/src/ccadical.h
++++ b/src/ccadical.h
+@@ -50,6 +50,25 @@ int ccadical_simplify (CCaDiCaL *);
+ 
+ /*------------------------------------------------------------------------*/
+ 
++// Extending C API (Christoph Jabs)
++
++bool ccadical_configure (CCaDiCaL *, const char *);
++void ccadical_phase (CCaDiCaL *, int lit);
++void ccadical_unphase (CCaDiCaL *, int lit);
++int ccadical_vars (CCaDiCaL *);
++bool ccadical_set_option_ret (CCaDiCaL *, const char *name, int val);
++bool ccadical_limit_ret (CCaDiCaL *, const char *name, int val);
++int64_t ccadical_redundant (CCaDiCaL *);
++int ccadical_simplify_rounds (CCaDiCaL *, int rounds);
++void ccadical_reserve (CCaDiCaL *, int min_max_var);
++int64_t ccadical_propagations (CCaDiCaL *);
++int64_t ccadical_decisions (CCaDiCaL *);
++int64_t ccadical_conflicts (CCaDiCaL *);
++bool ccadical_flip (CCaDiCaL *, int lit);
++bool ccadical_flippable (CCaDiCaL *, int lit);
++
++/*------------------------------------------------------------------------*/
++
+ // Support legacy names used before moving to more IPASIR conforming names.
+ 
+ #define ccadical_reset ccadical_release
+diff --git a/src/solver.cpp b/src/solver.cpp
+index 63293ad..d1153d6 100644
+--- a/src/solver.cpp
++++ b/src/solver.cpp
+@@ -832,6 +832,30 @@ int64_t Solver::irredundant () const {
+   return res;
+ }
+ 
++int64_t Solver::propagations () const {
++  TRACE ("propagations");
++  REQUIRE_VALID_STATE ();
++  int64_t res = internal->stats.propagations.search;
++  LOG_API_CALL_RETURNS ("propagations", res);
++  return res;
++}
++
++int64_t Solver::decisions () const {
++  TRACE ("decisions");
++  REQUIRE_VALID_STATE ();
++  int64_t res = internal->stats.decisions;
++  LOG_API_CALL_RETURNS ("decisions", res);
++  return res;
++}
++
++int64_t Solver::conflicts () const {
++  TRACE ("conflicts");
++  REQUIRE_VALID_STATE ();
++  int64_t res = internal->stats.conflicts;
++  LOG_API_CALL_RETURNS ("conflicts", res);
++  return res;
++}
++
+ /*------------------------------------------------------------------------*/
+ 
+ void Solver::freeze (int lit) {
+-- 
+2.41.0
+
diff --git a/cadical/patches/v160.patch b/cadical/patches/v160.patch
new file mode 100644
index 00000000..1c01fc34
--- /dev/null
+++ b/cadical/patches/v160.patch
@@ -0,0 +1,169 @@
+From 978c6b563055207218334ea9979802d5367cc09f Mon Sep 17 00:00:00 2001
+From: Christoph Jabs <christoph.jabs@helsinki.fi>
+Date: Wed, 23 Aug 2023 11:30:43 +0300
+Subject: [PATCH] extend C api
+
+---
+ src/cadical.hpp  |  6 +++++
+ src/ccadical.cpp | 63 ++++++++++++++++++++++++++++++++++++++++++++++++
+ src/ccadical.h   | 19 +++++++++++++++
+ src/solver.cpp   | 24 ++++++++++++++++++
+ 4 files changed, 112 insertions(+)
+
+diff --git a/src/cadical.hpp b/src/cadical.hpp
+index 26cb9ca..d7539fc 100644
+--- a/src/cadical.hpp
++++ b/src/cadical.hpp
+@@ -688,6 +688,12 @@ public:
+   void phase (int lit);
+   void unphase (int lit);
+ 
++  //------------------------------------------------------------------------
++  // Get some selected statistics
++  int64_t propagations () const;
++  int64_t decisions () const;
++  int64_t conflicts () const;
++
+   //------------------------------------------------------------------------
+ 
+   // Enables clausal proof tracing in DRAT format and returns 'true' if
+diff --git a/src/ccadical.cpp b/src/ccadical.cpp
+index ac11e44..9f7c943 100644
+--- a/src/ccadical.cpp
++++ b/src/ccadical.cpp
+@@ -173,4 +173,67 @@ void ccadical_melt (CCaDiCaL *ptr, int lit) {
+ int ccadical_frozen (CCaDiCaL *ptr, int lit) {
+   return ((Wrapper *) ptr)->solver->frozen (lit);
+ }
++
++/*------------------------------------------------------------------------*/
++
++// Extending C API (Christoph Jabs)
++
++bool ccadical_configure (CCaDiCaL *ptr, const char *name) {
++  return ((Wrapper *) ptr)->solver->configure (name);
++}
++
++void ccadical_phase (CCaDiCaL *ptr, int lit) {
++  ((Wrapper *) ptr)->solver->phase (lit);
++}
++
++void ccadical_unphase (CCaDiCaL *ptr, int lit) {
++  ((Wrapper *) ptr)->solver->unphase (lit);
++}
++
++int ccadical_vars (CCaDiCaL *ptr) {
++  return ((Wrapper *) ptr)->solver->vars ();
++}
++
++bool ccadical_set_option_ret (CCaDiCaL *wrapper, const char *name,
++                              int val) {
++  return ((Wrapper *) wrapper)->solver->set (name, val);
++}
++
++bool ccadical_limit_ret (CCaDiCaL *wrapper, const char *name, int val) {
++  return ((Wrapper *) wrapper)->solver->limit (name, val);
++}
++
++int64_t ccadical_redundant (CCaDiCaL *wrapper) {
++  return ((Wrapper *) wrapper)->solver->redundant ();
++}
++
++int ccadical_simplify_rounds (CCaDiCaL *wrapper, int rounds) {
++  return ((Wrapper *) wrapper)->solver->simplify (rounds);
++}
++
++void ccadical_reserve (CCaDiCaL *wrapper, int min_max_var) {
++  return ((Wrapper *) wrapper)->solver->reserve (min_max_var);
++}
++
++int64_t ccadical_propagations (CCaDiCaL *wrapper) {
++  return ((Wrapper *) wrapper)->solver->propagations ();
++}
++
++int64_t ccadical_decisions (CCaDiCaL *wrapper) {
++  return ((Wrapper *) wrapper)->solver->decisions ();
++}
++
++int64_t ccadical_conflicts (CCaDiCaL *wrapper) {
++  return ((Wrapper *) wrapper)->solver->conflicts ();
++}
++
++bool ccadical_flip (CCaDiCaL *wrapper, int lit) {
++  return ((Wrapper *) wrapper)->solver->flip (lit);
++}
++
++bool ccadical_flippable (CCaDiCaL *wrapper, int lit) {
++  return ((Wrapper *) wrapper)->solver->flippable (lit);
++}
++
++/*------------------------------------------------------------------------*/
+ }
+diff --git a/src/ccadical.h b/src/ccadical.h
+index 30a79b3..56fb16b 100644
+--- a/src/ccadical.h
++++ b/src/ccadical.h
+@@ -50,6 +50,25 @@ int ccadical_simplify (CCaDiCaL *);
+ 
+ /*------------------------------------------------------------------------*/
+ 
++// Extending C API (Christoph Jabs)
++
++bool ccadical_configure (CCaDiCaL *, const char *);
++void ccadical_phase (CCaDiCaL *, int lit);
++void ccadical_unphase (CCaDiCaL *, int lit);
++int ccadical_vars (CCaDiCaL *);
++bool ccadical_set_option_ret (CCaDiCaL *, const char *name, int val);
++bool ccadical_limit_ret (CCaDiCaL *, const char *name, int val);
++int64_t ccadical_redundant (CCaDiCaL *);
++int ccadical_simplify_rounds (CCaDiCaL *, int rounds);
++void ccadical_reserve (CCaDiCaL *, int min_max_var);
++int64_t ccadical_propagations (CCaDiCaL *);
++int64_t ccadical_decisions (CCaDiCaL *);
++int64_t ccadical_conflicts (CCaDiCaL *);
++bool ccadical_flip (CCaDiCaL *, int lit);
++bool ccadical_flippable (CCaDiCaL *, int lit);
++
++/*------------------------------------------------------------------------*/
++
+ // Support legacy names used before moving to more IPASIR conforming names.
+ 
+ #define ccadical_reset ccadical_release
+diff --git a/src/solver.cpp b/src/solver.cpp
+index 9ac3887..fd964fd 100644
+--- a/src/solver.cpp
++++ b/src/solver.cpp
+@@ -898,6 +898,30 @@ int64_t Solver::irredundant () const {
+   return res;
+ }
+ 
++int64_t Solver::propagations () const {
++  TRACE ("propagations");
++  REQUIRE_VALID_STATE ();
++  int64_t res = internal->stats.propagations.search;
++  LOG_API_CALL_RETURNS ("propagations", res);
++  return res;
++}
++
++int64_t Solver::decisions () const {
++  TRACE ("decisions");
++  REQUIRE_VALID_STATE ();
++  int64_t res = internal->stats.decisions;
++  LOG_API_CALL_RETURNS ("decisions", res);
++  return res;
++}
++
++int64_t Solver::conflicts () const {
++  TRACE ("conflicts");
++  REQUIRE_VALID_STATE ();
++  int64_t res = internal->stats.conflicts;
++  LOG_API_CALL_RETURNS ("conflicts", res);
++  return res;
++}
++
+ /*------------------------------------------------------------------------*/
+ 
+ void Solver::freeze (int lit) {
+-- 
+2.41.0
+
diff --git a/cadical/patches/v170.patch b/cadical/patches/v170.patch
new file mode 100644
index 00000000..4a04bba8
--- /dev/null
+++ b/cadical/patches/v170.patch
@@ -0,0 +1,169 @@
+From 9f5fe5b55adccf8ff01a6e2934983f61d78a91c7 Mon Sep 17 00:00:00 2001
+From: Christoph Jabs <christoph.jabs@helsinki.fi>
+Date: Wed, 23 Aug 2023 11:30:43 +0300
+Subject: [PATCH] extend C api
+
+---
+ src/cadical.hpp  |  6 +++++
+ src/ccadical.cpp | 63 ++++++++++++++++++++++++++++++++++++++++++++++++
+ src/ccadical.h   | 19 +++++++++++++++
+ src/solver.cpp   | 24 ++++++++++++++++++
+ 4 files changed, 112 insertions(+)
+
+diff --git a/src/cadical.hpp b/src/cadical.hpp
+index 26cb9ca..d7539fc 100644
+--- a/src/cadical.hpp
++++ b/src/cadical.hpp
+@@ -688,6 +688,12 @@ public:
+   void phase (int lit);
+   void unphase (int lit);
+ 
++  //------------------------------------------------------------------------
++  // Get some selected statistics
++  int64_t propagations () const;
++  int64_t decisions () const;
++  int64_t conflicts () const;
++
+   //------------------------------------------------------------------------
+ 
+   // Enables clausal proof tracing in DRAT format and returns 'true' if
+diff --git a/src/ccadical.cpp b/src/ccadical.cpp
+index ac11e44..9f7c943 100644
+--- a/src/ccadical.cpp
++++ b/src/ccadical.cpp
+@@ -173,4 +173,67 @@ void ccadical_melt (CCaDiCaL *ptr, int lit) {
+ int ccadical_frozen (CCaDiCaL *ptr, int lit) {
+   return ((Wrapper *) ptr)->solver->frozen (lit);
+ }
++
++/*------------------------------------------------------------------------*/
++
++// Extending C API (Christoph Jabs)
++
++bool ccadical_configure (CCaDiCaL *ptr, const char *name) {
++  return ((Wrapper *) ptr)->solver->configure (name);
++}
++
++void ccadical_phase (CCaDiCaL *ptr, int lit) {
++  ((Wrapper *) ptr)->solver->phase (lit);
++}
++
++void ccadical_unphase (CCaDiCaL *ptr, int lit) {
++  ((Wrapper *) ptr)->solver->unphase (lit);
++}
++
++int ccadical_vars (CCaDiCaL *ptr) {
++  return ((Wrapper *) ptr)->solver->vars ();
++}
++
++bool ccadical_set_option_ret (CCaDiCaL *wrapper, const char *name,
++                              int val) {
++  return ((Wrapper *) wrapper)->solver->set (name, val);
++}
++
++bool ccadical_limit_ret (CCaDiCaL *wrapper, const char *name, int val) {
++  return ((Wrapper *) wrapper)->solver->limit (name, val);
++}
++
++int64_t ccadical_redundant (CCaDiCaL *wrapper) {
++  return ((Wrapper *) wrapper)->solver->redundant ();
++}
++
++int ccadical_simplify_rounds (CCaDiCaL *wrapper, int rounds) {
++  return ((Wrapper *) wrapper)->solver->simplify (rounds);
++}
++
++void ccadical_reserve (CCaDiCaL *wrapper, int min_max_var) {
++  return ((Wrapper *) wrapper)->solver->reserve (min_max_var);
++}
++
++int64_t ccadical_propagations (CCaDiCaL *wrapper) {
++  return ((Wrapper *) wrapper)->solver->propagations ();
++}
++
++int64_t ccadical_decisions (CCaDiCaL *wrapper) {
++  return ((Wrapper *) wrapper)->solver->decisions ();
++}
++
++int64_t ccadical_conflicts (CCaDiCaL *wrapper) {
++  return ((Wrapper *) wrapper)->solver->conflicts ();
++}
++
++bool ccadical_flip (CCaDiCaL *wrapper, int lit) {
++  return ((Wrapper *) wrapper)->solver->flip (lit);
++}
++
++bool ccadical_flippable (CCaDiCaL *wrapper, int lit) {
++  return ((Wrapper *) wrapper)->solver->flippable (lit);
++}
++
++/*------------------------------------------------------------------------*/
+ }
+diff --git a/src/ccadical.h b/src/ccadical.h
+index 30a79b3..56fb16b 100644
+--- a/src/ccadical.h
++++ b/src/ccadical.h
+@@ -50,6 +50,25 @@ int ccadical_simplify (CCaDiCaL *);
+ 
+ /*------------------------------------------------------------------------*/
+ 
++// Extending C API (Christoph Jabs)
++
++bool ccadical_configure (CCaDiCaL *, const char *);
++void ccadical_phase (CCaDiCaL *, int lit);
++void ccadical_unphase (CCaDiCaL *, int lit);
++int ccadical_vars (CCaDiCaL *);
++bool ccadical_set_option_ret (CCaDiCaL *, const char *name, int val);
++bool ccadical_limit_ret (CCaDiCaL *, const char *name, int val);
++int64_t ccadical_redundant (CCaDiCaL *);
++int ccadical_simplify_rounds (CCaDiCaL *, int rounds);
++void ccadical_reserve (CCaDiCaL *, int min_max_var);
++int64_t ccadical_propagations (CCaDiCaL *);
++int64_t ccadical_decisions (CCaDiCaL *);
++int64_t ccadical_conflicts (CCaDiCaL *);
++bool ccadical_flip (CCaDiCaL *, int lit);
++bool ccadical_flippable (CCaDiCaL *, int lit);
++
++/*------------------------------------------------------------------------*/
++
+ // Support legacy names used before moving to more IPASIR conforming names.
+ 
+ #define ccadical_reset ccadical_release
+diff --git a/src/solver.cpp b/src/solver.cpp
+index 3887a97..6b1727b 100644
+--- a/src/solver.cpp
++++ b/src/solver.cpp
+@@ -906,6 +906,30 @@ int64_t Solver::irredundant () const {
+   return res;
+ }
+ 
++int64_t Solver::propagations () const {
++  TRACE ("propagations");
++  REQUIRE_VALID_STATE ();
++  int64_t res = internal->stats.propagations.search;
++  LOG_API_CALL_RETURNS ("propagations", res);
++  return res;
++}
++
++int64_t Solver::decisions () const {
++  TRACE ("decisions");
++  REQUIRE_VALID_STATE ();
++  int64_t res = internal->stats.decisions;
++  LOG_API_CALL_RETURNS ("decisions", res);
++  return res;
++}
++
++int64_t Solver::conflicts () const {
++  TRACE ("conflicts");
++  REQUIRE_VALID_STATE ();
++  int64_t res = internal->stats.conflicts;
++  LOG_API_CALL_RETURNS ("conflicts", res);
++  return res;
++}
++
+ /*------------------------------------------------------------------------*/
+ 
+ void Solver::freeze (int lit) {
+-- 
+2.41.0
+
diff --git a/cadical/src/lib.rs b/cadical/src/lib.rs
new file mode 100644
index 00000000..dc85204f
--- /dev/null
+++ b/cadical/src/lib.rs
@@ -0,0 +1,1047 @@
+//! # CaDiCaL Solver Interface
+//!
+//! Interface to the [CaDiCaL](https://github.com/arminbiere/cadical) incremental SAT solver.
+
+use core::ffi::{c_int, c_void, CStr};
+use std::{cmp::Ordering, ffi::CString, fmt};
+
+use cpu_time::ProcessTime;
+use ffi::CaDiCaLHandle;
+use rustsat::solvers::{
+    ControlSignal, GetInternalStats, Interrupt, InterruptSolver, Learn, LimitConflicts,
+    LimitDecisions, PhaseLit, Solve, SolveIncremental, SolveMightFail, SolveStats, SolverError,
+    SolverResult, SolverState, SolverStats, Terminate,
+};
+use rustsat::types::{Clause, Lit, TernaryVal, Var};
+
+#[derive(Debug, PartialEq, Eq, Default)]
+enum InternalSolverState {
+    #[default]
+    Configuring,
+    Input,
+    Sat,
+    Unsat(Vec<Lit>),
+}
+
+impl InternalSolverState {
+    fn to_external(&self) -> SolverState {
+        match self {
+            InternalSolverState::Configuring => SolverState::Configuring,
+            InternalSolverState::Input => SolverState::Input,
+            InternalSolverState::Sat => SolverState::Sat,
+            InternalSolverState::Unsat(_) => SolverState::Unsat,
+        }
+    }
+}
+
+type TermCallbackPtr<'a> = Box<dyn FnMut() -> ControlSignal + 'a>;
+type LearnCallbackPtr<'a> = Box<dyn FnMut(Clause) + 'a>;
+/// Double boxing is necessary to get thin pointers for casting
+type OptTermCallbackStore<'a> = Option<Box<TermCallbackPtr<'a>>>;
+/// Double boxing is necessary to get thin pointers for casting
+type OptLearnCallbackStore<'a> = Option<Box<LearnCallbackPtr<'a>>>;
+
+/// The CaDiCaL solver type
+pub struct CaDiCaL<'term, 'learn> {
+    handle: *mut CaDiCaLHandle,
+    state: InternalSolverState,
+    terminate_cb: OptTermCallbackStore<'term>,
+    learner_cb: OptLearnCallbackStore<'learn>,
+    stats: SolverStats,
+}
+
+impl Default for CaDiCaL<'_, '_> {
+    fn default() -> Self {
+        let solver = Self {
+            handle: unsafe { ffi::ccadical_init() },
+            state: Default::default(),
+            terminate_cb: Default::default(),
+            learner_cb: Default::default(),
+            stats: Default::default(),
+        };
+        let quiet = CString::new("quiet").unwrap();
+        unsafe { ffi::ccadical_set_option_ret(solver.handle, quiet.as_ptr(), 1) };
+        solver
+    }
+}
+
+impl CaDiCaL<'_, '_> {
+    fn get_core_assumps(&self, assumps: &Vec<Lit>) -> Result<Vec<Lit>, SolverError> {
+        let mut core = Vec::new();
+        core.reserve(assumps.len());
+        for a in assumps {
+            match unsafe { ffi::ccadical_failed(self.handle, a.to_ipasir()) } {
+                0 => (),
+                1 => core.push(!*a),
+                invalid => {
+                    return Err(SolverError::Api(format!(
+                        "ccadical_failed returned invalid value: {}",
+                        invalid
+                    )))
+                }
+            }
+        }
+        Ok(core)
+    }
+
+    /// Adds a clause that only exists for the next solver call. Only one such
+    /// clause can exist, a new new clause replaces the old one.
+    ///
+    /// _Note_: If this is used, in addition to [`SolveIncremental::core`],
+    /// [`CaDiCaL::tmp_clause_in_core`] needs to be checked to determine if the
+    /// temporary clause is part of the core.
+    pub fn add_tmp_clause(&mut self, clause: Clause) {
+        // Update wrapper-internal state
+        self.stats.n_clauses += 1;
+        self.stats.avg_clause_len =
+            (self.stats.avg_clause_len * ((self.stats.n_clauses - 1) as f32) + clause.len() as f32)
+                / self.stats.n_clauses as f32;
+        self.state = InternalSolverState::Input;
+        // Call CaDiCaL backend
+        for lit in &clause {
+            unsafe { ffi::ccadical_constrain(self.handle, lit.to_ipasir()) }
+        }
+        unsafe { ffi::ccadical_constrain(self.handle, 0) }
+    }
+
+    /// Checks whether the temporary clause is part of the core if in
+    /// unsatisfiable state. This needs to always be checked in addition to
+    /// [`SolveIncremental::core`] if a [`CaDiCaL::add_tmp_clause`] is used.
+    pub fn tmp_clause_in_core(&mut self) -> Result<bool, SolverError> {
+        match &self.state {
+            InternalSolverState::Unsat(_) => unsafe {
+                Ok(ffi::ccadical_constraint_failed(self.handle) != 0)
+            },
+            state => Err(SolverError::State(state.to_external(), SolverState::Unsat)),
+        }
+    }
+
+    /// Sets a pre-defined configuration for CaDiCaL's internal options
+    pub fn set_configuration(&mut self, config: Config) -> SolveMightFail {
+        if self.state == InternalSolverState::Configuring {
+            let config_name = match config {
+                Config::Default => CString::new("default").unwrap(),
+                Config::Plain => CString::new("plain").unwrap(),
+                Config::SAT => CString::new("sat").unwrap(),
+                Config::UNSAT => CString::new("unsat").unwrap(),
+            };
+            let ret = unsafe { ffi::ccadical_configure(self.handle, config_name.as_ptr()) };
+            if ret {
+                Ok(())
+            } else {
+                Err(SolverError::Api(
+                    "ccadical_configure returned false".to_string(),
+                ))
+            }
+        } else {
+            Err(SolverError::State(
+                self.state.to_external(),
+                SolverState::Configuring,
+            ))
+        }
+    }
+
+    /// Sets the value of a CaDiCaL option. For possible options, check CaDiCaL with `cadical --help`.
+    /// Requires state [`SolverState::Configuring`].
+    ///
+    /// # CaDiCaL Documentation
+    ///
+    /// Explicit version of setting an option.  If the option `<name>` exists
+    /// and `<val>` can be parsed then 'true' is returned.  If the option value
+    /// is out of range the actual value is computed as the closest (minimum or
+    /// maximum) value possible, but still `true` is returned.
+    pub fn set_option(&mut self, name: &str, value: c_int) -> SolveMightFail {
+        let c_name = match CString::new(name) {
+            Ok(cstr) => cstr,
+            Err(_) => {
+                return Err(SolverError::Api(format!(
+                    "CaDiCaL option {} cannot be converted to a C string",
+                    name
+                )))
+            }
+        };
+        if unsafe { ffi::ccadical_set_option_ret(self.handle, c_name.as_ptr(), value) } {
+            Ok(())
+        } else {
+            Err(SolverError::Api(format!(
+                "ccadical_set_option_ret returned false for option {}",
+                name
+            )))
+        }
+    }
+
+    /// Gets the value of a CaDiCaL option. For possible options, check CaDiCaL with `cadical --help`.
+    ///
+    /// # CaDiCaL Documentation
+    ///
+    /// Get the current value of the option `name`.  If `name` is invalid then
+    /// zero is returned.
+    pub fn get_option(&self, name: &str) -> Result<c_int, SolverError> {
+        let c_name = match CString::new(name) {
+            Ok(cstr) => cstr,
+            Err(_) => {
+                return Err(SolverError::Api(format!(
+                    "CaDiCaL option {} cannot be converted to a C string",
+                    name
+                )))
+            }
+        };
+        Ok(unsafe { ffi::ccadical_get_option(self.handle, c_name.as_ptr()) })
+    }
+
+    /// Sets an internal limit for CaDiCaL
+    ///
+    /// # CaDiCaL Documentation
+    ///
+    /// Specify search limits, where currently `name` can be "conflicts",
+    /// "decisions", "preprocessing", or "localsearch".  The first two limits
+    /// are unbounded by default.  Thus using a negative limit for conflicts or
+    /// decisions switches back to the default of unlimited search (for that
+    /// particular limit).  The preprocessing limit determines the number of
+    /// preprocessing rounds, which is zero by default.  Similarly, the local
+    /// search limit determines the number of local search rounds (also zero by
+    /// default).  As with `set`, the return value denotes whether the limit
+    /// `name` is valid.  These limits are only valid for the next `solve` or
+    /// `simplify` call and reset to their default after `solve` returns (as
+    /// well as overwritten and reset during calls to `simplify` and
+    /// `lookahead`).  We actually also have an internal "terminate" limit
+    /// which however should only be used for testing and debugging.
+    pub fn set_limit(&mut self, limit: Limit) -> SolveMightFail {
+        let (name, val) = match limit {
+            Limit::Terminate(val) => (CString::new("terminate").unwrap(), val),
+            Limit::Conflicts(val) => (CString::new("conflicts").unwrap(), val),
+            Limit::Decisions(val) => (CString::new("decisions").unwrap(), val),
+            Limit::Preprocessing(val) => (CString::new("preprocessing").unwrap(), val),
+            Limit::LocalSearch(val) => (CString::new("localsearch").unwrap(), val),
+        };
+        if unsafe { ffi::ccadical_limit_ret(self.handle, name.as_ptr(), val) } {
+            Ok(())
+        } else {
+            Err(SolverError::Api(format!(
+                "ccadical_limit_ret returned false for limit {}",
+                limit
+            )))
+        }
+    }
+
+    /// Gets the number of active variables
+    pub fn get_active(&self) -> i64 {
+        unsafe { ffi::ccadical_active(self.handle) }
+    }
+
+    /// Gets the number of active irredundant clauses
+    pub fn get_irredundant(&self) -> i64 {
+        unsafe { ffi::ccadical_irredundant(self.handle) }
+    }
+
+    /// Gets the number of active redundant clauses
+    pub fn get_redundant(&self) -> i64 {
+        unsafe { ffi::ccadical_redundant(self.handle) }
+    }
+
+    /// Gets the current literal value at the root level
+    pub fn current_lit_val(&self, lit: Lit) -> TernaryVal {
+        let int_val = unsafe { ffi::ccadical_fixed(self.handle, lit.to_ipasir()) };
+        match int_val.cmp(&0) {
+            Ordering::Greater => TernaryVal::True,
+            Ordering::Less => TernaryVal::False,
+            Ordering::Equal => TernaryVal::DontCare,
+        }
+    }
+
+    /// Freezes a literal. See CaDiCaL documentation for more details.
+    pub fn freeze_lit(&mut self, lit: Lit) {
+        unsafe { ffi::ccadical_freeze(self.handle, lit.to_ipasir()) }
+    }
+
+    /// Melts a literal. See CaDiCaL documentation for more details.
+    pub fn melt_lit(&mut self, lit: Lit) {
+        unsafe { ffi::ccadical_melt(self.handle, lit.to_ipasir()) }
+    }
+
+    /// Checks if a literal is frozen. See CaDiCaL documentation for more details.
+    pub fn is_frozen(&self, lit: Lit) -> bool {
+        (unsafe { ffi::ccadical_frozen(self.handle, lit.to_ipasir()) }) != 0
+    }
+
+    /// Prints the solver statistics from the CaDiCaL backend
+    pub fn print_stats(&self) {
+        unsafe { ffi::ccadical_print_statistics(self.handle) }
+    }
+
+    pub fn simplify(&mut self, rounds: u32) -> Result<SolverResult, SolverError> {
+        // If already solved, return state
+        if let InternalSolverState::Sat = self.state {
+            return Ok(SolverResult::Sat);
+        } else if let InternalSolverState::Unsat(_) = self.state {
+            return Ok(SolverResult::Unsat);
+        }
+        let rounds: c_int = match rounds.try_into() {
+            Ok(val) => val,
+            Err(_) => {
+                return Err(SolverError::Api(format!(
+                    "rounds value {} does not fit into c_int",
+                    rounds
+                )))
+            }
+        };
+        // Simplify with CaDiCaL backend
+        match unsafe { ffi::ccadical_simplify_rounds(self.handle, rounds) } {
+            0 => {
+                self.state = InternalSolverState::Input;
+                Ok(SolverResult::Interrupted)
+            }
+            10 => {
+                self.state = InternalSolverState::Sat;
+                Ok(SolverResult::Sat)
+            }
+            20 => {
+                self.state = InternalSolverState::Unsat(vec![]);
+                Ok(SolverResult::Unsat)
+            }
+            invalid => Err(SolverError::Api(format!(
+                "ccadical_simplify returned invalid value: {}",
+                invalid
+            ))),
+        }
+    }
+
+    pub fn simplify_assumps(
+        &mut self,
+        assumps: Vec<Lit>,
+        rounds: u32,
+    ) -> Result<SolverResult, SolverError> {
+        // If already solved, return state
+        if let InternalSolverState::Sat = self.state {
+            return Ok(SolverResult::Sat);
+        } else if let InternalSolverState::Unsat(_) = self.state {
+            return Ok(SolverResult::Unsat);
+        }
+        let rounds: c_int = match rounds.try_into() {
+            Ok(val) => val,
+            Err(_) => {
+                return Err(SolverError::Api(format!(
+                    "rounds value {} does not fit into c_int",
+                    rounds
+                )))
+            }
+        };
+        // Simplify with CaDiCaL backend under assumptions
+        for a in &assumps {
+            unsafe { ffi::ccadical_assume(self.handle, a.to_ipasir()) }
+        }
+        match unsafe { ffi::ccadical_simplify_rounds(self.handle, rounds) } {
+            0 => {
+                self.state = InternalSolverState::Input;
+                Ok(SolverResult::Interrupted)
+            }
+            10 => {
+                self.state = InternalSolverState::Sat;
+                Ok(SolverResult::Sat)
+            }
+            20 => {
+                self.state = InternalSolverState::Unsat(vec![]);
+                Ok(SolverResult::Unsat)
+            }
+            invalid => Err(SolverError::Api(format!(
+                "ccadical_simplify returned invalid value: {}",
+                invalid
+            ))),
+        }
+    }
+}
+
+impl Solve for CaDiCaL<'_, '_> {
+    fn signature(&self) -> &'static str {
+        let c_chars = unsafe { ffi::ccadical_signature() };
+        let c_str = unsafe { CStr::from_ptr(c_chars) };
+        c_str
+            .to_str()
+            .expect("CaDiCaL signature returned invalid UTF-8.")
+    }
+
+    fn reserve(&mut self, max_var: Var) -> SolveMightFail {
+        self.state = InternalSolverState::Input;
+        unsafe { ffi::ccadical_reserve(self.handle, max_var.to_ipasir()) };
+        Ok(())
+    }
+
+    fn solve(&mut self) -> Result<SolverResult, SolverError> {
+        // If already solved, return state
+        if let InternalSolverState::Sat = self.state {
+            return Ok(SolverResult::Sat);
+        } else if let InternalSolverState::Unsat(core) = &self.state {
+            if core.is_empty() {
+                return Ok(SolverResult::Unsat);
+            }
+        }
+        let start = ProcessTime::now();
+        // Solve with CaDiCaL backend
+        let res = unsafe { ffi::ccadical_solve(self.handle) };
+        self.stats.cpu_solve_time += start.elapsed();
+        match res {
+            0 => {
+                self.stats.n_terminated += 1;
+                self.state = InternalSolverState::Input;
+                Ok(SolverResult::Interrupted)
+            }
+            10 => {
+                self.stats.n_sat += 1;
+                self.state = InternalSolverState::Sat;
+                Ok(SolverResult::Sat)
+            }
+            20 => {
+                self.stats.n_unsat += 1;
+                self.state = InternalSolverState::Unsat(vec![]);
+                Ok(SolverResult::Unsat)
+            }
+            invalid => Err(SolverError::Api(format!(
+                "ccadical_solve returned invalid value: {}",
+                invalid
+            ))),
+        }
+    }
+
+    fn lit_val(&self, lit: Lit) -> Result<TernaryVal, SolverError> {
+        match &self.state {
+            InternalSolverState::Sat => {
+                let lit = lit.to_ipasir();
+                match unsafe { ffi::ccadical_val(self.handle, lit) } {
+                    0 => Ok(TernaryVal::DontCare),
+                    p if p == lit => Ok(TernaryVal::True),
+                    n if n == -lit => Ok(TernaryVal::False),
+                    // CaDiCaL returns -1 if variable is higher than max var
+                    dc if dc == -1 => Ok(TernaryVal::DontCare),
+                    invalid => Err(SolverError::Api(format!(
+                        "ccadical_val returned invalid value: {}",
+                        invalid
+                    ))),
+                }
+            }
+            other => Err(SolverError::State(other.to_external(), SolverState::Sat)),
+        }
+    }
+
+    fn add_clause(&mut self, clause: Clause) -> SolveMightFail {
+        // Update wrapper-internal state
+        self.stats.n_clauses += 1;
+        self.stats.avg_clause_len =
+            (self.stats.avg_clause_len * ((self.stats.n_clauses - 1) as f32) + clause.len() as f32)
+                / self.stats.n_clauses as f32;
+        self.state = InternalSolverState::Input;
+        // Call CaDiCaL backend
+        clause
+            .into_iter()
+            .for_each(|l| unsafe { ffi::ccadical_add(self.handle, l.to_ipasir()) });
+        unsafe { ffi::ccadical_add(self.handle, 0) };
+        Ok(())
+    }
+}
+
+impl SolveIncremental for CaDiCaL<'_, '_> {
+    fn solve_assumps(&mut self, assumps: Vec<Lit>) -> Result<SolverResult, SolverError> {
+        let start = ProcessTime::now();
+        // Solve with CaDiCaL backend
+        for a in &assumps {
+            unsafe { ffi::ccadical_assume(self.handle, a.to_ipasir()) }
+        }
+        let res = unsafe { ffi::ccadical_solve(self.handle) };
+        self.stats.cpu_solve_time += start.elapsed();
+        match res {
+            0 => {
+                self.stats.n_terminated += 1;
+                self.state = InternalSolverState::Input;
+                Ok(SolverResult::Interrupted)
+            }
+            10 => {
+                self.stats.n_sat += 1;
+                self.state = InternalSolverState::Sat;
+                Ok(SolverResult::Sat)
+            }
+            20 => {
+                self.stats.n_unsat += 1;
+                self.state = InternalSolverState::Unsat(self.get_core_assumps(&assumps)?);
+                Ok(SolverResult::Unsat)
+            }
+            invalid => Err(SolverError::Api(format!(
+                "ccadical_solve returned invalid value: {}",
+                invalid
+            ))),
+        }
+    }
+
+    fn core(&mut self) -> Result<Vec<Lit>, SolverError> {
+        match &self.state {
+            InternalSolverState::Unsat(core) => Ok(core.clone()),
+            other => Err(SolverError::State(other.to_external(), SolverState::Unsat)),
+        }
+    }
+}
+
+impl<'term> Terminate<'term> for CaDiCaL<'term, '_> {
+    /// Sets a terminator callback that is regularly called during solving.
+    ///
+    /// # Examples
+    ///
+    /// Terminate solver after 10 callback calls.
+    ///
+    /// ```
+    /// use rustsat::solvers::{ControlSignal, Solve, SolverResult, Terminate};
+    /// use rustsat_cadical::CaDiCaL;
+    ///
+    /// let mut solver = CaDiCaL::default();
+    ///
+    /// // Load instance
+    ///
+    /// let mut cnt = 1;
+    /// solver.attach_terminator(move || {
+    ///     if cnt > 10 {
+    ///         ControlSignal::Terminate
+    ///     } else {
+    ///         cnt += 1;
+    ///         ControlSignal::Continue
+    ///     }
+    /// });
+    ///
+    /// let ret = solver.solve().unwrap();
+    ///
+    /// // Assuming an instance is actually loaded and runs long enough
+    /// // assert_eq!(ret, SolverResult::Interrupted);
+    /// ```
+    fn attach_terminator<CB>(&mut self, cb: CB)
+    where
+        CB: FnMut() -> ControlSignal + 'term,
+    {
+        self.terminate_cb = Some(Box::new(Box::new(cb)));
+        let cb_ptr = self.terminate_cb.as_mut().unwrap().as_mut() as *const _ as *const c_void;
+        unsafe {
+            ffi::ccadical_set_terminate(self.handle, cb_ptr, Some(ffi::ccadical_terminate_cb))
+        }
+    }
+
+    fn detach_terminator(&mut self) {
+        self.terminate_cb = None;
+        unsafe { ffi::ccadical_set_terminate(self.handle, std::ptr::null(), None) }
+    }
+}
+
+impl<'learn> Learn<'learn> for CaDiCaL<'_, 'learn> {
+    /// Sets a learner callback that gets passed clauses up to a certain length learned by the solver.
+    ///
+    /// The callback goes out of scope with the solver, afterwards captured variables become accessible.
+    ///
+    /// # Examples
+    ///
+    /// Count number of learned clauses up to length 10.
+    ///
+    /// ```
+    /// use rustsat::solvers::{Solve, SolverResult, Learn};
+    /// use rustsat_cadical::CaDiCaL;
+    ///
+    /// let mut cnt = 0;
+    ///
+    /// {
+    ///     let mut solver = CaDiCaL::default();
+    ///     // Load instance
+    ///
+    ///     solver.attach_learner(|_| cnt += 1, 10);
+    ///
+    ///     solver.solve().unwrap();
+    /// }
+    ///
+    /// // cnt variable can be accessed from here on
+    /// ```
+    fn attach_learner<CB>(&mut self, cb: CB, max_len: usize)
+    where
+        CB: FnMut(Clause) + 'learn,
+    {
+        self.learner_cb = Some(Box::new(Box::new(cb)));
+        let cb_ptr = self.learner_cb.as_mut().unwrap().as_mut() as *const _ as *const c_void;
+        unsafe {
+            ffi::ccadical_set_learn(
+                self.handle,
+                cb_ptr,
+                max_len.try_into().unwrap(),
+                Some(ffi::ccadical_learn_cb),
+            )
+        }
+    }
+
+    fn detach_learner(&mut self) {
+        self.terminate_cb = None;
+        unsafe { ffi::ccadical_set_learn(self.handle, std::ptr::null(), 0, None) }
+    }
+}
+
+impl Interrupt for CaDiCaL<'_, '_> {
+    type Interrupter = Interrupter;
+    fn interrupter(&mut self) -> Self::Interrupter {
+        Interrupter {
+            handle: self.handle,
+        }
+    }
+}
+
+/// An Interrupter for the CaDiCaL solver
+pub struct Interrupter {
+    /// The C API handle
+    handle: *mut CaDiCaLHandle,
+}
+
+unsafe impl Send for Interrupter {}
+unsafe impl Sync for Interrupter {}
+
+impl InterruptSolver for Interrupter {
+    fn interrupt(&mut self) {
+        unsafe { ffi::ccadical_terminate(self.handle) }
+    }
+}
+
+impl PhaseLit for CaDiCaL<'_, '_> {
+    /// Forces the default decision phase of a variable to a certain value
+    fn phase_lit(&mut self, lit: Lit) -> Result<(), SolverError> {
+        unsafe { ffi::ccadical_phase(self.handle, lit.to_ipasir()) };
+        Ok(())
+    }
+
+    /// Undoes the effect of a call to [`CaDiCaL::phase_lit`]
+    fn unphase_var(&mut self, var: Var) -> Result<(), SolverError> {
+        unsafe { ffi::ccadical_unphase(self.handle, var.to_ipasir()) };
+        Ok(())
+    }
+}
+
+// >= v1.5.4
+#[cfg(any(
+    feature = "v1-5-4",
+    feature = "v1-5-5",
+    feature = "v1-5-6",
+    feature = "v1-6-0",
+    feature = "v1-7-0",
+    all(
+        not(feature = "v1-5-3"),
+        not(feature = "v1-5-2"),
+        not(feature = "v1-5-1"),
+        not(feature = "v1-5-0")
+    )
+))]
+impl rustsat::solvers::FlipLit for CaDiCaL<'_, '_> {
+    fn flip_lit(&mut self, lit: Lit) -> Result<bool, SolverError> {
+        Ok(unsafe { ffi::ccadical_flip(self.handle, lit.to_ipasir()) })
+    }
+
+    fn is_flippable(&mut self, lit: Lit) -> Result<bool, SolverError> {
+        Ok(unsafe { ffi::ccadical_flippable(self.handle, lit.to_ipasir()) })
+    }
+}
+
+impl LimitConflicts for CaDiCaL<'_, '_> {
+    fn limit_conflicts(&mut self, limit: Option<u32>) -> Result<(), SolverError> {
+        self.set_limit(Limit::Conflicts(if let Some(limit) = limit {
+            limit as c_int
+        } else {
+            -1
+        }))
+    }
+}
+
+impl LimitDecisions for CaDiCaL<'_, '_> {
+    fn limit_decisions(&mut self, limit: Option<u32>) -> Result<(), SolverError> {
+        self.set_limit(Limit::Decisions(if let Some(limit) = limit {
+            limit as c_int
+        } else {
+            -1
+        }))
+    }
+}
+
+impl GetInternalStats for CaDiCaL<'_, '_> {
+    fn propagations(&self) -> usize {
+        unsafe { ffi::ccadical_propagations(self.handle) }
+            .try_into()
+            .unwrap()
+    }
+
+    fn decisions(&self) -> usize {
+        unsafe { ffi::ccadical_decisions(self.handle) }
+            .try_into()
+            .unwrap()
+    }
+
+    fn conflicts(&self) -> usize {
+        unsafe { ffi::ccadical_conflicts(self.handle) }
+            .try_into()
+            .unwrap()
+    }
+}
+
+impl SolveStats for CaDiCaL<'_, '_> {
+    fn stats(&self) -> SolverStats {
+        let max_var_idx = unsafe { ffi::ccadical_vars(self.handle) };
+        let max_var = if max_var_idx > 0 {
+            Some(Var::new((max_var_idx - 1) as usize))
+        } else {
+            None
+        };
+        let mut stats = self.stats.clone();
+        stats.max_var = max_var;
+        stats
+    }
+
+    fn max_var(&self) -> Option<Var> {
+        let max_var_idx = unsafe { ffi::ccadical_vars(self.handle) };
+        if max_var_idx > 0 {
+            Some(Var::new((max_var_idx - 1) as usize))
+        } else {
+            None
+        }
+    }
+}
+
+impl Drop for CaDiCaL<'_, '_> {
+    fn drop(&mut self) {
+        unsafe { ffi::ccadical_release(self.handle) }
+    }
+}
+
+/// Possible CaDiCaL configurations
+#[derive(Debug, Clone, Copy, PartialEq, Eq)]
+pub enum Config {
+    /// Set default advanced internal options
+    Default,
+    /// Disable all internal preprocessing options
+    Plain,
+    /// Set internal options to target satisfiable instances
+    SAT,
+    /// Set internal options to target unsatisfiable instances
+    UNSAT,
+}
+
+impl fmt::Display for Config {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        match self {
+            Config::Default => write!(f, "default"),
+            Config::Plain => write!(f, "plain"),
+            Config::SAT => write!(f, "sat"),
+            Config::UNSAT => write!(f, "unsat"),
+        }
+    }
+}
+
+/// Possible CaDiCaL limits
+#[derive(Debug)]
+pub enum Limit {
+    /// The number of calls to [`CaDiCaL::terminate`] before CaDiCaL terminates
+    Terminate(c_int),
+    /// A limit on the number of conflicts
+    Conflicts(c_int),
+    /// A limit on the number of decisions
+    Decisions(c_int),
+    /// A limit on the rounds of internal preprocessing
+    Preprocessing(c_int),
+    /// A limit on the internal local search
+    LocalSearch(c_int),
+}
+
+impl fmt::Display for Limit {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        match self {
+            Limit::Terminate(val) => write!(f, "terminate ({})", val),
+            Limit::Conflicts(val) => write!(f, "conflicts ({})", val),
+            Limit::Decisions(val) => write!(f, "decisions ({})", val),
+            Limit::Preprocessing(val) => write!(f, "preprocessing ({})", val),
+            Limit::LocalSearch(val) => write!(f, "localsearch ({})", val),
+        }
+    }
+}
+
+#[cfg(test)]
+mod test {
+    use super::{CaDiCaL, Config, Limit};
+    use rustsat::{
+        lit,
+        solvers::{ControlSignal, Learn, Solve, SolverError, SolverResult, SolverState, Terminate},
+        types::{Lit, TernaryVal},
+    };
+
+    #[test]
+    fn build_destroy() {
+        let _solver = CaDiCaL::default();
+    }
+
+    #[test]
+    fn build_two() {
+        let _solver1 = CaDiCaL::default();
+        let _solver2 = CaDiCaL::default();
+    }
+
+    #[test]
+    fn tiny_instance_sat() {
+        let mut solver = CaDiCaL::default();
+        solver.add_binary(lit![0], !lit![1]).unwrap();
+        solver.add_binary(lit![1], !lit![2]).unwrap();
+        let ret = solver.solve();
+        match ret {
+            Err(e) => panic!("got error when solving: {}", e),
+            Ok(res) => assert_eq!(res, SolverResult::Sat),
+        }
+    }
+
+    #[test]
+    fn tiny_instance_unsat() {
+        let mut solver = CaDiCaL::default();
+        solver.add_unit(!lit![0]).unwrap();
+        solver.add_binary(lit![0], !lit![1]).unwrap();
+        solver.add_binary(lit![1], !lit![2]).unwrap();
+        solver.add_unit(lit![2]).unwrap();
+        let ret = solver.solve();
+        match ret {
+            Err(e) => panic!("got error when solving: {}", e),
+            Ok(res) => assert_eq!(res, SolverResult::Unsat),
+        }
+    }
+
+    #[test]
+    fn termination_callback() {
+        let mut solver = CaDiCaL::default();
+        solver.add_binary(lit![0], !lit![1]).unwrap();
+        solver.add_binary(lit![1], !lit![2]).unwrap();
+        solver.add_binary(lit![2], !lit![3]).unwrap();
+        solver.add_binary(lit![3], !lit![4]).unwrap();
+        solver.add_binary(lit![4], !lit![5]).unwrap();
+        solver.add_binary(lit![5], !lit![6]).unwrap();
+        solver.add_binary(lit![6], !lit![7]).unwrap();
+        solver.add_binary(lit![7], !lit![8]).unwrap();
+        solver.add_binary(lit![8], !lit![9]).unwrap();
+
+        solver.attach_terminator(|| ControlSignal::Terminate);
+
+        let ret = solver.solve();
+
+        match ret {
+            Err(e) => panic!("got error when solving: {}", e),
+            Ok(res) => assert_eq!(res, SolverResult::Interrupted),
+        }
+
+        // Note: since IPASIR doesn't specify _when_ the terminator callback needs
+        // to be called, there is no guarantee that the callback is actually
+        // called during solving. This might cause this test to fail with some solvers.
+    }
+
+    #[test]
+    fn learner_callback() {
+        let mut solver = CaDiCaL::default();
+        solver.add_binary(lit![0], !lit![1]).unwrap();
+        solver.add_binary(lit![1], !lit![2]).unwrap();
+        solver.add_binary(lit![2], !lit![3]).unwrap();
+        solver.add_binary(lit![3], !lit![4]).unwrap();
+        solver.add_binary(lit![4], !lit![5]).unwrap();
+        solver.add_binary(lit![5], !lit![6]).unwrap();
+        solver.add_binary(lit![6], !lit![7]).unwrap();
+        solver.add_binary(lit![7], !lit![8]).unwrap();
+        solver.add_binary(lit![8], !lit![9]).unwrap();
+        solver.add_unit(lit![9]).unwrap();
+        solver.add_unit(!lit![0]).unwrap();
+
+        let mut cl_len = 0;
+        let ret;
+
+        solver.attach_learner(
+            |clause| {
+                cl_len = clause.len();
+            },
+            10,
+        );
+
+        ret = solver.solve();
+
+        drop(solver);
+
+        // Note: it is hard to create a testing instance on which clause learning
+        // actually happens and therefore it is not actually tested if the
+        // callback is called
+
+        match ret {
+            Err(e) => panic!("got error when solving: {}", e),
+            Ok(res) => assert_eq!(res, SolverResult::Unsat),
+        }
+    }
+
+    #[test]
+    fn configure() {
+        let mut solver = CaDiCaL::default();
+        solver.set_configuration(Config::Default).unwrap();
+        solver.set_configuration(Config::Plain).unwrap();
+        solver.set_configuration(Config::SAT).unwrap();
+        solver.set_configuration(Config::UNSAT).unwrap();
+        solver.add_unit(lit![0]).unwrap();
+        assert_eq!(
+            solver.set_configuration(Config::Default),
+            Err(SolverError::State(
+                SolverState::Input,
+                SolverState::Configuring
+            ))
+        );
+    }
+
+    #[test]
+    fn options() {
+        let mut solver = CaDiCaL::default();
+        assert_eq!(solver.get_option("arena").unwrap(), 1);
+        solver.set_option("arena", 0).unwrap();
+        assert_eq!(solver.get_option("arena").unwrap(), 0);
+    }
+
+    #[test]
+    fn limit() {
+        let mut solver = CaDiCaL::default();
+        solver.set_limit(Limit::Conflicts(100)).unwrap();
+    }
+
+    #[test]
+    fn backend_stats() {
+        let mut solver = CaDiCaL::default();
+        solver.add_binary(lit![0], !lit![1]).unwrap();
+        solver.add_binary(lit![1], !lit![2]).unwrap();
+        solver.add_binary(lit![2], !lit![3]).unwrap();
+        solver.add_binary(lit![3], !lit![4]).unwrap();
+        solver.add_binary(lit![4], !lit![5]).unwrap();
+        solver.add_binary(lit![5], !lit![6]).unwrap();
+        solver.add_binary(lit![6], !lit![7]).unwrap();
+        solver.add_binary(lit![7], !lit![8]).unwrap();
+        solver.add_binary(lit![8], !lit![9]).unwrap();
+
+        assert_eq!(solver.get_active(), 10);
+        assert_eq!(solver.get_irredundant(), 9);
+        assert_eq!(solver.get_redundant(), 0);
+        assert_eq!(solver.current_lit_val(lit![0]), TernaryVal::DontCare);
+    }
+
+    #[test]
+    fn freezing() {
+        let mut solver = CaDiCaL::default();
+        solver.add_binary(lit![0], !lit![1]).unwrap();
+
+        solver.freeze_lit(lit![0]);
+
+        assert_eq!(solver.is_frozen(lit![0]), true);
+
+        solver.melt_lit(lit![0]);
+
+        assert_eq!(solver.is_frozen(lit![0]), false);
+    }
+}
+
+mod ffi {
+    use core::ffi::{c_char, c_int, c_void};
+    use rustsat::{solvers::ControlSignal, types::Lit};
+    use std::slice;
+
+    use super::{LearnCallbackPtr, TermCallbackPtr};
+
+    #[repr(C)]
+    pub struct CaDiCaLHandle {
+        _private: [u8; 0],
+    }
+
+    extern "C" {
+        // Redefinitions of CaDiCaL C API
+        pub fn ccadical_signature() -> *const c_char;
+        pub fn ccadical_init() -> *mut CaDiCaLHandle;
+        pub fn ccadical_release(solver: *mut CaDiCaLHandle);
+        pub fn ccadical_add(solver: *mut CaDiCaLHandle, lit_or_zero: c_int);
+        pub fn ccadical_assume(solver: *mut CaDiCaLHandle, lit: c_int);
+        pub fn ccadical_solve(solver: *mut CaDiCaLHandle) -> c_int;
+        pub fn ccadical_val(solver: *mut CaDiCaLHandle, lit: c_int) -> c_int;
+        pub fn ccadical_failed(solver: *mut CaDiCaLHandle, lit: c_int) -> c_int;
+        pub fn ccadical_set_terminate(
+            solver: *mut CaDiCaLHandle,
+            state: *const c_void,
+            terminate: Option<extern "C" fn(state: *const c_void) -> c_int>,
+        );
+        pub fn ccadical_set_learn(
+            solver: *mut CaDiCaLHandle,
+            state: *const c_void,
+            max_length: c_int,
+            learn: Option<extern "C" fn(state: *const c_void, clause: *const c_int)>,
+        );
+        pub fn ccadical_constrain(solver: *mut CaDiCaLHandle, lit: c_int);
+        pub fn ccadical_constraint_failed(solver: *mut CaDiCaLHandle) -> c_int;
+        pub fn ccadical_set_option_ret(
+            solver: *mut CaDiCaLHandle,
+            name: *const c_char,
+            val: c_int,
+        ) -> bool;
+        pub fn ccadical_get_option(solver: *mut CaDiCaLHandle, name: *const c_char) -> c_int;
+        pub fn ccadical_limit_ret(
+            solver: *mut CaDiCaLHandle,
+            name: *const c_char,
+            limit: c_int,
+        ) -> bool;
+        pub fn ccadical_print_statistics(solver: *mut CaDiCaLHandle);
+        pub fn ccadical_active(solver: *mut CaDiCaLHandle) -> i64;
+        pub fn ccadical_irredundant(solver: *mut CaDiCaLHandle) -> i64;
+        pub fn ccadical_redundant(solver: *mut CaDiCaLHandle) -> i64;
+        pub fn ccadical_fixed(solver: *mut CaDiCaLHandle, lit: c_int) -> c_int;
+        pub fn ccadical_terminate(solver: *mut CaDiCaLHandle);
+        pub fn ccadical_freeze(solver: *mut CaDiCaLHandle, lit: c_int);
+        pub fn ccadical_frozen(solver: *mut CaDiCaLHandle, lit: c_int) -> c_int;
+        pub fn ccadical_melt(solver: *mut CaDiCaLHandle, lit: c_int);
+        pub fn ccadical_simplify_rounds(solver: *mut CaDiCaLHandle, rounds: c_int) -> c_int;
+        pub fn ccadical_configure(solver: *mut CaDiCaLHandle, name: *const c_char) -> bool;
+        pub fn ccadical_phase(solver: *mut CaDiCaLHandle, lit: c_int);
+        pub fn ccadical_unphase(solver: *mut CaDiCaLHandle, lit: c_int);
+        pub fn ccadical_vars(solver: *mut CaDiCaLHandle) -> c_int;
+        pub fn ccadical_reserve(solver: *mut CaDiCaLHandle, min_max_var: c_int);
+        pub fn ccadical_propagations(solver: *mut CaDiCaLHandle) -> i64;
+        pub fn ccadical_decisions(solver: *mut CaDiCaLHandle) -> i64;
+        pub fn ccadical_conflicts(solver: *mut CaDiCaLHandle) -> i64;
+    }
+
+    // >= v1.5.4
+    #[cfg(any(
+        feature = "v1-5-4",
+        feature = "v1-5-5",
+        feature = "v1-5-6",
+        feature = "v1-6-0",
+        feature = "v1-7-0",
+        all(
+            not(feature = "v1-5-3"),
+            not(feature = "v1-5-2"),
+            not(feature = "v1-5-1"),
+            not(feature = "v1-5-0")
+        )
+    ))]
+    extern "C" {
+        pub fn ccadical_flip(solver: *mut CaDiCaLHandle, lit: c_int) -> bool;
+        pub fn ccadical_flippable(solver: *mut CaDiCaLHandle, lit: c_int) -> bool;
+    }
+
+    // Raw callbacks forwarding to user callbacks
+    pub extern "C" fn ccadical_terminate_cb(ptr: *const c_void) -> c_int {
+        let cb = unsafe { &mut *(ptr as *mut TermCallbackPtr<'_>) };
+        match cb() {
+            ControlSignal::Continue => 0,
+            ControlSignal::Terminate => 1,
+        }
+    }
+
+    pub extern "C" fn ccadical_learn_cb(ptr: *const c_void, clause: *const c_int) {
+        let cb = unsafe { &mut *(ptr as *mut LearnCallbackPtr<'_>) };
+
+        let mut cnt = 0;
+        for n in 0.. {
+            if unsafe { *clause.offset(n) } != 0 {
+                cnt += 1;
+            }
+        }
+        let int_slice = unsafe { slice::from_raw_parts(clause, cnt) };
+        let clause = int_slice
+            .iter()
+            .map(|il| {
+                Lit::from_ipasir(*il).expect("Invalid literal in learned clause from CaDiCaL")
+            })
+            .collect();
+        cb(clause)
+    }
+}
diff --git a/glucose/.gitignore b/glucose/.gitignore
new file mode 100644
index 00000000..4fffb2f8
--- /dev/null
+++ b/glucose/.gitignore
@@ -0,0 +1,2 @@
+/target
+/Cargo.lock
diff --git a/glucose/Cargo.toml b/glucose/Cargo.toml
new file mode 100644
index 00000000..4e94145e
--- /dev/null
+++ b/glucose/Cargo.toml
@@ -0,0 +1,27 @@
+[package]
+name = "rustsat-glucose"
+version = "0.1.0"
+edition = "2021"
+authors = ["Christoph Jabs <christoph.jabs@helsinki.fi>"]
+license = "MIT"
+description = "Interface to the SAT solver Glucose for the RustSAT library."
+keywords = ["sat solver", "rustsat"]
+readme = "README.md"
+
+build = "build.rs"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[features]
+glucose4-1 = []
+
+[dependencies]
+cpu-time = "1.0.0"
+rustsat = { version = ">= 0.2.0", path = "../rustsat", default-features = false }
+
+[build-dependencies]
+cc = { version = "1.0.79", features = ["parallel"] }
+git2 = "0.17.1"
+glob = "0.3.1"
+chrono = "0.4.24"
+cmake = "0.1.50"
diff --git a/glucose/README.md b/glucose/README.md
new file mode 100644
index 00000000..da9d7a18
--- /dev/null
+++ b/glucose/README.md
@@ -0,0 +1,8 @@
+# rustsat-glucose - Interface to the Glucose SAT Solver for RustSAT
+
+The Glucose SAT solver be used with the [RustSAT](https://github.com/chrjabs/rustsat) library.
+
+## Glucose Version
+
+The version of Glucose in this crate is Version 4.2.1.
+The used C++ source repository can be found [here](https://github.com/chrjabs/glucose4).
\ No newline at end of file
diff --git a/glucose/build.rs b/glucose/build.rs
new file mode 100644
index 00000000..567afbf7
--- /dev/null
+++ b/glucose/build.rs
@@ -0,0 +1,94 @@
+use std::{env, fs, path::Path, str};
+
+fn main() {
+    // Build C++ library
+    // Full commit hash needs to be provided
+    build(
+        "https://github.com/chrjabs/glucose4.git",
+        "main",
+        "e06dbf6d9b17b68794767617cf453b31e72a3226",
+    );
+
+    let out_dir = env::var("OUT_DIR").unwrap();
+
+    // Built solver is in out_dir
+    println!("cargo:rustc-link-search={}", out_dir);
+    println!("cargo:rustc-link-search={}/lib", out_dir);
+}
+
+fn build(repo: &str, branch: &str, commit: &str) {
+    let out_dir = env::var("OUT_DIR").unwrap();
+    let mut glucose_dir_str = out_dir.clone();
+    glucose_dir_str.push_str("/glucose");
+    let glucose_dir = Path::new(&glucose_dir_str);
+    if update_repo(glucose_dir, repo, branch, commit)
+        || !Path::new(&out_dir)
+            .join("lib")
+            .join("libglucose4.a")
+            .exists()
+    {
+        cmake::build(glucose_dir);
+    };
+
+    println!("cargo:rustc-link-lib=static=glucose4");
+
+    #[cfg(target_os = "macos")]
+    println!("cargo:rustc-flags=-l dylib=c++");
+
+    #[cfg(not(target_os = "macos"))]
+    println!("cargo:rustc-flags=-l dylib=stdc++");
+}
+
+/// Returns true if there were changes, false if not
+fn update_repo(path: &Path, url: &str, branch: &str, commit: &str) -> bool {
+    let mut changed = false;
+    let target_oid = git2::Oid::from_str(commit)
+        .unwrap_or_else(|e| panic!("Invalid commit hash {}: {}", commit, e));
+    let repo = match git2::Repository::open(path) {
+        Ok(repo) => {
+            // Check if already at correct commit
+            if let Some(oid) = repo.head().unwrap().target_peel() {
+                if oid == target_oid {
+                    return changed;
+                }
+            };
+            // Check if commit needs to be fetched
+            if repo.find_commit(target_oid).is_err() {
+                // Fetch repo
+                let mut remote = repo.find_remote("origin").unwrap_or_else(|e| {
+                    panic!("Expected remote \"origin\" in git repo {:?}: {}", path, e)
+                });
+                remote.fetch(&[branch], None, None).unwrap_or_else(|e| {
+                    panic!(
+                        "Could not fetch \"origin/{}\" for git repo {:?}: {}",
+                        branch, path, e
+                    )
+                });
+                drop(remote);
+            }
+            repo
+        }
+        Err(_) => {
+            if path.exists() {
+                fs::remove_dir_all(path).unwrap_or_else(|e| {
+                    panic!(
+                        "Could not delete directory {}: {}",
+                        path.to_str().unwrap(),
+                        e
+                    )
+                });
+            };
+            changed = true;
+            git2::Repository::clone(url, path)
+                .unwrap_or_else(|e| panic!("Could not clone repository {}: {}", url, e))
+        }
+    };
+    let target_commit = repo
+        .find_commit(target_oid)
+        .unwrap_or_else(|e| panic!("Could not find commit {}: {}", commit, e));
+    repo.checkout_tree(target_commit.as_object(), None)
+        .unwrap_or_else(|e| panic!("Could not checkout commit {}: {}", commit, e));
+    repo.set_head_detached(target_oid)
+        .unwrap_or_else(|e| panic!("Could not detach head at {}: {}", commit, e));
+    changed
+}
diff --git a/glucose/data b/glucose/data
new file mode 120000
index 00000000..4909e06e
--- /dev/null
+++ b/glucose/data
@@ -0,0 +1,1 @@
+../data
\ No newline at end of file
diff --git a/glucose/src/core.rs b/glucose/src/core.rs
new file mode 100644
index 00000000..afc4a630
--- /dev/null
+++ b/glucose/src/core.rs
@@ -0,0 +1,405 @@
+//! # Glucose Solver Interface Without Preprocessing (Core)
+//!
+//! Interface to the [Glucose](https://www.labri.fr/perso/lsimon/research/glucose/#glucose-4.2.1)
+//! incremental SAT solver.
+
+use core::ffi::{c_int, CStr};
+
+use super::{InternalSolverState, Limit};
+use cpu_time::ProcessTime;
+use ffi::Glucose4Handle;
+use rustsat::{
+    solvers::{
+        GetInternalStats, Interrupt, InterruptSolver, LimitConflicts, LimitPropagations, PhaseLit,
+        Solve, SolveIncremental, SolveMightFail, SolveStats, SolverError, SolverResult,
+        SolverState, SolverStats,
+    },
+    types::{Clause, Lit, TernaryVal, Var},
+};
+
+/// The Glucose 4 solver type without preprocessing
+pub struct Glucose {
+    handle: *mut Glucose4Handle,
+    state: InternalSolverState,
+    stats: SolverStats,
+}
+
+impl Default for Glucose {
+    fn default() -> Self {
+        Self {
+            handle: unsafe { ffi::cglucose4_init() },
+            state: Default::default(),
+            stats: Default::default(),
+        }
+    }
+}
+
+impl Glucose {
+    fn get_core_assumps(&self, assumps: &Vec<Lit>) -> Result<Vec<Lit>, SolverError> {
+        let mut core = Vec::new();
+        core.reserve(assumps.len());
+        for a in assumps {
+            match unsafe { ffi::cglucose4_failed(self.handle, a.to_ipasir()) } {
+                0 => (),
+                1 => core.push(!*a),
+                invalid => {
+                    return Err(SolverError::Api(format!(
+                        "cglucose4_failed returned invalid value: {}",
+                        invalid
+                    )))
+                }
+            }
+        }
+        Ok(core)
+    }
+
+    /// Sets an internal limit for Glucose
+    pub fn set_limit(&mut self, limit: Limit) {
+        match limit {
+            Limit::None => unsafe { ffi::cglucose4_set_no_limit(self.handle) },
+            Limit::Conflicts(limit) => unsafe { ffi::cglucose4_set_conf_limit(self.handle, limit) },
+            Limit::Propagations(limit) => unsafe {
+                ffi::cglucose4_set_prop_limit(self.handle, limit)
+            },
+        };
+    }
+
+    /// Gets the current number of assigned literals
+    pub fn n_assigns(&self) -> c_int {
+        unsafe { ffi::cglucose4_n_assigns(self.handle) }
+    }
+
+    /// Gets the current number of learnt clauses
+    pub fn n_learnts(&self) -> c_int {
+        unsafe { ffi::cglucose4_n_learnts(self.handle) }
+    }
+}
+
+impl Solve for Glucose {
+    fn signature(&self) -> &'static str {
+        let c_chars = unsafe { ffi::cglucose4_signature() };
+        let c_str = unsafe { CStr::from_ptr(c_chars) };
+        c_str
+            .to_str()
+            .expect("Glucose 4 signature returned invalid UTF-8.")
+    }
+
+    fn solve(&mut self) -> Result<SolverResult, SolverError> {
+        // If already solved, return state
+        if let InternalSolverState::Sat = self.state {
+            return Ok(SolverResult::Sat);
+        } else if let InternalSolverState::Unsat(core) = &self.state {
+            if core.is_empty() {
+                return Ok(SolverResult::Unsat);
+            }
+        }
+        let start = ProcessTime::now();
+        // Solve with glucose backend
+        let res = unsafe { ffi::cglucose4_solve(self.handle) };
+        self.stats.cpu_solve_time += start.elapsed();
+        match res {
+            0 => {
+                self.stats.n_terminated += 1;
+                self.state = InternalSolverState::Input;
+                Ok(SolverResult::Interrupted)
+            }
+            10 => {
+                self.stats.n_sat += 1;
+                self.state = InternalSolverState::Sat;
+                Ok(SolverResult::Sat)
+            }
+            20 => {
+                self.stats.n_unsat += 1;
+                self.state = InternalSolverState::Unsat(vec![]);
+                Ok(SolverResult::Unsat)
+            }
+            invalid => Err(SolverError::Api(format!(
+                "cglucose4_solve returned invalid value: {}",
+                invalid
+            ))),
+        }
+    }
+
+    fn lit_val(&self, lit: Lit) -> Result<TernaryVal, SolverError> {
+        match &self.state {
+            InternalSolverState::Sat => {
+                let lit = lit.to_ipasir();
+                match unsafe { ffi::cglucose4_val(self.handle, lit) } {
+                    0 => Ok(TernaryVal::DontCare),
+                    p if p == lit => Ok(TernaryVal::True),
+                    n if n == -lit => Ok(TernaryVal::False),
+                    invalid => Err(SolverError::Api(format!(
+                        "cglucose4_val returned invalid value: {}",
+                        invalid
+                    ))),
+                }
+            }
+            other => Err(SolverError::State(other.to_external(), SolverState::Sat)),
+        }
+    }
+
+    fn add_clause(&mut self, clause: Clause) -> SolveMightFail {
+        // Update wrapper-internal state
+        self.stats.n_clauses += 1;
+        self.stats.avg_clause_len =
+            (self.stats.avg_clause_len * ((self.stats.n_clauses - 1) as f32) + clause.len() as f32)
+                / self.stats.n_clauses as f32;
+        self.state = InternalSolverState::Input;
+        // Call glucose backend
+        clause.into_iter().for_each(|l| unsafe {
+            ffi::cglucose4_add(self.handle, l.to_ipasir());
+        });
+        unsafe { ffi::cglucose4_add(self.handle, 0) };
+        Ok(())
+    }
+}
+
+impl SolveIncremental for Glucose {
+    fn solve_assumps(&mut self, assumps: Vec<Lit>) -> Result<SolverResult, SolverError> {
+        let start = ProcessTime::now();
+        // Solve with glucose backend
+        for a in &assumps {
+            unsafe { ffi::cglucose4_assume(self.handle, a.to_ipasir()) }
+        }
+        let res = unsafe { ffi::cglucose4_solve(self.handle) };
+        self.stats.cpu_solve_time += start.elapsed();
+        match res {
+            0 => {
+                self.stats.n_terminated += 1;
+                self.state = InternalSolverState::Input;
+                Ok(SolverResult::Interrupted)
+            }
+            10 => {
+                self.stats.n_sat += 1;
+                self.state = InternalSolverState::Sat;
+                Ok(SolverResult::Sat)
+            }
+            20 => {
+                self.stats.n_unsat += 1;
+                self.state = InternalSolverState::Unsat(self.get_core_assumps(&assumps)?);
+                Ok(SolverResult::Unsat)
+            }
+            invalid => Err(SolverError::Api(format!(
+                "cglucose4_solve returned invalid value: {}",
+                invalid
+            ))),
+        }
+    }
+
+    fn core(&mut self) -> Result<Vec<Lit>, SolverError> {
+        match &self.state {
+            InternalSolverState::Unsat(core) => Ok(core.clone()),
+            other => Err(SolverError::State(other.to_external(), SolverState::Unsat)),
+        }
+    }
+}
+
+impl Interrupt for Glucose {
+    type Interrupter = Interrupter;
+    fn interrupter(&mut self) -> Self::Interrupter {
+        Interrupter {
+            handle: self.handle,
+        }
+    }
+}
+
+/// An Interrupter for the Glucose 4 Core solver
+pub struct Interrupter {
+    /// The C API handle
+    handle: *mut Glucose4Handle,
+}
+
+unsafe impl Send for Interrupter {}
+unsafe impl Sync for Interrupter {}
+
+impl InterruptSolver for Interrupter {
+    fn interrupt(&mut self) {
+        unsafe { ffi::cglucose4_interrupt(self.handle) }
+    }
+}
+
+impl PhaseLit for Glucose {
+    /// Forces the default decision phase of a variable to a certain value
+    fn phase_lit(&mut self, lit: Lit) -> Result<(), SolverError> {
+        unsafe { ffi::cglucose4_phase(self.handle, lit.to_ipasir()) };
+        Ok(())
+    }
+
+    /// Undoes the effect of a call to [`CaDiCaL::phase_lit`]
+    fn unphase_var(&mut self, var: Var) -> Result<(), SolverError> {
+        unsafe { ffi::cglucose4_unphase(self.handle, var.to_ipasir()) };
+        Ok(())
+    }
+}
+
+impl LimitConflicts for Glucose {
+    fn limit_conflicts(&mut self, limit: Option<u32>) -> Result<(), SolverError> {
+        self.set_limit(Limit::Conflicts(if let Some(limit) = limit {
+            limit as i64
+        } else {
+            -1
+        }));
+        Ok(())
+    }
+}
+
+impl LimitPropagations for Glucose {
+    fn limit_propagations(&mut self, limit: Option<u32>) -> Result<(), SolverError> {
+        self.set_limit(Limit::Propagations(if let Some(limit) = limit {
+            limit as i64
+        } else {
+            -1
+        }));
+        Ok(())
+    }
+}
+
+impl GetInternalStats for Glucose {
+    fn propagations(&self) -> usize {
+        unsafe { ffi::cglucose4_propagations(self.handle) }
+            .try_into()
+            .unwrap()
+    }
+
+    fn decisions(&self) -> usize {
+        unsafe { ffi::cglucose4_decisions(self.handle) }
+            .try_into()
+            .unwrap()
+    }
+
+    fn conflicts(&self) -> usize {
+        unsafe { ffi::cglucose4_conflicts(self.handle) }
+            .try_into()
+            .unwrap()
+    }
+}
+
+impl SolveStats for Glucose {
+    fn stats(&self) -> SolverStats {
+        let mut stats = self.stats.clone();
+        stats.max_var = self.max_var();
+        stats.n_clauses = self.n_clauses();
+        stats
+    }
+
+    fn max_var(&self) -> Option<Var> {
+        let max_var_idx = unsafe { ffi::cglucose4_n_vars(self.handle) };
+        if max_var_idx > 0 {
+            Some(Var::new((max_var_idx - 1) as usize))
+        } else {
+            None
+        }
+    }
+
+    fn n_clauses(&self) -> usize {
+        unsafe { ffi::cglucose4_n_clauses(self.handle) }
+            .try_into()
+            .unwrap()
+    }
+}
+
+impl Drop for Glucose {
+    fn drop(&mut self) {
+        unsafe { ffi::cglucose4_release(self.handle) }
+    }
+}
+
+#[cfg(test)]
+mod test {
+    use super::Glucose;
+    use rustsat::{
+        lit,
+        solvers::{Solve, SolveStats, SolverResult},
+        types::{Lit, Var},
+        var,
+    };
+
+    #[test]
+    fn build_destroy() {
+        let _solver = Glucose::default();
+    }
+
+    #[test]
+    fn build_two() {
+        let _solver1 = Glucose::default();
+        let _solver2 = Glucose::default();
+    }
+
+    #[test]
+    fn tiny_instance_sat() {
+        let mut solver = Glucose::default();
+        solver.add_binary(lit![0], !lit![1]).unwrap();
+        solver.add_binary(lit![1], !lit![2]).unwrap();
+        let ret = solver.solve();
+        match ret {
+            Err(e) => panic!("got error when solving: {}", e),
+            Ok(res) => assert_eq!(res, SolverResult::Sat),
+        }
+    }
+
+    #[test]
+    fn tiny_instance_unsat() {
+        let mut solver = Glucose::default();
+        solver.add_unit(!lit![0]).unwrap();
+        solver.add_binary(lit![0], !lit![1]).unwrap();
+        solver.add_binary(lit![1], !lit![2]).unwrap();
+        solver.add_unit(lit![2]).unwrap();
+        let ret = solver.solve();
+        match ret {
+            Err(e) => panic!("got error when solving: {}", e),
+            Ok(res) => assert_eq!(res, SolverResult::Unsat),
+        }
+    }
+
+    #[test]
+    fn backend_stats() {
+        let mut solver = Glucose::default();
+        solver.add_binary(lit![0], !lit![1]).unwrap();
+        solver.add_binary(lit![1], !lit![2]).unwrap();
+        solver.add_binary(lit![2], !lit![3]).unwrap();
+        solver.add_binary(lit![3], !lit![4]).unwrap();
+        solver.add_binary(lit![4], !lit![5]).unwrap();
+        solver.add_binary(lit![5], !lit![6]).unwrap();
+        solver.add_binary(lit![6], !lit![7]).unwrap();
+        solver.add_binary(lit![7], !lit![8]).unwrap();
+        solver.add_binary(lit![8], !lit![9]).unwrap();
+
+        assert_eq!(solver.n_learnts(), 0);
+        assert_eq!(solver.n_clauses(), 9);
+        assert_eq!(solver.max_var(), Some(var![9]));
+    }
+}
+
+mod ffi {
+    use core::ffi::{c_char, c_int};
+
+    #[repr(C)]
+    pub struct Glucose4Handle {
+        _private: [u8; 0],
+    }
+
+    extern "C" {
+        // Redefinitions of Glucose C API
+        pub fn cglucose4_signature() -> *const c_char;
+        pub fn cglucose4_init() -> *mut Glucose4Handle;
+        pub fn cglucose4_release(solver: *mut Glucose4Handle);
+        pub fn cglucose4_add(solver: *mut Glucose4Handle, lit_or_zero: c_int);
+        pub fn cglucose4_assume(solver: *mut Glucose4Handle, lit: c_int);
+        pub fn cglucose4_solve(solver: *mut Glucose4Handle) -> c_int;
+        pub fn cglucose4_val(solver: *mut Glucose4Handle, lit: c_int) -> c_int;
+        pub fn cglucose4_failed(solver: *mut Glucose4Handle, lit: c_int) -> c_int;
+        pub fn cglucose4_phase(solver: *mut Glucose4Handle, lit: c_int);
+        pub fn cglucose4_unphase(solver: *mut Glucose4Handle, lit: c_int);
+        pub fn cglucose4_n_assigns(solver: *mut Glucose4Handle) -> c_int;
+        pub fn cglucose4_n_clauses(solver: *mut Glucose4Handle) -> c_int;
+        pub fn cglucose4_n_learnts(solver: *mut Glucose4Handle) -> c_int;
+        pub fn cglucose4_n_vars(solver: *mut Glucose4Handle) -> c_int;
+        pub fn cglucose4_set_conf_limit(solver: *mut Glucose4Handle, limit: i64);
+        pub fn cglucose4_set_prop_limit(solver: *mut Glucose4Handle, limit: i64);
+        pub fn cglucose4_set_no_limit(solver: *mut Glucose4Handle);
+        pub fn cglucose4_interrupt(solver: *mut Glucose4Handle);
+        pub fn cglucose4_propagations(solver: *mut Glucose4Handle) -> u64;
+        pub fn cglucose4_decisions(solver: *mut Glucose4Handle) -> u64;
+        pub fn cglucose4_conflicts(solver: *mut Glucose4Handle) -> u64;
+    }
+}
diff --git a/glucose/src/lib.rs b/glucose/src/lib.rs
new file mode 100644
index 00000000..8c15f054
--- /dev/null
+++ b/glucose/src/lib.rs
@@ -0,0 +1,52 @@
+//! # Glucose 4 Solver Interface
+//!
+//! Interface to the [Glucose
+//! 4](https://www.labri.fr/perso/lsimon/research/glucose/#glucose-4.2.1)
+//! incremental SAT solver.
+
+use rustsat::{solvers::SolverState, types::Lit};
+use std::fmt;
+
+pub mod core;
+pub mod simp;
+
+#[derive(Debug, PartialEq, Eq, Default)]
+enum InternalSolverState {
+    #[default]
+    Configuring,
+    Input,
+    Sat,
+    Unsat(Vec<Lit>),
+}
+
+impl InternalSolverState {
+    fn to_external(&self) -> SolverState {
+        match self {
+            InternalSolverState::Configuring => SolverState::Configuring,
+            InternalSolverState::Input => SolverState::Input,
+            InternalSolverState::Sat => SolverState::Sat,
+            InternalSolverState::Unsat(_) => SolverState::Unsat,
+        }
+    }
+}
+
+/// Possible Glucose limits
+#[derive(Debug)]
+pub enum Limit {
+    /// No limits
+    None,
+    /// A limit on the number of conflicts
+    Conflicts(i64),
+    /// A limit on the number of propagations
+    Propagations(i64),
+}
+
+impl fmt::Display for Limit {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        match self {
+            Limit::None => write!(f, "none"),
+            Limit::Conflicts(val) => write!(f, "conflicts ({})", val),
+            Limit::Propagations(val) => write!(f, "propagations ({})", val),
+        }
+    }
+}
diff --git a/glucose/src/simp.rs b/glucose/src/simp.rs
new file mode 100644
index 00000000..1003226b
--- /dev/null
+++ b/glucose/src/simp.rs
@@ -0,0 +1,424 @@
+//! # Glucose 4 Solver Interface With Preprocessing (Simp)
+//!
+//! Interface to the [Glucose](https://www.labri.fr/perso/lsimon/research/glucose/#glucose-4.2.1)
+//! incremental SAT solver.
+
+use core::ffi::{c_int, CStr};
+
+use super::{InternalSolverState, Limit};
+use cpu_time::ProcessTime;
+use ffi::Glucose4Handle;
+use rustsat::{
+    solvers::{
+        GetInternalStats, Interrupt, InterruptSolver, LimitConflicts, LimitPropagations, PhaseLit,
+        Solve, SolveIncremental, SolveMightFail, SolveStats, SolverError, SolverResult,
+        SolverState, SolverStats,
+    },
+    types::{Clause, Lit, TernaryVal, Var},
+};
+
+/// The Glucose 4 solver type with preprocessing
+pub struct Glucose {
+    handle: *mut Glucose4Handle,
+    state: InternalSolverState,
+    stats: SolverStats,
+}
+
+impl Default for Glucose {
+    fn default() -> Self {
+        Self {
+            handle: unsafe { ffi::cglucosesimp4_init() },
+            state: Default::default(),
+            stats: Default::default(),
+        }
+    }
+}
+
+impl Glucose {
+    fn get_core_assumps(&self, assumps: &Vec<Lit>) -> Result<Vec<Lit>, SolverError> {
+        let mut core = Vec::new();
+        core.reserve(assumps.len());
+        for a in assumps {
+            match unsafe { ffi::cglucosesimp4_failed(self.handle, a.to_ipasir()) } {
+                0 => (),
+                1 => core.push(!*a),
+                invalid => {
+                    return Err(SolverError::Api(format!(
+                        "cglucosesimp4_failed returned invalid value: {}",
+                        invalid
+                    )))
+                }
+            }
+        }
+        Ok(core)
+    }
+
+    /// Sets an internal limit for Glucose
+    pub fn set_limit(&mut self, limit: Limit) {
+        match limit {
+            Limit::None => unsafe { ffi::cglucosesimp4_set_no_limit(self.handle) },
+            Limit::Conflicts(limit) => unsafe {
+                ffi::cglucosesimp4_set_conf_limit(self.handle, limit)
+            },
+            Limit::Propagations(limit) => unsafe {
+                ffi::cglucosesimp4_set_prop_limit(self.handle, limit)
+            },
+        };
+    }
+
+    /// Gets the current number of assigned literals
+    pub fn n_assigns(&self) -> c_int {
+        unsafe { ffi::cglucosesimp4_n_assigns(self.handle) }
+    }
+
+    /// Gets the current number of learnt clauses
+    pub fn n_learnts(&self) -> c_int {
+        unsafe { ffi::cglucosesimp4_n_learnts(self.handle) }
+    }
+
+    /// Freezes a literal.
+    pub fn freeze_lit(&mut self, lit: Lit) {
+        unsafe { ffi::cglucosesimp4_set_frozen(self.handle, lit.var().to_ipasir(), true) }
+    }
+
+    /// Melts a literal.
+    pub fn melt_lit(&mut self, lit: Lit) {
+        unsafe { ffi::cglucosesimp4_set_frozen(self.handle, lit.var().to_ipasir(), false) }
+    }
+
+    /// Checks if a variable has been eliminated by preprocessing.
+    pub fn var_eliminated(&mut self, var: Var) {
+        unsafe { ffi::cglucosesimp4_is_eliminated(self.handle, var.to_ipasir()) }
+    }
+}
+
+impl Solve for Glucose {
+    fn signature(&self) -> &'static str {
+        let c_chars = unsafe { ffi::cglucose4_signature() };
+        let c_str = unsafe { CStr::from_ptr(c_chars) };
+        c_str
+            .to_str()
+            .expect("Glucose 4 signature returned invalid UTF-8.")
+    }
+
+    fn solve(&mut self) -> Result<SolverResult, SolverError> {
+        // If already solved, return state
+        if let InternalSolverState::Sat = self.state {
+            return Ok(SolverResult::Sat);
+        } else if let InternalSolverState::Unsat(core) = &self.state {
+            if core.is_empty() {
+                return Ok(SolverResult::Unsat);
+            }
+        }
+        let start = ProcessTime::now();
+        // Solve with glucose backend
+        let res = unsafe { ffi::cglucosesimp4_solve(self.handle) };
+        self.stats.cpu_solve_time += start.elapsed();
+        match res {
+            0 => {
+                self.stats.n_terminated += 1;
+                self.state = InternalSolverState::Input;
+                Ok(SolverResult::Interrupted)
+            }
+            10 => {
+                self.stats.n_sat += 1;
+                self.state = InternalSolverState::Sat;
+                Ok(SolverResult::Sat)
+            }
+            20 => {
+                self.stats.n_unsat += 1;
+                self.state = InternalSolverState::Unsat(vec![]);
+                Ok(SolverResult::Unsat)
+            }
+            invalid => Err(SolverError::Api(format!(
+                "cglucosesimp4_solve returned invalid value: {}",
+                invalid
+            ))),
+        }
+    }
+
+    fn lit_val(&self, lit: Lit) -> Result<TernaryVal, SolverError> {
+        match &self.state {
+            InternalSolverState::Sat => {
+                let lit = lit.to_ipasir();
+                match unsafe { ffi::cglucosesimp4_val(self.handle, lit) } {
+                    0 => Ok(TernaryVal::DontCare),
+                    p if p == lit => Ok(TernaryVal::True),
+                    n if n == -lit => Ok(TernaryVal::False),
+                    invalid => Err(SolverError::Api(format!(
+                        "cglucosesimp4_val returned invalid value: {}",
+                        invalid
+                    ))),
+                }
+            }
+            other => Err(SolverError::State(other.to_external(), SolverState::Sat)),
+        }
+    }
+
+    fn add_clause(&mut self, clause: Clause) -> SolveMightFail {
+        // Update wrapper-internal state
+        self.stats.n_clauses += 1;
+        self.stats.avg_clause_len =
+            (self.stats.avg_clause_len * ((self.stats.n_clauses - 1) as f32) + clause.len() as f32)
+                / self.stats.n_clauses as f32;
+        self.state = InternalSolverState::Input;
+        // Call glucose backend
+        clause.into_iter().for_each(|l| unsafe {
+            ffi::cglucosesimp4_add(self.handle, l.to_ipasir());
+        });
+        unsafe { ffi::cglucosesimp4_add(self.handle, 0) };
+        Ok(())
+    }
+}
+
+impl SolveIncremental for Glucose {
+    fn solve_assumps(&mut self, assumps: Vec<Lit>) -> Result<SolverResult, SolverError> {
+        let start = ProcessTime::now();
+        // Solve with glucose backend
+        for a in &assumps {
+            unsafe { ffi::cglucosesimp4_assume(self.handle, a.to_ipasir()) }
+        }
+        let res = unsafe { ffi::cglucosesimp4_solve(self.handle) };
+        self.stats.cpu_solve_time += start.elapsed();
+        match res {
+            0 => {
+                self.stats.n_terminated += 1;
+                self.state = InternalSolverState::Input;
+                Ok(SolverResult::Interrupted)
+            }
+            10 => {
+                self.stats.n_sat += 1;
+                self.state = InternalSolverState::Sat;
+                Ok(SolverResult::Sat)
+            }
+            20 => {
+                self.stats.n_unsat += 1;
+                self.state = InternalSolverState::Unsat(self.get_core_assumps(&assumps)?);
+                Ok(SolverResult::Unsat)
+            }
+            invalid => Err(SolverError::Api(format!(
+                "cglucosesimp4_solve returned invalid value: {}",
+                invalid
+            ))),
+        }
+    }
+
+    fn core(&mut self) -> Result<Vec<Lit>, SolverError> {
+        match &self.state {
+            InternalSolverState::Unsat(core) => Ok(core.clone()),
+            other => Err(SolverError::State(other.to_external(), SolverState::Unsat)),
+        }
+    }
+}
+
+impl Interrupt for Glucose {
+    type Interrupter = Interrupter;
+    fn interrupter(&mut self) -> Self::Interrupter {
+        Interrupter {
+            handle: self.handle,
+        }
+    }
+}
+
+/// An Interrupter for the Glucose 4 Simp solver
+pub struct Interrupter {
+    /// The C API handle
+    handle: *mut Glucose4Handle,
+}
+
+unsafe impl Send for Interrupter {}
+unsafe impl Sync for Interrupter {}
+
+impl InterruptSolver for Interrupter {
+    fn interrupt(&mut self) {
+        unsafe { ffi::cglucosesimp4_interrupt(self.handle) }
+    }
+}
+
+impl PhaseLit for Glucose {
+    /// Forces the default decision phase of a variable to a certain value
+    fn phase_lit(&mut self, lit: Lit) -> Result<(), SolverError> {
+        unsafe { ffi::cglucosesimp4_phase(self.handle, lit.to_ipasir()) };
+        Ok(())
+    }
+
+    /// Undoes the effect of a call to [`CaDiCaL::phase_lit`]
+    fn unphase_var(&mut self, var: Var) -> Result<(), SolverError> {
+        unsafe { ffi::cglucosesimp4_unphase(self.handle, var.to_ipasir()) };
+        Ok(())
+    }
+}
+
+impl LimitConflicts for Glucose {
+    fn limit_conflicts(&mut self, limit: Option<u32>) -> Result<(), SolverError> {
+        self.set_limit(Limit::Conflicts(if let Some(limit) = limit {
+            limit as i64
+        } else {
+            -1
+        }));
+        Ok(())
+    }
+}
+
+impl LimitPropagations for Glucose {
+    fn limit_propagations(&mut self, limit: Option<u32>) -> Result<(), SolverError> {
+        self.set_limit(Limit::Propagations(if let Some(limit) = limit {
+            limit as i64
+        } else {
+            -1
+        }));
+        Ok(())
+    }
+}
+
+impl GetInternalStats for Glucose {
+    fn propagations(&self) -> usize {
+        unsafe { ffi::cglucosesimp4_propagations(self.handle) }
+            .try_into()
+            .unwrap()
+    }
+
+    fn decisions(&self) -> usize {
+        unsafe { ffi::cglucosesimp4_decisions(self.handle) }
+            .try_into()
+            .unwrap()
+    }
+
+    fn conflicts(&self) -> usize {
+        unsafe { ffi::cglucosesimp4_conflicts(self.handle) }
+            .try_into()
+            .unwrap()
+    }
+}
+
+impl SolveStats for Glucose {
+    fn stats(&self) -> SolverStats {
+        let mut stats = self.stats.clone();
+        stats.max_var = self.max_var();
+        stats.n_clauses = self.n_clauses();
+        stats
+    }
+
+    fn max_var(&self) -> Option<Var> {
+        let max_var_idx = unsafe { ffi::cglucosesimp4_n_vars(self.handle) };
+        if max_var_idx > 0 {
+            Some(Var::new((max_var_idx - 1) as usize))
+        } else {
+            None
+        }
+    }
+
+    fn n_clauses(&self) -> usize {
+        unsafe { ffi::cglucosesimp4_n_clauses(self.handle) }
+            .try_into()
+            .unwrap()
+    }
+}
+
+impl Drop for Glucose {
+    fn drop(&mut self) {
+        unsafe { ffi::cglucosesimp4_release(self.handle) }
+    }
+}
+
+#[cfg(test)]
+mod test {
+    use super::Glucose;
+    use rustsat::{
+        lit,
+        solvers::{Solve, SolveStats, SolverResult},
+        types::{Lit, Var},
+        var,
+    };
+
+    #[test]
+    fn build_destroy() {
+        let _solver = Glucose::default();
+    }
+
+    #[test]
+    fn build_two() {
+        let _solver1 = Glucose::default();
+        let _solver2 = Glucose::default();
+    }
+
+    #[test]
+    fn tiny_instance_sat() {
+        let mut solver = Glucose::default();
+        solver.add_binary(lit![0], !lit![1]).unwrap();
+        solver.add_binary(lit![1], !lit![2]).unwrap();
+        let ret = solver.solve();
+        match ret {
+            Err(e) => panic!("got error when solving: {}", e),
+            Ok(res) => assert_eq!(res, SolverResult::Sat),
+        }
+    }
+
+    #[test]
+    fn tiny_instance_unsat() {
+        let mut solver = Glucose::default();
+        solver.add_unit(!lit![0]).unwrap();
+        solver.add_binary(lit![0], !lit![1]).unwrap();
+        solver.add_binary(lit![1], !lit![2]).unwrap();
+        solver.add_unit(lit![2]).unwrap();
+        let ret = solver.solve();
+        match ret {
+            Err(e) => panic!("got error when solving: {}", e),
+            Ok(res) => assert_eq!(res, SolverResult::Unsat),
+        }
+    }
+
+    #[test]
+    fn backend_stats() {
+        let mut solver = Glucose::default();
+        solver.add_binary(lit![0], !lit![1]).unwrap();
+        solver.add_binary(lit![1], !lit![2]).unwrap();
+        solver.add_binary(lit![2], !lit![3]).unwrap();
+        solver.add_binary(lit![3], !lit![4]).unwrap();
+        solver.add_binary(lit![4], !lit![5]).unwrap();
+        solver.add_binary(lit![5], !lit![6]).unwrap();
+        solver.add_binary(lit![6], !lit![7]).unwrap();
+        solver.add_binary(lit![7], !lit![8]).unwrap();
+        solver.add_binary(lit![8], !lit![9]).unwrap();
+
+        assert_eq!(solver.n_learnts(), 0);
+        assert_eq!(solver.n_clauses(), 9);
+        assert_eq!(solver.max_var(), Some(var![9]));
+    }
+}
+
+mod ffi {
+    use core::ffi::{c_char, c_int};
+
+    #[repr(C)]
+    pub struct Glucose4Handle {
+        _private: [u8; 0],
+    }
+
+    extern "C" {
+        // Redefinitions of Glucose C API
+        pub fn cglucose4_signature() -> *const c_char;
+        pub fn cglucosesimp4_init() -> *mut Glucose4Handle;
+        pub fn cglucosesimp4_release(solver: *mut Glucose4Handle);
+        pub fn cglucosesimp4_add(solver: *mut Glucose4Handle, lit_or_zero: c_int);
+        pub fn cglucosesimp4_assume(solver: *mut Glucose4Handle, lit: c_int);
+        pub fn cglucosesimp4_solve(solver: *mut Glucose4Handle) -> c_int;
+        pub fn cglucosesimp4_val(solver: *mut Glucose4Handle, lit: c_int) -> c_int;
+        pub fn cglucosesimp4_failed(solver: *mut Glucose4Handle, lit: c_int) -> c_int;
+        pub fn cglucosesimp4_phase(solver: *mut Glucose4Handle, lit: c_int);
+        pub fn cglucosesimp4_unphase(solver: *mut Glucose4Handle, lit: c_int);
+        pub fn cglucosesimp4_n_assigns(solver: *mut Glucose4Handle) -> c_int;
+        pub fn cglucosesimp4_n_clauses(solver: *mut Glucose4Handle) -> c_int;
+        pub fn cglucosesimp4_n_learnts(solver: *mut Glucose4Handle) -> c_int;
+        pub fn cglucosesimp4_n_vars(solver: *mut Glucose4Handle) -> c_int;
+        pub fn cglucosesimp4_set_conf_limit(solver: *mut Glucose4Handle, limit: i64);
+        pub fn cglucosesimp4_set_prop_limit(solver: *mut Glucose4Handle, limit: i64);
+        pub fn cglucosesimp4_set_no_limit(solver: *mut Glucose4Handle);
+        pub fn cglucosesimp4_interrupt(solver: *mut Glucose4Handle);
+        pub fn cglucosesimp4_set_frozen(solver: *mut Glucose4Handle, var: c_int, frozen: bool);
+        pub fn cglucosesimp4_is_eliminated(solver: *mut Glucose4Handle, var: c_int);
+        pub fn cglucosesimp4_propagations(solver: *mut Glucose4Handle) -> u64;
+        pub fn cglucosesimp4_decisions(solver: *mut Glucose4Handle) -> u64;
+        pub fn cglucosesimp4_conflicts(solver: *mut Glucose4Handle) -> u64;
+    }
+}
diff --git a/kissat/.gitignore b/kissat/.gitignore
new file mode 100644
index 00000000..a255f58c
--- /dev/null
+++ b/kissat/.gitignore
@@ -0,0 +1,3 @@
+/target
+/Cargo.lock
+*.log
diff --git a/kissat/Cargo.toml b/kissat/Cargo.toml
new file mode 100644
index 00000000..53c89a6e
--- /dev/null
+++ b/kissat/Cargo.toml
@@ -0,0 +1,30 @@
+[package]
+name = "rustsat-kissat"
+version = "0.1.0"
+edition = "2021"
+authors = ["Christoph Jabs <christoph.jabs@helsinki.fi>"]
+license = "MIT"
+description = "Interface to the SAT solver kissat for the RustSAT library."
+keywords = ["sat solver", "rustsat"]
+readme = "README.md"
+
+build = "build.rs"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[features]
+v3-1-0 = []
+v3-0-0 = []
+sc2022-light = []
+sc2022-hyper = []
+sc2022-bulky = []
+
+[dependencies]
+cpu-time = "1.0.0"
+rustsat = { version = ">= 0.2.0", path = "../rustsat", default-features = false }
+
+[build-dependencies]
+cc = { version = "1.0.79", features = ["parallel"] }
+git2 = "0.17.1"
+glob = "0.3.1"
+chrono = "0.4.24"
diff --git a/kissat/README.md b/kissat/README.md
new file mode 100644
index 00000000..615b5b26
--- /dev/null
+++ b/kissat/README.md
@@ -0,0 +1,16 @@
+# rustsat-kissat - Interface to the kissat SAT Solver for RustSAT
+
+Armin Biere's SAT solver [Kissat](https://github.com/arminbiere/kissat) be used with the [RustSAT](https://github.com/chrjabs/rustsat) library.
+
+## Kissat Versions
+
+Kissat versions can be selected via cargo crate features.
+The following Kissat versions are available:
+- `v3-1-0`: [Version 3.1.0](https://github.com/arminbiere/kissat/releases/tag/rel-3.1.0)
+- `v3-0-0`: [Version 3.0.0](https://github.com/arminbiere/kissat/releases/tag/rel-3.0.0)
+- `sc2022-light`: [SAT Competition 2022 Light](https://github.com/arminbiere/kissat/releases/tag/sc2022-light)
+- `sc2022-hyper`: [SAT Competition 2022 Hyper](https://github.com/arminbiere/kissat/releases/tag/sc2022-hyper)
+- `sc2022-bulky`: [SAT Competition 2022 Bulky](https://github.com/arminbiere/kissat/releases/tag/sc2022-bulky)
+
+Without any features selected, the newest version will be used.
+If conflicting Kissat versions are requested, the newest requested version will be selected.
\ No newline at end of file
diff --git a/kissat/build-all.sh b/kissat/build-all.sh
new file mode 100755
index 00000000..d36d40b8
--- /dev/null
+++ b/kissat/build-all.sh
@@ -0,0 +1,31 @@
+#!/usr/bin/bash
+
+echo "Building default (newest) version"
+if [ "$1" == "--clean" ]; then cargo clean -p rustsat-kissat > /dev/null; fi
+cargo build &> def-build.log
+echo "Default (newest) build returned: $?"
+
+echo "Building sc2022-bulky"
+if [ "$1" == "--clean" ]; then cargo clean -p rustsat-kissat > /dev/null; fi
+cargo build --features=sc2022-bulky &> sc2022-bulky-build.log
+echo "sc2022-bulky build returned: $?"
+
+echo "Building sc2022-hyper"
+if [ "$1" == "--clean" ]; then cargo clean -p rustsat-kissat > /dev/null; fi
+cargo build --features=sc2022-hyper &> sc2022-hyper-build.log
+echo "sc2022-hyper build returned: $?"
+
+echo "Building sc2022-light"
+if [ "$1" == "--clean" ]; then cargo clean -p rustsat-kissat > /dev/null; fi
+cargo build --features=sc2022-light &> sc2022-light-build.log
+echo "sc2022-light build returned: $?"
+
+echo "Building v3.0.0"
+if [ "$1" == "--clean" ]; then cargo clean -p rustsat-kissat > /dev/null; fi
+cargo build --features=v3-0-0 &> v300-build.log
+echo "v3.0.0 build returned: $?"
+
+echo "Building v3.1.0"
+if [ "$1" == "--clean" ]; then cargo clean -p rustsat-kissat > /dev/null; fi
+cargo build --features=v3-1-0 &> v310-build.log
+echo "v3.1.0 build returned: $?"
diff --git a/kissat/build.rs b/kissat/build.rs
new file mode 100644
index 00000000..1c0f5ea2
--- /dev/null
+++ b/kissat/build.rs
@@ -0,0 +1,183 @@
+use glob::glob;
+use std::{
+    env,
+    fs::{self, File},
+    io::Write,
+    path::Path,
+    process::Command,
+    str,
+};
+
+fn main() {
+    // Select commit based on features. If conflict, always choose newest release
+    let tag = if cfg!(feature = "v3-1-0") {
+        "refs/tags/rel-3.1.0"
+    } else if cfg!(feature = "v3-0-0") {
+        "refs/tags/rel-3.0.0"
+    } else if cfg!(feature = "sc2022-light") {
+        "refs/tags/sc2022-light"
+    } else if cfg!(feature = "sc2022-hyper") {
+        "refs/tags/sc2022-hyper"
+    } else if cfg!(feature = "sc2022-bulky") {
+        "refs/tags/sc2022-bulky"
+    } else {
+        // default to newest version
+        "refs/tags/rel-3.1.0"
+    };
+
+    // Build C library
+    // Full commit hash needs to be provided
+    build("https://github.com/arminbiere/kissat.git", "master", tag);
+
+    let out_dir = env::var("OUT_DIR").unwrap();
+
+    // Built solver is in out_dir
+    println!("cargo:rustc-link-search={}", out_dir);
+    println!("cargo:rustc-link-search={}/lib", out_dir);
+}
+
+fn build(repo: &str, branch: &str, reference: &str) {
+    let out_dir = env::var("OUT_DIR").unwrap();
+    let mut kissat_dir_str = out_dir.clone();
+    kissat_dir_str.push_str("/kissat");
+    let kissat_dir = Path::new(&kissat_dir_str);
+    if update_repo(kissat_dir, repo, branch, reference)
+        || !Path::new(&out_dir).join("libkissat.a").exists()
+    {
+        // Repo changed, rebuild
+        // We specify the build manually here instead of calling make for better portability
+        let src_files = glob(&format!("{}/src/*.c", kissat_dir_str))
+            .unwrap()
+            .filter_map(|res| {
+                if let Ok(p) = res {
+                    if let Some(name) = p.file_name() {
+                        if name == "main.c"
+                            || name == "application.c"
+                            || name == "handle.c"
+                            || name == "parse.c"
+                            || name == "witness.c"
+                        {
+                            return None; // Filter out application files
+                        }
+                    };
+                    Some(p)
+                } else {
+                    None
+                }
+            });
+        // Setup build configuration
+        let mut kissat_build = cc::Build::new();
+        if env::var("PROFILE").unwrap() == "debug" {
+            kissat_build
+                .opt_level(0)
+                .define("DEBUG", None)
+                .warnings(true)
+                .debug(true);
+        } else {
+            kissat_build
+                .opt_level(3)
+                .define("NDEBUG", None)
+                .warnings(false);
+        }
+        // Generate build header
+        let mut build_header = File::create(kissat_dir.join("src").join("build.h"))
+            .expect("Could not create kissat build header");
+        let mut kissat_version =
+            fs::read_to_string(kissat_dir.join("VERSION")).expect("Cannot read kissat version");
+        kissat_version.retain(|c| c != '\n');
+        let (compiler_desc, compiler_flags) = get_compiler_description(kissat_build.get_compiler());
+        write!(
+                build_header,
+                "#define VERSION \"{}\"\n#define COMPILER \"{} {}\"\n#define ID \"{}\"\n#define BUILD \"{}\"\n#define DIR \"{}\"",
+                kissat_version, compiler_desc, compiler_flags, reference, chrono::Utc::now(), kissat_dir.as_os_str().to_str().unwrap()
+            ).expect("Failed to write kissat build.h");
+        // Build Kissat
+        kissat_build
+            .include(kissat_dir.join("src"))
+            .warnings(false)
+            .files(src_files)
+            .compile("kissat");
+    };
+
+    println!("cargo:rustc-link-lib=static=kissat");
+}
+
+/// Returns true if there were changes, false if not
+fn update_repo(path: &Path, url: &str, branch: &str, reference: &str) -> bool {
+    let mut changed = false;
+    let repo = match git2::Repository::open(path) {
+        Ok(repo) => {
+            if repo.find_reference(reference).is_err() {
+                // Fetch repo
+                let mut remote = repo.find_remote("origin").unwrap_or_else(|e| {
+                    panic!("Expected remote \"origin\" in git repo {:?}: {}", path, e)
+                });
+                remote.fetch(&[branch], None, None).unwrap_or_else(|e| {
+                    panic!(
+                        "Could not fetch \"origin/{}\" for git repo {:?}: {}",
+                        branch, path, e
+                    )
+                });
+                drop(remote);
+                changed = true;
+            }
+            repo
+        }
+        Err(_) => {
+            if path.exists() {
+                fs::remove_dir_all(path).unwrap_or_else(|e| {
+                    panic!(
+                        "Could not delete directory {}: {}",
+                        path.to_str().unwrap(),
+                        e
+                    )
+                });
+            };
+            changed = true;
+            git2::Repository::clone(url, path)
+                .unwrap_or_else(|e| panic!("Could not clone repository {}: {}", url, e))
+        }
+    };
+    let target_commit = repo
+        .find_reference(reference)
+        .expect("could not find specified reference")
+        .peel_to_commit()
+        .expect("could not peel to commit");
+    repo.checkout_tree(
+        target_commit.as_object(),
+        Some(git2::build::CheckoutBuilder::new().force()),
+    )
+    .expect("could not checkout commit");
+    repo.set_head_detached(target_commit.id())
+        .expect("could not detach head");
+    changed
+}
+
+/// Gets a description of the C(++) compiler used and the used flags
+fn get_compiler_description(compiler: cc::Tool) -> (String, String) {
+    let compiler_command = compiler.to_command();
+    let mut first_line = true;
+    let compiler_version = match Command::new(compiler_command.get_program())
+        .arg("--version")
+        .output()
+    {
+        Ok(output) => {
+            let mut version = String::from_utf8(output.stdout).unwrap();
+            version.retain(|c| {
+                if first_line && c == '\n' {
+                    first_line = false;
+                    false
+                } else {
+                    first_line
+                }
+            });
+            version
+        }
+        Err(_) => String::from(compiler_command.get_program().to_str().unwrap()),
+    };
+    let compiler_flags = compiler.cflags_env();
+    (
+        compiler_version,
+        String::from(compiler_flags.to_str().unwrap()),
+    )
+}
diff --git a/kissat/data b/kissat/data
new file mode 120000
index 00000000..4909e06e
--- /dev/null
+++ b/kissat/data
@@ -0,0 +1,1 @@
+../data
\ No newline at end of file
diff --git a/kissat/src/lib.rs b/kissat/src/lib.rs
new file mode 100644
index 00000000..349133d1
--- /dev/null
+++ b/kissat/src/lib.rs
@@ -0,0 +1,542 @@
+//! # Kissat Solver Interface
+//!
+//! Interface to the [Kissat](https://github.com/arminbiere/kissat) incremental SAT solver.
+
+use core::ffi::{c_int, c_uint, c_void, CStr};
+use std::{ffi::CString, fmt};
+
+use cpu_time::ProcessTime;
+use ffi::KissatHandle;
+use rustsat::{
+    solvers::{
+        ControlSignal, Interrupt, InterruptSolver, Solve, SolveMightFail, SolveStats, SolverError,
+        SolverResult, SolverState, SolverStats, Terminate,
+    },
+    types::{Clause, Lit, TernaryVal, Var},
+};
+
+#[derive(Debug, PartialEq, Eq, Default)]
+enum InternalSolverState {
+    #[default]
+    Configuring,
+    Input,
+    Sat,
+    Unsat(Vec<Lit>),
+    Error(String),
+}
+
+impl InternalSolverState {
+    fn to_external(&self) -> SolverState {
+        match self {
+            InternalSolverState::Configuring => SolverState::Configuring,
+            InternalSolverState::Input => SolverState::Input,
+            InternalSolverState::Sat => SolverState::Sat,
+            InternalSolverState::Unsat(_) => SolverState::Unsat,
+            InternalSolverState::Error(desc) => SolverState::Error(desc.clone()),
+        }
+    }
+}
+
+type TermCallbackPtr<'a> = Box<dyn FnMut() -> ControlSignal + 'a>;
+/// Double boxing is necessary to get thin pointers for casting
+type OptTermCallbackStore<'a> = Option<Box<TermCallbackPtr<'a>>>;
+
+/// The Kissat solver type
+pub struct Kissat<'term> {
+    handle: *mut KissatHandle,
+    state: InternalSolverState,
+    terminate_cb: OptTermCallbackStore<'term>,
+    stats: SolverStats,
+}
+
+impl Default for Kissat<'_> {
+    fn default() -> Self {
+        let solver = Self {
+            handle: unsafe { ffi::kissat_init() },
+            state: Default::default(),
+            terminate_cb: Default::default(),
+            stats: Default::default(),
+        };
+        let quiet = CString::new("quiet").unwrap();
+        unsafe { ffi::kissat_set_option(solver.handle, quiet.as_ptr(), 1) };
+        solver
+    }
+}
+
+impl Kissat<'_> {
+    /// Gets the commit ID that Kissat was built from
+    pub fn commit_id() -> &'static str {
+        let c_chars = unsafe { ffi::kissat_id() };
+        let c_str = unsafe { CStr::from_ptr(c_chars) };
+        c_str.to_str().expect("Kissat id returned invalid UTF-8.")
+    }
+
+    /// Gets the Kissat version
+    pub fn version() -> &'static str {
+        let c_chars = unsafe { ffi::kissat_version() };
+        let c_str = unsafe { CStr::from_ptr(c_chars) };
+        c_str
+            .to_str()
+            .expect("Kissat version returned invalid UTF-8.")
+    }
+
+    /// Gets the compiler Kissat was built with
+    pub fn compiler() -> &'static str {
+        let c_chars = unsafe { ffi::kissat_compiler() };
+        let c_str = unsafe { CStr::from_ptr(c_chars) };
+        c_str
+            .to_str()
+            .expect("Kissat compiler returned invalid UTF-8.")
+    }
+
+    /// Sets a pre-defined configuration for Kissat's internal options
+    pub fn set_configuration(&mut self, config: Config) -> SolveMightFail {
+        if self.state == InternalSolverState::Configuring {
+            let config_name = match config {
+                Config::Default => CString::new("default").unwrap(),
+                Config::Basic => CString::new("basic").unwrap(),
+                Config::Plain => CString::new("plain").unwrap(),
+                Config::SAT => CString::new("sat").unwrap(),
+                Config::UNSAT => CString::new("unsat").unwrap(),
+            };
+            let ret = unsafe { ffi::kissat_set_configuration(self.handle, config_name.as_ptr()) };
+            if ret != 0 {
+                Ok(())
+            } else {
+                Err(SolverError::Api("kissat_configure returned 0".to_string()))
+            }
+        } else {
+            Err(SolverError::State(
+                self.state.to_external(),
+                SolverState::Configuring,
+            ))
+        }
+    }
+
+    /// Sets the value of a Kissat option. For possible options, check Kissat with `kissat --help`.
+    /// Requires state [`SolverState::Configuring`].
+    pub fn set_option(&mut self, name: &str, value: c_int) -> SolveMightFail {
+        let c_name = match CString::new(name) {
+            Ok(cstr) => cstr,
+            Err(_) => {
+                return Err(SolverError::Api(format!(
+                    "Kissat option {} cannot be converted to a C string",
+                    name
+                )))
+            }
+        };
+        if unsafe { ffi::kissat_set_option(self.handle, c_name.as_ptr(), value) } != 0 {
+            Ok(())
+        } else {
+            Err(SolverError::Api(format!(
+                "kissat_set_option returned false for option {}",
+                name
+            )))
+        }
+    }
+
+    /// Gets the value of a Kissat option. For possible options, check Kissat with `kissat --help`.
+    pub fn get_option(&self, name: &str) -> Result<c_int, SolverError> {
+        let c_name = match CString::new(name) {
+            Ok(cstr) => cstr,
+            Err(_) => {
+                return Err(SolverError::Api(format!(
+                    "Kissat option {} cannot be converted to a C string",
+                    name
+                )))
+            }
+        };
+        Ok(unsafe { ffi::kissat_get_option(self.handle, c_name.as_ptr()) })
+    }
+
+    /// Sets an internal limit for Kissat
+    pub fn set_limit(&mut self, limit: Limit) {
+        match limit {
+            Limit::Conflicts(val) => unsafe { ffi::kissat_set_conflict_limit(self.handle, val) },
+            Limit::Decisions(val) => unsafe { ffi::kissat_set_decision_limit(self.handle, val) },
+        }
+    }
+
+    /// Prints the solver statistics from the Kissat backend
+    pub fn print_stats(&self) {
+        unsafe { ffi::kissat_print_statistics(self.handle) }
+    }
+}
+
+impl Solve for Kissat<'_> {
+    fn signature(&self) -> &'static str {
+        let c_chars = unsafe { ffi::kissat_signature() };
+        let c_str = unsafe { CStr::from_ptr(c_chars) };
+        c_str
+            .to_str()
+            .expect("Kissat signature returned invalid UTF-8.")
+    }
+
+    fn reserve(&mut self, max_var: Var) -> SolveMightFail {
+        self.state = match self.state {
+            InternalSolverState::Error(_) => {
+                return Err(SolverError::State(
+                    self.state.to_external(),
+                    SolverState::Input,
+                ))
+            }
+            _ => InternalSolverState::Input,
+        };
+        unsafe { ffi::kissat_reserve(self.handle, max_var.to_ipasir()) };
+        Ok(())
+    }
+
+    fn solve(&mut self) -> Result<SolverResult, SolverError> {
+        // If already solved, return state
+        if let InternalSolverState::Sat = self.state {
+            return Ok(SolverResult::Sat);
+        } else if let InternalSolverState::Unsat(_) = self.state {
+            return Ok(SolverResult::Unsat);
+        } else if let InternalSolverState::Error(desc) = &self.state {
+            return Err(SolverError::State(
+                SolverState::Error(desc.clone()),
+                SolverState::Input,
+            ));
+        }
+        let start = ProcessTime::now();
+        // Solve with Kissat backend
+        let res = unsafe { ffi::kissat_solve(self.handle) };
+        self.stats.cpu_solve_time += start.elapsed();
+        match res {
+            0 => {
+                self.stats.n_terminated += 1;
+                self.state = InternalSolverState::Input;
+                Ok(SolverResult::Interrupted)
+            }
+            10 => {
+                self.stats.n_sat += 1;
+                self.state = InternalSolverState::Sat;
+                Ok(SolverResult::Sat)
+            }
+            20 => {
+                self.stats.n_unsat += 1;
+                self.state = InternalSolverState::Unsat(vec![]);
+                Ok(SolverResult::Unsat)
+            }
+            invalid => Err(SolverError::Api(format!(
+                "kissat_solve returned invalid value: {}",
+                invalid
+            ))),
+        }
+    }
+
+    fn lit_val(&self, lit: Lit) -> Result<TernaryVal, SolverError> {
+        match &self.state {
+            InternalSolverState::Sat => {
+                let lit = lit.to_ipasir();
+                match unsafe { ffi::kissat_value(self.handle, lit) } {
+                    0 => Ok(TernaryVal::DontCare),
+                    p if p == lit => Ok(TernaryVal::True),
+                    n if n == -lit => Ok(TernaryVal::False),
+                    invalid => Err(SolverError::Api(format!(
+                        "kissat_val returned invalid value: {}",
+                        invalid
+                    ))),
+                }
+            }
+            other => Err(SolverError::State(other.to_external(), SolverState::Sat)),
+        }
+    }
+
+    fn add_clause(&mut self, clause: Clause) -> SolveMightFail {
+        // Kissat is non-incremental, so only add if in input or configuring state
+        match &mut self.state {
+            InternalSolverState::Input | InternalSolverState::Configuring => (),
+            InternalSolverState::Error(_) => {
+                return Err(SolverError::State(
+                    self.state.to_external(),
+                    SolverState::Input,
+                ))
+            }
+            other => {
+                let old_state = other.to_external();
+                // Transition into error state
+                *other = InternalSolverState::Error(String::from(
+                    "added clause while not in input state",
+                ));
+                return Err(SolverError::State(old_state, SolverState::Input));
+            }
+        }
+        // Update wrapper-internal state
+        self.stats.n_clauses += 1;
+        self.stats.avg_clause_len =
+            (self.stats.avg_clause_len * ((self.stats.n_clauses - 1) as f32) + clause.len() as f32)
+                / self.stats.n_clauses as f32;
+        clause.iter().for_each(|l| match self.stats.max_var {
+            None => self.stats.max_var = Some(l.var()),
+            Some(var) => {
+                if l.var() > var {
+                    self.stats.max_var = Some(l.var())
+                }
+            }
+        });
+        self.state = InternalSolverState::Input;
+        // Call Kissat backend
+        clause
+            .into_iter()
+            .for_each(|l| unsafe { ffi::kissat_add(self.handle, l.to_ipasir()) });
+        unsafe { ffi::kissat_add(self.handle, 0) };
+        Ok(())
+    }
+}
+
+impl<'term> Terminate<'term> for Kissat<'term> {
+    /// Sets a terminator callback that is regularly called during solving.
+    ///
+    /// # Examples
+    ///
+    /// Terminate solver after 10 callback calls.
+    ///
+    /// ```
+    /// use rustsat::solvers::{ControlSignal, Solve, SolverResult, Terminate};
+    /// use rustsat_kissat::Kissat;
+    ///
+    /// let mut solver = Kissat::default();
+    ///
+    /// // Load instance
+    ///
+    /// let mut cnt = 1;
+    /// solver.attach_terminator(move || {
+    ///     if cnt > 10 {
+    ///         ControlSignal::Terminate
+    ///     } else {
+    ///         cnt += 1;
+    ///         ControlSignal::Continue
+    ///     }
+    /// });
+    ///
+    /// let ret = solver.solve().unwrap();
+    ///
+    /// // Assuming an instance is actually loaded and runs long enough
+    /// // assert_eq!(ret, SolverResult::Interrupted);
+    /// ```
+    fn attach_terminator<CB>(&mut self, cb: CB)
+    where
+        CB: FnMut() -> ControlSignal + 'term,
+    {
+        self.terminate_cb = Some(Box::new(Box::new(cb)));
+        let cb_ptr = self.terminate_cb.as_mut().unwrap().as_mut() as *const _ as *const c_void;
+        unsafe { ffi::kissat_set_terminate(self.handle, cb_ptr, Some(ffi::kissat_terminate_cb)) }
+    }
+
+    fn detach_terminator(&mut self) {
+        self.terminate_cb = None;
+        unsafe { ffi::kissat_set_terminate(self.handle, std::ptr::null(), None) }
+    }
+}
+
+impl Interrupt for Kissat<'_> {
+    type Interrupter = Interrupter;
+
+    fn interrupter(&mut self) -> Self::Interrupter {
+        Interrupter {
+            handle: self.handle,
+        }
+    }
+}
+
+/// An Interrupter for the Kissat solver
+pub struct Interrupter {
+    /// The C API handle
+    handle: *mut KissatHandle,
+}
+
+unsafe impl Send for Interrupter {}
+unsafe impl Sync for Interrupter {}
+
+impl InterruptSolver for Interrupter {
+    fn interrupt(&mut self) {
+        unsafe { ffi::kissat_terminate(self.handle) }
+    }
+}
+
+impl SolveStats for Kissat<'_> {
+    fn stats(&self) -> SolverStats {
+        self.stats.clone()
+    }
+}
+
+impl Drop for Kissat<'_> {
+    fn drop(&mut self) {
+        unsafe { ffi::kissat_release(self.handle) }
+    }
+}
+
+/// Possible Kissat configurations
+#[derive(Debug, Clone, Copy, PartialEq, Eq)]
+pub enum Config {
+    /// Default configuration
+    Default,
+    /// Basic CDCL solving ([`Config::Plain`] but no restarts, minimize, reduce)
+    Basic,
+    /// Plain CDCL solving without advanced techniques
+    Plain,
+    /// Target satisfiable instances
+    SAT,
+    /// Target unsatisfiable instances
+    UNSAT,
+}
+
+impl fmt::Display for Config {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        match self {
+            Config::Default => write!(f, "default"),
+            Config::Basic => write!(f, "basic"),
+            Config::Plain => write!(f, "plain"),
+            Config::SAT => write!(f, "sat"),
+            Config::UNSAT => write!(f, "unsat"),
+        }
+    }
+}
+
+/// Possible Kissat limits
+#[derive(Debug)]
+pub enum Limit {
+    /// A limit on the number of conflicts
+    Conflicts(c_uint),
+    /// A limit on the number of decisions
+    Decisions(c_uint),
+}
+
+impl fmt::Display for Limit {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        match self {
+            Limit::Conflicts(val) => write!(f, "conflicts ({})", val),
+            Limit::Decisions(val) => write!(f, "decisions ({})", val),
+        }
+    }
+}
+
+#[cfg(test)]
+mod test {
+    use super::{Config, Kissat, Limit};
+    use rustsat::{
+        lit,
+        solvers::{Solve, SolverError, SolverResult, SolverState},
+        types::Lit,
+    };
+
+    #[test]
+    fn build_destroy() {
+        let _solver = Kissat::default();
+    }
+
+    #[test]
+    fn build_two() {
+        let _solver1 = Kissat::default();
+        let _solver2 = Kissat::default();
+    }
+
+    #[test]
+    fn tiny_instance_sat() {
+        let mut solver = Kissat::default();
+        solver.add_binary(lit![0], !lit![1]).unwrap();
+        solver.add_binary(lit![1], !lit![2]).unwrap();
+        let ret = solver.solve();
+        match ret {
+            Err(e) => panic!("got error when solving: {}", e),
+            Ok(res) => assert_eq!(res, SolverResult::Sat),
+        }
+    }
+
+    #[test]
+    fn tiny_instance_unsat() {
+        let mut solver = Kissat::default();
+        solver.add_unit(!lit![0]).unwrap();
+        solver.add_binary(lit![0], !lit![1]).unwrap();
+        solver.add_binary(lit![1], !lit![2]).unwrap();
+        solver.add_unit(lit![2]).unwrap();
+        let ret = solver.solve();
+        match ret {
+            Err(e) => panic!("got error when solving: {}", e),
+            Ok(res) => assert_eq!(res, SolverResult::Unsat),
+        }
+    }
+
+    #[test]
+    fn configure() {
+        let mut solver = Kissat::default();
+        solver.set_configuration(Config::Default).unwrap();
+        solver.set_configuration(Config::Basic).unwrap();
+        solver.set_configuration(Config::Plain).unwrap();
+        solver.set_configuration(Config::SAT).unwrap();
+        solver.set_configuration(Config::UNSAT).unwrap();
+        solver.add_unit(lit![0]).unwrap();
+        assert_eq!(
+            solver.set_configuration(Config::Default),
+            Err(SolverError::State(
+                SolverState::Input,
+                SolverState::Configuring
+            ))
+        );
+    }
+
+    #[test]
+    fn options() {
+        let mut solver = Kissat::default();
+        assert_eq!(solver.get_option("warmup").unwrap(), 1);
+        solver.set_option("warmup", 0).unwrap();
+        assert_eq!(solver.get_option("warmup").unwrap(), 0);
+    }
+
+    #[test]
+    fn limit() {
+        let mut solver = Kissat::default();
+        solver.set_limit(Limit::Conflicts(100));
+    }
+}
+
+mod ffi {
+    use super::TermCallbackPtr;
+    use core::ffi::{c_char, c_int, c_uint, c_void};
+    use rustsat::solvers::ControlSignal;
+
+    #[repr(C)]
+    pub struct KissatHandle {
+        _private: [u8; 0],
+    }
+
+    extern "C" {
+        // Redefinitions of Kissat API
+        pub fn kissat_signature() -> *const c_char;
+        pub fn kissat_init() -> *mut KissatHandle;
+        pub fn kissat_release(solver: *mut KissatHandle);
+        pub fn kissat_add(solver: *mut KissatHandle, lit_or_zero: c_int);
+        pub fn kissat_solve(solver: *mut KissatHandle) -> c_int;
+        pub fn kissat_value(solver: *mut KissatHandle, lit: c_int) -> c_int;
+        pub fn kissat_set_terminate(
+            solver: *mut KissatHandle,
+            state: *const c_void,
+            terminate: Option<extern "C" fn(state: *const c_void) -> c_int>,
+        );
+        pub fn kissat_terminate(solver: *mut KissatHandle);
+        pub fn kissat_reserve(solver: *mut KissatHandle, max_var: c_int);
+        pub fn kissat_id() -> *const c_char;
+        pub fn kissat_version() -> *const c_char;
+        pub fn kissat_compiler() -> *const c_char;
+        pub fn kissat_set_option(
+            solver: *mut KissatHandle,
+            name: *const c_char,
+            val: c_int,
+        ) -> c_int;
+        pub fn kissat_get_option(solver: *mut KissatHandle, name: *const c_char) -> c_int;
+        pub fn kissat_set_configuration(solver: *mut KissatHandle, name: *const c_char) -> c_int;
+        pub fn kissat_set_conflict_limit(solver: *mut KissatHandle, limit: c_uint);
+        pub fn kissat_set_decision_limit(solver: *mut KissatHandle, limit: c_uint);
+        pub fn kissat_print_statistics(solver: *mut KissatHandle);
+    }
+
+    // Raw callbacks forwarding to user callbacks
+    pub extern "C" fn kissat_terminate_cb(ptr: *const c_void) -> c_int {
+        let cb = unsafe { &mut *(ptr as *mut TermCallbackPtr) };
+        match cb() {
+            ControlSignal::Continue => 0,
+            ControlSignal::Terminate => 1,
+        }
+    }
+}
diff --git a/minisat/.gitignore b/minisat/.gitignore
new file mode 100644
index 00000000..4fffb2f8
--- /dev/null
+++ b/minisat/.gitignore
@@ -0,0 +1,2 @@
+/target
+/Cargo.lock
diff --git a/minisat/Cargo.toml b/minisat/Cargo.toml
new file mode 100644
index 00000000..9dc62eab
--- /dev/null
+++ b/minisat/Cargo.toml
@@ -0,0 +1,24 @@
+[package]
+name = "rustsat-minisat"
+version = "0.1.0"
+edition = "2021"
+authors = ["Christoph Jabs <christoph.jabs@helsinki.fi>"]
+license = "MIT"
+description = "Interface to the SAT solver Minisat for the RustSAT library."
+keywords = ["sat solver", "rustsat"]
+readme = "README.md"
+
+build = "build.rs"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]
+cpu-time = "1.0.0"
+rustsat = { version = ">= 0.2.0", path = "../rustsat", default-features = false }
+
+[build-dependencies]
+cc = { version = "1.0.79", features = ["parallel"] }
+git2 = "0.17.1"
+glob = "0.3.1"
+chrono = "0.4.24"
+cmake = "0.1.50"
diff --git a/minisat/README.md b/minisat/README.md
new file mode 100644
index 00000000..3fd1a0a1
--- /dev/null
+++ b/minisat/README.md
@@ -0,0 +1,8 @@
+# rustsat-minisat - Interface to the Minisat SAT Solver for RustSAT
+
+The Minisat SAT solver be used with the [RustSAT](https://github.com/chrjabs/rustsat) library.
+
+## Minisat Version
+
+The version of minisat in this crate is Version 2.2.0.
+The used C++ source repository can be found [here](https://github.com/chrjabs/minisat).
\ No newline at end of file
diff --git a/minisat/build.rs b/minisat/build.rs
new file mode 100644
index 00000000..3e58841c
--- /dev/null
+++ b/minisat/build.rs
@@ -0,0 +1,94 @@
+use std::{env, fs, path::Path, str};
+
+fn main() {
+    // Build C++ library
+    // Full commit hash needs to be provided
+    build(
+        "https://github.com/chrjabs/minisat.git",
+        "master",
+        "7767e6587e28d8c4f844dc018ffcbfdf49937514",
+    );
+
+    let out_dir = env::var("OUT_DIR").unwrap();
+
+    // Built solver is in out_dir
+    println!("cargo:rustc-link-search={}", out_dir);
+    println!("cargo:rustc-link-search={}/lib", out_dir);
+}
+
+fn build(repo: &str, branch: &str, commit: &str) {
+    let out_dir = env::var("OUT_DIR").unwrap();
+    let mut minisat_dir_str = out_dir.clone();
+    minisat_dir_str.push_str("/minisat");
+    let minisat_dir = Path::new(&minisat_dir_str);
+    if update_repo(minisat_dir, repo, branch, commit)
+        || !Path::new(&out_dir)
+            .join("lib")
+            .join("libminisat.a")
+            .exists()
+    {
+        cmake::build(minisat_dir);
+    };
+
+    println!("cargo:rustc-link-lib=static=minisat");
+
+    #[cfg(target_os = "macos")]
+    println!("cargo:rustc-flags=-l dylib=c++");
+
+    #[cfg(not(target_os = "macos"))]
+    println!("cargo:rustc-flags=-l dylib=stdc++");
+}
+
+/// Returns true if there were changes, false if not
+fn update_repo(path: &Path, url: &str, branch: &str, commit: &str) -> bool {
+    let mut changed = false;
+    let target_oid = git2::Oid::from_str(commit)
+        .unwrap_or_else(|e| panic!("Invalid commit hash {}: {}", commit, e));
+    let repo = match git2::Repository::open(path) {
+        Ok(repo) => {
+            // Check if already at correct commit
+            if let Some(oid) = repo.head().unwrap().target_peel() {
+                if oid == target_oid {
+                    return changed;
+                }
+            };
+            // Check if commit needs to be fetched
+            if repo.find_commit(target_oid).is_err() {
+                // Fetch repo
+                let mut remote = repo.find_remote("origin").unwrap_or_else(|e| {
+                    panic!("Expected remote \"origin\" in git repo {:?}: {}", path, e)
+                });
+                remote.fetch(&[branch], None, None).unwrap_or_else(|e| {
+                    panic!(
+                        "Could not fetch \"origin/{}\" for git repo {:?}: {}",
+                        branch, path, e
+                    )
+                });
+                drop(remote);
+            }
+            repo
+        }
+        Err(_) => {
+            if path.exists() {
+                fs::remove_dir_all(path).unwrap_or_else(|e| {
+                    panic!(
+                        "Could not delete directory {}: {}",
+                        path.to_str().unwrap(),
+                        e
+                    )
+                });
+            };
+            changed = true;
+            git2::Repository::clone(url, path)
+                .unwrap_or_else(|e| panic!("Could not clone repository {}: {}", url, e))
+        }
+    };
+    let target_commit = repo
+        .find_commit(target_oid)
+        .unwrap_or_else(|e| panic!("Could not find commit {}: {}", commit, e));
+    repo.checkout_tree(target_commit.as_object(), None)
+        .unwrap_or_else(|e| panic!("Could not checkout commit {}: {}", commit, e));
+    repo.set_head_detached(target_oid)
+        .unwrap_or_else(|e| panic!("Could not detach head at {}: {}", commit, e));
+    changed
+}
diff --git a/minisat/data b/minisat/data
new file mode 120000
index 00000000..4909e06e
--- /dev/null
+++ b/minisat/data
@@ -0,0 +1,1 @@
+../data
\ No newline at end of file
diff --git a/minisat/src/core.rs b/minisat/src/core.rs
new file mode 100644
index 00000000..86d07017
--- /dev/null
+++ b/minisat/src/core.rs
@@ -0,0 +1,405 @@
+//! # Minisat Solver Interface Without Preprocessing (Core)
+//!
+//! Interface to the [Minisat](https://github.com/niklasso/minisat) incremental
+//! SAT solver.
+
+use core::ffi::{c_int, CStr};
+
+use super::{InternalSolverState, Limit};
+use cpu_time::ProcessTime;
+use ffi::MinisatHandle;
+use rustsat::{
+    solvers::{
+        GetInternalStats, Interrupt, InterruptSolver, LimitConflicts, LimitPropagations, PhaseLit,
+        Solve, SolveIncremental, SolveMightFail, SolveStats, SolverError, SolverResult,
+        SolverState, SolverStats,
+    },
+    types::{Clause, Lit, TernaryVal, Var},
+};
+
+/// The Minisat solver type without preprocessing
+pub struct Minisat {
+    handle: *mut MinisatHandle,
+    state: InternalSolverState,
+    stats: SolverStats,
+}
+
+impl Default for Minisat {
+    fn default() -> Self {
+        Self {
+            handle: unsafe { ffi::cminisat_init() },
+            state: Default::default(),
+            stats: Default::default(),
+        }
+    }
+}
+
+impl Minisat {
+    fn get_core_assumps(&self, assumps: &Vec<Lit>) -> Result<Vec<Lit>, SolverError> {
+        let mut core = Vec::new();
+        core.reserve(assumps.len());
+        for a in assumps {
+            match unsafe { ffi::cminisat_failed(self.handle, a.to_ipasir()) } {
+                0 => (),
+                1 => core.push(!*a),
+                invalid => {
+                    return Err(SolverError::Api(format!(
+                        "cminisat_failed returned invalid value: {}",
+                        invalid
+                    )))
+                }
+            }
+        }
+        Ok(core)
+    }
+
+    /// Sets an internal limit for Minisat
+    pub fn set_limit(&mut self, limit: Limit) {
+        match limit {
+            Limit::None => unsafe { ffi::cminisat_set_no_limit(self.handle) },
+            Limit::Conflicts(limit) => unsafe { ffi::cminisat_set_conf_limit(self.handle, limit) },
+            Limit::Propagations(limit) => unsafe {
+                ffi::cminisat_set_prop_limit(self.handle, limit)
+            },
+        };
+    }
+
+    /// Gets the current number of assigned literals
+    pub fn n_assigns(&self) -> c_int {
+        unsafe { ffi::cminisat_n_assigns(self.handle) }
+    }
+
+    /// Gets the current number of learnt clauses
+    pub fn n_learnts(&self) -> c_int {
+        unsafe { ffi::cminisat_n_learnts(self.handle) }
+    }
+}
+
+impl Solve for Minisat {
+    fn signature(&self) -> &'static str {
+        let c_chars = unsafe { ffi::cminisat_signature() };
+        let c_str = unsafe { CStr::from_ptr(c_chars) };
+        c_str
+            .to_str()
+            .expect("Minisat signature returned invalid UTF-8.")
+    }
+
+    fn solve(&mut self) -> Result<SolverResult, SolverError> {
+        // If already solved, return state
+        if let InternalSolverState::Sat = self.state {
+            return Ok(SolverResult::Sat);
+        } else if let InternalSolverState::Unsat(core) = &self.state {
+            if core.is_empty() {
+                return Ok(SolverResult::Unsat);
+            }
+        }
+        let start = ProcessTime::now();
+        // Solve with minisat backend
+        let res = unsafe { ffi::cminisat_solve(self.handle) };
+        self.stats.cpu_solve_time += start.elapsed();
+        match res {
+            0 => {
+                self.stats.n_terminated += 1;
+                self.state = InternalSolverState::Input;
+                Ok(SolverResult::Interrupted)
+            }
+            10 => {
+                self.stats.n_sat += 1;
+                self.state = InternalSolverState::Sat;
+                Ok(SolverResult::Sat)
+            }
+            20 => {
+                self.stats.n_unsat += 1;
+                self.state = InternalSolverState::Unsat(vec![]);
+                Ok(SolverResult::Unsat)
+            }
+            invalid => Err(SolverError::Api(format!(
+                "cminisat_solve returned invalid value: {}",
+                invalid
+            ))),
+        }
+    }
+
+    fn lit_val(&self, lit: Lit) -> Result<TernaryVal, SolverError> {
+        match &self.state {
+            InternalSolverState::Sat => {
+                let lit = lit.to_ipasir();
+                match unsafe { ffi::cminisat_val(self.handle, lit) } {
+                    0 => Ok(TernaryVal::DontCare),
+                    p if p == lit => Ok(TernaryVal::True),
+                    n if n == -lit => Ok(TernaryVal::False),
+                    invalid => Err(SolverError::Api(format!(
+                        "cminisat_val returned invalid value: {}",
+                        invalid
+                    ))),
+                }
+            }
+            other => Err(SolverError::State(other.to_external(), SolverState::Sat)),
+        }
+    }
+
+    fn add_clause(&mut self, clause: Clause) -> SolveMightFail {
+        // Update wrapper-internal state
+        self.stats.n_clauses += 1;
+        self.stats.avg_clause_len =
+            (self.stats.avg_clause_len * ((self.stats.n_clauses - 1) as f32) + clause.len() as f32)
+                / self.stats.n_clauses as f32;
+        self.state = InternalSolverState::Input;
+        // Call minisat backend
+        clause.into_iter().for_each(|l| unsafe {
+            ffi::cminisat_add(self.handle, l.to_ipasir());
+        });
+        unsafe { ffi::cminisat_add(self.handle, 0) };
+        Ok(())
+    }
+}
+
+impl SolveIncremental for Minisat {
+    fn solve_assumps(&mut self, assumps: Vec<Lit>) -> Result<SolverResult, SolverError> {
+        let start = ProcessTime::now();
+        // Solve with minisat backend
+        for a in &assumps {
+            unsafe { ffi::cminisat_assume(self.handle, a.to_ipasir()) }
+        }
+        let res = unsafe { ffi::cminisat_solve(self.handle) };
+        self.stats.cpu_solve_time += start.elapsed();
+        match res {
+            0 => {
+                self.stats.n_terminated += 1;
+                self.state = InternalSolverState::Input;
+                Ok(SolverResult::Interrupted)
+            }
+            10 => {
+                self.stats.n_sat += 1;
+                self.state = InternalSolverState::Sat;
+                Ok(SolverResult::Sat)
+            }
+            20 => {
+                self.stats.n_unsat += 1;
+                self.state = InternalSolverState::Unsat(self.get_core_assumps(&assumps)?);
+                Ok(SolverResult::Unsat)
+            }
+            invalid => Err(SolverError::Api(format!(
+                "cminisat_solve returned invalid value: {}",
+                invalid
+            ))),
+        }
+    }
+
+    fn core(&mut self) -> Result<Vec<Lit>, SolverError> {
+        match &self.state {
+            InternalSolverState::Unsat(core) => Ok(core.clone()),
+            other => Err(SolverError::State(other.to_external(), SolverState::Unsat)),
+        }
+    }
+}
+
+impl Interrupt for Minisat {
+    type Interrupter = Interrupter;
+    fn interrupter(&mut self) -> Self::Interrupter {
+        Interrupter {
+            handle: self.handle,
+        }
+    }
+}
+
+/// An Interrupter for the Minisat Core solver
+pub struct Interrupter {
+    /// The C API handle
+    handle: *mut MinisatHandle,
+}
+
+unsafe impl Send for Interrupter {}
+unsafe impl Sync for Interrupter {}
+
+impl InterruptSolver for Interrupter {
+    fn interrupt(&mut self) {
+        unsafe { ffi::cminisat_interrupt(self.handle) }
+    }
+}
+
+impl PhaseLit for Minisat {
+    /// Forces the default decision phase of a variable to a certain value
+    fn phase_lit(&mut self, lit: Lit) -> Result<(), SolverError> {
+        unsafe { ffi::cminisat_phase(self.handle, lit.to_ipasir()) };
+        Ok(())
+    }
+
+    /// Undoes the effect of a call to [`CaDiCaL::phase_lit`]
+    fn unphase_var(&mut self, var: Var) -> Result<(), SolverError> {
+        unsafe { ffi::cminisat_unphase(self.handle, var.to_ipasir()) };
+        Ok(())
+    }
+}
+
+impl LimitConflicts for Minisat {
+    fn limit_conflicts(&mut self, limit: Option<u32>) -> Result<(), SolverError> {
+        self.set_limit(Limit::Conflicts(if let Some(limit) = limit {
+            limit as i64
+        } else {
+            -1
+        }));
+        Ok(())
+    }
+}
+
+impl LimitPropagations for Minisat {
+    fn limit_propagations(&mut self, limit: Option<u32>) -> Result<(), SolverError> {
+        self.set_limit(Limit::Propagations(if let Some(limit) = limit {
+            limit as i64
+        } else {
+            -1
+        }));
+        Ok(())
+    }
+}
+
+impl GetInternalStats for Minisat {
+    fn propagations(&self) -> usize {
+        unsafe { ffi::cminisat_propagations(self.handle) }
+            .try_into()
+            .unwrap()
+    }
+
+    fn decisions(&self) -> usize {
+        unsafe { ffi::cminisat_decisions(self.handle) }
+            .try_into()
+            .unwrap()
+    }
+
+    fn conflicts(&self) -> usize {
+        unsafe { ffi::cminisat_conflicts(self.handle) }
+            .try_into()
+            .unwrap()
+    }
+}
+
+impl SolveStats for Minisat {
+    fn stats(&self) -> SolverStats {
+        let mut stats = self.stats.clone();
+        stats.max_var = self.max_var();
+        stats.n_clauses = self.n_clauses();
+        stats
+    }
+
+    fn max_var(&self) -> Option<Var> {
+        let max_var_idx = unsafe { ffi::cminisat_n_vars(self.handle) };
+        if max_var_idx > 0 {
+            Some(Var::new((max_var_idx - 1) as usize))
+        } else {
+            None
+        }
+    }
+
+    fn n_clauses(&self) -> usize {
+        unsafe { ffi::cminisat_n_clauses(self.handle) }
+            .try_into()
+            .unwrap()
+    }
+}
+
+impl Drop for Minisat {
+    fn drop(&mut self) {
+        unsafe { ffi::cminisat_release(self.handle) }
+    }
+}
+
+#[cfg(test)]
+mod test {
+    use super::Minisat;
+    use rustsat::{
+        lit,
+        solvers::{Solve, SolveStats, SolverResult},
+        types::{Lit, Var},
+        var,
+    };
+
+    #[test]
+    fn build_destroy() {
+        let _solver = Minisat::default();
+    }
+
+    #[test]
+    fn build_two() {
+        let _solver1 = Minisat::default();
+        let _solver2 = Minisat::default();
+    }
+
+    #[test]
+    fn tiny_instance_sat() {
+        let mut solver = Minisat::default();
+        solver.add_binary(lit![0], !lit![1]).unwrap();
+        solver.add_binary(lit![1], !lit![2]).unwrap();
+        let ret = solver.solve();
+        match ret {
+            Err(e) => panic!("got error when solving: {}", e),
+            Ok(res) => assert_eq!(res, SolverResult::Sat),
+        }
+    }
+
+    #[test]
+    fn tiny_instance_unsat() {
+        let mut solver = Minisat::default();
+        solver.add_unit(!lit![0]).unwrap();
+        solver.add_binary(lit![0], !lit![1]).unwrap();
+        solver.add_binary(lit![1], !lit![2]).unwrap();
+        solver.add_unit(lit![2]).unwrap();
+        let ret = solver.solve();
+        match ret {
+            Err(e) => panic!("got error when solving: {}", e),
+            Ok(res) => assert_eq!(res, SolverResult::Unsat),
+        }
+    }
+
+    #[test]
+    fn backend_stats() {
+        let mut solver = Minisat::default();
+        solver.add_binary(lit![0], !lit![1]).unwrap();
+        solver.add_binary(lit![1], !lit![2]).unwrap();
+        solver.add_binary(lit![2], !lit![3]).unwrap();
+        solver.add_binary(lit![3], !lit![4]).unwrap();
+        solver.add_binary(lit![4], !lit![5]).unwrap();
+        solver.add_binary(lit![5], !lit![6]).unwrap();
+        solver.add_binary(lit![6], !lit![7]).unwrap();
+        solver.add_binary(lit![7], !lit![8]).unwrap();
+        solver.add_binary(lit![8], !lit![9]).unwrap();
+
+        assert_eq!(solver.n_learnts(), 0);
+        assert_eq!(solver.n_clauses(), 9);
+        assert_eq!(solver.max_var(), Some(var![9]));
+    }
+}
+
+mod ffi {
+    use core::ffi::{c_char, c_int};
+
+    #[repr(C)]
+    pub struct MinisatHandle {
+        _private: [u8; 0],
+    }
+
+    extern "C" {
+        // Redefinitions of Minisat C API
+        pub fn cminisat_signature() -> *const c_char;
+        pub fn cminisat_init() -> *mut MinisatHandle;
+        pub fn cminisat_release(solver: *mut MinisatHandle);
+        pub fn cminisat_add(solver: *mut MinisatHandle, lit_or_zero: c_int);
+        pub fn cminisat_assume(solver: *mut MinisatHandle, lit: c_int);
+        pub fn cminisat_solve(solver: *mut MinisatHandle) -> c_int;
+        pub fn cminisat_val(solver: *mut MinisatHandle, lit: c_int) -> c_int;
+        pub fn cminisat_failed(solver: *mut MinisatHandle, lit: c_int) -> c_int;
+        pub fn cminisat_phase(solver: *mut MinisatHandle, lit: c_int);
+        pub fn cminisat_unphase(solver: *mut MinisatHandle, lit: c_int);
+        pub fn cminisat_n_assigns(solver: *mut MinisatHandle) -> c_int;
+        pub fn cminisat_n_clauses(solver: *mut MinisatHandle) -> c_int;
+        pub fn cminisat_n_learnts(solver: *mut MinisatHandle) -> c_int;
+        pub fn cminisat_n_vars(solver: *mut MinisatHandle) -> c_int;
+        pub fn cminisat_set_conf_limit(solver: *mut MinisatHandle, limit: i64);
+        pub fn cminisat_set_prop_limit(solver: *mut MinisatHandle, limit: i64);
+        pub fn cminisat_set_no_limit(solver: *mut MinisatHandle);
+        pub fn cminisat_interrupt(solver: *mut MinisatHandle);
+        pub fn cminisat_propagations(solver: *mut MinisatHandle) -> u64;
+        pub fn cminisat_decisions(solver: *mut MinisatHandle) -> u64;
+        pub fn cminisat_conflicts(solver: *mut MinisatHandle) -> u64;
+    }
+}
diff --git a/minisat/src/lib.rs b/minisat/src/lib.rs
new file mode 100644
index 00000000..da8aedfe
--- /dev/null
+++ b/minisat/src/lib.rs
@@ -0,0 +1,52 @@
+//! # Minisat Solver Interface
+//!
+//! Interface to the [Minisat](https://github.com/niklasso/minisat) incremental
+//! SAT solver.
+
+use rustsat::{solvers::SolverState, types::Lit};
+use std::fmt;
+
+pub mod simp;
+
+pub mod core;
+
+#[derive(Debug, PartialEq, Eq, Default)]
+enum InternalSolverState {
+    #[default]
+    Configuring,
+    Input,
+    Sat,
+    Unsat(Vec<Lit>),
+}
+
+impl InternalSolverState {
+    fn to_external(&self) -> SolverState {
+        match self {
+            InternalSolverState::Configuring => SolverState::Configuring,
+            InternalSolverState::Input => SolverState::Input,
+            InternalSolverState::Sat => SolverState::Sat,
+            InternalSolverState::Unsat(_) => SolverState::Unsat,
+        }
+    }
+}
+
+/// Possible Minisat limits
+#[derive(Debug)]
+pub enum Limit {
+    /// No limits
+    None,
+    /// A limit on the number of conflicts
+    Conflicts(i64),
+    /// A limit on the number of propagations
+    Propagations(i64),
+}
+
+impl fmt::Display for Limit {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        match self {
+            Limit::None => write!(f, "none"),
+            Limit::Conflicts(val) => write!(f, "conflicts ({})", val),
+            Limit::Propagations(val) => write!(f, "propagations ({})", val),
+        }
+    }
+}
diff --git a/minisat/src/simp.rs b/minisat/src/simp.rs
new file mode 100644
index 00000000..f51ab195
--- /dev/null
+++ b/minisat/src/simp.rs
@@ -0,0 +1,424 @@
+//! # Minisat Solver Interface With Preprocessing (Simp)
+//!
+//! Interface to the [Minisat](https://github.com/niklasso/minisat) incremental
+//! SAT solver.
+
+use core::ffi::{c_int, CStr};
+
+use super::{InternalSolverState, Limit};
+use cpu_time::ProcessTime;
+use ffi::MinisatHandle;
+use rustsat::{
+    solvers::{
+        GetInternalStats, Interrupt, InterruptSolver, LimitConflicts, LimitPropagations, PhaseLit,
+        Solve, SolveIncremental, SolveMightFail, SolveStats, SolverError, SolverResult,
+        SolverState, SolverStats,
+    },
+    types::{Clause, Lit, TernaryVal, Var},
+};
+
+/// The Minisat solver type with preprocessing
+pub struct Minisat {
+    handle: *mut MinisatHandle,
+    state: InternalSolverState,
+    stats: SolverStats,
+}
+
+impl Default for Minisat {
+    fn default() -> Self {
+        Self {
+            handle: unsafe { ffi::cminisatsimp_init() },
+            state: Default::default(),
+            stats: Default::default(),
+        }
+    }
+}
+
+impl Minisat {
+    fn get_core_assumps(&self, assumps: &Vec<Lit>) -> Result<Vec<Lit>, SolverError> {
+        let mut core = Vec::new();
+        core.reserve(assumps.len());
+        for a in assumps {
+            match unsafe { ffi::cminisatsimp_failed(self.handle, a.to_ipasir()) } {
+                0 => (),
+                1 => core.push(!*a),
+                invalid => {
+                    return Err(SolverError::Api(format!(
+                        "cminisatsimp_failed returned invalid value: {}",
+                        invalid
+                    )))
+                }
+            }
+        }
+        Ok(core)
+    }
+
+    /// Sets an internal limit for Minisat
+    pub fn set_limit(&mut self, limit: Limit) {
+        match limit {
+            Limit::None => unsafe { ffi::cminisatsimp_set_no_limit(self.handle) },
+            Limit::Conflicts(limit) => unsafe {
+                ffi::cminisatsimp_set_conf_limit(self.handle, limit)
+            },
+            Limit::Propagations(limit) => unsafe {
+                ffi::cminisatsimp_set_prop_limit(self.handle, limit)
+            },
+        };
+    }
+
+    /// Gets the current number of assigned literals
+    pub fn n_assigns(&self) -> c_int {
+        unsafe { ffi::cminisatsimp_n_assigns(self.handle) }
+    }
+
+    /// Gets the current number of learnt clauses
+    pub fn n_learnts(&self) -> c_int {
+        unsafe { ffi::cminisatsimp_n_learnts(self.handle) }
+    }
+
+    /// Freezes a literal.
+    pub fn freeze_lit(&mut self, lit: Lit) {
+        unsafe { ffi::cminisatsimp_set_frozen(self.handle, lit.var().to_ipasir(), true) }
+    }
+
+    /// Melts a literal.
+    pub fn melt_lit(&mut self, lit: Lit) {
+        unsafe { ffi::cminisatsimp_set_frozen(self.handle, lit.var().to_ipasir(), false) }
+    }
+
+    /// Checks if a variable has been eliminated by preprocessing.
+    pub fn var_eliminated(&mut self, var: Var) {
+        unsafe { ffi::cminisatsimp_is_eliminated(self.handle, var.to_ipasir()) }
+    }
+}
+
+impl Solve for Minisat {
+    fn signature(&self) -> &'static str {
+        let c_chars = unsafe { ffi::cminisat_signature() };
+        let c_str = unsafe { CStr::from_ptr(c_chars) };
+        c_str
+            .to_str()
+            .expect("Minisat signature returned invalid UTF-8.")
+    }
+
+    fn solve(&mut self) -> Result<SolverResult, SolverError> {
+        // If already solved, return state
+        if let InternalSolverState::Sat = self.state {
+            return Ok(SolverResult::Sat);
+        } else if let InternalSolverState::Unsat(core) = &self.state {
+            if core.is_empty() {
+                return Ok(SolverResult::Unsat);
+            }
+        }
+        let start = ProcessTime::now();
+        // Solve with minisat backend
+        let res = unsafe { ffi::cminisatsimp_solve(self.handle) };
+        self.stats.cpu_solve_time += start.elapsed();
+        match res {
+            0 => {
+                self.stats.n_terminated += 1;
+                self.state = InternalSolverState::Input;
+                Ok(SolverResult::Interrupted)
+            }
+            10 => {
+                self.stats.n_sat += 1;
+                self.state = InternalSolverState::Sat;
+                Ok(SolverResult::Sat)
+            }
+            20 => {
+                self.stats.n_unsat += 1;
+                self.state = InternalSolverState::Unsat(vec![]);
+                Ok(SolverResult::Unsat)
+            }
+            invalid => Err(SolverError::Api(format!(
+                "cminisatsimp_solve returned invalid value: {}",
+                invalid
+            ))),
+        }
+    }
+
+    fn lit_val(&self, lit: Lit) -> Result<TernaryVal, SolverError> {
+        match &self.state {
+            InternalSolverState::Sat => {
+                let lit = lit.to_ipasir();
+                match unsafe { ffi::cminisatsimp_val(self.handle, lit) } {
+                    0 => Ok(TernaryVal::DontCare),
+                    p if p == lit => Ok(TernaryVal::True),
+                    n if n == -lit => Ok(TernaryVal::False),
+                    invalid => Err(SolverError::Api(format!(
+                        "cminisatsimp_val returned invalid value: {}",
+                        invalid
+                    ))),
+                }
+            }
+            other => Err(SolverError::State(other.to_external(), SolverState::Sat)),
+        }
+    }
+
+    fn add_clause(&mut self, clause: Clause) -> SolveMightFail {
+        // Update wrapper-internal state
+        self.stats.n_clauses += 1;
+        self.stats.avg_clause_len =
+            (self.stats.avg_clause_len * ((self.stats.n_clauses - 1) as f32) + clause.len() as f32)
+                / self.stats.n_clauses as f32;
+        self.state = InternalSolverState::Input;
+        // Call minisat backend
+        clause.into_iter().for_each(|l| unsafe {
+            ffi::cminisatsimp_add(self.handle, l.to_ipasir());
+        });
+        unsafe { ffi::cminisatsimp_add(self.handle, 0) };
+        Ok(())
+    }
+}
+
+impl SolveIncremental for Minisat {
+    fn solve_assumps(&mut self, assumps: Vec<Lit>) -> Result<SolverResult, SolverError> {
+        let start = ProcessTime::now();
+        // Solve with minisat backend
+        for a in &assumps {
+            unsafe { ffi::cminisatsimp_assume(self.handle, a.to_ipasir()) }
+        }
+        let res = unsafe { ffi::cminisatsimp_solve(self.handle) };
+        self.stats.cpu_solve_time += start.elapsed();
+        match res {
+            0 => {
+                self.stats.n_terminated += 1;
+                self.state = InternalSolverState::Input;
+                Ok(SolverResult::Interrupted)
+            }
+            10 => {
+                self.stats.n_sat += 1;
+                self.state = InternalSolverState::Sat;
+                Ok(SolverResult::Sat)
+            }
+            20 => {
+                self.stats.n_unsat += 1;
+                self.state = InternalSolverState::Unsat(self.get_core_assumps(&assumps)?);
+                Ok(SolverResult::Unsat)
+            }
+            invalid => Err(SolverError::Api(format!(
+                "cminisatsimp_solve returned invalid value: {}",
+                invalid
+            ))),
+        }
+    }
+
+    fn core(&mut self) -> Result<Vec<Lit>, SolverError> {
+        match &self.state {
+            InternalSolverState::Unsat(core) => Ok(core.clone()),
+            other => Err(SolverError::State(other.to_external(), SolverState::Unsat)),
+        }
+    }
+}
+
+impl Interrupt for Minisat {
+    type Interrupter = Interrupter;
+    fn interrupter(&mut self) -> Self::Interrupter {
+        Interrupter {
+            handle: self.handle,
+        }
+    }
+}
+
+/// An Interrupter for the Minisat Simp solver
+pub struct Interrupter {
+    /// The C API handle
+    handle: *mut MinisatHandle,
+}
+
+unsafe impl Send for Interrupter {}
+unsafe impl Sync for Interrupter {}
+
+impl InterruptSolver for Interrupter {
+    fn interrupt(&mut self) {
+        unsafe { ffi::cminisatsimp_interrupt(self.handle) }
+    }
+}
+
+impl PhaseLit for Minisat {
+    /// Forces the default decision phase of a variable to a certain value
+    fn phase_lit(&mut self, lit: Lit) -> Result<(), SolverError> {
+        unsafe { ffi::cminisatsimp_phase(self.handle, lit.to_ipasir()) };
+        Ok(())
+    }
+
+    /// Undoes the effect of a call to [`CaDiCaL::phase_lit`]
+    fn unphase_var(&mut self, var: Var) -> Result<(), SolverError> {
+        unsafe { ffi::cminisatsimp_unphase(self.handle, var.to_ipasir()) };
+        Ok(())
+    }
+}
+
+impl LimitConflicts for Minisat {
+    fn limit_conflicts(&mut self, limit: Option<u32>) -> Result<(), SolverError> {
+        self.set_limit(Limit::Conflicts(if let Some(limit) = limit {
+            limit as i64
+        } else {
+            -1
+        }));
+        Ok(())
+    }
+}
+
+impl LimitPropagations for Minisat {
+    fn limit_propagations(&mut self, limit: Option<u32>) -> Result<(), SolverError> {
+        self.set_limit(Limit::Propagations(if let Some(limit) = limit {
+            limit as i64
+        } else {
+            -1
+        }));
+        Ok(())
+    }
+}
+
+impl GetInternalStats for Minisat {
+    fn propagations(&self) -> usize {
+        unsafe { ffi::cminisatsimp_propagations(self.handle) }
+            .try_into()
+            .unwrap()
+    }
+
+    fn decisions(&self) -> usize {
+        unsafe { ffi::cminisatsimp_decisions(self.handle) }
+            .try_into()
+            .unwrap()
+    }
+
+    fn conflicts(&self) -> usize {
+        unsafe { ffi::cminisatsimp_conflicts(self.handle) }
+            .try_into()
+            .unwrap()
+    }
+}
+
+impl SolveStats for Minisat {
+    fn stats(&self) -> SolverStats {
+        let mut stats = self.stats.clone();
+        stats.max_var = self.max_var();
+        stats.n_clauses = self.n_clauses();
+        stats
+    }
+
+    fn max_var(&self) -> Option<Var> {
+        let max_var_idx = unsafe { ffi::cminisatsimp_n_vars(self.handle) };
+        if max_var_idx > 0 {
+            Some(Var::new((max_var_idx - 1) as usize))
+        } else {
+            None
+        }
+    }
+
+    fn n_clauses(&self) -> usize {
+        unsafe { ffi::cminisatsimp_n_clauses(self.handle) }
+            .try_into()
+            .unwrap()
+    }
+}
+
+impl Drop for Minisat {
+    fn drop(&mut self) {
+        unsafe { ffi::cminisatsimp_release(self.handle) }
+    }
+}
+
+#[cfg(test)]
+mod test {
+    use super::Minisat;
+    use rustsat::{
+        lit,
+        solvers::{Solve, SolveStats, SolverResult},
+        types::{Lit, Var},
+        var,
+    };
+
+    #[test]
+    fn build_destroy() {
+        let _solver = Minisat::default();
+    }
+
+    #[test]
+    fn build_two() {
+        let _solver1 = Minisat::default();
+        let _solver2 = Minisat::default();
+    }
+
+    #[test]
+    fn tiny_instance_sat() {
+        let mut solver = Minisat::default();
+        solver.add_binary(lit![0], !lit![1]).unwrap();
+        solver.add_binary(lit![1], !lit![2]).unwrap();
+        let ret = solver.solve();
+        match ret {
+            Err(e) => panic!("got error when solving: {}", e),
+            Ok(res) => assert_eq!(res, SolverResult::Sat),
+        }
+    }
+
+    #[test]
+    fn tiny_instance_unsat() {
+        let mut solver = Minisat::default();
+        solver.add_unit(!lit![0]).unwrap();
+        solver.add_binary(lit![0], !lit![1]).unwrap();
+        solver.add_binary(lit![1], !lit![2]).unwrap();
+        solver.add_unit(lit![2]).unwrap();
+        let ret = solver.solve();
+        match ret {
+            Err(e) => panic!("got error when solving: {}", e),
+            Ok(res) => assert_eq!(res, SolverResult::Unsat),
+        }
+    }
+
+    #[test]
+    fn backend_stats() {
+        let mut solver = Minisat::default();
+        solver.add_binary(lit![0], !lit![1]).unwrap();
+        solver.add_binary(lit![1], !lit![2]).unwrap();
+        solver.add_binary(lit![2], !lit![3]).unwrap();
+        solver.add_binary(lit![3], !lit![4]).unwrap();
+        solver.add_binary(lit![4], !lit![5]).unwrap();
+        solver.add_binary(lit![5], !lit![6]).unwrap();
+        solver.add_binary(lit![6], !lit![7]).unwrap();
+        solver.add_binary(lit![7], !lit![8]).unwrap();
+        solver.add_binary(lit![8], !lit![9]).unwrap();
+
+        assert_eq!(solver.n_learnts(), 0);
+        assert_eq!(solver.n_clauses(), 9);
+        assert_eq!(solver.max_var(), Some(var![9]));
+    }
+}
+
+mod ffi {
+    use core::ffi::{c_char, c_int};
+
+    #[repr(C)]
+    pub struct MinisatHandle {
+        _private: [u8; 0],
+    }
+
+    extern "C" {
+        // Redefinitions of Minisat C API
+        pub fn cminisat_signature() -> *const c_char;
+        pub fn cminisatsimp_init() -> *mut MinisatHandle;
+        pub fn cminisatsimp_release(solver: *mut MinisatHandle);
+        pub fn cminisatsimp_add(solver: *mut MinisatHandle, lit_or_zero: c_int);
+        pub fn cminisatsimp_assume(solver: *mut MinisatHandle, lit: c_int);
+        pub fn cminisatsimp_solve(solver: *mut MinisatHandle) -> c_int;
+        pub fn cminisatsimp_val(solver: *mut MinisatHandle, lit: c_int) -> c_int;
+        pub fn cminisatsimp_failed(solver: *mut MinisatHandle, lit: c_int) -> c_int;
+        pub fn cminisatsimp_phase(solver: *mut MinisatHandle, lit: c_int);
+        pub fn cminisatsimp_unphase(solver: *mut MinisatHandle, lit: c_int);
+        pub fn cminisatsimp_n_assigns(solver: *mut MinisatHandle) -> c_int;
+        pub fn cminisatsimp_n_clauses(solver: *mut MinisatHandle) -> c_int;
+        pub fn cminisatsimp_n_learnts(solver: *mut MinisatHandle) -> c_int;
+        pub fn cminisatsimp_n_vars(solver: *mut MinisatHandle) -> c_int;
+        pub fn cminisatsimp_set_conf_limit(solver: *mut MinisatHandle, limit: i64);
+        pub fn cminisatsimp_set_prop_limit(solver: *mut MinisatHandle, limit: i64);
+        pub fn cminisatsimp_set_no_limit(solver: *mut MinisatHandle);
+        pub fn cminisatsimp_interrupt(solver: *mut MinisatHandle);
+        pub fn cminisatsimp_set_frozen(solver: *mut MinisatHandle, var: c_int, frozen: bool);
+        pub fn cminisatsimp_is_eliminated(solver: *mut MinisatHandle, var: c_int);
+        pub fn cminisatsimp_propagations(solver: *mut MinisatHandle) -> u64;
+        pub fn cminisatsimp_decisions(solver: *mut MinisatHandle) -> u64;
+        pub fn cminisatsimp_conflicts(solver: *mut MinisatHandle) -> u64;
+    }
+}
diff --git a/rustsat/Cargo.toml b/rustsat/Cargo.toml
new file mode 100644
index 00000000..e11eacb4
--- /dev/null
+++ b/rustsat/Cargo.toml
@@ -0,0 +1,54 @@
+[package]
+name = "rustsat"
+version = "0.2.0"
+edition = "2021"
+authors = ["Christoph Jabs <christoph.jabs@helsinki.fi>"]
+license = "MIT"
+description = "This library aims to provide implementations of elements commonly used in the development on software in the area of satisfiability solving. The focus of the library is to provide as much ease of use without giving up on performance."
+keywords = ["sat", "satisfiability", "encodings"]
+repository = "https://github.com/chrjabs/rustsat"
+readme = "../README.md"
+
+build = "build.rs"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]
+nom = "7.1.1"
+bzip2 = { version = "0.4.4", optional = true }
+flate2 = { version = "1.0.25", optional = true, features = ["zlib-ng"], default-features = false }
+xz2 = { version = "0.1.7", optional = true }
+rustc-hash = { version = "1.1.0", optional = true }
+cpu-time = "1.0.0"
+rand = { version = "0.8.5", optional = true }
+clap = { optional = true, version = "4.2.4", features = ["derive", "cargo"] }
+concolor-clap = { optional = true, version = "0.1.0" }
+termcolor = { optional = true, version = "1.2.0" }
+atty = { optional = true, version = "0.2.14" }
+visibility = { version = "0.0.1" }
+
+[build-dependencies]
+cc = { version = "1.0.79", features = ["parallel"] }
+git2 = "0.17.1"
+glob = "0.3.1"
+chrono = "0.4.24"
+cmake = "0.1.50"
+
+[features]
+default = [
+  "optimization",
+  "fxhash"
+]
+internals = []
+fxhash = ["dep:rustc-hash"]
+ipasir = []
+optimization = []
+multiopt = ["optimization"]
+compression = ["dep:bzip2", "dep:flate2", "dep:xz2"]
+rand = ["dep:rand"]
+all = [
+  "multiopt",
+  "compression",
+  "rand",
+  "fxhash"
+]
diff --git a/build.rs b/rustsat/build.rs
similarity index 100%
rename from build.rs
rename to rustsat/build.rs
diff --git a/src/encodings.rs b/rustsat/src/encodings.rs
similarity index 100%
rename from src/encodings.rs
rename to rustsat/src/encodings.rs
diff --git a/src/encodings/am1.rs b/rustsat/src/encodings/am1.rs
similarity index 76%
rename from src/encodings/am1.rs
rename to rustsat/src/encodings/am1.rs
index 455d3450..f5519550 100644
--- a/src/encodings/am1.rs
+++ b/rustsat/src/encodings/am1.rs
@@ -10,24 +10,16 @@
 //!     encodings::am1::{self, Encode},
 //!     instances::{BasicVarManager, ManageVars},
 //!     lit,
-//!     solvers::{self, SolveIncremental, Solve, SolverResult},
 //!     types::{Lit, Var},
 //!     var,
 //! };
 //!
-//! let mut solver = solvers::new_default_inc_solver();
 //! let mut var_manager = BasicVarManager::default();
 //! var_manager.increase_next_free(var![3]);
 //!
 //! let mut encoder = am1::new_default_am1();
 //! encoder.extend(vec![lit![0], lit![1], lit![2]]);
-//! solver.add_cnf(encoder.encode(&mut var_manager).unwrap()).unwrap();
-//!  
-//! let res = solver.solve_assumps(vec![!lit![0], lit![1], lit![2]]).unwrap();
-//! assert_eq!(res, SolverResult::Unsat);
-//!
-//! let res = solver.solve_assumps(vec![!lit![0], lit![1], !lit![2]]).unwrap();
-//! assert_eq!(res, SolverResult::Sat);
+//! let encoding = encoder.encode(&mut var_manager).unwrap();
 //! ```
 
 use super::Error;
diff --git a/src/encodings/am1/pairwise.rs b/rustsat/src/encodings/am1/pairwise.rs
similarity index 100%
rename from src/encodings/am1/pairwise.rs
rename to rustsat/src/encodings/am1/pairwise.rs
diff --git a/src/encodings/card.rs b/rustsat/src/encodings/card.rs
similarity index 94%
rename from src/encodings/card.rs
rename to rustsat/src/encodings/card.rs
index 6d1c8f77..b1515927 100644
--- a/src/encodings/card.rs
+++ b/rustsat/src/encodings/card.rs
@@ -12,29 +12,16 @@
 //!     encodings::{card, card::{BoundBoth, Encode}},
 //!     instances::{BasicVarManager, ManageVars},
 //!     lit, solvers,
-//!     solvers::{SolverResult, Solve, SolveIncremental},
 //!     types::{Clause, Lit, Var},
 //!     var,
 //! };
 //!
-//! let mut solver = solvers::new_default_inc_solver();
-//! solver.add_clause(clause![lit![0], lit![1], lit![2], lit![3]]);
 //! let mut var_manager = BasicVarManager::default();
 //! var_manager.increase_next_free(var![4]);
 //!
 //! let mut enc = card::new_default_inc_both();
 //! enc.extend(vec![lit![0], lit![1], lit![2], lit![3]]);
-//! solver.add_cnf(enc.encode_both(3..4, &mut var_manager));
-//!
-//! let mut assumps = enc.enforce_eq(3).unwrap();
-//! assumps.extend(vec![lit![0], lit![1], lit![2], !lit![3]]);
-//! let res = solver.solve_assumps(assumps).unwrap();
-//! assert_eq!(res, SolverResult::Sat);
-//!
-//! let mut assumps = enc.enforce_eq(3).unwrap();
-//! assumps.extend(vec![!lit![0], !lit![1], lit![2], lit![3]]);
-//! let res = solver.solve_assumps(assumps).unwrap();
-//! assert_eq!(res, SolverResult::Unsat);
+//! let encoding = enc.encode_both(3..4, &mut var_manager);
 //! ```
 //!
 //! When using cardinality and pseudo-boolean encodings at the same time, it is
diff --git a/src/encodings/card/simulators.rs b/rustsat/src/encodings/card/simulators.rs
similarity index 100%
rename from src/encodings/card/simulators.rs
rename to rustsat/src/encodings/card/simulators.rs
diff --git a/src/encodings/card/totalizer.rs b/rustsat/src/encodings/card/totalizer.rs
similarity index 100%
rename from src/encodings/card/totalizer.rs
rename to rustsat/src/encodings/card/totalizer.rs
diff --git a/src/encodings/pb.rs b/rustsat/src/encodings/pb.rs
similarity index 95%
rename from src/encodings/pb.rs
rename to rustsat/src/encodings/pb.rs
index 7f3e0c6f..25e635e6 100644
--- a/src/encodings/pb.rs
+++ b/rustsat/src/encodings/pb.rs
@@ -12,13 +12,10 @@
 //!     encodings::{pb, pb::{BoundBoth, Encode}},
 //!     instances::{BasicVarManager, ManageVars},
 //!     lit, solvers,
-//!     solvers::{SolverResult, Solve, SolveIncremental},
 //!     types::{Clause, Lit, Var, RsHashMap},
 //!     var,
 //! };
 //!
-//! let mut solver = solvers::new_default_inc_solver();
-//! solver.add_clause(clause![lit![0], lit![1], lit![2], lit![3]]);
 //! let mut var_manager = BasicVarManager::default();
 //! var_manager.increase_next_free(var![4]);
 //!
@@ -29,17 +26,7 @@
 //! lits.insert(lit![2], 2);
 //! lits.insert(lit![3], 6);
 //! enc.extend(lits);
-//! solver.add_cnf(enc.encode_both(4..5, &mut var_manager));
-//!
-//! let mut assumps = enc.enforce_eq(4).unwrap();
-//! assumps.extend(vec![!lit![0], lit![1], lit![2], !lit![3]]);
-//! let res = solver.solve_assumps(assumps).unwrap();
-//! assert_eq!(res, SolverResult::Sat);
-//!
-//! let mut assumps = enc.enforce_eq(4).unwrap();
-//! assumps.extend(vec![!lit![0], !lit![1], lit![2], lit![3]]);
-//! let res = solver.solve_assumps(assumps).unwrap();
-//! assert_eq!(res, SolverResult::Unsat);
+//! let encoding = enc.encode_both(4..5, &mut var_manager);
 //! ```
 //!
 //! When using cardinality and pseudo-boolean encodings at the same time, it is
diff --git a/src/encodings/pb/gte.rs b/rustsat/src/encodings/pb/gte.rs
similarity index 100%
rename from src/encodings/pb/gte.rs
rename to rustsat/src/encodings/pb/gte.rs
diff --git a/src/encodings/pb/simulators.rs b/rustsat/src/encodings/pb/simulators.rs
similarity index 100%
rename from src/encodings/pb/simulators.rs
rename to rustsat/src/encodings/pb/simulators.rs
diff --git a/src/instances.rs b/rustsat/src/instances.rs
similarity index 100%
rename from src/instances.rs
rename to rustsat/src/instances.rs
diff --git a/src/instances/fio.rs b/rustsat/src/instances/fio.rs
similarity index 100%
rename from src/instances/fio.rs
rename to rustsat/src/instances/fio.rs
diff --git a/src/instances/fio/dimacs.rs b/rustsat/src/instances/fio/dimacs.rs
similarity index 100%
rename from src/instances/fio/dimacs.rs
rename to rustsat/src/instances/fio/dimacs.rs
diff --git a/src/instances/fio/opb.rs b/rustsat/src/instances/fio/opb.rs
similarity index 99%
rename from src/instances/fio/opb.rs
rename to rustsat/src/instances/fio/opb.rs
index 7f628a09..0fa1c566 100644
--- a/src/instances/fio/opb.rs
+++ b/rustsat/src/instances/fio/opb.rs
@@ -357,9 +357,10 @@ fn opb_data(input: &str, opts: Options) -> IResult<&str, OpbData> {
         #[cfg(feature = "optimization")]
         map_res(|i| objective(i, opts), |obj| Ok::<_, ()>(OpbData::Obj(obj))),
         #[cfg(not(feature = "optimization"))]
-        map_res(|i| objective(i, opts), |obj| {
-            Ok::<_, ()>(OpbData::Obj(String::from(obj)))
-        }),
+        map_res(
+            |i| objective(i, opts),
+            |obj| Ok::<_, ()>(OpbData::Obj(String::from(obj))),
+        ),
     ))(input)
 }
 
diff --git a/src/instances/multiopt.rs b/rustsat/src/instances/multiopt.rs
similarity index 100%
rename from src/instances/multiopt.rs
rename to rustsat/src/instances/multiopt.rs
diff --git a/src/instances/opt.rs b/rustsat/src/instances/opt.rs
similarity index 100%
rename from src/instances/opt.rs
rename to rustsat/src/instances/opt.rs
diff --git a/src/instances/sat.rs b/rustsat/src/instances/sat.rs
similarity index 100%
rename from src/instances/sat.rs
rename to rustsat/src/instances/sat.rs
diff --git a/src/lib.rs b/rustsat/src/lib.rs
similarity index 100%
rename from src/lib.rs
rename to rustsat/src/lib.rs
diff --git a/src/solvers.rs b/rustsat/src/solvers.rs
similarity index 75%
rename from src/solvers.rs
rename to rustsat/src/solvers.rs
index ce994783..aa730bcd 100644
--- a/src/solvers.rs
+++ b/rustsat/src/solvers.rs
@@ -6,17 +6,14 @@
 //!
 //! ## Available Solvers
 //!
+//! Solvers are available through separate crates.
+//!
 //! ### CaDiCaL
 //!
 //! [CaDiCaL](https://github.com/arminbiere/cadical) is a fully incremental SAT
 //! solver by Armin Biere implemented in C++. It includes incremental
-//! inprocessing. CaDiCaL is the default incremental solver for RustSAT. The
-//! actual version used in RustSAT is from a fork of CaDiCaL available
-//! [here](https://github.com/chrjabs/cadical/). This fork extends CaDiCaL's C
-//! interface to make all functionality of the C++ interface available.
-//!
-//! Including CaDiCaL in a build of RustSAT is controlled by the `cadical`
-//! feature.
+//! inprocessing. It is available through the
+//! [`rustsat-cadical`](https://crates.io/crates/rustsat-cadical) crate.
 //!
 //! #### References
 //!
@@ -25,17 +22,14 @@
 //!   Entering the SAT Competition 2020_, SAT Competition 2020.
 //! - Original Repository:
 //!   [https://github.com/arminbiere/cadical](https://github.com/arminbiere/cadical)
-//! - Fork used in RustSAT:
-//!   [https://github.com/chrjabs/cadical](https://github.com/chrjabs/cadical)
+//! - Solver crate:
+//!   [https://crates.io/crates/rustsat-cadical](https://crates.io/crates/rustsat-cadical)
 //!
 //! ### Kissat
 //!
 //! [Kissat](https://github.com/arminbiere/kissat) is a non-incremental SAT
-//! solver by Armin Biere implemented in C. Kissat is the default
-//! non-incremental solver for RustSAT.
-//!
-//! Including Kissat in a build of RustSAT is controlled by the `kissat`
-//! feature.
+//! solver by Armin Biere implemented in C. It is available through the
+//! [`rustsat-kissat`](https://crates.io/crates/rustsat-kissat) crate.
 //!
 //! #### References
 //!
@@ -44,14 +38,14 @@
 //!   Entering the SAT Competition 2020_, SAT Competition 2020.
 //! - Repository:
 //!   [https://github.com/arminbiere/kissat](https://github.com/arminbiere/kissat)
+//! - Solver crate:
+//!   [https://github.com/chrjabs/rustsat-kissat](https://github.com/chrjabs/rustsat-kissat)
 //!
 //! ### Minisat
 //!
 //! [Minisat](https://github.com/niklasso/minisat) is an incremental SAT solver
-//! by Niklas Een and Niklas Sörensson.
-//!
-//! Including Minisat in a build of RustSAT is controlled by the `minisat`
-//! feature.
+//! by Niklas Een and Niklas Sörensson. It is available through the
+//! [`rustsat-minisat`](https://crates.io/crates/rustsat-minisat) crate.
 //!
 //! #### References
 //!
@@ -59,13 +53,17 @@
 //!   2003.
 //! - Repository:
 //!   [https://github.com/niklasso/minisat](https://github.com/niklasso/minisat)
+//! - Solver crate:
+//!   [https://crates.io/crates/rustsat-minisat](https://crates.io/crates/rustsat-minisat)
+//! - Fork used in solver crate:
+//!   [https://github.com/chrjabs/minisat](https://github.com/chrjabs/minisat)
 //!
 //! ### Glucose
 //!
 //! [Glucose](https://www.labri.fr/perso/lsimon/research/glucose/) is a SAT
 //! solver based on Minisat and developed by Gilles Audemard and Laurent Simon.
-//! Currently only Glucose version 4 (4.2.1) is included in RustSAT, controlled
-//! by the feature `glucose4`.
+//! It is available through the
+//! [`rustsat-glucose`](https://crates.io/crates/rustsat-glucose) crate.
 //!
 //! #### References
 //!
@@ -73,6 +71,10 @@
 //!   Modern SAT Solvers_, IJCAI 2009.
 //! - More references at the [Glucose
 //!   webpage](https://www.labri.fr/perso/lsimon/research/glucose/)
+//! - Solver crate:
+//!   [https://crates.io/crates/rustsat-glucose](https://crates.io/crates/rustsat-glucose)
+//! - Fork used in solver crate:
+//!   [https://github.com/chrjabs/glucose4](https://github.com/chrjabs/glucose4)
 //!
 //! ### IPASIR
 //!
@@ -80,10 +82,10 @@
 //! solvers. RustSAT's IPASIR interface is disabled by default since linking to
 //! multiple solvers implementing IPASIR at the same time is not possible. The
 //! main reason for including the IPASIR interface in RustSAT is to make it
-//! easier to include solvers not natively supported by RustSAT. For this,
-//! disable the default features of RustSAT to disable potentially conflicting
-//! solvers. Then enable the `ipasir` feature and modify the following lines in
-//! the build script `build.rs` accordingly.
+//! easier to include solvers that don't have Rust interface crates. For this,
+//! make sure to not depend on any other SAT solver crate to avoid potential
+//! namespace conflicts. Then enable the `ipasir` feature and modify the
+//! following lines in the build script `build.rs` accordingly.
 //!
 //! ```text
 //! // Link to custom IPASIR solver
@@ -112,34 +114,6 @@ mod ipasir;
 #[cfg(feature = "ipasir")]
 pub use ipasir::IpasirSolver;
 
-#[cfg(feature = "cadical")]
-pub mod cadical;
-#[cfg(feature = "cadical")]
-pub use cadical::CaDiCaL;
-
-#[cfg(feature = "kissat")]
-pub mod kissat;
-#[cfg(feature = "kissat")]
-pub use kissat::Kissat;
-
-#[cfg(feature = "glucose4")]
-pub mod glucose4;
-#[cfg(feature = "glucose4")]
-pub use glucose4::GlucoseCore4;
-#[cfg(feature = "glucose4")]
-pub use glucose4::GlucoseSimp4;
-#[cfg(feature = "glucose4")]
-pub use glucose4::GlucoseSimp4 as Glucose4;
-
-#[cfg(feature = "minisat")]
-pub mod minisat;
-#[cfg(feature = "minisat")]
-pub use minisat::MinisatCore;
-#[cfg(feature = "minisat")]
-pub use minisat::MinisatSimp;
-#[cfg(feature = "minisat")]
-pub use minisat::MinisatSimp as Minisat;
-
 /// Trait for all SAT solvers in this library.
 /// Solvers outside of this library can also implement this trait to be able to
 /// use them with this library.
@@ -269,6 +243,14 @@ pub trait PhaseLit {
     }
 }
 
+/// Trait for all solvers that can flip a literal in the current assignment
+pub trait FlipLit {
+    /// Attempts flipping the literal in the given assignment and returns `true` if successful
+    fn flip_lit(&mut self, lit: Lit) -> Result<bool, SolverError>;
+    /// Checks if the literal can be flipped in the given assignment without flipping it
+    fn is_flippable(&mut self, lit: Lit) -> Result<bool, SolverError>;
+}
+
 /// Trait for all solvers that can limit the number of conflicts
 pub trait LimitConflicts {
     /// Sets or removes a limit on the number of conflicts
@@ -378,30 +360,6 @@ pub trait SolveStats {
     }
 }
 
-#[derive(Debug, PartialEq, Eq, Default)]
-#[allow(dead_code)] // Not all solvers use all states
-enum InternalSolverState {
-    #[default]
-    Configuring,
-    Input,
-    Sat,
-    Unsat(Vec<Lit>),
-    Error(String),
-}
-
-impl InternalSolverState {
-    #[cfg(solver)]
-    fn to_external(&self) -> SolverState {
-        match self {
-            InternalSolverState::Configuring => SolverState::Configuring,
-            InternalSolverState::Input => SolverState::Input,
-            InternalSolverState::Sat => SolverState::Sat,
-            InternalSolverState::Unsat(_) => SolverState::Unsat,
-            InternalSolverState::Error(desc) => SolverState::Error(desc.clone()),
-        }
-    }
-}
-
 /// States that the solver can be in.
 #[derive(Debug, Clone, PartialEq, Eq)]
 pub enum SolverState {
@@ -481,78 +439,3 @@ impl fmt::Display for SolverError {
         }
     }
 }
-
-/// The default solver, depending on the library configuration.
-/// Solvers are ordered by the following priority:
-///
-/// 1. [`Kissat`]
-/// 2. [`CaDiCaL`]
-/// 3. [`GlucoseSimp4`]
-/// 4. [`MinisatSimp`]
-/// 5. [`IpasirSolver`]
-#[cfg(feature = "kissat")]
-pub type DefSolver<'term, 'learn> = Kissat<'term>;
-#[cfg(all(not(feature = "kissat"), feature = "cadical"))]
-pub type DefSolver<'term, 'learn> = CaDiCaL<'term, 'learn>;
-#[cfg(all(
-    not(feature = "kissat"),
-    not(feature = "cadical"),
-    feature = "glucose4"
-))]
-pub type DefSolver<'term, 'learn> = GlucoseSimp4;
-#[cfg(all(
-    not(feature = "kissat"),
-    not(feature = "cadical"),
-    not(feature = "glucose4"),
-    feature = "minisat"
-))]
-pub type DefSolver<'term, 'learn> = MinisatSimp;
-#[cfg(all(
-    not(feature = "kissat"),
-    not(feature = "cadical"),
-    not(feature = "glucose4"),
-    not(feature = "minisat"),
-    feature = "ipasir"
-))]
-pub type DefSolver<'term, 'learn> = IpasirSolver<'term, 'learn>;
-
-/// The default incremental solver, depending on the library configuration.
-/// Solvers are ordered by the following priority:
-///
-/// 1. [`CaDiCaL`]
-/// 2. [`GlucoseSimp4`]
-/// 3. [`MinisatSimp`]
-/// 4. [`IpasirSolver`]
-#[cfg(feature = "cadical")]
-pub type DefIncSolver<'term, 'learn> = CaDiCaL<'term, 'learn>;
-#[cfg(all(not(feature = "cadical"), feature = "glucose4"))]
-pub type DefIncSolver<'term, 'learn> = GlucoseSimp4;
-#[cfg(all(
-    not(feature = "cadical"),
-    not(feature = "glucose4"),
-    feature = "minisat"
-))]
-pub type DefIncSolver<'term, 'learn> = MinisatSimp;
-#[cfg(all(
-    not(feature = "cadical"),
-    not(feature = "glucose4"),
-    not(feature = "minisat"),
-    feature = "ipasir"
-))]
-pub type DefIncSolver<'term, 'learn> = IpasirSolver<'term, 'learn>;
-
-#[cfg(solver)]
-/// Constructs a default non-incremental solver. Since the return value cannot
-/// be upcast, it might be necessary to directly instantiate a solver. For now
-/// the default is an instance of CaDiCaL.
-pub fn new_default_solver() -> impl Solve {
-    DefSolver::default()
-}
-
-#[cfg(incsolver)]
-/// Constructs a default incremental solver. Since the return value cannot be
-/// upcast, it might be necessary to directly instantiate a solver. For now the
-/// default is an instance of CaDiCaL.
-pub fn new_default_inc_solver() -> impl SolveIncremental {
-    DefIncSolver::default()
-}
diff --git a/src/solvers/cadical.rs b/rustsat/src/solvers/cadical.rs
similarity index 100%
rename from src/solvers/cadical.rs
rename to rustsat/src/solvers/cadical.rs
diff --git a/src/solvers/glucose4.rs b/rustsat/src/solvers/glucose4.rs
similarity index 100%
rename from src/solvers/glucose4.rs
rename to rustsat/src/solvers/glucose4.rs
diff --git a/src/solvers/glucose4/core.rs b/rustsat/src/solvers/glucose4/core.rs
similarity index 100%
rename from src/solvers/glucose4/core.rs
rename to rustsat/src/solvers/glucose4/core.rs
diff --git a/src/solvers/glucose4/simp.rs b/rustsat/src/solvers/glucose4/simp.rs
similarity index 100%
rename from src/solvers/glucose4/simp.rs
rename to rustsat/src/solvers/glucose4/simp.rs
diff --git a/src/solvers/ipasir.rs b/rustsat/src/solvers/ipasir.rs
similarity index 94%
rename from src/solvers/ipasir.rs
rename to rustsat/src/solvers/ipasir.rs
index b3f11815..2d58cce4 100644
--- a/src/solvers/ipasir.rs
+++ b/rustsat/src/solvers/ipasir.rs
@@ -6,14 +6,37 @@
 use core::ffi::{c_int, c_void, CStr};
 
 use super::{
-    ControlSignal, InternalSolverState, Learn, OptLearnCallbackStore, OptTermCallbackStore, Solve,
-    SolveIncremental, SolveMightFail, SolveStats, SolverError, SolverResult, SolverState,
-    SolverStats, Terminate,
+    ControlSignal, Learn, OptLearnCallbackStore, OptTermCallbackStore, Solve, SolveIncremental,
+    SolveMightFail, SolveStats, SolverError, SolverResult, SolverState, SolverStats, Terminate,
 };
 use crate::types::{Clause, Lit, TernaryVal};
 use cpu_time::ProcessTime;
 use ffi::IpasirHandle;
 
+#[derive(Debug, PartialEq, Eq, Default)]
+#[allow(dead_code)] // Not all solvers use all states
+enum InternalSolverState {
+    #[default]
+    Configuring,
+    Input,
+    Sat,
+    Unsat(Vec<Lit>),
+    Error(String),
+}
+
+impl InternalSolverState {
+    #[cfg(solver)]
+    fn to_external(&self) -> SolverState {
+        match self {
+            InternalSolverState::Configuring => SolverState::Configuring,
+            InternalSolverState::Input => SolverState::Input,
+            InternalSolverState::Sat => SolverState::Sat,
+            InternalSolverState::Unsat(_) => SolverState::Unsat,
+            InternalSolverState::Error(desc) => SolverState::Error(desc.clone()),
+        }
+    }
+}
+
 /// Type for an IPASIR solver.
 pub struct IpasirSolver<'term, 'learn> {
     handle: *mut IpasirHandle,
diff --git a/src/solvers/kissat.rs b/rustsat/src/solvers/kissat.rs
similarity index 100%
rename from src/solvers/kissat.rs
rename to rustsat/src/solvers/kissat.rs
diff --git a/src/solvers/minisat.rs b/rustsat/src/solvers/minisat.rs
similarity index 100%
rename from src/solvers/minisat.rs
rename to rustsat/src/solvers/minisat.rs
diff --git a/src/solvers/minisat/core.rs b/rustsat/src/solvers/minisat/core.rs
similarity index 100%
rename from src/solvers/minisat/core.rs
rename to rustsat/src/solvers/minisat/core.rs
diff --git a/src/solvers/minisat/simp.rs b/rustsat/src/solvers/minisat/simp.rs
similarity index 100%
rename from src/solvers/minisat/simp.rs
rename to rustsat/src/solvers/minisat/simp.rs
diff --git a/src/types.rs b/rustsat/src/types.rs
similarity index 100%
rename from src/types.rs
rename to rustsat/src/types.rs
diff --git a/src/types/constraints.rs b/rustsat/src/types/constraints.rs
similarity index 100%
rename from src/types/constraints.rs
rename to rustsat/src/types/constraints.rs
diff --git a/tools/.gitignore b/tools/.gitignore
new file mode 100644
index 00000000..4fffb2f8
--- /dev/null
+++ b/tools/.gitignore
@@ -0,0 +1,2 @@
+/target
+/Cargo.lock
diff --git a/tools/Cargo.toml b/tools/Cargo.toml
new file mode 100644
index 00000000..1e59edc8
--- /dev/null
+++ b/tools/Cargo.toml
@@ -0,0 +1,47 @@
+[package]
+name = "rustsat-tools"
+version = "0.1.0"
+edition = "2021"
+authors = ["Christoph Jabs <christoph.jabs@helsinki.fi>"]
+license = "MIT"
+description = "Tools and examples built on the RustSAT library"
+keywords = ["rustsat", "sat", "satisfiability"]
+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]
+rustsat = { version = "0.2.0", path = "../rustsat", features = ["compression", "multiopt", "rand"] }
+rustsat-cadical = { version = "0.1.0", path = "../cadical" }
+clap = { version = "4.2.4", features = ["derive", "cargo"] }
+concolor-clap = { version = "0.1.0" }
+termcolor = { version = "1.2.0" }
+atty = { version = "0.2.14" }
+
+[[bin]]
+name = "enumerator"
+
+[[bin]]
+name = "cnf2opb"
+
+[[bin]]
+name = "opb2cnf"
+
+[[bin]]
+name = "wcnf2opb"
+
+[[bin]]
+name = "opb2wcnf"
+
+[[bin]]
+name = "mcnf2opb"
+
+[[bin]]
+name = "opb2mcnf"
+
+[[bin]]
+name = "shuffledimacs"
+
+[[bin]]
+name = "gbmosplit"
diff --git a/tools/README.md b/tools/README.md
new file mode 100644
index 00000000..4dc717f7
--- /dev/null
+++ b/tools/README.md
@@ -0,0 +1,4 @@
+# rustsat-tools - Tools and Unittests for the RustSAT Library
+
+This crate contains tools and unit tests for the RustSAT library.
+Unittests are here because they depend on solver interface crates, which in turn depend on RustSAT, which creates a dependency cycle if the tests are in RustSAT directly.
diff --git a/tools/data b/tools/data
new file mode 120000
index 00000000..4909e06e
--- /dev/null
+++ b/tools/data
@@ -0,0 +1,1 @@
+../data
\ No newline at end of file
diff --git a/examples/cnf2opb.rs b/tools/src/bin/cnf2opb.rs
similarity index 89%
rename from examples/cnf2opb.rs
rename to tools/src/bin/cnf2opb.rs
index c0778b3d..862b6eb0 100644
--- a/examples/cnf2opb.rs
+++ b/tools/src/bin/cnf2opb.rs
@@ -23,9 +23,10 @@ struct Args {
 
 fn main() {
     let args = Args::parse();
-    let mut opb_opts = OpbOptions::default();
-    opb_opts.first_var_idx = args.first_var_idx;
-    opb_opts.no_negated_lits = args.avoid_negated_lits;
+    let opb_opts = OpbOptions {
+        first_var_idx: args.first_var_idx,
+        no_negated_lits: args.avoid_negated_lits,
+    };
 
     let inst: SatInstance = if let Some(in_path) = args.in_path {
         SatInstance::from_dimacs_path(in_path).expect("error parsing the input file")
diff --git a/examples/enumerator.rs b/tools/src/bin/enumerator.rs
similarity index 97%
rename from examples/enumerator.rs
rename to tools/src/bin/enumerator.rs
index b9205477..3f110b8b 100644
--- a/examples/enumerator.rs
+++ b/tools/src/bin/enumerator.rs
@@ -52,7 +52,7 @@ fn main() {
         SatInstance::from_dimacs_path(in_path).expect("error parsing the input file");
     let (cnf, vm) = inst.as_cnf();
 
-    let mut solver = solvers::new_default_inc_solver();
+    let mut solver = rustsat_cadical::CaDiCaL::default();
     solver
         .reserve(vm.max_var().expect("no variables in instance"))
         .expect("error reserving memory in solver");
diff --git a/examples/gbmosplit.rs b/tools/src/bin/gbmosplit.rs
similarity index 97%
rename from examples/gbmosplit.rs
rename to tools/src/bin/gbmosplit.rs
index 0237d0e0..3a825a36 100644
--- a/examples/gbmosplit.rs
+++ b/tools/src/bin/gbmosplit.rs
@@ -179,7 +179,7 @@ struct Args {
     /// results will be printed.
     out_path: Option<PathBuf>,
     /// The splitting algorithm to use
-    #[arg(long, default_value_t = SplitAlg::GBMO)]
+    #[arg(long, default_value_t = SplitAlg::Gbmo)]
     split_alg: SplitAlg,
     /// The maximum number of weight combinations to check when thoroughly checking GBMO
     #[arg(long, default_value_t = 100000)]
@@ -195,24 +195,24 @@ struct Args {
 enum SplitAlg {
     /// Only detect non-generalized boolean multilevel optimization. (This
     /// detects lexicographic optimization of unweighted MO instances.)
-    BMO,
+    Bmo,
     /// Detect generalized boolean multilevel optimization, but only with the
     /// gcd method. (This detects lexicographic optimization of weighted MO
     /// instances.)
-    GCD,
+    Gcd,
     /// Full generalized boolean multilevel optimization detection. (With this
     /// detection, weights of higher ranked objectives can potentially not be
     /// divided/normalized.)
     #[default]
-    GBMO,
+    Gbmo,
 }
 
 impl fmt::Display for SplitAlg {
     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
         match self {
-            SplitAlg::BMO => write!(f, "bmo"),
-            SplitAlg::GCD => write!(f, "gcd"),
-            SplitAlg::GBMO => write!(f, "gbmo"),
+            SplitAlg::Bmo => write!(f, "bmo"),
+            SplitAlg::Gcd => write!(f, "gcd"),
+            SplitAlg::Gbmo => write!(f, "gbmo"),
         }
     }
 }
@@ -265,9 +265,9 @@ fn split<VM: ManageVars>(
     sorted_clauses.sort_by(|wc1, wc2| wc1.1.cmp(&wc2.1));
 
     let (mut objs, split_stats) = match cli.split_alg {
-        SplitAlg::BMO => split_bmo(sorted_clauses),
-        SplitAlg::GCD => split_gbmo(sorted_clauses, cli),
-        SplitAlg::GBMO => split_gbmo(sorted_clauses, cli),
+        SplitAlg::Bmo => split_bmo(sorted_clauses),
+        SplitAlg::Gcd => split_gbmo(sorted_clauses, cli),
+        SplitAlg::Gbmo => split_gbmo(sorted_clauses, cli),
     };
 
     // add offset of original objective to last objective
@@ -337,14 +337,12 @@ fn split_bmo(sorted_clauses: Vec<(Clause, usize)>) -> (Vec<Objective>, SplitStat
 }
 
 fn gcd(mut a: usize, mut b: usize) -> usize {
-    // Euclid's algorithm with XOR swap
+    // Euclid's algorithm
     while b != 0 {
         a %= b;
-        a ^= b;
-        b ^= a;
-        a ^= b;
+        std::mem::swap(&mut a, &mut b);
     }
-    return a;
+    a
 }
 
 fn get_sums_pot_splits_gcds(
@@ -446,7 +444,7 @@ fn split_gbmo(sorted_clauses: Vec<(Clause, usize)>, cli: &Cli) -> (Vec<Objective
     for split_end in pot_split_ends {
         // checking strictly for truly separate objectives
         if sums[split_end] < gcds[split_end + 1]
-            || (cli.split_alg == SplitAlg::GBMO
+            || (cli.split_alg == SplitAlg::Gbmo
                 && check_split_thorough_gbmo(
                     &sorted_clauses[split_end + 1..],
                     sums[split_end],
diff --git a/examples/mcnf2opb.rs b/tools/src/bin/mcnf2opb.rs
similarity index 89%
rename from examples/mcnf2opb.rs
rename to tools/src/bin/mcnf2opb.rs
index 43c31900..f9156c95 100644
--- a/examples/mcnf2opb.rs
+++ b/tools/src/bin/mcnf2opb.rs
@@ -23,9 +23,10 @@ struct Args {
 
 fn main() {
     let args = Args::parse();
-    let mut opb_opts = OpbOptions::default();
-    opb_opts.first_var_idx = args.first_var_idx;
-    opb_opts.no_negated_lits = args.avoid_negated_lits;
+    let opb_opts = OpbOptions {
+        first_var_idx: args.first_var_idx,
+        no_negated_lits: args.avoid_negated_lits,
+    };
 
     let inst: MultiOptInstance = if let Some(in_path) = args.in_path {
         MultiOptInstance::from_dimacs_path(in_path).expect("error parsing the input file")
diff --git a/examples/opb2cnf.rs b/tools/src/bin/opb2cnf.rs
similarity index 93%
rename from examples/opb2cnf.rs
rename to tools/src/bin/opb2cnf.rs
index a6b4a54f..998f2762 100644
--- a/examples/opb2cnf.rs
+++ b/tools/src/bin/opb2cnf.rs
@@ -20,8 +20,10 @@ struct Args {
 
 fn main() {
     let args = Args::parse();
-    let mut opb_opts = OpbOptions::default();
-    opb_opts.first_var_idx = args.first_var_idx;
+    let opb_opts = OpbOptions {
+        first_var_idx: 0,
+        ..Default::default()
+    };
 
     let inst: SatInstance = if let Some(in_path) = args.in_path {
         SatInstance::from_opb_path(in_path, opb_opts).expect("error parsing the input file")
diff --git a/examples/opb2mcnf.rs b/tools/src/bin/opb2mcnf.rs
similarity index 94%
rename from examples/opb2mcnf.rs
rename to tools/src/bin/opb2mcnf.rs
index 80a99716..9a97a6f7 100644
--- a/examples/opb2mcnf.rs
+++ b/tools/src/bin/opb2mcnf.rs
@@ -20,8 +20,10 @@ struct Args {
 
 fn main() {
     let args = Args::parse();
-    let mut opb_opts = OpbOptions::default();
-    opb_opts.first_var_idx = 0;
+    let opb_opts = OpbOptions {
+        first_var_idx: 0,
+        ..Default::default()
+    };
 
     let inst: MultiOptInstance = if let Some(in_path) = args.in_path {
         MultiOptInstance::from_opb_path(in_path, opb_opts).expect("error parsing the input file")
diff --git a/examples/opb2wcnf.rs b/tools/src/bin/opb2wcnf.rs
similarity index 93%
rename from examples/opb2wcnf.rs
rename to tools/src/bin/opb2wcnf.rs
index a23f0405..13b2dffd 100644
--- a/examples/opb2wcnf.rs
+++ b/tools/src/bin/opb2wcnf.rs
@@ -20,8 +20,10 @@ struct Args {
 
 fn main() {
     let args = Args::parse();
-    let mut opb_opts = OpbOptions::default();
-    opb_opts.first_var_idx = 0;
+    let opb_opts = OpbOptions {
+        first_var_idx: 0,
+        ..Default::default()
+    };
 
     let inst: OptInstance = if let Some(in_path) = args.in_path {
         OptInstance::from_opb_path(in_path, opb_opts).expect("error parsing the input file")
diff --git a/examples/shuffledimacs.rs b/tools/src/bin/shuffledimacs.rs
similarity index 80%
rename from examples/shuffledimacs.rs
rename to tools/src/bin/shuffledimacs.rs
index d5fc8b2e..645d1568 100644
--- a/examples/shuffledimacs.rs
+++ b/tools/src/bin/shuffledimacs.rs
@@ -5,7 +5,7 @@
 //!
 //! Usage: shuffledimacs [dimacs [m,w]cnf file] [output path]
 
-use std::path::PathBuf;
+use std::path::{Path, PathBuf};
 
 use rustsat::instances::{self, BasicVarManager, ManageVars, RandReindVarManager};
 
@@ -17,11 +17,9 @@ macro_rules! print_usage {
 }
 
 enum FileType {
-    CNF,
-    #[cfg(feature = "optimization")]
-    WCNF,
-    #[cfg(feature = "multiopt")]
-    MCNF,
+    Cnf,
+    Wcnf,
+    Mcnf,
 }
 
 fn main() {
@@ -29,7 +27,7 @@ fn main() {
     let out_path = PathBuf::from(&std::env::args().nth(2).unwrap_or_else(|| print_usage!()));
 
     match determine_file_type(&in_path) {
-        FileType::CNF => {
+        FileType::Cnf => {
             let mut inst = instances::SatInstance::<BasicVarManager>::from_dimacs_path(in_path)
                 .expect("Could not parse CNF");
             let n_vars = inst.var_manager().n_used();
@@ -39,8 +37,7 @@ fn main() {
                 .to_dimacs_path(out_path)
                 .expect("Could not write CNF");
         }
-        #[cfg(feature = "optimization")]
-        FileType::WCNF => {
+        FileType::Wcnf => {
             let mut inst = instances::OptInstance::<BasicVarManager>::from_dimacs_path(in_path)
                 .expect("Could not parse WCNF");
             let n_vars = inst.get_constraints().var_manager().n_used();
@@ -50,8 +47,7 @@ fn main() {
                 .to_dimacs_path(out_path)
                 .expect("Could not write WCNF");
         }
-        #[cfg(feature = "multiopt")]
-        FileType::MCNF => {
+        FileType::Mcnf => {
             let mut inst =
                 instances::MultiOptInstance::<BasicVarManager>::from_dimacs_path(in_path)
                     .expect("Could not parse MCNF");
@@ -71,27 +67,25 @@ macro_rules! is_one_of {
     }
 }
 
-fn determine_file_type(in_path: &PathBuf) -> FileType {
+fn determine_file_type(in_path: &Path) -> FileType {
     if let Some(ext) = in_path.extension() {
         let path_without_compr = in_path.with_extension("");
         let ext = if is_one_of!(ext, "gz", "bz2") {
             // Strip compression extension
             match path_without_compr.extension() {
                 Some(ext) => ext,
-                None => return FileType::CNF, // Fallback default
+                None => return FileType::Cnf, // Fallback default
             }
         } else {
             ext
         };
-        #[cfg(feature = "optimization")]
         if "wcnf" == ext {
-            return FileType::WCNF;
+            return FileType::Wcnf;
         };
-        #[cfg(feature = "multiopt")]
         if "mcnf" == ext {
-            return FileType::MCNF;
+            return FileType::Mcnf;
         };
-        return FileType::CNF; // Fallback default
+        return FileType::Cnf; // Fallback default
     };
-    FileType::CNF // Fallback default
+    FileType::Cnf // Fallback default
 }
diff --git a/examples/wcnf2opb.rs b/tools/src/bin/wcnf2opb.rs
similarity index 89%
rename from examples/wcnf2opb.rs
rename to tools/src/bin/wcnf2opb.rs
index ffaf8a0f..7e1e2c17 100644
--- a/examples/wcnf2opb.rs
+++ b/tools/src/bin/wcnf2opb.rs
@@ -23,9 +23,10 @@ struct Args {
 
 fn main() {
     let args = Args::parse();
-    let mut opb_opts = OpbOptions::default();
-    opb_opts.first_var_idx = args.first_var_idx;
-    opb_opts.no_negated_lits = args.avoid_negated_lits;
+    let opb_opts = OpbOptions {
+        first_var_idx: args.first_var_idx,
+        no_negated_lits: args.avoid_negated_lits,
+    };
 
     let inst: OptInstance = if let Some(in_path) = args.in_path {
         OptInstance::from_dimacs_path(in_path).expect("error parsing the input file")


Test patch:
diff --git a/.github/workflows/check-test.yml b/.github/workflows/check-test.yml
index 02051b86..67b56dd3 100644
--- a/.github/workflows/check-test.yml
+++ b/.github/workflows/check-test.yml
@@ -19,7 +19,7 @@ jobs:
       - name: Install stable toolchain
         uses: dtolnay/rust-toolchain@stable
       - name: Run cargo check
-        run: cargo check --verbose --features=all-non-conflicting
+        run: cargo check --workspace --verbose --features=all
           
   test:
     name: Test suite
@@ -30,4 +30,4 @@ jobs:
       - name: Install stable toolchain
         uses: dtolnay/rust-toolchain@stable
       - name: Run cargo test suite
-        run: cargo test --verbose --features=all-non-conflicting
+        run: cargo test --workspace --verbose
diff --git a/cadical/test-all.sh b/cadical/test-all.sh
new file mode 100755
index 00000000..4c6af39f
--- /dev/null
+++ b/cadical/test-all.sh
@@ -0,0 +1,41 @@
+#!/usr/bin/bash
+
+echo "Testing default (newest) version"
+cargo test &> def-test.log
+echo "Default (newest) test returned: $?"
+
+echo "Testing v1.5.0"
+cargo test --features=v1-5-0 &> v150-test.log
+echo "v1.5.0 test returned: $?"
+
+echo "Testing v1.5.1"
+cargo test --features=v1-5-1 &> v151-test.log
+echo "v1.5.1 test returned: $?"
+
+echo "Testing v1.5.2"
+cargo test --features=v1-5-2 &> v152-test.log
+echo "v1.5.2 test returned: $?"
+
+echo "Testing v1.5.3"
+cargo test --features=v1-5-3 &> v153-test.log
+echo "v1.5.3 test returned: $?"
+
+echo "Testing v1.5.4"
+cargo test --features=v1-5-4 &> v154-test.log
+echo "v1.5.4 test returned: $?"
+
+echo "Testing v1.5.5"
+cargo test --features=v1-5-5 &> v155-test.log
+echo "v1.5.5 test returned: $?"
+
+echo "Testing v1.5.6"
+cargo test --features=v1-5-6 &> v156-test.log
+echo "v1.5.6 test returned: $?"
+
+echo "Testing v1.6.0"
+cargo test --features=v1-6-0 &> v160-test.log
+echo "v1.6.0 test returned: $?"
+
+echo "Testing v1.7.0"
+cargo test --features=v1-7-0 &> v170-test.log
+echo "v1.7.0 test returned: $?"
diff --git a/cadical/tests/incremental.rs b/cadical/tests/incremental.rs
new file mode 100644
index 00000000..2479394a
--- /dev/null
+++ b/cadical/tests/incremental.rs
@@ -0,0 +1,87 @@
+use rustsat::{
+    instances::{BasicVarManager, SatInstance},
+    lit,
+    solvers::{SolveIncremental, SolverResult},
+    types::Lit,
+};
+use rustsat_cadical::CaDiCaL;
+
+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(vec![!lit![0], !lit![1]]).unwrap();
+    assert_eq!(res, SolverResult::Unsat);
+    let res = solver
+        .solve_assumps(vec![lit![0], lit![1], lit![2], lit![3]])
+        .unwrap();
+    assert_eq!(res, SolverResult::Unsat);
+    let res = solver
+        .solve_assumps(vec![lit![0], lit![1], lit![2], !lit![3]])
+        .unwrap();
+    assert_eq!(res, SolverResult::Unsat);
+    let res = solver
+        .solve_assumps(vec![lit![0], lit![1], !lit![2], lit![3]])
+        .unwrap();
+    assert_eq!(res, SolverResult::Unsat);
+    let res = solver
+        .solve_assumps(vec![lit![0], lit![1], !lit![2], !lit![3]])
+        .unwrap();
+    assert_eq!(res, SolverResult::Sat);
+    let res = solver
+        .solve_assumps(vec![lit![0], !lit![1], lit![2], lit![3]])
+        .unwrap();
+    assert_eq!(res, SolverResult::Unsat);
+    let res = solver
+        .solve_assumps(vec![lit![0], !lit![1], lit![2], !lit![3]])
+        .unwrap();
+    assert_eq!(res, SolverResult::Sat);
+    let res = solver
+        .solve_assumps(vec![lit![0], !lit![1], !lit![2], lit![3]])
+        .unwrap();
+    assert_eq!(res, SolverResult::Unsat);
+    let res = solver
+        .solve_assumps(vec![lit![0], !lit![1], !lit![2], !lit![3]])
+        .unwrap();
+    assert_eq!(res, SolverResult::Unsat);
+    let res = solver
+        .solve_assumps(vec![!lit![0], lit![1], lit![2], lit![3]])
+        .unwrap();
+    assert_eq!(res, SolverResult::Unsat);
+    let res = solver
+        .solve_assumps(vec![!lit![0], lit![1], lit![2], !lit![3]])
+        .unwrap();
+    assert_eq!(res, SolverResult::Unsat);
+    let res = solver
+        .solve_assumps(vec![!lit![0], lit![1], !lit![2], lit![3]])
+        .unwrap();
+    assert_eq!(res, SolverResult::Sat);
+    let res = solver
+        .solve_assumps(vec![!lit![0], lit![1], !lit![2], !lit![3]])
+        .unwrap();
+    assert_eq!(res, SolverResult::Sat);
+    let res = solver
+        .solve_assumps(vec![!lit![0], !lit![1], lit![2], lit![3]])
+        .unwrap();
+    assert_eq!(res, SolverResult::Unsat);
+    let res = solver
+        .solve_assumps(vec![!lit![0], !lit![1], lit![2], !lit![3]])
+        .unwrap();
+    assert_eq!(res, SolverResult::Unsat);
+    let res = solver
+        .solve_assumps(vec![!lit![0], !lit![1], !lit![2], lit![3]])
+        .unwrap();
+    assert_eq!(res, SolverResult::Unsat);
+    let res = solver
+        .solve_assumps(vec![!lit![0], !lit![1], !lit![2], !lit![3]])
+        .unwrap();
+    assert_eq!(res, SolverResult::Unsat);
+}
+
+#[test]
+fn assumption_sequence() {
+    let solver = CaDiCaL::default();
+    test_assumption_sequence(solver);
+}
diff --git a/cadical/tests/phasing.rs b/cadical/tests/phasing.rs
new file mode 100644
index 00000000..39dc63f3
--- /dev/null
+++ b/cadical/tests/phasing.rs
@@ -0,0 +1,34 @@
+use rustsat::{
+    instances::{BasicVarManager, SatInstance},
+    lit,
+    solvers::{PhaseLit, Solve, SolverResult},
+    types::{Lit, TernaryVal, Var},
+    var,
+};
+use rustsat_cadical::CaDiCaL;
+
+fn test_phase_saving<S: Solve + PhaseLit>(mut solver: S) {
+    let inst: SatInstance<BasicVarManager> =
+        SatInstance::from_dimacs_path("./data/small.cnf").unwrap();
+    solver.add_cnf(inst.as_cnf().0).unwrap();
+    solver.phase_lit(lit![0]).unwrap();
+    solver.phase_lit(!lit![1]).unwrap();
+    solver.phase_lit(lit![2]).unwrap();
+    solver.phase_lit(!lit![3]).unwrap();
+    let res = solver.solve().unwrap();
+    assert_eq!(res, SolverResult::Sat);
+    let sol = solver.solution(var![3]).unwrap();
+    assert_eq!(sol.lit_value(lit![0]), TernaryVal::True);
+    assert_eq!(sol.lit_value(lit![1]), TernaryVal::False);
+    assert_eq!(sol.lit_value(lit![2]), TernaryVal::True);
+    assert_eq!(sol.lit_value(lit![3]), TernaryVal::False);
+    solver.unphase_var(var![1]).unwrap();
+    solver.unphase_var(var![0]).unwrap();
+}
+
+#[test]
+fn phase_saving() {
+    let mut solver = CaDiCaL::default();
+    solver.set_option("lucky", 0).unwrap();
+    test_phase_saving(solver);
+}
diff --git a/cadical/tests/small.rs b/cadical/tests/small.rs
new file mode 100644
index 00000000..169fe6e9
--- /dev/null
+++ b/cadical/tests/small.rs
@@ -0,0 +1,70 @@
+use rustsat::{
+    instances::{BasicVarManager, SatInstance},
+    solvers::{Solve, SolverResult},
+};
+use rustsat_cadical::CaDiCaL;
+
+fn small_sat_instance<S: Solve>(mut solver: S) {
+    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);
+}
+
+fn small_unsat_instance<S: Solve>(mut solver: S) {
+    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);
+}
+
+#[test]
+fn small_sat() {
+    let solver = CaDiCaL::default();
+    small_sat_instance(solver);
+}
+
+#[test]
+fn small_unsat() {
+    let solver = CaDiCaL::default();
+    small_unsat_instance(solver);
+}
+
+#[test]
+fn sat_small_sat() {
+    let mut solver = CaDiCaL::default();
+    solver
+        .set_configuration(rustsat_cadical::Config::SAT)
+        .unwrap();
+    small_sat_instance(solver);
+}
+
+#[test]
+fn sat_small_unsat() {
+    let mut solver = CaDiCaL::default();
+    solver
+        .set_configuration(rustsat_cadical::Config::SAT)
+        .unwrap();
+    small_unsat_instance(solver);
+}
+
+#[test]
+fn unsat_small_sat() {
+    let mut solver = CaDiCaL::default();
+    solver
+        .set_configuration(rustsat_cadical::Config::UNSAT)
+        .unwrap();
+    small_sat_instance(solver);
+}
+
+#[test]
+fn unsat_small_unsat() {
+    let mut solver = CaDiCaL::default();
+    solver
+        .set_configuration(rustsat_cadical::Config::UNSAT)
+        .unwrap();
+    small_unsat_instance(solver);
+}
diff --git a/glucose/tests/incremental.rs b/glucose/tests/incremental.rs
new file mode 100644
index 00000000..d87124cb
--- /dev/null
+++ b/glucose/tests/incremental.rs
@@ -0,0 +1,87 @@
+use rustsat::{
+    instances::{BasicVarManager, SatInstance},
+    lit,
+    solvers::{SolveIncremental, SolverResult},
+    types::Lit,
+};
+use rustsat_glucose::core::Glucose;
+
+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(vec![!lit![0], !lit![1]]).unwrap();
+    assert_eq!(res, SolverResult::Unsat);
+    let res = solver
+        .solve_assumps(vec![lit![0], lit![1], lit![2], lit![3]])
+        .unwrap();
+    assert_eq!(res, SolverResult::Unsat);
+    let res = solver
+        .solve_assumps(vec![lit![0], lit![1], lit![2], !lit![3]])
+        .unwrap();
+    assert_eq!(res, SolverResult::Unsat);
+    let res = solver
+        .solve_assumps(vec![lit![0], lit![1], !lit![2], lit![3]])
+        .unwrap();
+    assert_eq!(res, SolverResult::Unsat);
+    let res = solver
+        .solve_assumps(vec![lit![0], lit![1], !lit![2], !lit![3]])
+        .unwrap();
+    assert_eq!(res, SolverResult::Sat);
+    let res = solver
+        .solve_assumps(vec![lit![0], !lit![1], lit![2], lit![3]])
+        .unwrap();
+    assert_eq!(res, SolverResult::Unsat);
+    let res = solver
+        .solve_assumps(vec![lit![0], !lit![1], lit![2], !lit![3]])
+        .unwrap();
+    assert_eq!(res, SolverResult::Sat);
+    let res = solver
+        .solve_assumps(vec![lit![0], !lit![1], !lit![2], lit![3]])
+        .unwrap();
+    assert_eq!(res, SolverResult::Unsat);
+    let res = solver
+        .solve_assumps(vec![lit![0], !lit![1], !lit![2], !lit![3]])
+        .unwrap();
+    assert_eq!(res, SolverResult::Unsat);
+    let res = solver
+        .solve_assumps(vec![!lit![0], lit![1], lit![2], lit![3]])
+        .unwrap();
+    assert_eq!(res, SolverResult::Unsat);
+    let res = solver
+        .solve_assumps(vec![!lit![0], lit![1], lit![2], !lit![3]])
+        .unwrap();
+    assert_eq!(res, SolverResult::Unsat);
+    let res = solver
+        .solve_assumps(vec![!lit![0], lit![1], !lit![2], lit![3]])
+        .unwrap();
+    assert_eq!(res, SolverResult::Sat);
+    let res = solver
+        .solve_assumps(vec![!lit![0], lit![1], !lit![2], !lit![3]])
+        .unwrap();
+    assert_eq!(res, SolverResult::Sat);
+    let res = solver
+        .solve_assumps(vec![!lit![0], !lit![1], lit![2], lit![3]])
+        .unwrap();
+    assert_eq!(res, SolverResult::Unsat);
+    let res = solver
+        .solve_assumps(vec![!lit![0], !lit![1], lit![2], !lit![3]])
+        .unwrap();
+    assert_eq!(res, SolverResult::Unsat);
+    let res = solver
+        .solve_assumps(vec![!lit![0], !lit![1], !lit![2], lit![3]])
+        .unwrap();
+    assert_eq!(res, SolverResult::Unsat);
+    let res = solver
+        .solve_assumps(vec![!lit![0], !lit![1], !lit![2], !lit![3]])
+        .unwrap();
+    assert_eq!(res, SolverResult::Unsat);
+}
+
+#[test]
+fn assumption_sequence() {
+    let solver = Glucose::default();
+    test_assumption_sequence(solver);
+}
diff --git a/glucose/tests/phasing.rs b/glucose/tests/phasing.rs
new file mode 100644
index 00000000..a80eeb02
--- /dev/null
+++ b/glucose/tests/phasing.rs
@@ -0,0 +1,38 @@
+use rustsat::{
+    instances::{BasicVarManager, SatInstance},
+    lit,
+    solvers::{PhaseLit, Solve, SolverResult},
+    types::{Lit, TernaryVal, Var},
+    var,
+};
+use rustsat_glucose::{core, simp};
+
+fn test_phase_saving<S: Solve + PhaseLit>(mut solver: S) {
+    let inst: SatInstance<BasicVarManager> =
+        SatInstance::from_dimacs_path("./data/small.cnf").unwrap();
+    solver.add_cnf(inst.as_cnf().0).unwrap();
+    solver.phase_lit(lit![0]).unwrap();
+    solver.phase_lit(!lit![1]).unwrap();
+    solver.phase_lit(lit![2]).unwrap();
+    solver.phase_lit(!lit![3]).unwrap();
+    let res = solver.solve().unwrap();
+    assert_eq!(res, SolverResult::Sat);
+    let sol = solver.solution(var![3]).unwrap();
+    assert_eq!(sol.lit_value(lit![0]), TernaryVal::True);
+    assert_eq!(sol.lit_value(lit![1]), TernaryVal::False);
+    assert_eq!(sol.lit_value(lit![2]), TernaryVal::True);
+    assert_eq!(sol.lit_value(lit![3]), TernaryVal::False);
+    solver.unphase_var(var![1]).unwrap();
+    solver.unphase_var(var![0]).unwrap();
+}
+#[test]
+fn core_phase_saving() {
+    let solver = core::Glucose::default();
+    test_phase_saving(solver);
+}
+
+#[test]
+fn simp_phase_saving() {
+    let solver = simp::Glucose::default();
+    test_phase_saving(solver);
+}
diff --git a/glucose/tests/small.rs b/glucose/tests/small.rs
new file mode 100644
index 00000000..ca02f36d
--- /dev/null
+++ b/glucose/tests/small.rs
@@ -0,0 +1,50 @@
+use rustsat::{
+    instances::{BasicVarManager, SatInstance},
+    solvers::{Solve, SolverResult},
+};
+use rustsat_glucose::{core, simp};
+
+fn small_sat_instance<S: Solve>(mut solver: S) {
+    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);
+}
+
+fn small_unsat_instance<S: Solve>(mut solver: S) {
+    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);
+}
+
+#[test]
+fn core_small_sat() {
+    let solver = core::Glucose::default();
+    small_sat_instance(solver);
+}
+
+// Note: this instance seems too hard for glucose to solve
+#[test]
+#[ignore]
+fn core_small_unsat() {
+    let solver = core::Glucose::default();
+    small_unsat_instance(solver);
+}
+
+#[test]
+fn simp_small_sat() {
+    let solver = simp::Glucose::default();
+    small_sat_instance(solver);
+}
+
+// Note: this instance seems too hard for glucose to solve
+#[test]
+#[ignore]
+fn simp_small_unsat() {
+    let solver = simp::Glucose::default();
+    small_unsat_instance(solver);
+}
diff --git a/kissat/test-all.sh b/kissat/test-all.sh
new file mode 100755
index 00000000..3bd2d5e1
--- /dev/null
+++ b/kissat/test-all.sh
@@ -0,0 +1,25 @@
+#!/usr/bin/bash
+
+echo "Testing default (newest) version"
+cargo test &> def-test.log
+echo "Default (newest) test returned: $?"
+
+echo "Testing sc2022-bulky"
+cargo test --features=sc2022-bulky &> sc2022-bulky-test.log
+echo "sc2022-bulky test returned: $?"
+
+echo "Testing sc2022-hyper"
+cargo test --features=sc2022-hyper &> sc2022-hyper-test.log
+echo "sc2022-hyper test returned: $?"
+
+echo "Testing sc2022-light"
+cargo test --features=sc2022-light &> sc2022-light-test.log
+echo "sc2022-light test returned: $?"
+
+echo "Testing v3.0.0"
+cargo test --features=v3-0-0 &> v300-test.log
+echo "v3.0.0 test returned: $?"
+
+echo "Testing v3.1.0"
+cargo test --features=v3-1-0 &> v310-test.log
+echo "v3.1.0 test returned: $?"
diff --git a/kissat/tests/small.rs b/kissat/tests/small.rs
new file mode 100644
index 00000000..b2a65dc3
--- /dev/null
+++ b/kissat/tests/small.rs
@@ -0,0 +1,70 @@
+use rustsat::{
+    instances::{BasicVarManager, SatInstance},
+    solvers::{Solve, SolverResult},
+};
+use rustsat_kissat::Kissat;
+
+fn small_sat_instance<S: Solve>(mut solver: S) {
+    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);
+}
+
+fn small_unsat_instance<S: Solve>(mut solver: S) {
+    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);
+}
+
+#[test]
+fn small_sat() {
+    let solver = Kissat::default();
+    small_sat_instance(solver);
+}
+
+#[test]
+fn small_unsat() {
+    let solver = Kissat::default();
+    small_unsat_instance(solver);
+}
+
+#[test]
+fn sat_small_sat() {
+    let mut solver = Kissat::default();
+    solver
+        .set_configuration(rustsat_kissat::Config::SAT)
+        .unwrap();
+    small_sat_instance(solver);
+}
+
+#[test]
+fn sat_small_unsat() {
+    let mut solver = Kissat::default();
+    solver
+        .set_configuration(rustsat_kissat::Config::SAT)
+        .unwrap();
+    small_unsat_instance(solver);
+}
+
+#[test]
+fn unsat_small_sat() {
+    let mut solver = Kissat::default();
+    solver
+        .set_configuration(rustsat_kissat::Config::UNSAT)
+        .unwrap();
+    small_sat_instance(solver);
+}
+
+#[test]
+fn unsat_small_unsat() {
+    let mut solver = Kissat::default();
+    solver
+        .set_configuration(rustsat_kissat::Config::UNSAT)
+        .unwrap();
+    small_unsat_instance(solver);
+}
diff --git a/tests/incremental_solver.rs b/minisat/tests/incremental.rs
similarity index 70%
rename from tests/incremental_solver.rs
rename to minisat/tests/incremental.rs
index ee5da3c1..06fb61de 100644
--- a/tests/incremental_solver.rs
+++ b/minisat/tests/incremental.rs
@@ -1,16 +1,15 @@
-#![allow(dead_code, unused)]
-
 use rustsat::{
     instances::{BasicVarManager, SatInstance},
-    lit, solvers,
+    lit,
     solvers::{SolveIncremental, SolverResult},
     types::Lit,
 };
+use rustsat_minisat::core::Minisat;
 
-fn assumption_sequence<S: SolveIncremental>(mut solver: S) {
+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);
+    solver.add_cnf(inst.as_cnf().0).unwrap();
     let res = solver.solve().unwrap();
     assert_eq!(res, SolverResult::Sat);
     let res = solver.solve_assumps(vec![!lit![0], !lit![1]]).unwrap();
@@ -82,47 +81,10 @@ fn assumption_sequence<S: SolveIncremental>(mut solver: S) {
 }
 
 #[test]
-#[cfg(feature = "ipasir")]
-fn ipasir_small_sat() {
-    let solver = solvers::IpasirSolver::default();
-    assumption_sequence(solver);
-}
-
-#[test]
-#[cfg(feature = "cadical")]
-fn cadical_assumption_sequence() {
-    let solver = solvers::CaDiCaL::default();
-    assumption_sequence(solver);
-}
-
-#[test]
-#[cfg(feature = "glucose4")]
-fn glucosecore4_assumption_sequence() {
-    let solver = solvers::GlucoseCore4::default();
-    assumption_sequence(solver);
-}
-
-// Note: Cannot test prepro version of glucose with this small example because
-// the variable are eliminated by preprocessing
-// #[test]
-// #[cfg(feature = "glucose4")]
-// fn glucosesimp4_assumption_sequence() {
-//     let solver = solvers::GlucoseSimp4::default();
-//     assumption_sequence(solver);
-// }
-
-#[test]
-#[cfg(feature = "minisat")]
-fn minisatcore_assumption_sequence() {
-    let solver = solvers::MinisatCore::default();
-    assumption_sequence(solver);
+fn assumption_sequence() {
+    let solver = Minisat::default();
+    test_assumption_sequence(solver);
 }
 
 // Note: Cannot test prepro version of minisat with this small example because
 // the variable are eliminated by preprocessing
-// #[test]
-// #[cfg(feature = "minisat")]
-// fn minisatsimp_assumption_sequence() {
-//     let solver = solvers::MinisatSimp::default();
-//     assumption_sequence(solver);
-// }
diff --git a/minisat/tests/phasing.rs b/minisat/tests/phasing.rs
new file mode 100644
index 00000000..61746ce5
--- /dev/null
+++ b/minisat/tests/phasing.rs
@@ -0,0 +1,38 @@
+use rustsat::{
+    instances::{BasicVarManager, SatInstance},
+    lit,
+    solvers::{PhaseLit, Solve, SolverResult},
+    types::{Lit, TernaryVal, Var},
+    var,
+};
+use rustsat_minisat::{core, simp};
+
+fn test_phase_saving<S: Solve + PhaseLit>(mut solver: S) {
+    let inst: SatInstance<BasicVarManager> =
+        SatInstance::from_dimacs_path("./data/small.cnf").unwrap();
+    solver.add_cnf(inst.as_cnf().0).unwrap();
+    solver.phase_lit(lit![0]).unwrap();
+    solver.phase_lit(!lit![1]).unwrap();
+    solver.phase_lit(lit![2]).unwrap();
+    solver.phase_lit(!lit![3]).unwrap();
+    let res = solver.solve().unwrap();
+    assert_eq!(res, SolverResult::Sat);
+    let sol = solver.solution(var![3]).unwrap();
+    assert_eq!(sol.lit_value(lit![0]), TernaryVal::True);
+    assert_eq!(sol.lit_value(lit![1]), TernaryVal::False);
+    assert_eq!(sol.lit_value(lit![2]), TernaryVal::True);
+    assert_eq!(sol.lit_value(lit![3]), TernaryVal::False);
+    solver.unphase_var(var![1]).unwrap();
+    solver.unphase_var(var![0]).unwrap();
+}
+#[test]
+fn core_phase_saving() {
+    let solver = core::Minisat::default();
+    test_phase_saving(solver);
+}
+
+#[test]
+fn simp_phase_saving() {
+    let solver = simp::Minisat::default();
+    test_phase_saving(solver);
+}
diff --git a/minisat/tests/small.rs b/minisat/tests/small.rs
new file mode 100644
index 00000000..50a99f2c
--- /dev/null
+++ b/minisat/tests/small.rs
@@ -0,0 +1,51 @@
+use rustsat::{
+    instances::{BasicVarManager, SatInstance},
+    solvers::{Solve, SolverResult},
+};
+use rustsat_minisat::{core, simp};
+
+#[test]
+fn core_small_sat() {
+    let mut solver = core::Minisat::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 core_small_unsat() {
+    let mut solver = core::Minisat::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);
+}
+
+#[test]
+fn simp_small_sat() {
+    let mut solver = simp::Minisat::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 = simp::Minisat::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);
+}
diff --git a/tests/phasing.rs b/tests/phasing.rs
deleted file mode 100644
index f4a741f3..00000000
--- a/tests/phasing.rs
+++ /dev/null
@@ -1,64 +0,0 @@
-#![allow(dead_code, unused)]
-
-use rustsat::{
-    instances::{BasicVarManager, SatInstance},
-    lit, solvers,
-    solvers::{PhaseLit, Solve, SolverResult},
-    types::{Lit, TernaryVal, Var},
-    var,
-};
-
-fn phase_saving<S: Solve + PhaseLit>(mut solver: S) {
-    let inst: SatInstance<BasicVarManager> =
-        SatInstance::from_dimacs_path("./data/small.cnf").unwrap();
-    solver.add_cnf(inst.as_cnf().0);
-    solver.phase_lit(lit![0]);
-    solver.phase_lit(!lit![1]);
-    solver.phase_lit(lit![2]);
-    solver.phase_lit(!lit![3]);
-    let res = solver.solve().unwrap();
-    assert_eq!(res, SolverResult::Sat);
-    let sol = solver.solution(var![3]).unwrap();
-    assert_eq!(sol.lit_value(lit![0]), TernaryVal::True);
-    assert_eq!(sol.lit_value(lit![1]), TernaryVal::False);
-    assert_eq!(sol.lit_value(lit![2]), TernaryVal::True);
-    assert_eq!(sol.lit_value(lit![3]), TernaryVal::False);
-    solver.unphase_var(var![1]);
-    solver.unphase_var(var![0]);
-}
-
-#[test]
-#[cfg(feature = "cadical")]
-fn cadical_phase_saving() {
-    let mut solver = solvers::CaDiCaL::default();
-    solver.set_option("lucky", 0);
-    phase_saving(solver);
-}
-
-#[test]
-#[cfg(feature = "glucose4")]
-fn glucosecore4_phase_saving() {
-    let solver = solvers::GlucoseCore4::default();
-    phase_saving(solver);
-}
-
-#[test]
-#[cfg(feature = "glucose4")]
-fn glucosesimp4_phase_saving() {
-    let solver = solvers::GlucoseSimp4::default();
-    phase_saving(solver);
-}
-
-#[test]
-#[cfg(feature = "minisat")]
-fn minisat_phase_saving() {
-    let solver = solvers::MinisatCore::default();
-    phase_saving(solver);
-}
-
-#[test]
-#[cfg(feature = "minisat")]
-fn minisatsimp_phase_saving() {
-    let solver = solvers::MinisatSimp::default();
-    phase_saving(solver);
-}
diff --git a/tests/solvers.rs b/tests/solvers.rs
deleted file mode 100644
index 84af8ca4..00000000
--- a/tests/solvers.rs
+++ /dev/null
@@ -1,170 +0,0 @@
-#![allow(dead_code, unused)]
-
-use rustsat::{
-    instances::{BasicVarManager, SatInstance},
-    solvers,
-    solvers::{Solve, SolverResult},
-};
-
-fn small_sat_instance<S: Solve>(mut solver: S) {
-    let inst: SatInstance<BasicVarManager> =
-        SatInstance::from_dimacs_path("./data/AProVE11-12.cnf").unwrap();
-    solver.add_cnf(inst.as_cnf().0);
-    let res = solver.solve().unwrap();
-    assert_eq!(res, SolverResult::Sat);
-}
-
-fn small_unsat_instance<S: Solve>(mut solver: S) {
-    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);
-    let res = solver.solve().unwrap();
-    assert_eq!(res, SolverResult::Unsat);
-}
-
-#[test]
-#[cfg(feature = "ipasir")]
-fn ipasir_small_sat() {
-    let solver = solvers::IpasirSolver::default();
-    small_sat_instance(solver);
-}
-
-#[test]
-#[cfg(feature = "ipasir")]
-fn ipasir_small_unsat() {
-    let solver = solvers::IpasirSolver::default();
-    small_unsat_instance(solver);
-}
-
-#[test]
-#[cfg(feature = "cadical")]
-fn cadical_small_sat() {
-    let solver = solvers::CaDiCaL::default();
-    small_sat_instance(solver);
-}
-
-#[test]
-#[cfg(feature = "cadical")]
-fn cadical_small_unsat() {
-    let solver = solvers::CaDiCaL::default();
-    small_unsat_instance(solver);
-}
-
-#[test]
-#[cfg(feature = "cadical")]
-fn cadical_sat_small_sat() {
-    let mut solver = solvers::CaDiCaL::default();
-    solver
-        .set_configuration(solvers::cadical::Config::SAT)
-        .unwrap();
-    small_sat_instance(solver);
-}
-
-#[test]
-#[cfg(feature = "cadical")]
-fn cadical_unsat_small_unsat() {
-    let mut solver = solvers::CaDiCaL::default();
-    solver
-        .set_configuration(solvers::cadical::Config::UNSAT)
-        .unwrap();
-    small_unsat_instance(solver);
-}
-
-#[test]
-#[cfg(feature = "kissat")]
-fn kissat_small_sat() {
-    let solver = solvers::Kissat::default();
-    small_sat_instance(solver);
-}
-
-#[test]
-#[cfg(feature = "kissat")]
-fn kissat_small_unsat() {
-    let solver = solvers::Kissat::default();
-    small_unsat_instance(solver);
-}
-
-#[test]
-#[cfg(feature = "kissat")]
-fn kissat_sat_small_sat() {
-    let mut solver = solvers::Kissat::default();
-    solver
-        .set_configuration(solvers::kissat::Config::SAT)
-        .unwrap();
-    small_sat_instance(solver);
-}
-
-#[test]
-#[cfg(feature = "kissat")]
-fn kissat_unsat_small_unsat() {
-    let mut solver = solvers::Kissat::default();
-    solver
-        .set_configuration(solvers::kissat::Config::UNSAT)
-        .unwrap();
-    small_unsat_instance(solver);
-}
-
-#[test]
-#[cfg(feature = "glucose4")]
-fn glucosecore4_small_sat() {
-    let solver = solvers::GlucoseCore4::default();
-    small_sat_instance(solver);
-}
-
-// Note: this instance seems too hard for glucose to solve
-#[test]
-#[ignore]
-#[cfg(feature = "glucose4")]
-fn glucosecore4_small_unsat() {
-    let solver = solvers::GlucoseCore4::default();
-    small_unsat_instance(solver);
-}
-
-#[test]
-#[cfg(feature = "glucose4")]
-fn glucosesimp4_small_sat() {
-    let solver = solvers::GlucoseSimp4::default();
-    small_sat_instance(solver);
-}
-
-// Note: this instance seems too hard for glucose to solve
-#[test]
-#[ignore]
-#[cfg(feature = "glucose4")]
-fn glucosesimp4_small_unsat() {
-    let solver = solvers::GlucoseSimp4::default();
-    small_unsat_instance(solver);
-}
-
-#[test]
-#[cfg(feature = "minisat")]
-fn minisatcore_small_sat() {
-    let solver = solvers::MinisatCore::default();
-    small_sat_instance(solver);
-}
-
-// Note: this instance seems too hard for minisat to solve
-#[test]
-#[ignore]
-#[cfg(feature = "minisat")]
-fn minisatcore_small_unsat() {
-    let solver = solvers::MinisatCore::default();
-    small_unsat_instance(solver);
-}
-
-#[test]
-#[cfg(feature = "minisat")]
-fn minisatsimp_small_sat() {
-    let solver = solvers::MinisatSimp::default();
-    small_sat_instance(solver);
-}
-
-// Note: this instance seems too hard for minisat to solve
-#[test]
-#[ignore]
-#[cfg(feature = "minisat")]
-fn minisatsimp_small_unsat() {
-    let solver = solvers::MinisatSimp::default();
-    small_unsat_instance(solver);
-}
diff --git a/tests/am1_encodings.rs b/tools/tests/am1_encodings.rs
similarity index 92%
rename from tests/am1_encodings.rs
rename to tools/tests/am1_encodings.rs
index 2f116749..55f1e771 100644
--- a/tests/am1_encodings.rs
+++ b/tools/tests/am1_encodings.rs
@@ -1,16 +1,15 @@
-#![cfg(incsolver)]
-
 use rustsat::{
     encodings::am1::{Encode, Pairwise},
     instances::{BasicVarManager, ManageVars},
     lit,
-    solvers::{self, Solve, SolveIncremental, SolverResult},
+    solvers::{Solve, SolveIncremental, SolverResult},
     types::{Lit, Var},
     var,
 };
+use rustsat_cadical::CaDiCaL;
 
 fn test_am1<AM1: Encode>(mut enc: AM1) {
-    let mut solver = solvers::new_default_inc_solver();
+    let mut solver = CaDiCaL::default();
     let mut var_manager = BasicVarManager::default();
     var_manager.increase_next_free(var![3]);
 
diff --git a/tests/card_encodings.rs b/tools/tests/card_encodings.rs
similarity index 96%
rename from tests/card_encodings.rs
rename to tools/tests/card_encodings.rs
index 65e29918..c0e6eaa2 100644
--- a/tests/card_encodings.rs
+++ b/tools/tests/card_encodings.rs
@@ -1,5 +1,3 @@
-#![cfg(incsolver)]
-
 use rustsat::{
     clause,
     encodings::card::{
@@ -8,14 +6,15 @@ use rustsat::{
     },
     instances::{BasicVarManager, ManageVars},
     lit,
-    solvers::{new_default_inc_solver, Solve, SolveIncremental, SolverResult},
+    solvers::{Solve, SolveIncremental, SolverResult},
     types::{Clause, Lit, Var},
     var,
 };
+use rustsat_cadical::CaDiCaL;
 
 fn test_inc_both_card<CE: BoundBothIncremental>(mut enc: CE) {
     // Set up instance
-    let mut solver = new_default_inc_solver();
+    let mut solver = CaDiCaL::default();
     solver.add_clause(clause![lit![0], lit![1]]).unwrap();
     solver.add_clause(clause![lit![1]]).unwrap();
     solver.add_clause(clause![lit![1], lit![2]]).unwrap();
@@ -90,7 +89,7 @@ fn test_inc_both_card<CE: BoundBothIncremental>(mut enc: CE) {
 
 fn test_both_card<CE: BoundBoth>(mut enc: CE) {
     // Set up instance
-    let mut solver = new_default_inc_solver();
+    let mut solver = CaDiCaL::default();
     solver.add_clause(clause![lit![0], lit![1]]).unwrap();
     solver.add_clause(clause![lit![1]]).unwrap();
     solver.add_clause(clause![lit![1], lit![2]]).unwrap();
@@ -125,7 +124,7 @@ fn test_both_card<CE: BoundBoth>(mut enc: CE) {
 /// Requires a cardinality encoding with upper and lower bounding functionality
 fn test_both_card_min_enc<CE: BoundBoth>(mut enc: CE) {
     // Set up instance
-    let mut solver = new_default_inc_solver();
+    let mut solver = CaDiCaL::default();
     let mut var_manager = BasicVarManager::default();
     var_manager.increase_next_free(var![4]);
 
diff --git a/tests/cnf.rs b/tools/tests/cnf.rs
similarity index 95%
rename from tests/cnf.rs
rename to tools/tests/cnf.rs
index 8c59d15a..9e3a0cb4 100644
--- a/tests/cnf.rs
+++ b/tools/tests/cnf.rs
@@ -1,11 +1,10 @@
-#![cfg(incsolver)]
-
 use rustsat::{
     instances::Cnf,
     lit,
-    solvers::{new_default_inc_solver, Solve, SolveIncremental, SolverResult},
+    solvers::{Solve, SolveIncremental, SolverResult},
     types::Lit,
 };
+use rustsat_cadical::CaDiCaL;
 
 #[test]
 fn cnf_implications() {
@@ -16,7 +15,7 @@ fn cnf_implications() {
 
     let mut cnf = Cnf::new();
     cnf.add_lit_impl_lit(a0, b0);
-    let mut solver = new_default_inc_solver();
+    let mut solver = CaDiCaL::default();
     solver.add_cnf(cnf).unwrap();
     let ret = solver.solve_assumps(vec![a0, b0]).unwrap();
     assert_eq!(ret, SolverResult::Sat);
@@ -29,7 +28,7 @@ fn cnf_implications() {
 
     let mut cnf = Cnf::new();
     cnf.add_lit_impl_clause(a0, vec![b0, b1]);
-    let mut solver = new_default_inc_solver();
+    let mut solver = CaDiCaL::default();
     solver.add_cnf(cnf).unwrap();
     let ret = solver.solve_assumps(vec![a0, b0, b1]).unwrap();
     assert_eq!(ret, SolverResult::Sat);
@@ -50,7 +49,7 @@ fn cnf_implications() {
 
     let mut cnf = Cnf::new();
     cnf.add_lit_impl_cube(a0, vec![b0, b1]);
-    let mut solver = new_default_inc_solver();
+    let mut solver = CaDiCaL::default();
     solver.add_cnf(cnf).unwrap();
     let ret = solver.solve_assumps(vec![a0, b0, b1]).unwrap();
     assert_eq!(ret, SolverResult::Sat);
@@ -71,7 +70,7 @@ fn cnf_implications() {
 
     let mut cnf = Cnf::new();
     cnf.add_cube_impl_lit(vec![a0, a1], b0);
-    let mut solver = new_default_inc_solver();
+    let mut solver = CaDiCaL::default();
     solver.add_cnf(cnf).unwrap();
     let ret = solver.solve_assumps(vec![a0, a1, b0]).unwrap();
     assert_eq!(ret, SolverResult::Sat);
@@ -92,7 +91,7 @@ fn cnf_implications() {
 
     let mut cnf = Cnf::new();
     cnf.add_clause_impl_lit(vec![a0, a1], b0);
-    let mut solver = new_default_inc_solver();
+    let mut solver = CaDiCaL::default();
     solver.add_cnf(cnf).unwrap();
     let ret = solver.solve_assumps(vec![a0, a1, b0]).unwrap();
     assert_eq!(ret, SolverResult::Sat);
@@ -113,7 +112,7 @@ fn cnf_implications() {
 
     let mut cnf = Cnf::new();
     cnf.add_cube_impl_clause(vec![a0, a1], vec![b0, b1]);
-    let mut solver = new_default_inc_solver();
+    let mut solver = CaDiCaL::default();
     solver.add_cnf(cnf).unwrap();
     let ret = solver.solve_assumps(vec![a0, a1, b0, b1]).unwrap();
     assert_eq!(ret, SolverResult::Sat);
@@ -150,7 +149,7 @@ fn cnf_implications() {
 
     let mut cnf = Cnf::new();
     cnf.add_clause_impl_clause(vec![a0, a1], vec![b0, b1]);
-    let mut solver = new_default_inc_solver();
+    let mut solver = CaDiCaL::default();
     solver.add_cnf(cnf).unwrap();
     let ret = solver.solve_assumps(vec![a0, a1, b0, b1]).unwrap();
     assert_eq!(ret, SolverResult::Sat);
@@ -187,7 +186,7 @@ fn cnf_implications() {
 
     let mut cnf = Cnf::new();
     cnf.add_clause_impl_cube(vec![a0, a1], vec![b0, b1]);
-    let mut solver = new_default_inc_solver();
+    let mut solver = CaDiCaL::default();
     solver.add_cnf(cnf).unwrap();
     let ret = solver.solve_assumps(vec![a0, a1, b0, b1]).unwrap();
     assert_eq!(ret, SolverResult::Sat);
@@ -224,7 +223,7 @@ fn cnf_implications() {
 
     let mut cnf = Cnf::new();
     cnf.add_cube_impl_cube(vec![a0, a1], vec![b0, b1]);
-    let mut solver = new_default_inc_solver();
+    let mut solver = CaDiCaL::default();
     solver.add_cnf(cnf).unwrap();
     let ret = solver.solve_assumps(vec![a0, a1, b0, b1]).unwrap();
     assert_eq!(ret, SolverResult::Sat);
diff --git a/tests/compression.rs b/tools/tests/compression.rs
similarity index 83%
rename from tests/compression.rs
rename to tools/tests/compression.rs
index 7cf36a6b..1f831c6b 100644
--- a/tests/compression.rs
+++ b/tools/tests/compression.rs
@@ -1,16 +1,15 @@
-#![cfg(feature = "compression")]
-
 use rustsat::{
     instances::{BasicVarManager, SatInstance},
+    solvers::Solve,
     solvers::SolverResult,
-    solvers::{self, Solve},
 };
+use rustsat_cadical::CaDiCaL;
 
 #[test]
 fn small_sat_instance_gzip() {
     let inst: SatInstance<BasicVarManager> =
         SatInstance::from_dimacs_path("./data/AProVE11-12.cnf.gz").unwrap();
-    let mut solver = solvers::new_default_solver();
+    let mut solver = CaDiCaL::default();
     solver.add_cnf(inst.as_cnf().0).unwrap();
     let res = solver.solve().unwrap();
     assert_eq!(res, SolverResult::Sat);
@@ -22,7 +21,7 @@ fn small_unsat_instance_gzip() {
         "./data/smtlib-qfbv-aigs-ext_con_032_008_0256-tseitin.cnf.gz",
     )
     .unwrap();
-    let mut solver = solvers::new_default_solver();
+    let mut solver = CaDiCaL::default();
     solver.add_cnf(inst.as_cnf().0).unwrap();
     let res = solver.solve().unwrap();
     assert_eq!(res, SolverResult::Unsat);
@@ -32,7 +31,7 @@ fn small_unsat_instance_gzip() {
 fn small_sat_instance_bz2() {
     let inst: SatInstance<BasicVarManager> =
         SatInstance::from_dimacs_path("./data/AProVE11-12.cnf.bz2").unwrap();
-    let mut solver = solvers::new_default_solver();
+    let mut solver = CaDiCaL::default();
     solver.add_cnf(inst.as_cnf().0).unwrap();
     let res = solver.solve().unwrap();
     assert_eq!(res, SolverResult::Sat);
@@ -44,7 +43,7 @@ fn small_unsat_instance_bz2() {
         "./data/smtlib-qfbv-aigs-ext_con_032_008_0256-tseitin.cnf.bz2",
     )
     .unwrap();
-    let mut solver = solvers::new_default_solver();
+    let mut solver = CaDiCaL::default();
     solver.add_cnf(inst.as_cnf().0).unwrap();
     let res = solver.solve().unwrap();
     assert_eq!(res, SolverResult::Unsat);
diff --git a/tests/constraints.rs b/tools/tests/constraints.rs
similarity index 97%
rename from tests/constraints.rs
rename to tools/tests/constraints.rs
index c58b79a7..9e69b88e 100644
--- a/tests/constraints.rs
+++ b/tools/tests/constraints.rs
@@ -1,14 +1,13 @@
-#![cfg(incsolver)]
-
 use rustsat::{
     instances::SatInstance,
-    lit, solvers,
+    lit,
     solvers::{Solve, SolveIncremental, SolverResult},
     types::{
         constraints::{CardConstraint, PBConstraint},
         Lit, RsHashMap,
     },
 };
+use rustsat_cadical::CaDiCaL;
 
 macro_rules! test_card {
     ( $constr:expr, $sat_assump:expr, $unsat_assump:expr ) => {{
@@ -16,7 +15,7 @@ macro_rules! test_card {
         inst.add_card_constr($constr);
         let (cnf, _) = inst.as_cnf();
         println!("{:?}", cnf);
-        let mut solver = solvers::new_default_inc_solver();
+        let mut solver = CaDiCaL::default();
         solver.add_cnf(cnf).unwrap();
         assert_eq!(
             solver.solve_assumps($sat_assump).unwrap(),
@@ -35,7 +34,7 @@ macro_rules! test_pb {
         inst.add_pb_constr($constr);
         let (cnf, _) = inst.as_cnf();
         println!("{:?}", cnf);
-        let mut solver = solvers::new_default_inc_solver();
+        let mut solver = CaDiCaL::default();
         solver.add_cnf(cnf).unwrap();
         assert_eq!(
             solver.solve_assumps($sat_assump).unwrap(),
diff --git a/tests/opb.rs b/tools/tests/opb.rs
similarity index 90%
rename from tests/opb.rs
rename to tools/tests/opb.rs
index f99aac51..5733bd40 100644
--- a/tests/opb.rs
+++ b/tools/tests/opb.rs
@@ -1,15 +1,11 @@
-#![cfg(solver)]
-
 use rustsat::{
     instances::{fio::opb::Options, SatInstance},
-    solvers::{self, Solve, SolverResult},
+    solvers::{Solve, SolverResult},
 };
+use rustsat_cadical::CaDiCaL;
 
-#[cfg(feature = "multiopt")]
 use rustsat::instances::MultiOptInstance;
-#[cfg(feature = "optimization")]
 use rustsat::types::RsHashMap;
-#[cfg(feature = "optimization")]
 use rustsat::{
     instances::{Objective, OptInstance},
     lit,
@@ -21,7 +17,7 @@ macro_rules! opb_test {
         let inst: SatInstance = SatInstance::from_opb_path($path, Options::default()).unwrap();
         let (cnf, _) = inst.as_cnf();
         println!("{:?}", cnf);
-        let mut solver = solvers::new_default_solver();
+        let mut solver = CaDiCaL::default();
         solver.add_cnf(cnf).unwrap();
         assert_eq!(solver.solve().unwrap(), $expect);
     }};
@@ -37,7 +33,6 @@ fn opb_tiny_unsat() {
     opb_test!("./data/tiny-unsat.opb", SolverResult::Unsat);
 }
 
-#[cfg(feature = "optimization")]
 #[test]
 fn opb_opt() {
     let inst: OptInstance =
@@ -60,7 +55,6 @@ fn opb_opt() {
     assert_eq!(inst, OptInstance::compose(true_constr, true_obj));
 }
 
-#[cfg(feature = "multiopt")]
 #[test]
 fn opb_multi_opt() {
     let inst: MultiOptInstance =
diff --git a/tests/pb_encodings.rs b/tools/tests/pb_encodings.rs
similarity index 96%
rename from tests/pb_encodings.rs
rename to tools/tests/pb_encodings.rs
index 9c792364..d510fe49 100644
--- a/tests/pb_encodings.rs
+++ b/tools/tests/pb_encodings.rs
@@ -1,5 +1,3 @@
-#![cfg(incsolver)]
-
 use rustsat::{
     clause,
     encodings::{
@@ -12,14 +10,15 @@ use rustsat::{
     },
     instances::{BasicVarManager, ManageVars},
     lit,
-    solvers::{new_default_inc_solver, Solve, SolveIncremental, SolverResult},
+    solvers::{Solve, SolveIncremental, SolverResult},
     types::{Clause, Lit, RsHashMap, Var},
     var,
 };
+use rustsat_cadical::CaDiCaL;
 
 fn test_inc_pb_ub<PBE: BoundUpperIncremental>(mut enc: PBE) {
     // Set up instance
-    let mut solver = new_default_inc_solver();
+    let mut solver = CaDiCaL::default();
     solver.add_clause(clause![lit![0], lit![1]]).unwrap();
     solver.add_clause(clause![lit![1]]).unwrap();
     solver.add_clause(clause![lit![1], lit![2]]).unwrap();
@@ -111,7 +110,7 @@ fn test_inc_pb_ub<PBE: BoundUpperIncremental>(mut enc: PBE) {
 
 fn test_pb_eq<PBE: BoundBothIncremental>(mut enc: PBE) {
     // Set up instance
-    let mut solver = new_default_inc_solver();
+    let mut solver = CaDiCaL::default();
     let mut var_manager = BasicVarManager::default();
     var_manager.increase_next_free(var![3]);
 
@@ -168,7 +167,7 @@ fn test_pb_eq<PBE: BoundBothIncremental>(mut enc: PBE) {
 
 fn test_pb_lb<PBE: BoundLower>(mut enc: PBE) {
     // Set up instance
-    let mut solver = new_default_inc_solver();
+    let mut solver = CaDiCaL::default();
     solver
         .add_clause(clause![!lit![0], !lit![1], !lit![2]])
         .unwrap();
@@ -199,7 +198,7 @@ fn test_pb_lb<PBE: BoundLower>(mut enc: PBE) {
 
 fn test_pb_ub_min_enc<PBE: BoundUpper>(mut enc: PBE) {
     // Set up instance
-    let mut solver = new_default_inc_solver();
+    let mut solver = CaDiCaL::default();
     let mut var_manager = BasicVarManager::default();
     var_manager.increase_next_free(var![4]);