Sehr gute Platzierungen bei Solver-Competition

Im Rahmen der diesjährigen "21th International Conference on Theory and Applications of Satisfiability Testing" Konferenz (SAT '18) in Oxford, UK wurden die Freiburger Solver HQS und Pacose in den Kategorien DQBF bzw. MaxSAT ausgezeichnet.

Direktzugriff

Artikelaktionen

Bei den diesjährigen Evaluationen von QBF und MaxSAT im Rahmen der SAT-Konferenz gehören die an der TF entwickelten Solver HQS und Pacose zu den Spitzenreitern.

HQS wurde im Rahmen des DFG-Projekts "Solving Dependency Quantified Boolean Formulas" entwickelt [Wimmer et al. 2017]. Er ist ein Solver für sogenannte abhängigkeitsquantifizierte Boolesche Formeln (engl. Dependency Quantified Boolean Formulas, DQBF) und hat den diesjährigen DQBF-Track mit 172 gelösten Instanzen eindeutig dominiert (zum Vergleich: der zweitplatzierte Solver löste 118 Instanzen). DQBFs spielen beispielsweise eine Rolle in der Verifikation und Synthese von unvollständigen digitalen Schaltungen (siehe: http://www.qbflib.org/qbfeval18.php).

Pacose ist ein Solver zum Lösen von gewichteten Optimierungsproblemen der u. a. auf einer neuen Kodierung DPW [Paxian et al. 2018] basiert. Er konnte sich bei der diesjährigen MaxSAT Competition im internationalen Vergleich behaupten und einige Benchmark Kategorien eindeutig dominieren (siehe: https://maxsat-evaluations.github.io/2018/results/complete/weighted/summary.html).Weighted MaxSAT wird in der Arbeitsgruppe für Rechnerarchitektur u.a. verwendet um Pfade mit maximalem Stromverbrauch in Schaltkreisen zu berechnen [Sauer et al. 2016].

Fußzeile

Benutzerspezifische Werkzeuge