💻 computer science

Extending CDCL to disjunctions of parity equations

Dieser Beitrag stellt $\text{CDCL}(\oplus)$ vor, eine Verallgemeinerung des Conflict-Driven Clause Learning-Rahmens auf XNF-Formeln, die Paritätslogik unterstützt und das $\text{Res}(\oplus)$ -Beweissystem polynomiell simuliert, wobei auf Benchmarks mit Paritätsbeschränkungen signifikante Leistungsverbesserungen gegenüber bestehenden Solvern demonstriert werden.

Ursprüngliche Autoren: Paul Beame, Glenn Sun

Veröffentlicht 2026-05-15

📖 4 Min. Lesezeit☕ Kaffeepausen-Lektüre

CC BY 4.0

Ursprüngliche Autoren: Paul Beame, Glenn Sun

Originalarbeit lizenziert unter CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dies ist eine KI-generierte Erklärung des untenstehenden Papers. Sie wurde nicht von den Autoren verfasst oder gebilligt. Für technische Genauigkeit konsultieren Sie das Originalpaper. Vollständigen Haftungsausschluss lesen

Stellen Sie sich vor, Sie versuchen, einen riesigen, verwickelten Knoten aus Logikrätseln zu lösen. Seit Jahrzehnten ist das beste Werkzeug zum Entwirren dieser Knoten eine Methode namens CDCL (Conflict-Driven Clause Learning). Betrachten Sie CDCL als einen sehr klugen Detektiv, der Vermutungen anstellt, den Hinweisen folgt und wenn er auf eine Sackgasse (einen Widerspruch) stößt, eine wertvolle Lektion aus diesem Fehler zieht, damit er denselben Fehler nicht wiederholt.

Dieser Detektiv hat jedoch einen blinden Fleck. Er ist hervorragend darin, Rätsel mit einfachen „Wahr/Falsch"-Aussagen zu lösen, hat aber Schwierigkeiten, wenn die Hinweise Paritätsgleichungen beinhalten – mathematische Aussagen darüber, ob eine Gruppe von Elementen eine gerade oder ungerade Summe ergibt (wie etwa zu prüfen, ob die Anzahl der roten Murmeln in einer Tasche gerade ist).

