##  [Beweisbreite](/de/node/60904) 

 Definition

Ein Maß für die maximale syntaktische Größe (z. B. die Anzahl der Literale in einer Klausel) von Zwischenformeln oder Klauseln, die in einem Beweis auftreten; bei Resolutionbeweisen ist dies typischerweise die maximale Klauselbreite.

 

 

 

 

 

 





## Prinzip

Prinzip

Erfasst die Spitzenkombinatorik der Zwischenobjekte: breitere Klauseln oder Formeln deuten auf größere kombinatorische Kombinationen von Literalen hin, die gleichzeitig behandelt werden müssen.

 

 

 

 

 





## Demonstration

Demonstration

In resolutionbasierten SAT-Beweisen ist die Beweisbreite die größte Anzahl von Literalen in irgendeiner während der Widerlegung erzeugten Klausel; Beweise, die zwangsläufig breitklausige Formeln erzeugen, sind oft schwieriger zu finden.

 

 

 

 

## Fehlanwendung

Fehlanwendung

Kleine Breite pauschal mit Einfachheit gleichzusetzen, ohne die Effekte der Kodierung zu berücksichtigen, ist irreführend; in einer Kodierung mag ein Beweis geringe Breite haben, in einer anderen aber hohe Breite oder Länge besitzen.

 

 

 

 

 





## Konsequenz

Konsequenz

Breitenuntergrenzen können genutzt werden, um exponentielle Untergrenzen für die Beweislänge in der Resolution zu beweisen; die Kontrolle der Breite ist eine zentrale Technik beim Entwurf parametrisierter oder FPT-Algorithmen.

 

 

 

 

## Umkehrung

Umkehrung

Man kann stattdessen die durchschnittliche Breite oder die Gesamtanzahl der Symbole betrachten, um die gesamte Formelmasse statt der Spitzenbreite zu betonen, womit der Fokus von worst-case-Intermediäraufblähung auf aggregierte Kosten verlagert wird.

 

 

 

 

 





## Abgrenzung

Abgrenzung

Breite ist an die gewählte Repräsentation (Klauseln, Sequents, Formeln) und an die syntaktische Einheit, die gezählt wird (Literale vs Atome vs Symbole) gebunden; sie misst nicht direkt sequentielle Schritte oder Speicher, sofern nicht mit anderen Metriken kombiniert.

 

 

 

 

 





## Semantische Spannung

Semantische Spannung

Steht im Wettbewerb mit Länge und Raum: schmale Beweise können trotzdem lang oder raumaufwändig sein, und kurz(zeitig)e Beweise können breite Zwischenformeln benötigen; Breite isoliert die gleichzeitige kombinatorische Forderung.

 

 

 

 

 





## Synthese

Synthese

Beweisbreite quantifiziert die maximale gleichzeitig auftretende kombinatorische Last eines Beweises; zusammen mit Länge und Raum hilft sie, Engpässe bei der Suche vorherzusagen und Transformationen oder Kodierungen zu leiten, die Zwischenrepräsentationen klein halten.