rsat

SolHop SAT and MaxSAT Solver.

Currently, a stochastic local search based on probSAT and a CDCL solver based on MiniSAT has been implemented. More algorithms will be available soon.

This projetct is still in development. The APIs can change a lot before the first stable release v1.0.0.

Install and Run

Install

sh cargo install rsat

Help

```sh $ rsat --help rsat 0.1.6 SolHOP SAT and MaxSAT Solver

USAGE: rsat [FLAGS] [OPTIONS]

FLAGS: -h, --help Prints help information -p, --parallel Enables data parallelism (currently only for sls solver) -V, --version Prints version information

OPTIONS: -a, --alg Algorithm to use (1 -> CDCL, 2 -> SLS) [default: 1] --max-flips Maxinum number of flips in each try of SLS [default: 1000] --max-tries Maximum number of tries for SLS [default: 100]

ARGS: Input file in DIMACS format ```

Usage

sh rsat input.cnf -a 1

where input.cnf is the input SAT instance in DIMACS format. Use -a 2 to invoke the SLS solver. Also see help for some options.

Below are some examples:

Example 1

Input

txt c comment p cnf 3 4 1 0 -1 -2 0 2 -3 0 -3 0

Output

txt SAT 1 -2 -3 0

Example 2

Input

txt c comment p cnf 3 4 1 0 -1 -2 0 2 -3 0 3 0

Output

txt UNSAT

Note: The SLS solver will never be available to prove UNSAT. It will give the best model that has been found so far.

txt UNKNOWN -1 2 3 0

License

MIT