Algorithm Engineering für MONET und verwandte Abdeckungsprobleme
Zusammenfassung der Projektergebnisse
Vergleichende Studie bekannter Algorithmen. Wir haben viele bekannte MONET-Algorithmen miteinander verglichen. Dabei haben wir versucht, die einzelnen Unterschiede herauszuarbeiten und getestet, welche Merkmale zu den größten Laufzeitunterschieden führten. Zu Beginn haben wir uns auf Multiplikationsalgorithmen konzentriert. Bei der Vielzahl an Multiplikationsalgorithmen stellt sich heraus, dass der theoretische Flaschenhals - die Größe des Zwischenergebnisses - zwar korrekt ist, aber durch keinen der Ansätze signifikant verbessert wird. Vielmehr dominiert hier der DL-Algorithmus, da er versucht die Minimierung der Formeln eleganter zu lösen. Unsere Ergebnisse zeigen, dass die Stellschraube Formeminimierung signifikante Vebesserungen bringt. Weiterhin haben wir die beiden FK-Algorithmen untersucht. Hierbei haben wir die Algorithmen durch verschiedene Parameter ergänzt und untersucht, wie sich dieser Parameter auf die Algorithmen auswirken. Wir haben dafür einzelne Methoden aus der SAT-Community verwendet und versucht, einige Konzepte verschiedener SAT-Algorlthmen zu verwenden. Wir konnten feststellen, dass die Wahl einer geschickten Variable für den Algorithmus FK-B signifikant für die Laufzeit ist. Der Algorithmus FK-A ist davon nicht betroffen. Außerderm führten uns die Experimente mit den FK-Algorithmen anschließend zu einer SAT-Formulierung. Experimente für neue Ansätze. Zunächst wurde eine Verbesserung der Multiplikation mit Minimalitätsüberprüfung untersucht. Leider stellte sich heraus, dass einige erarbeitete Ideen kurze Zeit später in CoRR erschienen sind. Daraufhin haben wir den Fokus aufdie FK-Algorithmen gelegt, was uns zu einer SAT-Formulierung führte. Die Experimente zeigten, dass dieser Ansatz vielversprechend ist. Außerdem konnten wir den damit verbundenen Schnitttest durch Verwendung der Multiplikationsansätze verbessern. Instanzen. Neben den bekannten Instanzen konstruierten wir einige Instanzen aus dem Data-Mining. Dazu verwendeten wir Daten aus dem UC Irvine Machine Learning Repository (UCI) und dem Frequent Itemset Mining Implementations Repository (FIMI). Die Instanzen sind im Repository von Takeaki Uno zu finden. Außerdem konnten wir die durch die SAT-Reduktion produzierten Instanzen für die SAT-Community zur Verfügung stellen. Diese sind auf reges Interesse gestoßen! Einfache Fälle. Wir haben begonnen, den in Poylnomialzeit lösbaren Fall degenerierter Instanzen zu Implementieren. Wir erhofften uns aufschlussreiche Ergebnisse für die Multiplikationsalgorithmen, da wir mit Hilfe eines solchen Algorithmus' versuchen wollten, günstige Permutationen für die Multiplikationsalgorithmen zu finden. Die Implementierung konnte bisher nicht abgeschlossen werden.
Projektbezogene Publikationen (Auswahl)
- How to apply SAT-solving for the equivalence test of monotone normal forms, Theory and Applications of Satisfiability Testing (SAT '11) , Ann Arbor, 2011. LNCS
Martin Mundhenk and Robert Zeranski
- Upward Planarity via SAT, 20th International Symposium on Graph Drawing (GD '12), Redmond, 2012. LNCS
Markus Chimani and Robert Zeranski
