Д. Соколов (Академический Университет)

Трудные примеры для эвристических близоруких DPLL алгоритмов. (продолжение)

Доказательство теоремы, анонсированной на прошлом семинаре.