You can receive the latest copy of the Riss and Coprocessor tool collection from http://tools.computational-logic.org
Please send bug reports to norbert.manthey@tu-dresden.de
All tools in this package are highly configurable. For a simple comparison, most techniques are disabled by default. Hence, you should specify options to use. For both Riss and Coprocessor, using -config=Riss427 is a fair starting point.
For a quick example on how to retrieve, build and use the solver on a Linux machine, have a look at doc/TUTORIAL.md!
This software package contains the SAT solver Riss, and might contain related tools:
| Tool | Description |
|---|---|
| Coprocessor | CNF simplifier |
| Priss | simple portfolio SAT solver |
The tool box uses CMake as build tool chain. In-source builds are not recommended. It is better to build the different build types (release, debug) in a separate directory.
To compile the project, libz is required, which can be installed for example with
sudo apt-get install zlib1g-devTo test the ipasir package, curl is required, which can be installed for example with
sudo apt-get install curl# Create a directory for the build
mkdir debug
cd debug/
# Create a debug build configuration
cmake -D CMAKE_BUILD_TYPE=Debug ..
# Create release build Intel compiler
cmake -D CMAKE_BUILD_TYPE=Release -D CMAKE_CXX_COMPILER=icpc ..
# If you want DRAT proof support, configure cmake the following
cmake -D DRATPROOF=ON ..
# You get a list of all targets with
make help
# Two different configurations of the riss solver
# (with and without simplification enabled)
make riss-simp
make riss-core
# Copy all scripts to the bin/ directory
make scriptsTo configure your build, pass the described options to cmake like this
cmake -D OPTION_NAME=value ..| Option | Description | Default |
|---|---|---|
| CMAKE_BUILD_TYPE | "Debug" or "Release" | Release |
| CMAKE_CXX_COMPILER | C++ compiler that should be used | g++ |
| STATIC_BINARIES | Build fully statically linked binaries | ON |
| WARNINGS | Set verbose warning flags | OFF |
| QUIET | Disable Wcpp | OFF |
Riss supports two different C interfaces, where one is the IPASIR interface, which has been set up for incremental track of the SAT Race in 2015. The actual interface of Riss supports a few more routines. Furthermore, Coprocessor's simplification can be used via a C interface.
After running cmake (see above), build the following library:
make riss-coprocessor-lib-staticThen, include the header file "riss/ipasir.h" into your project, and link against the library.
The available parameters can be listed for each tool by calling:
bin/<tool> --help
Due to the large number of parameters, a more helpful alternative is:
bin/<tool> --help -helpLevel=0 --help-verb
The configuration specification can be written to a pcs file automatically. Before using this file with an automated configuration framework, please check that only necessary parameters appear in the file. The procedure will include all parameters, also the cpu or memory limit parameters, and is currently considered experimental.
bin/ -pcs-file=
Using Riss to solve a formula <input.cnf> use
bin/riss <input.cnf> [solution] [solverOptions]
Using Riss to solve a formula <input.cnf> and generating a DRUP proof, the
following call can be used. Depending on the proof verification tool the option
-no-proofFormat should be specified. Note, not all formula simplification
techniques support generating a DRAT proof.
bin/riss <input.cnf> -proof=input.proof -no-proofFormat [solution] [solverOptions]
The script cp.sh provides a simple setup for using Coprocessor as a formula
simplification tool and afterwards running a SAT solver. The used SAT solver can
be exchanged by changing the variable satsolver in the head of the script.
bin/cp.sh <input.cnf> [coprocessorOptions]
The parallel portfolio solver priss uses incarnations of riss and executes them in parallel. To obtain a version that executes exact copies of the solver, issue the following call, and add the CNF formula as well. Furthermore, you might want to specify the number of used threads by adding "-threads=X"
bin/priss -ppconfig= -no-addSetup -no-pr -no-ps -psetup=PLAIN -pAllSetup=-independent