Semantic versus syntactic cutting planes

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F67985840%3A_____%2F16%3A00458241" target="_blank" >RIV/67985840:_____/16:00458241 - isvavai.cz</a>

Výsledek na webu

<a href="http://dx.doi.org/10.4230/LIPIcs.STACS.2016.35" target="_blank" >http://dx.doi.org/10.4230/LIPIcs.STACS.2016.35</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.4230/LIPIcs.STACS.2016.35" target="_blank" >10.4230/LIPIcs.STACS.2016.35</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Semantic versus syntactic cutting planes

Popis výsledku v původním jazyce

In this paper, we compare the strength of the semantic and syntactic version of the cutting planes proof system. First, we show that the lower bound technique of Pudlák applies also to semantic cutting planes: the proof system has feasible interpolation via monotone real circuits, which gives an exponential lower bound on lengths of semantic cutting planes refutations. Second, we show that semantic refutations are stronger than syntactic ones. In particular, we give a formula for which any refutation in syntactic cutting planes requires exponential length, while there is a polynomial length refutation in semantic cutting planes. In other words, syntactic cutting planes does not p-simulate semantic cutting planes. We also give two incompatible integer inequalities which require exponential length refutation in syntactic cutting planes.

Název v anglickém jazyce

Semantic versus syntactic cutting planes

Popis výsledku anglicky

In this paper, we compare the strength of the semantic and syntactic version of the cutting planes proof system. First, we show that the lower bound technique of Pudlák applies also to semantic cutting planes: the proof system has feasible interpolation via monotone real circuits, which gives an exponential lower bound on lengths of semantic cutting planes refutations. Second, we show that semantic refutations are stronger than syntactic ones. In particular, we give a formula for which any refutation in syntactic cutting planes requires exponential length, while there is a polynomial length refutation in semantic cutting planes. In other words, syntactic cutting planes does not p-simulate semantic cutting planes. We also give two incompatible integer inequalities which require exponential length refutation in syntactic cutting planes.

Druh

D - Stať ve sborníku

CEP obor

BA - Obecná matematika

OECD FORD obor

—

Projekt

—

Návaznosti

I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Rok uplatnění

2016

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016)

ISBN

978-3-95977-001-9

ISSN

1868-8969

e-ISSN

—

Počet stran výsledku

13

Strana od-do

1-13

Název nakladatele

Schloss Dagstuhl, Leibniz-Zentrum für Informatik

Místo vydání

Dagstuhl

Místo konání akce

Orléans

Datum konání akce

17. 2. 2016

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—