In den letzten 15 Jahren ist immer noch kein anderer auf den Gedanken gekommen, die speziellen Eigenschaften des kontrollierten Ausmultiplizierens im Kontext der Modulo-2-Arithmetik zu untersuchen, was nicht weiter verwunderlich ist, da eine tiefere Analyse mit Bleistift und Papier praktisch unmöglich ist. Daher denke ich, dass ich die Arbeit wohl selbst leisten muss.
Meine Zielvorstellung ist es, den Stand der Dinge auf arXiv.org veröffentlichen. Für das Sponsoring ist mein Sohn Moritz bereit, seinen guten Namen herzugeben.
Welche Themen am interessantesten sind und wann ein veröffentlichswürdiger Stand erreicht ist, kann ich leider nur schlecht beurteilen. Speziell beim Formulieren von Beweisen fällt es mir schwer, zu erkennen wann etwas genügend bewiesen ist. Es ist daher nicht unbedingt notwendig sich mit der Materie gut auszukennen, um mir mit Anmerkungen wie “Beweis fehlt”, “Definition nicht vollständig”, “Zuviel des Guten”, “Zu wenig Information”, etc. auf die Sprünge zu helfen.
Der aktuellste Stand ist unter dem Titel Structural Single State Mutinex Logic abrufbar.
Eine informelle Einführung in die Grundlage des schrittweisen Ausmultiplizierens ist in [SCH2013CDF] zu finden.
In chapter Emacs Package ist ein Anwendungsbeispiel, das hoffentlich gut illustriert, wie die Matrix funktioniert und Verfahren wie Kavanaugh-Maps durch eine systematische fehlerresistente Lösung ersetzt.
Der Arbeitstitel erklärt sich aus der Tatsache, dass Begriffe wie “structural logic” und “state logic” bereits mit anderen Konzepten belegt sind. Nach verschiedenen Versuchen meine Erkenntnisse zu formulieren habe ich bewusst einen induktiven Beweis mit eigener Nomenklatur gewählt, da es sonst immer wieder passiert, dass Schlussfolgerungen aus anderen Bereichen der Logik unterstellt werden, die innerhalb der Satoku Matrix nur bedingt gültig, bzw. nicht relevant sind.
Meiner Meinung nach ist eine wichtige Erkenntnis, dass die Erfüllbarkeit eines 2-SAT Problems bei der Satoku Matrix bereits mit der Konsolidierung der Anfangsmatrix nachgewiesen oder widerlegt ist.
Es ist kein “Suchlauf” nötig um irgendeine Belegung zu finden. Das Ermitteln einer Belegung entspricht in diesem Kontext der Reduktion der k-SAT-Matrix auf eine 1-SAT Matrix. Diese Reduktion ist zwar möglich, zum Nachweis der Erfüllbarkeit aber völlig unnötig.
Insgesamt treten Variablen und deren Belegung bei den Verfahren innerhalb der Matrix komplett in den Hintergrund.
Durch die Konsolidierung der Matrix werden eine Reihe von Algorithmen möglich, die in dieser Form weder in der reinen Graphentherie noch in der mathematischen Logik/Booleschen Algebra realisiert werden können.
Mit dem Nachweis, dass konsolidierte 2-SAT-Klauseln keine versteckten Widersprüche enthalten können, ist es möglich alle 2-SAT-Klauseln in den Verfahren zur Lösungsermittlung unberücksichtigt zu lassen. Das gilt nicht für Resolutionsverfahren mit conflict-driven clause learning (CDCL).
Die Untersuchung von ca. 11000 schweren Problemen aus dem Bereich 9x9 Sudoku zeigt, dass es mit einem kleinen Satz von simplen Algorithmen mit polynomieller Laufzeit möglich ist, diese Sudokus ohne Raten und Backtracking zu lösen. Mir ist derzeit kein anderer Algorithmus bekannt, der das schafft.
Ich löse regelmäßig die schwersten dieser Sudokus manuell mit einer Matriximplementation in Emacs-Lisp. Die 9x9 Sudoku-Probleme haben gerade noch eine Größe, die es erträglich macht.
Das Konzept beruht auf dem Ausmultiplizieren von CNF Formeln um die Blake Canonical Form BCF zu erhalten. Da ich das in der Ausbildung mal für einen 8-fach XOR-Adressvergleicher über 30 Seiten hinweg durchexerziert hatte, um nachzuweisen, dass er sich nicht in einem GALV12 realisieren lässt, war ich die längste Zeit der Meinung, dass Ausmultiplizieren extrem nervig und langweilig ist. Und mit Dezimalarithmetik ist es das auch.
Bei Modulo-2 Arithmetik ergibt sich aber ein interessanter Effekt, der es erlaubt, einen Teil des Ausmultiplizierens unter bestimmten Umständen vorwegzunehmen, indem erforderliche Konsequenzen propagiert werden können. Das ganze ist illustriert in [SCH2013CDF].
Um diesen Effekt zu nutzen, ist es nötig die komplette Konfliktsituation einer CNF-Formel zu kennen. Eine adjacency matrix bietet diesen Überblick. CNF-Klauseln fehlt diese Möglichkeit. Um die zwangsläufigen Konsequenzen erkennen zu können ist es auch nötig die Kapazität der CNF-Klausel zu kennen. Diese Information geht beim Übergang auf die adjacency matrix normalerweise verloren.
Wenn man die Literale von CNF-Klauseln durch DNF-Klauseln ersetzt, erhält man die Möglichkeit die zwingenden Konsequenzen zu verfolgen, es erschwert aber das Backtracking für DPLL.
Der flachen adjacency matrix fehlt die Klauselinformation komplett. Die Algorithmen der Graphentheorie finden in der Satoku Matrix grundsätzlich keine Anwendung. Die Konsolidierung und andere Umformungen der Matrix zerstören die Eigenschaften der adjacency matrix jedoch nicht.