.. -*- coding: utf-8 -*- .. role:: sref(numref) .. role:: xref(numref) .. Copyright (C) 2025, Wolfgang Scherer, .. This file is part of HDP Sudoku. .. Permission is granted to copy, distribute and/or modify this document .. under the terms of the GNU Free Documentation License, Version 1.3 .. or any later version published by the Free Software Foundation; .. with no Invariant Sections, no Front-Cover Texts, and no Back-Cover Texts. .. A copy of the license is included in the section entitled "GNU .. Free Documentation License". .. inline comments (with du_comment_role) .. role:: rem(comment) .. role:: html(raw) :format: html .. role:: shx(code) :language: sh .. rst-class:: narrow xmedium xlarge xhuge xultra ################################################## :rem:`|||:sec:|||`\ Call to Arms ################################################## .. . (progn (forward-line 1) (snip-insert "rst_b.peek-a-boo" t t "rst") (insert "")) .. >>CODD Introduction 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. .. ================================================== :rem:`|||:sec:|||`\ Basic Principles ================================================== An |implicant| is a product term of a |DNF| which implies truth of a boolean function when it becomes true, whereas an |implicate| is a sum term of a |CNF| that implies falsehood of a boolean function when it becomes false. A definition of |implicant| and |implicate| can be found in [CHENG201115]_. See also `BWLect `_ When I first discovered the triangular adjacency matrix, I realized, that a valid solution for a |CNF| problem could be obtained by following a path from the top to the bottom. This was very similar to the method described by Shiny\ [SHINY]_. .. . ||:here:|| .. \|:here:| .. >>CODD Notes .. ================================================== .. :rem:`|||:sec:|||`\ Footnotes .. ================================================== :html:`
` .. \[#] .. \|:info:| put local references here .. \|:info:| put local definitions here .. include:: doc_defs.inc .. include:: abbrev_defs.inc .. include:: doc_defs_combined.inc .. .. \||<-snap->|| doc_standalone .. include:: doc/doc_defs_secret.inc .. \||<-snap->|| doc_standalone .. \||<-snap->|| not_doc_standalone .. include:: doc_defs_secret.inc .. \||<-snap->|| not_doc_standalone .. _`Wolfgang Scherer`: wolfgang.scherer@gmx.de