##  [Cutting-Planes-Methode](/de/node/60054) 

 Definition

Ein Beweis- und Widerlegungsverfahren, das auf linearen Ungleichungen arbeitet, die 0–1-Ganzheitsbedingungen repräsentieren: Man leitet neue gültige lineare Ungleichungen durch lineare Kombinationen ab und wendet ganzzahliges Abrunden (Cuts) an, um fraktionale Lösungen zu eliminieren und schließlich einen expliziten Widerspruch (z. B. 0 ≥ 1) für propositionale Kodierungen arithmetischer Einschränkungen zu erhalten.

 

 

 

 

 

 





## Prinzip

Prinzip

Vorhandene Ungleichungen linear kombinieren, um unzulässige Kombinationen sichtbar zu machen, und dann gültige Rundungsregeln (Integritäts-Schnitte) anwenden, die auf ganzen Lösungen gültig bleiben, um stärkere Ungleichungen zu erzeugen, bis ein Widerspruch erreicht ist.

 

 

 

 

 





## Demonstration

Demonstration

Kodieren Sie eine einfach unlösbare Klauselmenge als lineare Ungleichungen über Variablen x_i ∈ {0,1}; wenden Sie Cutting-Planes-Regeln an, z.B. Ungleichungen aufsummieren, Koeffizienten teilen und konstante Terme aufrunden, und fahren Sie fort, bis eine unmögliche Schranke wie 1 ≤ 0 entsteht, die die Unlösbarkeit bezeugt.

 

 

 

 

## Fehlanwendung

Fehlanwendung

Cutting-Planes-Ableitungen als automatisch effiziente SAT-Lösungsrezepte zu betrachten, ohne das Wachstum der Koeffizienten oder die Bit-Size zu berücksichtigen, oder Abrundungsschritte unsachgemäß anzuwenden (d.h. auf eine Weise zu runden, die für ganzzahlige Lösungen nicht korrekt ist), was zu falschen Folgerungen führen kann.

 

 

 

 

 





## Konsequenz

Konsequenz

Ergibt ein mächtiges algebraisches Beweissystem mit Bezug zur Ganzzahligen Programmierung: Es kann viele Argumentationsmuster über die Resolution hinaus simulieren, trägt zu Ergebnissen in der Beweiskomplexität bei und bildet die Grundlage für Schnitte-Algorithmen in Optimierung und automatischer Beweisführung.

 

 

 

 

## Umkehrung

Umkehrung

Im Gegensatz zur rein syntaktischen Klauselmanipulation der Resolution arbeitet Cutting Planes im arithmetischen Bereich mit linearen Kombinationen und Runden; das Umkehren der Perspektive hilft bei der Methodenauswahl entsprechend der Struktur der Beschränkungen.

 

 

 

 

 





## Abgrenzung

Abgrenzung

Gilt für propositionale Repräsentationen linearer Ganzheitsbedingungen und für Beweise in der ganzzahligen Programmierung; ist nicht unmittelbar auf beliebige nichtlineare Arithmetik anwendbar ohne Linearisierung, und der praktische Einsatz muss Koeffizientenwachstum und numerische Probleme kontrollieren.

 

 

 

 

 





## Semantische Spannung

Semantische Spannung

Spannung zu rein kombinatorischen Beweissystemen (z. B. Resolution, Polynomial Calculus): Cutting Planes kann für bestimmte Kodierungen deutlich stärker sein, ist aber in anderen Fällen weniger praktikabel; Abwägungen betreffen algebraische Ausdrucksfähigkeit gegenüber Koeffizientenmanagement und Bit-Komplexität.

 

 

 

 

 





## Synthese

Synthese

Die Cutting-Planes-Methode wandelt logische Inkonsistenz in eine arithmetische Ableitungsaufgabe: Durch lineare Kombinationen von Beschränkungen und korrekte Integritäts-Schnitte verstärkt man das System, bis ein numerischer Widerspruch die Unlösbarkeit zertifiziert.