Пятница 20.12. Пётр Смирнов: «Автоматизация резолюционной системы доказательств NP-трудна»

10 views

Skip to first unread message

Пётр Смирнов

unread,

Dec 18, 2019, 8:27:04 AM12/18/19

to spb-complexity

Тема: Автоматизация резолюционной системы доказательств NP-трудна
Время: пятница 20.12.2019 17:00
Место: аудитория 106
Докладчик: Пётр Смирнов

На очередной сессии reading group мы докажем, что резолюционная система доказательств неавтоматизируема за полиномиальное время, если $\mathrm{P}\neq \mathrm{NP}$ .

Более того, эта система неавтоматизируема за квазиполиномиальное время, если $\mathrm{NP}\not\subseteq \mathrm{QP}$ , и неавтоматизируема за субэкспоненциальное время, если $\mathrm{NP}\not\subseteq \mathrm{SUBEXP}$ .

Для доказательства мы покажем, что задача разделения формул с резолюционными доказательствами полиномиального размера и формул, не имеющих субэкспоненциальных резолюционных доказательств, является NP-трудной. А именно, мы построим полиномиально вычислимую функцию $G$ , которая по 3-КНФ формуле $F$ выдаст КНФ-формулу $G(F)$ со следующим свойством: если $F$ выполнима, то $G(F)$ имеет полиномиальное резолюционное доказательство, а в противном случае $G(F)$ не имеет субэкспоненциальных резолюционных доказательств.

Доклад основан на статье А. Ацериаса и М. Мюллера «Automating Resolution is NP-Hard», представленной на FOCS 2019.
Препринт статьи: https://arxiv.org/pdf/1904.02991.pdf.

Reply all

Reply to author

Forward

0 new messages