Počet záznamů: 1
A note on SAT algorithms and proof complexity
- 1.
SYSNO ASEP 0380502 Druh ASEP J - Článek v odborném periodiku Zařazení RIV J - Článek v odborném periodiku Poddruh J Článek ve WOS Název A note on SAT algorithms and proof complexity Tvůrce(i) Krajíček, Jan (MU-W) SAI, ORCID Zdroj.dok. Information Processing Letters. - : Elsevier - ISSN 0020-0190
Roč. 112, č. 12 (2012), s. 490-493Poč.str. 4 s. Jazyk dok. eng - angličtina Země vyd. NL - Nizozemsko Klíč. slova computational complexity Vědní obor RIV BA - Obecná matematika CEP IAA100190902 GA AV ČR - Akademie věd CEZ AV0Z10190503 - MU-W (2005-2011) UT WOS 000303959300007 EID SCOPUS 84859539294 DOI https://doi.org/10.1016/j.ipl.2012.03.009 Anotace We apply classical proof complexity ideas to transfer lengths-of-proofs lower bounds for a propositional proof system P into examples of hard unsatisfiable formulas for a class Alg(P) of SAT algorithms determined by P. The class Alg(P) contains those algorithms M for which P proves in polynomial size tautologies expressing the soundness of M. For example, the class Alg(F-d) determined by a depth d Frege system contains the commonly considered enhancements of DPLL (even for small d). Exponential lower bounds are known for all F-d. Such results can be interpreted as a form of consistency of P not equal NP. Further we show how the soundness statements can be used to find hard satisfiable instances, if they exist. Pracoviště Matematický ústav Kontakt Jarmila Štruncová, struncova@math.cas.cz, library@math.cas.cz, Tel.: 222 090 757 Rok sběru 2013
Počet záznamů: 1