SAT-Solver für Formeln in XNF

In diesem Vortrag führen wir die XOR-OR-AND-Normalform (XNF) für logische Formeln ein und präsentieren einen ersten Algorithmus zur Lösung jener. Die XNF verallgemeinert die wohlbekannte konjunktive Normalform, indem sie Literale durch XORs von Literalen, so genannte Linerale, ersetzt. Wir präsentieren Methoden zur Konvertierung Boolescher Polynomsysteme zu Formeln in 2-XNF, also Formeln in XNF, bei denen jede Klausel maximal zwei Linerale enthält. Experimente mit dem Verschlüsselungssystem ASCON-128 zeigen, dass Verschlüsselungssysteme mit vielen XOR-Operationen durch die XNF effizienter dargestellt werden können als mit herkömmlichen Konvertierungsmethoden. Anschließend präsentieren wir 2-Xornado, unseren neuen Graph-basierten SAT-Solver zur Lösung von Formeln in 2-XNF. Wir vergleichen 2-Xornado mit herkömmlichen SAT-Solvern mit XOR-Unterstützung und algebraischen Solvern für Boolesche Polynome anhand von Beispielen aus der Kryptoanalyse.