Riss - including Pcasso and Priss
Riss - including Pcasso and Priss
SAT Solver -- a programm that solves the satisfiability testing problem
People
- Norbert Manthey, Kilian Gebhardt, Aaron Stephan, Lucas Kalert, Franziska Krüger,
Research Groups
- Contact Sibylle Möhle
- http://tools.computational-logic.org
- Publication date July 1, 2012
Riss is a SAT solver (package) that is based on MiniSat 2.2 and Glucose 2.2 and uses the conflict driven clause learning algorithm. It furthermore includes the formula simplification tool Coprocessor, which can be used to simplify the formula before search, as well as during search. Riss includes many search algorithm extensions, and currently (2014) has about 500 parameters. Another feature of Riss is that it can emit unsatisfiability proofs in the DRAT format for almost all implemented techniques. These proofs can also be verified online while solving the actual problem.
The Riss framework furthermore includes a CNF formula feature extraction tool, so that equipped with a machine learning tool, a configuration of Riss can be chosen on a formula basis. Furthermore, there is the parallel portfolio solver Priss, which is also able to produce unsatisfiability proofs while respecting shared clauses.
Another parallel solving algorithm is included, iterative partitionin. The related system is called Pcasso. Instead of running multiple configurations of a solver on a single formula, Pcasso partitions the search space of the formula, an assigns solvers to each partition, as well as to the original formula. If there are idle resources, partitions are re-partitioned recursively. Furthermore, Pcasso does allow clause sharing. Inprocessing is currently not supported, but will be added in the near furture.
