Quelltext der Seite Riss

{{DataOrTool
|name=Riss - including Pcasso and Priss
|short description EN=SAT Solver -- a programm that solves the satisfiability testing problem
|short description DE=SAT Solver - ein Programm, welches das Erfüllbarkeitsproblem löst
|contact persons=Sibylle Möhle; 
|contributors=Norbert Manthey, Kilian Gebhardt, Aaron Stephan, Lucas Kalert, Franziska Krüger,
|link=http://tools.computational-logic.org
|publication date=2012/07/01
|long description EN=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.
|long description DE=Riss ist ein SAT Solver (Softwarepaket), welches auf MiniSat 2.2 und Glucose 2.2 basiert, und welches the conflict driven clause learning Algorithmus verwended. Riss beherbergt außerdem den Formelvereinfacher Coprocessor, der Formeln vor, und während, der Suche bearbeiten kann. Riss schließt viele Suchalgorithmuserweiterungen ein, und enthält im Moment (2014) circa 500 Parameter. Während der Suche kann Riss einen Unerfüllbarkeitsbeweis im DRAT-Format generieren, sodass sowohl Antworten für erfüllbare, als auch für unerfüllbare Probleme überprüft werden können. Diese Beweise können auch schon während der Suche überprüft werden.

Das Softwarepaket enthält außerdem ein Werkzeug, welches Features der CNF-Formel extrahieren kann, sodass zusammen mit einem Machine-Learning Werkzeug eine Konfiguration für Riss basierend auf der gegebenen Formel ausgewählt werden kann. Weiterhin ist der paralleler Portfolio-Solver Priss enthalten, welcher auch Unerfüllbarkeitsbeweise während der parallelen Suche ausgeben kann, wobei geteilte Klauseln berücksichtigt werden.

Ein weitere paralleler Lösungsansatz ist enthalten, Iterative Partitioning. Das dazugehörige System pcasso lässt nicht mehrere Solver auf der Formel laufen, sondern unterteilt den Suchraum des Problems in Partitionen, und weist anschließend jeder Partition einen sequentiellen Solver zu. Zusätzlich wird die originale Formel gelöst. Wenn weitere Resourcen zur Verfügung stehen, werden die Partitinoen ihrerseite wieder unterteilt und parallel zu den anderen Partitionen gelöst. Pcasso kann außerdem gelernte Klauseln teilen. Formelvereinfachung während der Suche werden im Moment nicht unterstützt.
|Forschungsgruppe=Wissensverarbeitung
|dataOrTool=Tool
|Projektstatus=abgeschlossen
}}