CryptoMiniSat

The Oracle solver (derived from SharpSAT-TD) optimizes assumption handling by avoiding the standard CDCL approach of backtracking to level 0 and replaying assumptions sequentially. Instead, it uses a Three-Tier Level Scheme to partition assignments by decision level, allowing assumptions to persist across multiple Solve() calls without being undone by standard backtracking.

Three-Tier Level Scheme

By recording an assignment in lit_val[] and vs[v].level without pushing it onto the decided[] trail, the assignment becomes invisible to UnDecide(k), effectively making it a persistent state that survives the rollback of the main CDCL search.

When using the Oracle solver, the Solve() method is designed to benefit from pre-set assumptions.

1. Pre-set assumptions: Any literals pre-set via SetAssumpLit are already assigned (LitVal == 1), so the solver skips them at zero cost during the assumption loop.
2. Dynamic assumptions: Any remaining dynamic assumptions are queued at level 2.
3. Single propagation wave: Instead of $N$ waves, a single Propagate(2) call handles all level 2 consequences simultaneously.
4. Persistent state: UnDecide(2) at the end of the call rolls back the CDCL search (levels $\ge 2$) but does not touch the watch-free, trail-free pre-set assumptions. This allows assumptions to persist into the next Solve() call.

TriState Oracle::Solve(const vector<Lit>& assumps, ...) {
    for (const auto& lit : assumps) {
        if (LitVal(lit) == -1) { UnDecide(2); return false; }
        else if (LitVal(lit) == 0) { Decide(lit, 2); }
        // LitVal(lit) == 1: pre-set by SetAssumpLit, skip entirely
    }
    Propagate(2);        // one single propagation wave for all assumptions
    HardSolve(...);
    UnDecide(2);         // rolls back CDCD search, not the pre-set assumptions
}

CryptoMiniSat uses CMake and automatically fetches cadical and cadiback dependencies. You only need to install gmp and zlib on your system.

1. Install System Dependencies

Debian/Ubuntu:

sudo apt-get install build-essential cmake ninja-build git libgmp-dev zlib1g-dev

macOS (Homebrew):

brew install cmake ninja gmp

Windows (MSYS2/MINGW64):

pacman -S mingw-w64-x86_64-gcc mingw-w64-x86_64-cmake mingw-w64-x86_64-ninja \
          mingw-w64-x86_64-gmp mingw-w64-x86_64-zlib git

2. Compile

Run these commands in your terminal:

git clone https://github.com/msoos/cryptominisat
cd cryptominisat
mkdir build && cd build
cmake -G Ninja -DCMAKE_BUILD_TYPE=Release ..
cmake --build .

To build a fully static binary (no shared-library dependencies at runtime), use the -DBUILD_SHARED_LIBS=OFF flag.

cd cryptominisat
mkdir build && cd build
cmake -G Ninja -DCMAKE_BUILD_TYPE=Release -DBUILD_SHARED_LIBS=OFF ..
cmake --build .

The build process uses scikit-build-core and CMake. CMake automatically handles cadical and cadiback dependencies. The only manual dependency required is GMP.

Linux Setup

Requires libgmp-dev (Debian/Ubuntu) or gmp-devel (RHEL/CentOS).

sudo apt-get install libgmp-dev   # or: yum install gmp-devel
python -m venv venv
source venv/bin/activate
pip install scikit-build-core cmake ninja build
pip install . --no-build-isolation

macOS Setup

Requires gmp via Homebrew.

brew install gmp
python -m venv venv
source venv/bin/activate
pip install scikit-build-core cmake ninja build
pip install . --no-build-isolation

Build a wheel without installing

To generate a standalone wheel in the dist/ directory:

python -m venv venv
source venv/bin/activate
pip install scikit-build-core cmake ninja build
python -m build --wheel --no-isolation

Note on Portability:

• macOS: Wheels are fully self-contained (GMP is bundled via delocate).
• Linux: Wheels depend on libgmp.so.10 (part of the manylinux ABI).