Почему между решателями SAT существует огромная разница?

25

SAT решатели очень важны при алгебраических атаках , например, walksat и minisat .

Тем не менее, при решении проблем с эталонными тестами, имеющихся здесь, существует огромная разница в производительности - Walksat намного быстрее, чем minisat для этих задач. Почему это?

Эта реализация walksat, похоже, имеет некоторые улучшения производительности - есть ли причина, по которой она не была включена в международные соревнования SAT ?

ir01
источник
Ваш второй вопрос о том, почему определенный алгоритм был исключен из определенного конкурса, вероятно, выходит за рамки этого сайта. Ваш первый вопрос о том, что делает один алгоритм часто быстрее другого, я считаю честной игрой, но, возможно, потребуется перефразировать его, чтобы сделать его более понятным для теории.
Лев Рейзин
Краткое примечание: Minisat довольно старый, кажется, не поддерживается, и не участвовал в конкурсе. Кроме того, что вы подразумеваете под "огромным" и на какой трек вы ссылаетесь (случайный / созданный / приложение)?
Раду GRIGore
5
@Radu: MiniSAT 2.2.0 был выпущен в июле 2010 года. Я бы не сказал, что он не поддерживается. Кроме того, код довольно стабилен и чист, поэтому нечастые обновления могут не быть проблемой. Я согласен, хотя, что новые решатели лучше отражают современное состояние.
Виджай Д
1
Вопрос кросс-пост от Crypto.SE crypto.stackexchange.com/questions/153/… .
М. Алагган

Ответы:

33

Да, между MiniSAT и WalkSAT есть большая разница. Во-первых, давайте поясним - MiniSAT - это конкретная реализация универсального класса алгоритмов DPLL / CDCL, которые используют отслеживание возвратов и изучение предложений, тогда как WalkSAT - это общее название алгоритма, который чередует жадные и случайные шаги.

В общем случае DPLL / CDCL намного быстрее для структурированных экземпляров SAT, а WalkSAT быстрее для случайных k-SAT. Промышленные и прикладные экземпляры SAT, как правило, имеют большую структуру, поэтому DPLL / CDCL доминирует в большинстве современных решателей SAT. Однако, например, один метод может выиграть, что является одной из причин, почему портфельные решатели стали популярными.

Я сильно обеспокоен вашим утверждением о том, что WalkSAT намного быстрее, чем MiniSAT в случаях на этой странице. Во-первых, там есть гигабайты экземпляров SAT - сколько вы пытались сравнить их? WalkSAT совсем не конкурентоспособен в большинстве случаев, поэтому его не часто можно увидеть на соревнованиях.

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

Гек Беннетт
источник
17

AИксYВYИкс

Хорошая статья , чтобы читать по этой теме это один на Нудельман и др . Суть статьи в том, чтобы определить простые для вычисления функции экземпляров SAT, которые могут сказать вам, какие алгоритмы, вероятно, будут работать хорошо, а какие нет. Используя эту технику, можно создать алгоритм на основе портфеля, который быстро проанализирует экземпляр проблемы, а затем решит экземпляр с помощью наиболее подходящего алгоритма. За этим следует ряд документов; поиск в Google SATzilla найдет много материалов для чтения.

AВ

Джеймс Кинг
источник