The SAT Solving Package Riss
Author: Norbert Manthey
On this web page the development of the SAT solver and the co-developed tools is described, and the tools are explained. These tools include the parallel portfolio solver Priss with inprocessing and information sharing, the parallel search space partitioning solver Pcasso with inprocessign and information sharing, as well as the CNF formula simplifier Coprocessor with its front-ends for MaxSAT and QBF formulas.
Furthermore, we developed a CNF extraction tool, which furthermore can be used to predict a solver configuration for a given CNF formula. Based on Riss, Priss and Coprocessor, we furthermore developed the BMC solver ShiftBMC for hardware circuits.
Get the tool: Select one of the below versions and follow the instructions. Precompiled Windows binaries can be found for version Riss 3g.
Run the tool:
Note that all features of Riss and the included tools are turned off by default, effectively turning Riss into a basic CDCL solver without advanced extensions (and without CNF simplification).
From version Riss 4.27 on, the tool supports a simple configuration selection, previous versions have to be executed by enabling simplication by hand.
These instructions can be found below.
For more recent versions, just type
./riss -conf=Riss427 inputCNF
This command enables all techniques (with their current implementation), as they have been selected for version Riss 4.27.
Riss 5 (with Coprocessor, Qprocessor, Mprocessor, Priss, Pcasso and BlackBox)
The package of Riss 5 is available as binary, as the version that has been submitted to SAT Race 2015.
Riss 4.27 (with Coprocessor, Qprocessor, Mprocessor, ShiftBMC, Priss, Pcasso and BlackBox)
The available version of the SAT solver package Riss includes all the tools that have been developed based on the base SAT solver.
These tools include the forula simplifier Coprocessor, which can also be applied to QBF and MaxSAT formulas (Qprocessor and Mprocessor).
Furthermore, the CNF feature extraction, as has been used in Riss BlackBox, is embedded in the package.
Finally, the sequential solver is used in the Hardware model checker ShiftBMC.
The search space partitioning SAT solver Pcasso, as well as the portfolio solver Priss are also available from the source package.
Some of these tools (Riss, Priss, partially Coprocessor) support printing unsatisflity proofs in the DRAT format for unsatisfiable formulas. The solver engine alows to verify these proofs already online during search.
Usage of the SAT solver
A more detailed introduction to the SAT solver Riss and Coprocessor are given below for Riss 3g, and these information is still valid for Riss 4.27
How to run the tools? For some of the tools, there exists a calling script in the directory scripts.
How to find first help? Run the tool with the parameter --help (will print a very long list).
Riss3g and Coprocessor 3 (and the QBF front-end Qprocessor)
For convenience, pre-compiled windows binaries are provided (thanks to Axel Kemper for creating these binaries). Linux binaries can be downloaded from the SAT Competition web page.
From Riss2 to Riss3g
Preprocessing is important for CDCL SAT Solvers. Compared to the widely used SAT preprocessor SatElite, the new version of Coprocessor is capable of techniques that have been invented after the release of SatElite.
The major difference between riss 2 (see below) and Riss3g is the used solving engine -- while riss 2 used a module based SAT solving engine, which was modular but not competitive, Riss3g uses the solving engine of Glucose, which is based on Minisat, and thus this solving engine can be easily adopted to improvements that are proposed to Minisat or Glucose. Furthermore, Minisat or Glucose could be replaced by Riss3g, enabling other projects to use the strength of the built-in preprocessor. Additionally, the parameter interface of the tool has been moved to the Minisat format.
Since formula simplification is important, but techniques like variable elimination are expensive if executed until completion, a parallel version of this algorithm has been developed and is included in Coprocessor 3. Furthermore, subsumption and self-subsuming resolution can be run in parallel.
Usage of the SAT solver Riss3g
In this section a brief overview of the usage for the SAT solver is given to enable a quick and easy start with the tool. When no parameters are specified, the tool behaves as Glucose 2.2 with its default parameters.
How to use the tool for SAT solving? Run the solver with wanted parameters./riss3g INSTANCE MODEL
How to print UNSAT proofs? A restricted subset of techniques inside of Riss support the output of unsatisfiability proofs.
Hence, adding more parameters to the commandline of Riss might result in unsound proofs.
Especially, the CNF simplifier Coprocessor cannot be used (yet).
Instead, the internal implementation of the SatELite preprocessor is enabled when the riss3gSimp binary is used.
The supported proof format is DRUP.
A verifier for these formats are available from the SAT competition 2013 web page (EDACC verifier), as well as the pure implementation of Marijn Heule (drup-trim).
The restricted binary is riss3gSimp. Depending on the proof verifier, you might either be forced to print the used format (SAT competition), or not to print it (drup-trim).
Hence, one of the following two lines should be used:
To print the DRUP proof and also print the proof format (for the EDACC verifier): ./riss3gSimp input.cnf -drup=input.proof -no-enabled_cp3
To NOT print the proof format (for drup-trim): ./riss3gSimp input.cnf -drup=input.proof -no-proofFormat -no-enabled_cp3
What is a good parameter setup? Add the parameters described in the help section of Coprocessor below.
How get help without this web page? In the tar ball there is a README file that explains the basic usage of the tool. Furthermore, the compiled solver can display how to use its parameters if the parameter -help is added. For a more verbose help --help-verb can be passed on the commandline.
How to run the preprocessor alone? See the next section.
Usage of the CNF simplifier Coprocessor 3
Preprocessing is important for CDCL SAT Solvers. Compared to the widely used SAT preprocessor SatElite, the new version of Coprocessor is capable of techniques that have been invented after the release of SatElite. Furthermore, this tool allows to use SAT preprocessing for incremental SAT, PBO and MaxSAT for the first time, leading to performance boosts of these solvers as well.
Coprocessor is the build-in preprocessor of the SAT solver riss and has been extended such that it can be used as a standalone binary. This binary can be used to preprocess a formula in CNF and output the undo information as well. The tool can also be used to postprocess the model for the preprocessed formula to obtain a model for the original formula again.
Techniques that are implemented, but not present in SatElite include Failed Literal Probing, Blocked Clause Elimination, Hidden Tautology Elimination and some more. The aim of Coprocessor is to provide a simplifier that is able to run each technique independently or in a user order. This way, preprocessing techniques can be analyzed and optimized for certain use cases.
Since it is also valueable to preprocess SAT formulae, that should be used for optimization procedures (e.g. MaxSAT) or where clauses should be added afterwards, simplifying the formula can be very helpful to increase the overall speed. Coprocessor provides an interface that disallows to touch variables that are influenced by the optimization or by adding new clauses. This way, the simplification can still be executed on the remaining set of variables. Preliminary studies on PB and MaxSAT showed that this technique is valueable.
In this section a brief overview of the usage for the standalone preprocessor is given to enable a quick and easy start with the tool. Most of the presented parameters can also be used for the preprocessor when used before or during search. Note, all simplification techniques are turned off by default!
How to get the preprocessor? Download the version from above and extract the tar ball. To build the SAT solver run make coprocessor
How to compile the tool? See detailed instructions of the included README.md file
How to simplify a formula? By default the whole preprocessor is disabled and no simplification is executed. Depending on the parameters, Coprocessor 3 can output the simplified formula, and a file that stores the information to extend a model of the simplified formula into a model for the original input formula. A typical commandline looks like ./coprocessor INSTANCE -dimacs=OUTPUTFORMULA -cp3_undo=UNDOINFO
What is a good parameter setup? Additionally to the above parameters, the following command line seems to well for application instances.
If Coprocessor, or Riss is executed with
-enabled_cp3 -cp3_stats -up -subsimp -all_strength_res=3 -bva -cp3_bva_limit=120000 -bve -bve_red_lits=1 -no-bve_BCElim -unhide -no-cp3_uhdUHLE -cp3_uhdIters=5 -dense
This commandline enabled executes unit propagation, unhiding (Unhide), bounded variable addition (BVA) and bounded variable elimination (BVE) in this order. Finally, the gaps in the variables of the formula are closed, which reduces the maximum variable of the formula. Furthermore, for ternary clauses all self-subsuming resolvents are produced. BVA is limited to touch 120000 clauses. BVE reduces the number of clauses, and does not apply blocked clause elimination. Finally, unhiding is not executing unhiding literal elimination and uses five iterations of the unhiding algorithm. After all simplifications have been executed, the preprocessor prints statistics about the execution and effects of single simpification techniques.
How to create a model for the input formula? If the simplified formula has been solved by some SAT solver, the model can be extended for a model of the input formula again. The model needs to be given to the preprocessor via a file. A possible command line can look like ./coprocessor -cp3_post -cp3_undo=UNDOINFO -cp3_model=MODELFILE
Note Coprocessor accepts both the format of SAT competitions and the format of Minisat as models.
Note that you do not need to extend a model, if the formula is unsatisfiable.
Note that you do need the UNDOINFO file, if a correct model should be created.
How to run variable elimination in parallel? To run variable elimination in parallel, a number of threads needs to be specified. An example command line is./coprocessor INSTANCE -dimacs=MODEL -enabled_cp3 -bve -cp3_threads=N , where N is the number of threads that should be used.
How to run single techniques? The preprocessor enables access to the implemented techniques. Each technique is represented by a single letter. The following list shows the letters and the associated techniques:
u - Boolean Constraint Propagation
s - Self-Subsuming Resolution
v - Variable Elimination
w - Variable Addition
e - Equivalent Literal Elimination
h - Hidden Tautology Elimination
c - Covered Clause Elimination
p - Probing and Failed Literal Detection
x - XOR detection and gaussian elimination
f - Cardinality constraint detection and Fourier-Motzkin reasoning
To choose a technique that should be executed, the parameter -cp3_ptechs has to be specified on the commandline. For running a set of techniques until completion, the corresponding set of letters can be surrounded by '[' and ']+'.
Note, that nested brackets cannot be handled correctly.
Note, each technique that should be used has to be enabled also via the commandline.
This syntax tells the simplifier that it should run the sourrounded techniques until no simplifications can be executed any more. To simplify the formula with Boolean Constraint Propagation, Self-Subsuming Resolution and Equivalent Literal Elimination, type -cp3_ptechs=[use]+.
Pcasso - a Parallel CooperAtive Sat SOlver
Recent parallel SAT solvers are based on the portfolio approach, which simply executes different solvers in parallel. Since these solvers can have different strength, a lucky portfolio solver might contain a configuration of a solver that can solve the current input formula fast. Therefore, the overall performance of these solvers is comparably fast. However, the approach is limited, because all solvers solve the same input formula, and the approach scales only with the number of available cores. To overcome this issue, search space partitioning SAT solvers have been proposed (see splitter). Where splitter was only a research implementation that shows that search space partitioning scales better than the portfolio approach, Pcasso is an improved version of this tool, incorporating sophisticated techniques to make it competitive to modern portfolio SAT solvers.
A brief system description of the parallel partitioning solver Pcasso is available here
The SAT Solver Framework priss (version 2)
The framework includes the modern preprocessor Coprocessor, which implements most of the recently published preprocessing techniques. The included CDCL solver riss can use components such as unit propagation or a decision heuristic from external libraries. Furthermore, riss is able to simplify the input formula during search and implements many other extensions that have been proposed to the CDCL algorithm. The parallel framework runs solvers in parallel and allows the communication of clauses and equivalent literals. Based on the idea in ppfolio, we also added ssa, an improved Sparrow-like SLS solver with an up to doubled flips per second ratio, to the portfolio and allow communication among the two solving paradigms.
A brief system description of the CDCL solver riss is available here
Usage of the SAT solver
In this section a brief overview of the usage for the solver is given to enable a quick and easy start with the tool.
How to get the SAT solver? Follow this link download and extract the tar ball.
How to get the parallel SAT solver? Follow this link download and extract the tar ball.
How to use the tool for solving SAT? To run the solver type ./riss INSTANCE or ./priss INSTANCE for the parallel solver.
Can I use parameters? To list available parameters, type ./riss --help or ./priss --help. We will soon add a more detailed list of parameters here.