Dieser Artikel stellt einen neuen, verbesserten Detektiv namens CDCL(⊕) (ausgesprochen „CDCL-Parität") und einen Softwareprototypen namens Xorcle vor. So funktioniert es, unter Verwendung einfacher Analogien:

1. Das Problem: Der „Gerade/Ungerade"-blinde Fleck

Standard-CDCL-Detektive betrachten Hinweise wie „Wenn A wahr ist, muss B falsch sein." Doch einige Probleme sind in einer Sprache verfasst wie „Wenn die Anzahl der wahren Elemente in dieser Gruppe gerade ist..."

Der alte Weg: Frühere Versuche, diese Probleme zu lösen, versuchten, die „gerade/ungerade"-Mathematik in einfache Wahr/Falsch-Hinweise zu übersetzen. Das ist vergleichbar mit dem Versuch, eine komplexe 3D-Skulptur zu beschreiben, indem man nur flache, 2D-Schatten zeichnet. Es funktioniert, aber die Zeichnung wird riesig und unübersichtlich, was den Detektiv sehr langsam macht.
Der neue Weg: CDCL(⊕) spricht die „gerade/ungerade"-Sprache von Natur aus. Es übersetzt die Hinweise nicht; es versteht sie direkt.

2. Die Superkraft: Lineare Algebra als Werkzeug

Wenn der neue Detektiv auf eine Sackgasse stößt, betrachtet er nicht nur die spezifischen Hinweise, die das Problem verursacht haben. Er nutzt lineare Algebra (ein mathematisches Teilgebiet, das sich mit Gleichungen befasst), um Hinweise zu mischen und zu kombinieren.

Die Analogie: Stellen Sie sich vor, Sie haben zwei Hinweise: „Die Summe von A und B ist gerade" und „Die Summe von B und C ist gerade." Ein Standard-Detektiv könnte stecken bleiben. Der neue Detektiv erkennt jedoch, dass, wenn man diese beiden Hinweise addiert, das „B" sich wegcancelt, und man einen brandneuen, mächtigen Hinweis erhält: „Die Summe von A und C ist gerade."
Dies ermöglicht dem Detektiv, Muster und Abkürzungen zu erkennen, die die alte Methode völlig übersehen würde.

3. Die Theorie: Beweis, dass der Detektiv schlauer ist

Die Autoren haben nicht nur einen schnelleren Detektiv gebaut; sie haben mathematisch bewiesen, dass dieser neue Detektiv für diese Art von Rätseln universell überlegen ist.

Sie zeigten, dass CDCL(⊕) jeden Beweis simulieren kann, den das „Paritätslogik"-System (genannt Res(⊕)) produzieren kann.
Die Metapher: Es ist wie der Beweis, dass ein Meisterkoch (CDCL(⊕)) jedes Gericht zubereiten kann, das ein bestimmter Grilltyp (Res(⊕)) zubereiten kann, aber der Koch dies auch viel schneller tun kann, wenn ihm erlaubt wird, ein paar strategische Entscheidungen zu treffen (Neustarts und Entscheidungen).

4. Der Prototyp: Xorcle

Das Team baute eine funktionierende Version dieses Detektivs namens Xorcle (ein Wortspiel aus „XOR" und „Oracle").

Die Ergebnisse: Sie testeten Xorcle gegen die derzeit besten Detektive (wie Kissat und CryptoMiniSAT) an einer Vielzahl von Rätseln.
- Bei nativen Paritätsrätseln: Xorcle war deutlich schneller und löste Probleme, bei denen die anderen Schwierigkeiten hatten oder die sie nicht rechtzeitig fertigstellen konnten.
- Bei „schwierigen" Standardrätseln: Selbst bei Rätseln, die im alten „Wahr/Falsch"-Format verfasst waren (speziell eine Art namens Tseitin-Formeln), war Xorcle überraschend schnell. Während andere Detektive eine exponentiell lange Zeit benötigten (stellen Sie sich vor, Sie warten, bis das Universum zu Ende geht), löste Xorcle sie in einer Zeit, die fast linear wuchs (wie das Gehen auf einer geraden Linie).

5. Wie es „denkt" (Die Mechanik)

Um dies zu ermöglichen, mussten die Autoren neue Regeln erfinden, wie der Detektiv lernt:

Überwachen von Gleichungen: Anstatt nur einzelne Variablen zu beobachten (wie „Ist A wahr?"), überwacht der Detektiv ganze Gruppen von Gleichungen.
Basiswechsel: Wenn der Detektiv aus einem Fehler lernen muss, schreibt er nicht nur eine neue Regel auf. Er ordnet sein gesamtes Verständnis des Problems neu an (ändert die „Basis"), um genau zu isolieren, welcher Teil der Mathematik den Fehler verursacht hat. Das ist vergleichbar mit einem Mechaniker, der anstatt nur zu sagen „der Motor ist defekt", die Motorteile neu organisiert, um genau zu sehen, welches Zahnrad abgenutzt ist.

Zusammenfassung

Kurz gesagt, stellt dieser Artikel eine neue Art vor, Logikrätsel zu lösen, die „gerade gegen ungerade"-Mathematik beinhalten. Indem sie den Standard-Lösungsalgorithmus so verbesserten, dass er diese Gleichungen von Natur aus versteht, schufen die Autoren ein Werkzeug (Xorcle), das theoretisch bewiesenermaßen leistungsfähiger ist und empirisch nachgewiesen wurde, dass es bei spezifischen, schwierigen Problemtypen deutlich schneller ist als aktuelle State-of-the-Art-Löser. Sie schufen zudem eine neue Art, den Denkprozess des Detektivs (Proof Logging) zu protokollieren, damit andere die Lösung verifizieren können.

Technische Zusammenfassung: Erweiterung von CDCL auf Disjunktionen von Paritätsgleichungen

Problemstellung

Conflict-Driven Clause Learning (CDCL) ist die vorherrschende Methode für SAT-Lösung, ist jedoch fundamental durch das Resolutionsbeweissystem begrenzt. Probleme, die in der Resolution eine exponentielle Beweisgröße erfordern (wie Tseitin-Formeln oder das bijektive Taubeneprinzip), sind für CDCL nachweislich schwer. Zwar integrieren einige Solver Fragmente stärkerer Beweissysteme – wie Pseudo-Boolean-Solver, die Cutting Planes verwenden, oder CNF-XOR-Solver, die Paritätsgleichungen behandeln –, doch behandeln diese Ansätze Paritätslogik oft als separates Modul oder beschränken sich auf spezifische Normalformen (z. B. CNF-XOR).

Die spezifische Lücke, die diese Arbeit adressiert, ist das Fehlen eines CDCL-artigen Algorithmus, der XNF-Formeln (XOR-OR-AND Normalform) nativ verarbeitet. XNF-Formeln bestehen aus Konjunktionen von linearen Klauseln, die Disjunktionen von Paritätsgleichungen sind (z. B. $(x \oplus y) \lor \neg(y \oplus z)$ ). Während das Res(⊕)-Beweissystem (Resolution, generalisiert auf XNF) für bestimmte Probleme bekanntermaßen exponentiell stärker als die Resolution ist, integrieren bestehende Solver Res(⊕)-Schlussfolgerungen nicht vollständig in die CDCL-Schleife, und sie liefern keinen theoretischen Beweis dafür, dass ein CDCL-artiger Algorithmus Res(⊕) polynomiell simulieren kann.

Methodik

Die Autoren schlagen CDCL(⊕) vor, eine Verallgemeinerung des CDCL-Algorithmus, die direkt auf XNF-Formeln operiert. Die Methodik stützt sich auf drei Kernkomponenten:

Neue Inferenzregeln für Res(⊕):
Die Autoren führen eine neue Charakterisierung des Res(⊕)-Beweissystems ein, die die Standard-Resolutions- und Abschwächungs-Regeln durch Addition und Basiswechsel ersetzt.
- Addition: Aus $C \lor f$ und $D \lor g$ wird $C \lor D \lor (f + g)$ abgeleitet.
- Basiswechsel: Aus $C$ wird jedes $D$ abgeleitet, sodass $C \equiv D$ (semantisch äquivalent).
  Entscheidend definieren sie eine affine Resolutions-Regel, bei der Gleichungen (via Basiswechsel) „isoliert" werden, um eine Kürzung durch Addition zu ermöglichen. Dies eliminiert die Notwendigkeit des exponentiellen Suchraums, der mit der Abschwächungsregel verbunden ist, und ermöglicht eine polynomielle Simulation.
Unit-Propagation mit linearer Algebra:
Im Gegensatz zum klassischen CDCL, das auf Literalzuweisungen basiert, führt CDCL(⊕) Unit-Propagation unter Verwendung linearer Algebra über $\mathbb{F}_2$ durch.
- Der Solver verwaltet eine Menge bekannter Einheiten (Gleichungen) $U$ .
- Die Propagation prüft, ob eine lineare Klausel $C$ unter der Voraussetzung von $U$ eine neue Gleichung $f$ oder einen Widerspruch ($1$) impliziert.
- Dies wird implementiert, indem die „lineare Negation" einer Klausel (der Unterraum der Zuweisungen, die die Klausel falsifizieren) gegen den Spann von $U$ reduziert wird. Wenn die Negation der Klausel im Spann von $U$ plus einer einzelnen Gleichung $f$ enthalten ist, wird $f$ abgeleitet.
Klausellernen durch Konfliktanalyse:
Der Artikel passt die 1-UIP-Strategie (First Unique Implication Point) für das Klausellernen an das XNF-Szenario an. Da Implikationsgraphen nicht direkt auf lineare Gleichungen übertragbar sind, arbeitet der Lernalgorithmus semantisch:
- Er beginnt mit der Konfliktklausel (dem Grund für den Widerspruch).
- Er wendet iterativ Basiswechsel an, um die Gleichung zu isolieren, die für die letzte Entscheidung verantwortlich ist.
- Er wendet die Additions-Regel an, um die isolierte Klausel mit dem Grund des Konflikts zu kombinieren und effektiv die Entscheidungsvariable auszulöschen.
- Dieser Prozess wiederholt sich, bis eine assertierende Klausel gefunden ist (eine Klausel, die eine Propagation auf dem aktuellen Entscheidungsniveau erzwingt).

Hauptbeiträge

Theoretische Beiträge

Bidirektionale Verbindung: Der Artikel beweist, dass CDCL(⊕) nicht nur Res(⊕)-Beweise erzeugt, sondern das Res(⊕)-Beweissystem auch polynomiell simuliert, gegeben nichtdeterministische Entscheidungen und Neustarts. Dies spiegelt die klassische Beziehung zwischen CDCL und Resolution wider.
Neue Charakterisierung des Beweissystems: Die Autoren stellen eine neue Menge von Inferenzregeln (Addition und Basiswechsel) bereit, die polynomiell äquivalent zu Res(⊕) sind, aber die Abschwächungsregel nicht enthalten, was sie für die algorithmische Implementierung geeignet macht.
Input-Res(⊕)-Äquivalenz: Der Artikel beweist, dass die Unit-Propagation in CDCL(⊕) einem Fragment von Res(⊕) entspricht, das als Input Res(⊕) bekannt ist, und verallgemeinert damit ein bekanntes Ergebnis für klassisches CDCL.
Verbesserter Simulationsfaktor: Der Simulationsbeweis verbessert den polynomiellen Faktor für die klassische CDCL/Resolution-Beziehung (unter Übereinstimmung mit dem Ergebnis in [7] durch ein einfacheres Argument), indem optimiert wird, wie Zerlegungen von Klauseln absorbiert werden.

Praktische Beiträge

Xorcle-Implementierung: Die Autoren stellen Xorcle vor, einen Proof-of-Concept-Solver für CDCL(⊕).
- Es implementiert effiziente lineare Algebra über $\mathbb{F}_2$ unter Verwendung von Bit-Packing.
- Es führt CSIDS (Clause State Independent Decaying Sum) ein, eine neue Heuristik für die Klauselauswahl, die VSIDS und CMTF auf den XNF-Kontext verallgemeinert.
- Es führt LRUP(⊕) ein, eine Erweiterung des LRUP-Protokollierungsformats zur Unterstützung von Paritätsausdrücken.
Heuristiken für XNF: Der Artikel beschreibt Anpassungen für überwachte Strukturen (Durchlaufen von Klauseln anstatt komplexer Watchlisten aufgrund linearer Abhängigkeiten zu pflegen), Entscheidungsverfahren (Verzweigung auf zufälligen Gleichungen aus der Negation einer Klausel) und Phasenauswahl (Bevorzugung der Falsifizierung von Klauseln).

Experimentelle Ergebnisse

Die Autoren bewerteten Xorcle an einer Suite von Benchmarks, darunter:

Ascon-128: Eine kryptographiebezogene 2-XNF-Familie.
Zufällige und eingeschränkte k-XNFs: Synthetische Formeln mit variierenden Anzahlen von Variablen und Gleichungen.
Tseitin-Formeln: CNF-kodierte Paritätsprobleme, die für die Resolution bekanntermaßen schwer sind.

Wichtige Erkenntnisse:

Leistung bei XNF: Xorcle übertraf bestehende Solver (Kissat, CryptoMiniSAT und 2-Xornado) bei nativen XNF-Benchmarks. Bemerkenswerterweise übertraf es 2-Xornado (einen dedizierten 2-XNF-Solver) bei Ascon-128-Instanzen, trotz der Verwendung allgemeiner XNF-Logik.
Leistung bei Tseitin-Formeln: Bei in CNF kodierten Tseitin-Formeln zeigte Xorcle eine nahezu polynomielle Skalierung der Laufzeit, wohingegen auf Resolution basierende Solver bekanntermaßen exponentielle Zeit benötigen. Dies wurde ohne Vorverarbeitung erreicht und stützte sich ausschließlich auf die Kern-CDCL(⊕)-Logik.
Qualität der Entscheidungen: Xorcle benötigte signifikant weniger Entscheidungen als konkurrierende Solver, was darauf hindeutet, dass die paritätsbasierten Verzweigungs- und Ableitungsmechanismen für diese Problemklassen effektiver sind.

Bedeutung und Behauptungen

Der Artikel behauptet, dass CDCL(⊕) den ersten rigorosen theoretischen Rahmen und die praktische Implementierung bietet, die Paritätslogik vollständig in das CDCL-Paradigma integrieren.

Theoretische Bedeutung: Es wird festgestellt, dass die Grenzen von CDCL nicht inhärent zur algorithmischen Struktur, sondern zum zugrundeliegenden Beweissystem (Resolution) gehören. Durch den Wechsel zu Res(⊕) kann CDCL theoretisch Probleme lösen, die für Standard-CDCL exponentiell schwer sind.
Praktische Bedeutung: Die Ergebnisse deuten darauf hin, dass natives XNF-Lösen machbar und potenziell überlegen gegenüber der Konvertierung von XNF in CNF oder CNF-XOR ist. Die Fähigkeit, Tseitin-Formeln in nahezu polynomieller Zeit ohne Vorverarbeitung zu lösen, unterstreicht das Potenzial der Paritätslogik, bekannte Härtebarrieren in der SAT-Lösung zu überwinden.
Zukünftige Richtungen: Die Autoren vermerken bescheiden, dass Xorcle ein Proof-of-Concept ist. Es fehlen derzeit mehrere Standard-CDCL-Optimierungen (z. B. Klauselentfernung, fortgeschrittene Neustarts, dynamische Heuristiken), und Konzepte wie „1-UIP" oder „Klauselminimierung" sind noch nicht vollständig auf das semantische XNF-Setting verallgemeinert. Die Arbeit ebnet den Weg für weitere Forschung zu Heuristiken, die speziell CNF-Formeln adressieren, die implizit Paritätslogik erfordern.