Начиная SAT решающих работ

24

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

Зируй Ван
источник
6
Вы уже реализовали алгоритм DPLL? Вы точно настроили и отшлифовали свою реализацию, чтобы она работала очень быстро?
Юкка Суомела
5
Руководство по удовлетворенности - amazon.co.uk/… (возможно, проверьте библиотеку, стоимость довольно высока).
MGwynne
1
@Jukka: комментарий -> ответ?
Суреш Венкат
4
Я не согласен с Юккой. Зачем изобретать велосипед? Нет причин переделывать то, что MiniSAT уже предоставляет с открытым исходным кодом. Если вы заинтересованы в добавлении в среду CDCL, ваше добавление покажет повышенную производительность MiniSAT. Кроме того, DPLL само по себе недостаточно; много улучшений было сделано. В основном, следуйте ответу Миколаса!
Гек Беннетт
1
См. Также связанный вопрос cstheory.stackexchange.com/q/1988
Андраш Саламон,

Ответы:

18

Отличный обзор для начинающих дает следующая статья от 2009 года.

Есть несколько способов попасть в технические аспекты. Вы даже можете начать с оригинальной статьи Дэвиса-Путнэма. Это предельно ясно и имеет подробные примеры. Обсуждая оптимизацию SAT в курсе, мы обнаружили, что некоторые из них уже могут представить. Бумага Дэвиса-Лоджмена-Лавленда (я чувствую) менее поучительна, но она настолько коротка, что вы можете ее прочитать.

Могут быть способы наверстать упущенное в событиях следующих 50 лет. Я бы порекомендовал слайды лекций. Просто поиск «DPLL» приведет ко многим учебникам. Если вы просматриваете их, я уверен, что туман рассеется - до некоторой степени. Есть также много полезных опросов. Бумага Чжан-Малика - хорошее место для начала. В Руководстве по удовлетворенности есть несколько статей, которые могут оказаться полезными.

Я поддерживаю предложение Миколаоса. Код MiniSAT чистый и имеет управляемый размер. Вы можете играть с этим. Есть несколько других решателей, которые вы можете попробовать. CryptoMiniSat также довольно чистый. Вам также следует проконсультироваться с работами Армина Бьера , который пишет решатели SAT и пишет о написании решателей SAT.

Виджай Д
источник
17

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

Тогда я бы порекомендовал скачать исходный код minisat и прочитать его описание .

Конечно, это может быть индивидуально, но я считаю, что поиск исходного кода наиболее ценен.

Миколас
источник
9

Если вы ошеломлены всей этой работой, почему бы вам не начать делать вид, что никто не работал над проблемой раньше? Если ваша цель состоит в том, чтобы в конечном итоге создать конкурентоспособный SAT решатель, это будет довольно долгий путь. Начав просто играть без «проверки решений», так сказать, вы получите больше, чем потерять.

NмNм

Nм

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

Начните с хорошей обзорной статьи. Легко напасть на предмет по частям и запутаться в литературе под разными названиями для одних и тех же техник и одного и того же имени для разных техник. Кроме того, легко воспроизвести старые алгоритмические битвы (например, списки встреч, списки «голова-хвост» или два наблюдаемых литерала для реализаций DPLL), если вы не знаете, в каком состоянии это находится.

Решатели удовлетворенности по Gomes, et. и др. даст вам грубую планировку земли.

Улучшение SAT Solvers с использованием самых современных методов от Manthey приблизит вас к настоящему.

Кайл Джонс
источник