rustsat

Crates.io	rustsat
lib.rs	rustsat
version	0.6.1
source	src
created_at	2023-07-11 11:50:15.889028
updated_at	2024-10-16 14:41:04.70735
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.
homepage
repository	https://github.com/chrjabs/rustsat
max_upload_size
id	913734
size	7,607,994

Christoph Jabs (chrjabs)

documentation

README

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 of 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.

Example

let mut instance: SatInstance = SatInstance::new();
let l1 = instance.new_lit();
let l2 = instance.new_lit();
instance.add_binary(l1, l2);
instance.add_binary(!l1, l2);
instance.add_unit(l1);
let mut solver = rustsat_minisat::core::Minisat::default();
solver.add_cnf(instance.as_cnf().0).unwrap();
let res = solver.solve().unwrap();
assert_eq!(res, SolverResult::Sat);
let sol = solver.full_solution().unwrap();
assert_eq!(sol[l1.var()], TernaryVal::True);
assert_eq!(sol[l2.var()], TernaryVal::True);

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`.
`rustsat-ipasir`	IPASIR bindings to use any compliant solver with `rustsat`.

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
`optimization`	Include optimization (MaxSAT) data structures etc.
`multiopt`	Include data structures etc. for multi-objective optimization.
`compression`	Enable parsing and writing compressed input.
`fxhash`	Use the faster firefox hash function from `rustc-hash` in `rustsat`.
`rand`	Enable randomization features. (Shuffling clauses etc.)
`ipasir-display`	Changes `Display` trait for `Lit` and `Var` types to follow IPASIR variables indexing.
`bench`	Enable benchmark tests. Behind feature flag since it requires unstable Rust.
`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.

Examples

For example usage 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.

Python Bindings

This library also comes with experimental Python bindings to use its encodings from Python. The Python bindings are available at PyPI. For more details see the Python API documentation.

Contributing

We are welcoming contributions in the form of pull requests and suggestions. Kindly make sure to read CONTRIBUTING.md first.

Commit count: 546