Возможно ли внедрение решения для SAT?

10

Меня интересуют "сложные" отдельные примеры NP-полных задач.

Райан Уильямс обсудил проблему SAT0 в блоге Ричарда Липтона . SAT0 спрашивает, имеет ли экземпляр SAT конкретное решение, состоящее из всех 0. Это заставило меня задуматься о создании экземпляров SAT, которые, вероятно, будут «сложными».

Рассмотрим экземпляр SAT с предложениями и переменными, где является «достаточно большим» в том смысле, что он попадает в область за пределами фазового перехода, где почти все экземпляры являются неудовлетворительными. Пусть будет случайным назначением значений .m n α = m / n x ϕϕmnα=m/nxϕ

Можно ли изменить для получения нового экземпляра , чтобы был "в значительной степени похож" на , но чтобы было удовлетворительным условием для ?ϕ | x ϕ | x ϕ x ϕ | Иксϕϕ|xϕ|xϕxϕ|x

Например, можно попытаться добавить к каждому предложению случайно выбранный литерал из решения, чего еще нет в предложении. Это гарантирует, что является решением.x

Или это безнадежно, что приводит к быстрому алгоритму поиска «скрытого» решения, как в следующей недавней статье?

Я знаю о дискуссии Кука и Митчелла и работе, на которую они ссылаются. Тем не менее, я не смог найти ничего о том, что происходит со структурой формулы, когда кто-то пытается явно вставить в нее удовлетворительное назначение. Если это фольклор, указатели будут очень кстати!

  • Стивен А. Кук и Дэвид Дж. Митчелл, Нахождение трудных примеров проблемы удовлетворенности: обзор , серия DIMACS по дискретной математике и теоретической информатике 35 1–17, AMS, ISBN 0-8218-0479-0, 1997. ( PS )
Андраш Саламон
источник

Ответы:

13

Вы можете взять любую формулу и изменить ее на формулу где - это "жесткий" экземпляр SAT, единственным решением которого является . Один из способов построения такой формулы - использование криптографии: если - односторонняя перестановка, и мы выбираем случайным образом и устанавливаем , то можно преобразовать в формулу SAT, так что является ее единственным решением, и, таким образом, нахождение соответствует обращению . (Нам нужно, чтобы этот был случайным, но это что-то похожее в любом случае предполагается, если мы находимφ ψ x ψ x x f : { 0 , 1 } n{ 0 , 1 } n x y = f ( x ) y x x f x xφφψxψxxf:{0,1}n{0,1}nxy=f(x)yxxfxx должно быть трудно.)

Боаз Барак
источник
Ах, имеет полиномиальный размер в и . Спасибо! ϕ ψ xϕψxϕψx
Андрас Саламон
6

Если я правильно понимаю саму суть вашего вопроса, вы хотите взять сравнительно легкий экземпляр (так как вы ставите себя в районе , где ), и преобразовать его в сложное путем вложения решения. Я сомневаюсь, что это сработает.mn>4.3

Экспериментальные данные показывают, что при построении случайного экземпляра «вокруг» заранее определенного решения такой случай будет легче обычного (по сравнению с аналогичными экземплярами, имеющими одинаковые n и m ). Это как если бы скрытое решение помогло решить SAT, направляя его через пространство поиска. Обычно, чтобы построить такой экземпляр, мы генерируем случайные предложения как обычно (например, выбирая k литералов случайным образом и отрицая каждый из них с вероятностью p = 1xnmk ) но мы отбрасываем те пункты, которые не удовлетворены нашим скрытым решениемx. Что касается вашего подхода построенияϕ| xот и жесткий случайϕ: я никогда не пробовал это, но я «чувствую», чтоϕ| хстанет легче, если не тривиально. Я полагаю, что выполнение этого увеличило бы количество обращенийлитераловx(количество обращений литералаl- это число вхожденийlв заданной формуле), и что это привело бы решатель SAT к цели. Может быть, пространства решенийϕиϕ| Иксp=12xϕ|xϕϕ|xxllϕϕ|xбудет аналогичным (если не почти идентичным), как это происходит в примере SAT0 Райана Уильямса (почти идентичные пространства решений, но совершенно другой твердости). Вы пробовали свой подход на практике? Было бы интересно посмотреть, как один и тот же SAT-решатель ведет себя на и на ϕ | х .ϕϕ|x

РЕДАКТИРОВАТЬ 1 (23 сентября 2010 г.): Подумав немного больше, я чувствую, что на самом деле пространство решения будет сильно отличаться от ϕ . Вы добавляете литерал в каждое предложение, так что вы даете большую степень свободы таким предложениям (т. Е. У каждого предложения больше шансов быть удовлетворенным): возможно, результирующее пространство решений будет массово преобразовано.ϕ|xϕ

РЕДАКТИРОВАТЬ 2 (1 октября 2010): я думал о следующей очень простой и не оригинальной идее. Дан начальный экземпляр и присваивание x :ϕx

  1. Удалить из все те пункты, которые не удовлетворены x . Это увеличит пространство решения, и в него должно быть вставлено x .ϕxx

  2. Предположим, вы удалили статей. Теперь случайным образом добавьте m x новых предложений, следя за тем, чтобы они не были неудовлетворены x (это снова сузит пространство решения, но без выталкивания x из него).mxmxxx

Я не знаю, сработает ли это или нет. Я еще не пробовал. Точнее, я не уверен, что шагу 1 всегда удается внедрить в пространство решения (возможно, x исключается некоторой комбинацией предложений, даже если каждое из них не неудовлетворено x ?).xxx

Джорджио Камерани
источник
Спасибо за комментарии, я согласен, что пространство решения будет изменено. Как указано в вопросе, я хочу знать, есть ли способ изменить формулу, чтобы скрыть решение. Добавление литералов в каждое предложение означает доказательство существования того, что можно добавить решение в формулу. Я не хотел сказать, что это единственный, лучший или даже хороший метод.
Андрас Саламон
xϕ|xϕx
В идеале нужен метод, вычисляемый по времени, который не изменяет пространство решений «слишком сильно» ...
Андрас Саламон,
n3log n
3lognn2nn3logn
4

Наилучший способ генерирования сложных экземпляров проблем с NP-завершением, о которых я знаю, - это использовать отображение Кука, чтобы свести тщательно отобранные экземпляры некоторых других сложных задач NP (таких как проблема дискретного логарифма или целочисленная факторизация) к SAT. Это те же «сложные проблемы», которые используются математиками для обеспечения криптографической безопасности в таких протоколах, как RSA и Diffie-Hellman.

Филип Уайт
источник
Ссылки, пожалуйста?
gphilip
не уверен, почему понизить за этот ответ. Кто бы это ни сделал, он должен объяснить.
Суреш Венкат