SATISFIABILITY, BRANCH-WIDTH AND TSEITIN TAUTOLOGIES

[Artur Ryazanov]

Уважаемые участники complexity-семинара,

Дата и время: 01.11.19 16:00
Место: аудитория 106

На следующей сессии reading-group мы рассмотрим графовый параметр branch-width и его связь с резолюционными доказательствами. В частности, мы рассмотрим SAT-solver, порождающий доказательство любой невыполнимой КНФ-формулы F размера 2^bw(F) * poly(|F|), где bw(F) -- это branch-width формулы. Мы докажем, что для Цейтинских формул минимальная ширина резолюционного доказательства с точностью до константы совпадает с branch-width, а также, обсудим связь branch-width и tree-width.
Branch-декомпозиция КНФ-формулы ширины w это расположение клозов формулы в узлах подвешенного двоичного дерева, такое, что для любой вершины этого дерева клозы в поддереве вершины имеют не более w общих переменных с клозами вне поддерева. Branch-width формулы это минимальная ширина её branch-декомпозиции.

Статья: Михаила Алехновича и Александра Разборова SATISFIABILITY, BRANCH-WIDTH AND TSEITIN TAUTOLOGIES

С уважением,

Артур Рязанов