Ф. Парт (АУ)

Сложность параметризованных резолюций

Доклад по статье: Beyersdorff, Galesi, Laura "Hardness of Parameterized
Resolution"

Доклад будет посвящен последним результатам в области сложности
параметризованных доказательств. Это направление Computer Science возникло
совсем недавно с целью посредством доказательства нижних оценок для
параметризованных систем доказательств получить неравенство классов
параметризованных языков W[2] и co-W[2], а значит и неравенство W[2] и FPT.
В первой статье Dantchev et al. "Parameterized proof complexity" были
сформулированы основные определения, а также приведена классификация размера
параметризованных tree-like резолюций на семействах пропозициональных
формул, являющихся записью формул логики первого порядка для конечных
моделей. В частности, было доказано, что параметризованные tree-like
резолюции не fpt-ограничены т.е. имеют большие доказательства на некоторых
семействах формул. В статье "Hardness of Parameterized Resolution" этот
результат был передоказан с использованием асимметричного варианта игр
Prover'a и Deleyer'a, что позволяет обойтись без привлечения формул первого
порядка. Также в статье приводятся следующие результаты:

1) Определяется класс семейств параметризованных противоречий, имеющих
короткие доказательства в параметризованных tree-like резолюциях.
2) Доказывается, что параметризованные dag-like резолюции не fpt-ограничены.
Для этого применяются игры Prover'a и Delayer'a придуманные Пудлаком для
доказательства нижних оценок на обычные dag-like резолюции.