Vše

Co hledáte?

Vše
Projekty
Výsledky výzkumu
Subjekty

Rychlé hledání

  • Projekty podpořené TA ČR
  • Významné projekty
  • Projekty s nejvyšší státní podporou
  • Aktuálně běžící projekty

Chytré vyhledávání

  • Takto najdu konkrétní +slovo
  • Takto z výsledků -slovo zcela vynechám
  • “Takto můžu najít celou frázi”

DRAT proofs, propagation redundancy, and extended resolution

Identifikátory výsledku

  • Kód výsledku v IS VaVaI

    <a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F67985840%3A_____%2F19%3A00507739" target="_blank" >RIV/67985840:_____/19:00507739 - isvavai.cz</a>

  • Výsledek na webu

    <a href="http://dx.doi.org/10.1007/978-3-030-24258-9_5" target="_blank" >http://dx.doi.org/10.1007/978-3-030-24258-9_5</a>

  • DOI - Digital Object Identifier

    <a href="http://dx.doi.org/10.1007/978-3-030-24258-9_5" target="_blank" >10.1007/978-3-030-24258-9_5</a>

Alternativní jazyky

  • Jazyk výsledku

    angličtina

  • Název v původním jazyce

    DRAT proofs, propagation redundancy, and extended resolution

  • Popis výsledku v původním jazyce

    We study the proof complexity of RAT proofs and related systems including BC, SPR, and PR which use blocked clauses and (subset) propagation redundancy. These systems arise in satisfiability (SAT) solving, and allow inferences which preserve satisfiability but not logical implication. We introduce a new inference SR using substitution redundancy. We consider systems both with and without deletion. With new variables allowed, the systems are known to have the same proof theoretic strength as extended resolution. We focus on the systems that do not allow new variables to be introduced. Our first main result is that the systems DRAT $${}^-$$, DSPR $${}^-$$ and DPR $${}^-$$, which allow deletion but not new variables, are polynomially equivalent. By earlier work of Kiesl, Rebola-Pardo and Heule, they are also equivalent to DBC $${}^-$$. Without deletion and without new variables, we show that SPR $${}^-$$ can polynomially simulate PR $${}^-$$ provided only short clauses are inferred by SPR inferences. Our next main results are that many of the well-known “hard” principles have polynomial size SPR $${}^-$$ refutations (without deletions or new variables). These include the pigeonhole principle, bit pigeonhole principle, parity principle, Tseitin tautologies, and clique-coloring tautologies, SPR $${}^-$$ can also handle or-fication and xor-ification. Our final result is an exponential size lower bound for RAT $${}^-$$ refutations, giving exponential separations between RAT $${}^-$$ and both DRAT $${}^-$$ and SPR $${}^-$$.

  • Název v anglickém jazyce

    DRAT proofs, propagation redundancy, and extended resolution

  • Popis výsledku anglicky

    We study the proof complexity of RAT proofs and related systems including BC, SPR, and PR which use blocked clauses and (subset) propagation redundancy. These systems arise in satisfiability (SAT) solving, and allow inferences which preserve satisfiability but not logical implication. We introduce a new inference SR using substitution redundancy. We consider systems both with and without deletion. With new variables allowed, the systems are known to have the same proof theoretic strength as extended resolution. We focus on the systems that do not allow new variables to be introduced. Our first main result is that the systems DRAT $${}^-$$, DSPR $${}^-$$ and DPR $${}^-$$, which allow deletion but not new variables, are polynomially equivalent. By earlier work of Kiesl, Rebola-Pardo and Heule, they are also equivalent to DBC $${}^-$$. Without deletion and without new variables, we show that SPR $${}^-$$ can polynomially simulate PR $${}^-$$ provided only short clauses are inferred by SPR inferences. Our next main results are that many of the well-known “hard” principles have polynomial size SPR $${}^-$$ refutations (without deletions or new variables). These include the pigeonhole principle, bit pigeonhole principle, parity principle, Tseitin tautologies, and clique-coloring tautologies, SPR $${}^-$$ can also handle or-fication and xor-ification. Our final result is an exponential size lower bound for RAT $${}^-$$ refutations, giving exponential separations between RAT $${}^-$$ and both DRAT $${}^-$$ and SPR $${}^-$$.

Klasifikace

  • Druh

    D - Stať ve sborníku

  • CEP obor

  • OECD FORD obor

    10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Návaznosti výsledku

  • Projekt

    <a href="/cs/project/GA19-05497S" target="_blank" >GA19-05497S: Složitost matematických důkazů a struktur</a><br>

  • Návaznosti

    I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Ostatní

  • Rok uplatnění

    2019

  • 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ů

Údaje specifické pro druh výsledku

  • Název statě ve sborníku

    Theory and Applications of Satisfiability Testing – SAT 2019

  • ISBN

    978-3-030-24257-2

  • ISSN

    0302-9743

  • e-ISSN

  • Počet stran výsledku

    19

  • Strana od-do

    71-89

  • Název nakladatele

    Springer

  • Místo vydání

    Cham

  • Místo konání akce

    Lisbon

  • Datum konání akce

    9. 7. 2019

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

    WRD - Celosvětová akce

  • Kód UT WoS článku