Die Gesamtanzahl der Knoten, die in einem Such- oder Beweisbaum während eines automatisierten Beweis- oder Suchverfahrens erzeugt werden; jeder Knoten repräsentiert ein eigenes Teilziel, eine partielle Zuordnung, eine Zwischenformel oder einen Inferenzzustand.

Prinzip

Misst kombinatorische Verzweigung und Duplikation im Suchprozess: größere Größe spiegelt gewöhnlich mehr Verzweigungen, Backtracking oder wiederholte Erkundung ähnlicher Zustände wider.

Demonstration

Bei einem backtracking-basierten SAT-Solver zählt die Suchbaumgröße jeden Entscheidungs-Knoten und jeden durch Propagation entstandenen Knoten, die beim Durchsuchen partieller Zuordnungen bis zur gefundenen erfüllenden Belegung oder Widerlegung erzeugt werden.

Fehlanwendung

Die Suchbaumgröße als direkten Proxy für die Laufzeit im Realbetrieb zu verwenden, ohne Kosten pro Knoten, Parallelität oder Memoisierung (DAG-Kompression) zu berücksichtigen, kann zu irreführenden Schlussfolgerungen führen.

Konsequenz

Richtig gemessen liefert die Suchbaumgröße eine obere Schranke für die Anzahl der Inferenzschritte oder Knoten-Besuche; exponentielle Baumgröße impliziert potenziell exponentielle Laufzeit bei sequentieller Suche.

Umkehrung

Statt Knoten zu zählen, kann man nur unterscheidbare Zustände nach wertbasierter Canonicalisierung (DAG-Größe) zählen; das verringert die Zählung durch Zusammenführung identischer Teilprobleme und verlagert den Fokus von Erkundung auf Wiederverwendung.

Abgrenzung

Gilt für baumförmige Erkundungsspuren; schließt Kosten innerhalb eines Knotens (z. B. aufwändige Constraint-Propagation) aus, erfasst keine DAG-Wiederverwendung, es sei denn Knoten werden zusammengeführt, und hängt von der gewählten Granularität ab, was als Knoten gilt.

Semantische Spannung

Steht in Spannung zu Maßen wie Beweislänge und Beweisraum: Baumgröße betont Verzweigungsstruktur und Duplikation, während Länge sequentielle Inferenzen und Raum den Speicherbedarf misst.

Synthese

Die Suchbaumgröße ist eine kombinatorische Zählung, die das Ausmaß der Verzweigung und redundanten Erkundung in einer Suche quantifiziert; zusammen mit pro-Knoten-Kosten und Wiederverwendungsanalyse sagt sie die praktische Schwierigkeit voraus und lenkt Heuristiken zur Reduktion der Verzweigung oder Ermöglichung von Zusammenführungen.