DROPS

Document

DOI: 10.4230/LIPIcs.FSTTCS.2019.43

New Results on Cutting Plane Proofs for Horn Constraint Systems

Authors: Hans Kleine Büning, Piotr Wojciechowski, and K. Subramani

Published in: LIPIcs, Volume 150, 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019)

Abstract

In this paper, we investigate properties of cutting plane based refutations for a class of integer programs called Horn constraint systems (HCS). Briefly, a system of linear inequalities A * x >= b is called a Horn constraint system, if each entry in A belongs to the set {0,1,-1} and furthermore there is at most one positive entry per row. Our focus is on deriving refutations i.e., proofs of unsatisfiability of such programs using cutting planes as a proof system. We also look at several properties of these refutations. Horn constraint systems can be considered as a more general form of propositional Horn formulas, i.e., CNF formulas with at most one positive literal per clause. Cutting plane calculus (CP) is a well-known calculus for deciding the unsatisfiability of propositional CNF formulas and integer programs. Usually, CP consists of a pair of inference rules. These are called the addition rule (ADD) and the division rule (DIV). In this paper, we show that cutting plane calculus is still complete for Horn constraints when every intermediate constraint is required to be Horn. We also investigate the lengths of cutting plane proofs for Horn constraint systems.

Cite as

Hans Kleine Büning, Piotr Wojciechowski, and K. Subramani. New Results on Cutting Plane Proofs for Horn Constraint Systems. In 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 150, pp. 43:1-43:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{kleinebuning_et_al:LIPIcs.FSTTCS.2019.43,
  author =	{Kleine B\"{u}ning, Hans and Wojciechowski, Piotr and Subramani, K.},
  title =	{{New Results on Cutting Plane Proofs for Horn Constraint Systems}},
  booktitle =	{39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019)},
  pages =	{43:1--43:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-131-3},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{150},
  editor =	{Chattopadhyay, Arkadev and Gastin, Paul},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2019.43},
  URN =		{urn:nbn:de:0030-drops-116056},
  doi =		{10.4230/LIPIcs.FSTTCS.2019.43},
  annote =	{Keywords: Horn constraints, cutting planes, proof length}
}

Search Results

Documents authored by Subramani, K.

New Results on Cutting Plane Proofs for Horn Constraint Systems

Abstract

Cite as

Thanks for your feedback!

Could not send message