Обзор преобразований, связанных с использованием SAT решателей

13

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

Такой опрос ускользнул от меня, потому что он не существует, или я просто пропустил его?

ds.algorithms reference-request sat optimization Энтони Лабарре
источник
Что именно вы подразумеваете под "вариантами САТ"?
Джорджио Камерани
К
4
Не волнуйся, это правильное слово, я должен был это понять. С чисто практической точки зрения, однако, я не думаю, что это имеет значение (главное, насколько экономна ваша кодировка). Не могли бы вы предоставить более подробную информацию о проблеме оптимизации, которую вы пытаетесь решить? Я очень заинтересован в практическом применении SAT и в технических аспектах решения SAT.
Джорджио Камерани
Это немного сбивает с толку, что вы говорите о проблеме оптимизации, но в то же время о SAT. Обычно для оптимальности вам нужно что-то более сильное, например, MAX-SAT. Может быть, вы могли бы уточнить это.
Миколас
этот вопрос может быть несколько связан: cstheory.stackexchange.com/q/4314/4506
Миколас

Ответы:

9

Не уверен, что это то, что вы ищете, но вот один: Сильва Дж. М., Практическое применение булевой удовлетворенности .

Миколас
источник
2
Я не смог получить к нему доступ по вашей ссылке, вот еще одна . На первый взгляд, статья кажется довольно интересной, но больше ориентирована на приложения, чем на то, что я ищу.
Энтони Лабарр
@ Энтони, ну, ты же сказал, что интересуешься практическим аспектом :-) Во всяком случае, существующие основные решатели на самом деле не делают различий между различными типами SAT. В прошлом, например, проводилась работа по использованию бинарных предложений. Но существующие решатели просто используют DPLL + единичное обучение + предложение. Однако некоторые препроцессоры используют эту структуру. Но, опять же, не очень с точки зрения сложности. классификация.
Миколас
8

В главе 2 « Руководства по удовлетворенности» рассматриваются аспекты, которые следует учитывать при разработке этих преобразований, а также список ссылок, которые отвечают на мой вопрос. Это помогло мне найти несколько примеров, на которые можно взглянуть, чтобы ознакомиться с этими преобразованиями:

Энтони Лабарре
источник