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.
Project description
rustsat - A Comprehensive SAT Library for Rust
rustsat
is a collection of interfaces and utilities for working with the boolean satisfiability problem in Rust.
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.
Crates
The RustSAT project is split up into multiple crates that are all contained in this repository. These are the crates the project consists of:
Crate | Description |
---|---|
rustsat |
The main library, containing basic types, traits, encodings, parsers, and more. |
rustsat-tools |
A collection of small helpful tools based on RustSAT that can be installed as binaries. For a list of available tools, see this directory with short descriptions of the tools in the headers of the files. |
rustsat-<satsolver> |
Interfaces to SAT solvers that can be used alongside rustsat . Currently interfaces are available for cadical , kissat , glucose , and minisat . |
Installation
To use the RustSAT library as a dependency in your project, simply run cargo add rustsat
.
To use an SAT solver interface in your project, run cargo add rustsat-<satsolver>
.
Typically, the version of the SAT solver can be selected via crate features, refer to the documentation of the respective SAT solver crate for details.
To install the binary tools in rustsat-tools
run cargo install rustsat-tools
.
Features
Feature name | Description |
---|---|
internals |
Make some internal data structures for e.g. encodings public. This is useful when basing a more complex encoding on the rustsat implementation of another encoding. Note that the internal API might change between releases. |
fxhash |
Use the faster firefox hash function from rustc-hash in rustsat . |
ipasir |
Include and link the IPASIR solver interface. |
optimization |
Include optimization (MaxSAT) data structures etc. |
multiopt |
Include data structures etc. for multi-objective optimization. |
compression |
Enable parsing and writing compressed input. |
bench |
Enable benchmark tests. Behind feature flag since it requires unstable Rust. |
rand |
Enable randomization features. (Shuffling clauses etc.) |
Examples
For example useage refer to the small example tools in the rustsat-tools
crate at tools/src/bin
. For a bigger
example you can look at this multi-objective optimization
solver.
For an example of how to use the C-API, see rustsat/examples/capi*.cpp
.
Versions
Note that at the current state of development, releases of RustSAT are not following semantic versioning, meaning the API can change between minor releases. For a more detailed changelog including all patch versions, see GitHub Releases.
Version 0.3.x
- Alternative totalizer implementation based on a totalizer database
- Dynamic polynomial watchdog encoing
- Changes to public API: changed some vectores to slices
- Changed internal variable/literal representation from
usize
tou32
Version 0.2.x
Solver interfaces factored out into seperate crates. See detailed changes in GitHub Releases.
Version 0.1.2
Updated initial version with working dependencies
Version 0.1.0 and 0.1.1
Yanked because of dependencies that don't exist anymore
Project details
Download files
Download the file for your platform. If you're not sure which to choose, learn more about installing packages.
Source Distribution
Built Distributions
Hashes for rustsat-0.4.0-cp37-abi3-win_amd64.whl
Algorithm | Hash digest | |
---|---|---|
SHA256 | 16b6a958dabcd1bc8d3fd868b3e6bba610447a60b8d694dff037ccda39089f3b |
|
MD5 | d7e1674f0934e3234f6cf880d1d6abfd |
|
BLAKE2b-256 | 5e90d5b1b13fec57754bd1f07e948ee6ad4590a686546caaf51b336d7709a719 |
Hashes for rustsat-0.4.0-cp37-abi3-win32.whl
Algorithm | Hash digest | |
---|---|---|
SHA256 | 11f89083ae22e4f0c0cd883bd5c195f7491f39719c1ed0d34f61595af88040db |
|
MD5 | 47e909b21f838c899c317dd884546948 |
|
BLAKE2b-256 | 6e96a382d64a365248bf5cb172ddd483b4393eb2c0eaac2c8b0c65d1ff930411 |
Hashes for rustsat-0.4.0-cp37-abi3-manylinux_2_17_x86_64.manylinux2014_x86_64.whl
Algorithm | Hash digest | |
---|---|---|
SHA256 | b1c494bb17022d80cb99dfe51f6cd7f7e277a819849735483ede2b0de9bd96dd |
|
MD5 | 29655002bd4619dfbf25619a10cec8fb |
|
BLAKE2b-256 | 28873ea6ca7fa00bb5fb5c420045d0d03f75a27cdee94f2733e299380c26238a |
Hashes for rustsat-0.4.0-cp37-abi3-manylinux_2_17_s390x.manylinux2014_s390x.whl
Algorithm | Hash digest | |
---|---|---|
SHA256 | 568472600db304afec99d43d7a2dc96d66e66b6c0d84f4eb9c456d9970a542a2 |
|
MD5 | 65e53ea9e7e6b0f721469d71e143e61f |
|
BLAKE2b-256 | 6b1fa35973fbcc1dfabfeab1db3239c957a25e6304c5815208442aa57f2b32d8 |
Hashes for rustsat-0.4.0-cp37-abi3-manylinux_2_17_ppc64le.manylinux2014_ppc64le.whl
Algorithm | Hash digest | |
---|---|---|
SHA256 | aefcbae057de4334201c0295cae39b908f2f04ba5c1317db765a9475e7a93b23 |
|
MD5 | d1a9d12716f8ef67bbf3a5d56f1ddac3 |
|
BLAKE2b-256 | 9e0667d9b77ee7076f2007a28dac88e8c43b1de0c0b3bb6f3df7c03621564bbc |
Hashes for rustsat-0.4.0-cp37-abi3-manylinux_2_17_armv7l.manylinux2014_armv7l.whl
Algorithm | Hash digest | |
---|---|---|
SHA256 | 1ed569833054aa7a5d2df2980f3e9676e01fd8cf3839697c89d4b8f1ad990daa |
|
MD5 | 9457c4229082b9690464234520d069b2 |
|
BLAKE2b-256 | 802d8dee04a41efadd8c99023f1b9834f8dce59a1ba43de21fe4168f5e4b2212 |
Hashes for rustsat-0.4.0-cp37-abi3-manylinux_2_17_aarch64.manylinux2014_aarch64.whl
Algorithm | Hash digest | |
---|---|---|
SHA256 | 9bed21b0a04574d7facf6ca3d0d107a2a613bfc3271c8b186caa341d8137b524 |
|
MD5 | 10662500b4c9dbec7601bcedcf38f342 |
|
BLAKE2b-256 | 1ec25503f0344ca29219dd51f73dd29b53d8c591e8e46274ce9118bc2fee8f3c |
Hashes for rustsat-0.4.0-cp37-abi3-manylinux_2_5_i686.manylinux1_i686.whl
Algorithm | Hash digest | |
---|---|---|
SHA256 | 69a62ab7c0593e55cc0075cc2c9139716497c46ec20bcc33dff5f67fab64cb92 |
|
MD5 | 431736a88dfa9cbd7ce7d795ff46e533 |
|
BLAKE2b-256 | e9f5bf05dc515bc0904c5487ac4f3d1e9ee46427e19a1cc9a06263191333e90d |
Hashes for rustsat-0.4.0-cp37-abi3-macosx_11_0_arm64.whl
Algorithm | Hash digest | |
---|---|---|
SHA256 | a2da8ad19c251781de59e5976ae80f42418f9e3f1cbfb157a98e1d1df7e1ae2a |
|
MD5 | 8e2983da1d0d4d74255bf961b6608eb8 |
|
BLAKE2b-256 | e6393d3c1877394d86bad3833ca10ed509ad3c9501777a19526455baa42d3c97 |
Hashes for rustsat-0.4.0-cp37-abi3-macosx_10_7_x86_64.whl
Algorithm | Hash digest | |
---|---|---|
SHA256 | 768f97da4e8994b3f89aeef8d8d1eaec4607ac92d44bdb3d9586de0919ef2805 |
|
MD5 | d2acdfa6c8c255a0226610ab765e1838 |
|
BLAKE2b-256 | 26cd99d7c5a988053f4c86d31d6ce41011a0212ff5c3267f01c4a9f3d10a8f71 |