Erfüllbarkeitsproblem und Varianten

Ich bin Norbert Manthey, ein Softwareentwickler mit Interesse für systemnahe Programmierung in C++ und C. Ich arbeite für Amazon AWS. In meiner Freizeit entwickle ich Constraint Solver. Während der Entwicklung bevorzuge ich kleine inkrementelle Änderungen, und Prototypen-Entwicklung, habe aber auch mit statischer Analyse, typischen Programmierfehlern und deren Behebung Erfahrung. Manuelle Schritte führe ich meist genau einmal durch, und skripte beziehungsweise automatisiere sie für die nächsten Iterationen.

Während meines Studiums und für meine Doktorarbeit habe ich einen eigenen SAT Solver - Riss - implementiert, sowie ihn auf viele Probleme angewendet. Dabei habe ich Formelvereinfachungstechniken entwickelt, sowie parallele Suchverfahren. Riss kann inzwischen als Löser in weiteren Werkzeugen verwendet werden, welche verwandte Probleme Lösen, unter anderem MaxSAT oder MUS, sowie Hardware- und Softwaremodelchecker.

Meine Doktorarbeit beschreibt viele Facetten des Erfüllbarkeitsproblems, von abstrakten Lösungsmodellen über Eigenschaften und Kodierungsvorschlägen bis hin zu sequentiellen und parallelen Lösungsansätzen und Formelvereinfachungen.

Die implementierten Systeme sammle ich auf github.