Journal article:
Samuel R. Buss and Peter Clote.
"Cutting planes, connectivity and threshold logic."
Archive for Mathematical Logic 35 (1996) 33-63.
Download article: postscript or PDF.
Abstract: Originating from work in operations research the cutting plane refutation system $CP$ is an extension of resolution, where unsatisfiable propositional logic formulas in conjunctive normal form are recognized by showing the non-existence of boolean solutions to associated families of linear inequalities. Polynomial size $CP$ proofs are given for the undirected $s$-$t$ connectivity principle. The subsystems $CP_q$ of $CP$, for $q\ge 2$, are shown to be polynomially equivalent to $CP$, thus answering problem~$19$ from the list of open problems of \cite{clotekrajicek}. We present a normal form theorem for $CP_2$-proofs and thereby for arbitrary $CP$-proofs. As a corollary, we show that the coefficients and constant terms in arbitrary cutting plane proofs may be exponentially bounded by the number of steps in the proof, at the cost of an at most polynomial increase in the number of steps in the proof. The extension $CPLE^+$, introduced in \cite{clote10} and there shown to $p$-simulate Frege systems, is proved to be polynomially equivalent to Frege systems. Lastly, since linear inequalities are related to threshold gates, we introduce a new threshold logic and prove a completeness theorem.