Riss - including Pcasso and Priss
Riss - including Pcasso and Priss
SAT Solver - ein Programm, welches das Erfüllbarkeitsproblem löst
Personen
- Norbert Manthey, Kilian Gebhardt, Aaron Stephan, Lucas Kalert, Franziska Krüger,
Gruppen
- Kontaktperson Sibylle Möhle
- http://tools.computational-logic.org
- Veröffentlichungsdatum 1. Juli 2012
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.
