#sat #solver #logic #satisfiability #minisat

sys cadical

Rust bindings for the CaDiCaL SAT solver

14 releases

0.1.14 Nov 25, 2022
0.1.13 Oct 30, 2020
0.1.12 Jun 18, 2020

#187 in Math

Download history 49/week @ 2023-11-04 43/week @ 2023-11-11 42/week @ 2023-11-18 124/week @ 2023-11-25 17/week @ 2023-12-02 47/week @ 2023-12-09 36/week @ 2023-12-16 56/week @ 2023-12-23 31/week @ 2023-12-30 27/week @ 2024-01-06 41/week @ 2024-01-13 135/week @ 2024-01-20 84/week @ 2024-01-27 18/week @ 2024-02-03 72/week @ 2024-02-10 276/week @ 2024-02-17

455 downloads per month
Used in 5 crates (4 directly)

MIT license

18K SLoC

C++ 17K SLoC // 0.2% comments Rust 524 SLoC

CaDiCaL SAT solver

Build Status Crate Documentation GitHub

This is a stand alone crate that contains both the C++ source code of the CaDiCaL incremental SAT solver together with its Rust binding. The C++ files are compiled and statically linked during the build process. This crate works on Linux, Apple OSX, Windows, Android, iOS, Raspberry Pi, NetBSD and FreeBSD.

CaDiCaL won first place in the SAT track of the SAT Race 2019 and second overall place. It was written by Armin Biere, and it is available under the MIT license.

The literals are unwrapped positive and negative integers, exactly as in the DIMACS format. The common IPASIR operations are presented in a safe Rust interface.

let mut sat: cadical::Solver = Default::default();
sat.add_clause([1, 2]);
sat.add_clause([-1, 2]);
assert_eq!(sat.solve(), Some(true));
assert_eq!(sat.value(2), Some(true));

The C++ library is build with assertions disabled and with optimization level 3 by default. C++ assertions are enabled only when cargo is building a debug version and the cpp-debug feature of the library is enabled.