Studienarbeit aus dem Jahr 2015 im Fachbereich Informatik - Internet, neue Technologien, Universit t Hildesheim (Stiftung), Sprache: Deutsch, Abstract: Es existieren verschiedene Werkzeuge und Algorithmen, die Variabilit tsmodelle in aussagenlogische Formeln bersetzen k nnen. Diese Formeln k nnen dann mithilfe von SAT-Solvern auf ihre Erf llbarkeit berpr ft werden. Als Anwendungsbeispiel dient das Variabilit tsmodell des Linux Kernels, das durch Verwendung von KConfig Dateien definiert und konfiguriert werden kann. Diese Arbeit vergleicht die vorhandenen Werkzeuge und Algorithmen, die KConfig-Modelle in das DIMACS oder CNF Format bersetzen. Der Vergleich basiert dabei auf der vorhandenen Literatur. Dabei wird insbesondere darauf eingegangen, ob die erstellten bersetzungen berhaupt korrekt sind, ob redundante Daten erzeugt werden und wie die Werkzeuge und Algorithmen mit nicht-Boolesche Elemente umgehen.