Хорошо известные классы булевых формул, которые требуют экспоненциально длинных доказательств с разрешением

27

Вы можете часто находить методы разрезающих плоскостей, переменное распространение, ветвление и связывание, обучение по пунктам, интеллектуальное возвращение в исходное положение или даже эвристику человека, сплетенную вручную, в решениях SAT. Тем не менее, на протяжении десятилетий лучшие SAT решатели в значительной степени полагались на методы проверки разрешения и использовали комбинацию других вещей просто для помощи и для прямого поиска в стиле разрешения. Очевидно, есть подозрение, что ЛЮБОЙ алгоритм не сможет решить вопрос о выполнимости за полиномиальное время, по крайней мере, в некоторых случаях.

В 1985 году Хакен доказал в своей статье «Непреодолимость разрешения», что принцип голубиной дыры, закодированный в CNF, не допускает доказательств разрешения полиномиального размера. Несмотря на то, что это доказывает неразрешимость алгоритмов, основанных на разрешении, оно также дает критерии, по которым можно судить о передовых решателях - и на самом деле, одно из многих соображений, которые возникают при разработке решателя SAT сегодня, - это то, как оно может работать на известных «тяжелых» случаях.

Наличие списка классов булевых формул, которые доказуемо допускают доказательства с экспоненциальным размером, полезно в том смысле, что оно дает «сложные» формулы для проверки новых решателей SAT. Какая работа была проделана при составлении таких классов вместе? У кого-нибудь есть ссылка, содержащая такой список и соответствующие доказательства? Пожалуйста, перечислите один класс булевой формулы в ответе.

Ross Snider
источник
сообщество вики?
Opt
Я сделал это сообщество вики согласно предложению.
Росс Снайдер
1
Дополнительный аспект этого вопроса, который меня заинтересует: существуют ли явные известные многоразмерные доказательства для расширенного разрешения для этих сложных случаев (например, доказательство Кука для слабых формул голубиных отверстий)?
MGwynne

Ответы:

21

Трудные случаи для разрешения :

  1. Формулы Цейтина (над графами расширителей).

  2. mnnm>n

  3. nO(n1.5ϵ)0<ϵ<1/2

Хорошее, относительно современное техническое обследование для определения нижней границы сложности доказательства, см .:

Натан Сегерлинд: сложность пропозициональных доказательств. Бюллетень символической логики 13 (4): 417-481 (2007) доступен по адресу: http://www.math.ucla.edu/~asl/bsl/1304/1304-001.ps

оборота Иддо Цамерет
источник
Это хороший пример ответа. Было бы даже лучше ответить, если бы он был разделен на несколько.
Росс Снайдер
9

Есть много хороших обзоров и книг по пропозициональной доказательственной сложности, которые содержат такие списки. Многие системы доказательств p-имитируют разрешение, поэтому любая сложная для них формула будет трудноразрешимой.

Книги:
1. Ян Крайчек, «Ограниченная арифметика, логика высказываний и теория сложности», 1995 г.
2. Стивен А. Кук и Фунг Негуен, «Логические основы сложности доказательства», 2010 г.

Обзоры:
1. Пол Бим и Тонианн Питасси, «Сложность доказательства предложения: прошлое, настоящее и будущее», 2001 г.
2. Сэмюэль Р. Бусс, «Ограниченная арифметическая и сложность предложения доказательства», 1997 г.
3. Аласдэр Уркхарт, «Сложность пропозициональные доказательства ", 1995

Также смотрите перечисленные здесь и здесь .

каве
источник
8

2n×2n2×1

Михаил Алехнович. Изуродованную проблему шахматной доски экспоненциально трудно решить. Теоретическая компьютерная наука 310 (1-3): 513-525 (2004). http://dx.doi.org/10.1016/S0304-3975(03)00395-5

Ян Йоханнсен
источник
8

n(k)22k=12logni,jKxi,ji,jK¬xi,jK{1,,n}|K|=k

Ян Йоханнсен
источник
Спасибо. Это очень интересный ответ (хотя обозначения немного отличаются, я мог бы следовать). Мой советник старшекурсников изучал теорию Рамси. Ему также удалось установить этот интерес ко мне.
Росс Снайдер
1

Разве DIMACS не поддерживает образцы наборов жестких экземпляров SAT? Я не смог найти его там просто беглым взглядом, но если вы введете «SAT» в поле их поиска, это вызовет много обращений, включая несколько статей / выступлений на сложных экземплярах SAT.

Kurt
источник
Особые трудные случаи (в отличие от семейства экземпляров) находятся здесь satcompetition.org (см. « Тесты ».)
Radu GRIGore