Une méthode de preuve et de réfutation opérant sur des inégalités linéaires représentant des contraintes entières 0–1 : on dérive de nouvelles inégalités valides par combinaisons linéaires puis on applique des règles d'arrondi entières (coupe) pour éliminer les solutions fractionnaires et aboutir finalement à une contradiction explicite (p.ex. 0 ≥ 1) pour des codages propositionnels de contraintes arithmétiques.

Principe

Combiner linéairement des inégalités existantes pour mettre en évidence des combinaisons impossibles, puis utiliser des règles d'arrondi valides (coupes d'intégralité) qui préservent la validité sur assignations entières afin d'obtenir des inégalités plus fortes jusqu'à la contradiction.

Démonstration

Coder un petit ensemble insatisfiable de clauses en inégalités linéaires sur des variables x_i ∈ {0,1} ; appliquer les règles Cutting Planes pour ajouter des combinaisons arrondies — par exemple sommer des inégalités, diviser des coefficients et arrondir vers le haut les termes constants — et poursuivre jusqu'à dériver une borne impossible comme 1 ≤ 0, attestant l'insatisfaisabilité.

Mauvaise application

Considérer les dérivations Cutting Planes comme des recettes de SAT-solving automatiquement efficaces sans contrôler la croissance des coefficients ou la taille en bits, ou appliquer des étapes d'arrondi de manière invalide (c.-à-d. arrondir d'une façon non sûre pour les solutions entières), ce qui peut conduire à des inférences incorrectes.

Conséquence

Fournit un système de preuve algébrique puissant lié à la programmation entière : il peut simuler des motifs de raisonnement non couverts par la résolution, éclaire des séparations en complexité de preuve et sert de base aux algorithmes de coupes en optimisation et raisonnement automatique.

Inversion

En contraste, la manipulation syntactique de clauses à la résolution vise l'élimination combinatoire d'assignations, tandis que Cutting Planes opère dans le domaine arithmétique avec des combinaisons linéaires et de l'arrondi ; inverser la perspective aide à choisir la méthode adaptée selon la structure des contraintes.

Limite

S'applique aux représentations propositionnelles de contraintes linéaires entières et aux preuves en programmation entière ; elle n'est pas directement applicable à l'arithmétique non linéaire sans linéarisation, et l'usage pratique exige de maîtriser la croissance des coefficients et les problèmes numériques.

Tension sémantique

En tension avec les systèmes de preuve purement combinatoires (p.ex. résolution, calcul polynômial) : Cutting Planes peut être strictement plus puissant pour certains encodages mais moins pratique pour d'autres ; les compromis portent sur l'expressivité algébrique versus la gestion des coefficients et la complexité en taille binaire.

Synthèse

La Méthode Cutting Planes transforme un problème d'incohérence logique en une tâche de dérivation arithmétique : en prenant des combinaisons linéaires de contraintes et en appliquant des coupes d'intégralité correctes, on renforce le système jusqu'à obtenir une contradiction numérique certifiant l'insatisfaisabilité.