Literatura k tematu "slozitost resoluce" (jaro'09):
Texty na webu (postupne budu doplnovat):
Zakladni definice (a trocha historie),
Tseitinova
limited extension, korektnost, uplnost, priklad
PHP. Cook-Reckhow definice dukazoveho systemu,
hlavni problem o delkach dukazu, souvislost s NP vs. coNP.
DPLL a stromove resolucni dukazy.
Prvnich cca 12 stranek v mych
skriptech.
Spodni odhad pro PHP v R:
Buss-Turan (presentace a zobecneni
Hakenova dukazu).
Spodni odhad pro stromovou resoluci R^*:
str. 13 - 18 v mych
skriptech.
Postacujici podminka
pro spodni odhady pro R^* v jazyce t.modelu:
V.3.2 v me clanku a
diplomka T.Auera (Complexity of propositional proofs
in resolution, 2001) na FF UK.
Metoda nahodnych restrikci. Relativizace kombinatorickych
principu:
Dantchev - Riis (sekce 2 a 4).
Sire (width) resolucnich dukazu a trade-off s velikosti:
Ben-Sasson - Wigderson, a aplikace.
Sire a oblazkove hry: Atserias - Dalmau.
Prostorova slozitost resolucnich dukazu:
Esteban - Toran a
Esteban.
Zobecneni resoluce:
rozsirena resoluce ER (clanek
Cook 1975, Sekce 5) a
system R^+ (Sekce 1) a podsystemy R(f).
Tzv. feasible interpolation pro
resoluci a aplikace.