- optimierte SAT-Kodierung für
binäre Addition, Multiplikation
- Optimierung von Parametern für
Constraint-Solver (innerhalb eines
Terminationsbeweisers)
- „didaktisch wertvolle``
Implementierungen (d. h. in Haskell)
wichtiger Algorithmen (DPLL, CDCL,
Fourier-Motzkin, DPLL(T))
- ...und daraus abgeleitete autotool-Aufgaben
- Verbesserung von satchmo-smt (bitblasting SMT solver)
- SAT-Kodierungen
in der Bioinformatik (RNA folding)
- SAT-Kodierungen für Zweipersonen(end)spiele
- SAT-Solver auf (hoch)paralleler Hardware
2014-03-31
