License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSTTCS.2019.43
URN: urn:nbn:de:0030-drops-116056
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2019/11605/
Go to the corresponding LIPIcs Volume Portal

Kleine Büning, Hans ; Wojciechowski, Piotr ; Subramani, K.

New Results on Cutting Plane Proofs for Horn Constraint Systems

pdf-format:
LIPIcs-FSTTCS-2019-43.pdf (0.5 MB)

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.

BibTeX - Entry

@InProceedings{kleinebning_et_al:LIPIcs:2019:11605,
  author =	{Hans Kleine B{\"u}ning and Piotr Wojciechowski and K. Subramani},
  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 =	{Arkadev Chattopadhyay and Paul Gastin},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2019/11605},
  URN =		{urn:nbn:de:0030-drops-116056},
  doi =		{10.4230/LIPIcs.FSTTCS.2019.43},
  annote =	{Keywords: Horn constraints, cutting planes, proof length}
}

Keywords: Horn constraints, cutting planes, proof length
Collection: 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019)
Issue Date: 2019
Date of publication: 04.12.2019

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI