Какое точное определение Random K-SAT?

12

Есть 4 различных ограничения, которые мы можем иметь при определении Random K-SAT.
1) Общее количество литералов в заданных предложениях в точности равно K или AT большинству K
2) Данный литерал может использоваться с заменой или без замены в одном и том же предложении (A или A или A)
3) Данная переменная может использоваться с или без замены в том же пункте (A или ~ A или ~ A)
4) Данные пункты могут использоваться с или без замены в заданной формуле.
Каково было бы наиболее «правильное» определение? Каковы плюсы и минусы использования этих разных определений?

Тайфун Пей
источник
17
Я не думаю, что существует единственное общепринятое определение.
Цуёси Ито
5
Еще один другой выбор, который вы можете сделать, это выбрать фиксированное количество предложений (с заменой или без) или выбрать выборку Пуассона (каждое предложение включается независимо с фиксированной вероятностью).
Дэвид Эппштейн
4
@Tsuyoshi, Geekster: Я согласен с Tsuyoshi, насколько я знаю, что SAT Solvers не нуждается ни в каком определении Random k-SAT, какой бы метод они ни использовали (DPLL, локальный поиск, распространение в опросе). Я на 100% уверен, что любой серьезный SAT Solver удалит дублированные предложения, тавтологические предложения и дублированные литералы перед началом поиска. Некоторые решатели также удаляют подгруппы.
Джорджио Камерани
4
Я не думаю, что есть ответ на вопрос в текущей форме, потому что никакие определения не кажутся «более правильными», чем другие, и «минусы и плюсы», вероятно, зависят от того, для чего вы хотите использовать результаты случайного k-SAT. Я проголосовал, чтобы закрыть это как не реальный вопрос.
Tsuyoshi Ito
4
Я предполагаю, что вопрос можно переформулировать, убрать «наиболее правильную» часть и сконцентрироваться на минусах и плюсах под некоторыми конкретными результатами. (Или ответ может проходить через каждый возможный результат.) Поскольку этот вопрос чем-то похож на вопрос о кратковременном сокращении, который, кажется, находится в рамках безо всяких аргументов, лично я хотел бы, чтобы этот вопрос оставался открытым.
Сянь-Чжи Чан 之 之

Ответы:

15

k

k k

Две основные модели:

Selman случайная модель - Повторные пункт являются разрешены . Кайл дал эту хорошую ссылку в комментариях к своему ответу, но ошибочно предположил, что модель не допускает повторных предложений. Связанная (немного другая) версия статьи содержит более подробное обсуждение случайной модели в Разделе 3: «Этот метод генерации допускает дублирование предложений в формуле ... Однако, когда N получает большие дубликаты, они станут редкими, потому что мы обычно выберите только линейное количество предложений. "

m2k(nk)

Эквивалентность мест фазовых переходов :

Однако фазовый переход (порог выполнимости 50%) происходит при одном и том же отношении к переменной, независимо от того, какая из этих моделей выбрана по существу по той причине, что Selman et al. отметил в своей статье.

Пусть обозначает ожидаемое количество идентичных пар предложений в случайном -SAT экземпляре Сельмана. Вероятность того, что данная пара предложений идентична, равна , тогда как общее количество пар предложений равно . По линейности ожидания, .A(n,m,k)(n,m,k)p=1/(2k(nk))N=(m2)A(n,m,k)=pN=(m2)/2k(nk)

По теореме 3 в [1] доказываемая верхняя граница расположения фазового перехода -SAT с использованием модели Ахлиопты возникает при . Исправив и установив мы получимm = O ( 2 k n ) k 3 m = O ( 2 k n )km=O(2kn)k3m=O(2kn)

A(n,m,k)=(m2)/2k(nk)=O(m2)/O(nk)=O(n2)/O(nk) .

Тогда, поскольку , , это означает, что в ожидании будет множество повторяющихся предложений вокруг -SAT фазовый переход при генерации случайных формул САТ с использованием модели Сельмана.k3klimnO(n2)/O(nk)=0k

Бесстыдная самореклама - я кратко обсуждаю эти темы в разделе 4.1 моей магистерской работы .

Случайный QBF

Как выясняется, ситуация гораздо интереснее для случайного QBF. Что касается AFAIK, в первых трех работах по случайному QBF каждая предложена новая случайная модель, критикующая своего предшественника.

Смотрите следующие документы:

  • Cadoli et al. «Экспериментальный анализ вычислительных затрат на оценку количественных булевых формул». AI * IA 1997
  • Гент + Уолш «За пределами NP: фазовый переход QSAT». AAAI / IAAI 1999
  • Chen + Interian "Модель для генерации случайных количественных булевых формул". IJCAI 2005
Гек Беннетт
источник
14

[Отредактировано для ясности]

Наиболее широко используемое определение в научной литературе - это определение, которое требует ровно k различных переменных в предложении, а не дублирующих предложений. Если вы ослабите ограничение по отдельным переменным, большая часть существующих исследований не будет иметь смысла для вас, потому что ваши результаты не будут совпадать с их результатами. Хорошо известный фазовый переход sat / unsat будет происходить с другим отношением «условие-переменная» (если этот переход существует вообще), и вы не найдете сложных примеров SAT, которые можно было бы ожидать из литературы.

Кайл Джонс
источник
3
Генерирование Митчелла, Сельмана и Левеска проблем порождения трудностей с удовлетворением . Раздел 4 описывает то, что они называют «Случайный K-SAT». Газета не говорит об ослаблении ограничений; это происходит из-за того, что я модифицировал случайный генератор 3SAT и добавил много экземпляров в типичный решатель SAT на основе DPLL.
Кайл Джонс
5
«Наиболее правильное определение - это такое, которое дает фазовый переход sat / unsat на уровне около 4,26 предложений на переменную для случайного 3SAT». Ты, наверное, шутишь.
Цуёси Ито
1
@ Tsuyoshi: Хотя «самый правильный» определенно сложен, я думаю, что аргумент в том, что эта версия является стандартной и одной из наиболее изученных.
Гек Беннетт
2
Вы делаете странное утверждение, что 4.26 - это магическое число, которое выделяет конкретное определение термина «случайный k-SAT» как наиболее правильное. Если это не шутка, я не знаю, что сказать.
Tsuyoshi Ito
4
Нет, я утверждаю, что обнаружение фазового перехода и все последующие исследования и последующие статьи согласуются с определением по умолчанию случайного k-SAT, которое я и дал. Если вы используете другое определение, многие статьи не будут иметь смысла для вас, потому что ваши результаты не будут совпадать с их результатами. Если вы работаете над SAT-решателем, вы найдете простые случаи, когда в каждой статье, которую я читал, говорится, что вы должны найти сложные. В этом нет ничего волшебного, просто установили соглашение в этой точке. Если вы хотите привести контрпримеры, сделайте это.
Кайл Джонс