Riss: Unterschied zwischen den Versionen
Norbert Manthey (Diskussion | Beiträge) Keine Bearbeitungszusammenfassung |
Aaron Stephan (Diskussion | Beiträge) Keine Bearbeitungszusammenfassung |
||
| Zeile 4: | Zeile 4: | ||
|short description DE=SAT Solver - ein Programm, welches das Erfüllbarkeitsproblem löst | |short description DE=SAT Solver - ein Programm, welches das Erfüllbarkeitsproblem löst | ||
|contact persons=Norbert Manthey | |contact persons=Norbert Manthey | ||
|contributors=Norbert Manthey | |contributors=Norbert Manthey , Kilian Gebhardt, Aaron Stephan, Lucas Kalert, Franziska Krüger | ||
|link=http://tools.computational-logic.org | |link=http://tools.computational-logic.org | ||
|publication date=2012/07/01 | |publication date=2012/07/01 | ||
Version vom 18. März 2015, 15:14 Uhr
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 Norbert Manthey
- 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.
