zum Inhalt springen

SAT-Solving

Im Rahmen des SAT-Solving-Projekts beschäftigen wir uns mit der Entwicklung von Algorithmen zum exakten Lösen des NP-vollständigen aussagenlogischen Erfüllbarkeitsproblems, kurz SAT. Es wurden sowohl sequentielle als auch parallele  SAT-Solver entwickelt.

Bei unserem Solver satUZK handelt es sich um einen vollständigen, CDCL-basierten SAT-Solver. Neben den üblichen Algorithmen und Datenstrukturen des modernen SAT-Solving wird satUZK von folgenden Techniken unterstützt: Restarts, Conflict Clause Strengthening sowie Pre- und Inprocessing Algorithmen wie z.B. Bounded Variable Elimination durch Resolution, Subsumption, Blocked Clause Elimination, Distillation und Unhiding.

Darauf basierend wurde eine parallele Version des Solvers entwickelt, bei welcher mehrere Instanzen von satUZK auf jeweils einem CPU-Core gestartet werden. Diese tauschen untereinander gelernte Klauseln über Shared-Memory aus. Der Austausch erfolgt entweder direkt oder über einen so genannten Reducer, der versucht die eingehenden Klauseln zu verkürzen. Eine Reducer-Instanz kann dabei einen separaten CPU-Core verwenden.

Im Projekt wurde außerdem ein Portfolio-basierter SAT-Solver pfolioUZK entwickelt. Es handelt sich dabei um einen Ansatz, in dem mehrere Instanzen von bekannten, sequentiellen und parallelen SAT-Solvern (aus dem so genannten Portfolio) auf den im System verfügbaren CPU-Cores gestartet werden. Alle Solver-Instanzen versuchen dann parallel und unabhängig voneinander, d.h. ohne jegliche Kommunikation untereinander, das SAT-Problem zu lösen.

Downloads

 

Auszeichnungen

Unsere Solver wurden bereits bei folgenden internationalen Wettbewerben ausgezeichnet:

  • SAT Competition 2013: Bronzemedaille in der Kategorie Core solvers, Sequential, Application SAT für den Solver satUZK
  • SAT Challenge 2012: Bester Sovler in der Kategorie Parallel Track: Application SAT+UNSAT für den Solver pfolioUZK

 

Veröffentlichungen

  • van der Grinten, Alexander; Wotzlaw, Andreas; Speckenmeyer, Ewald: satUZK: Solver Description. In: Belov, A.; Diepold, D.; Heule, M. J. H.; Järvisalo, M. (Ed.), Proceedings of SAT Competition 2014: Solver and Benchmark Descriptions. Department of Computer Science Series of Publications B, Volume B-2014-2, University of Helsinki
  • Wotzlaw, Andreas; van der Grinten, Alexander; Speckenmeyer, Ewald: Effectiveness of pre- and inprocessing for CDCL-based SAT solving. CoRR abs/1310.4756, 2013.
  • van der Grinten, Alexander; Wotzlaw, Andreas; Speckenmeyer, Ewald: satUZK: Solver Description. In: Balint, A.; Belov, A.; Heule, M. J. H.; Järvisalo, M. (Ed.), Proceedings of SAT Competition 2013: Solver and Benchmark Descriptions. Department of Computer Science Series of Publications B, Volume B-2013-1, University of Helsinki.
  • Wotzlaw, Andreas; van der Grinten, Alexander; Speckenmeyer, Ewald; Porschen, Stefan: pfolioUZK: Solver Description. In: Balint, A.; Belov, A.; Diepold, D.; Gerber, S.; Järvisalo, M.; Sinz, C. (Ed.), Proceedings of SAT Challenge 2012: Solver and Benchmark Descriptions, Volume B-2012-2 of Department of Computer Science Series of Publications B, University of Helsinki.
  • van der Grinten, Alexander; Wotzlaw, Andreas; Speckenmeyer, Ewald; Porschen, Stefan: satUZK: Solver Description. In: Balint, A.; Belov, A.; Diepold, D.; Gerber, S.; Järvisalo, M.; Sinz, C. (Ed.), Proceedings of SAT Challenge 2012: Solver and Benchmark Descriptions, Volume B-2012-2 of Department of Computer Science Series of Publications B, University of Helsinki.
  • van der Grinten, Alexander: Preprocessing- und Inprocessing-Techniken in CDCL-basierten SAT-Solvern, Bachelorarbeit, Univ. Köln, 2012.

 

Abschlussarbeiten: Im Rahmen des Projekts bieten wir Themen für Abschlussarbeiten aus dem Bereich Effiziente Algorithmen, Kombinatorik und Parallele Programmierung an. Sollten Sie Interesse an einer Mitarbeit haben, wenden Sie sich bitte an Andreas Wotzlaw.