Решатели SAT становятся все более и более эффективными в решении больших случаев и используются в качестве бэкэнда в различных контекстах. Каждый раз, когда кто-то хочет использовать их для решения проблемы в определенной области, он / она должен придумать специальную кодировку, которая не только имеет правильный набор решений, но также помещает ограничения (даже избыточные) в форму это помогает эвристике решателей быстрее находить решение.
Многие такие кодировки кажутся мне очень распространенными, например: утверждение, что конечный набор узлов связан как дерево, или как DAG, или список отсортирован ...
Существует ли репозиторий / книга рецептов общих кодировок для общих проблем с оптимизированными решениями?
reference-request
satisfiability
sat-solvers
Bordaigorl
источник
источник
Ответы:
Несколько лет назад я прочитал обзорную статью Магнуса Бьорка « Успешные методы кодирования SAT ».
Абстрактный:
источник
Это всегда хорошая идея, чтобы сначала проверить Руководство по удовлетворенности [1] (я думаю, это не в свободном доступе, извините). Здесь глава 2 называется «Кодировки CNF». По крайней мере, книга содержит литературные ссылки о состоянии дел на момент написания, и вы можете расширить свой поиск по ним.
Кроме того, здесь и здесь есть два недавних слайда по предварительной обработке SAT. На слайдах дан краткий обзор методов предварительной обработки, а также дополнительные ссылки. Идея состоит в том, что вместо того, чтобы пытаться «вручную» моделировать проблему эффективным способом, вы просто моделируете ее самым простым способом, нажимаете кнопку go, и программное обеспечение дает вам эффективное кодирование.
[1] Biere, Armin, Marijn Heule и Hans van Maaren, ред. Справочник удовлетворенности. Том 185. IOS Press, 2009.
источник
не совсем прямой ответ, но другой, все более тесно связанный аспект: некоторые из них охватываются относительно новой областью исследований, известной как SMT, Satisfiability Modulo Theories . Основная идея состоит в том, чтобы объединить кодировки проблем (например, целочисленную арифметику, графики и т. д.) в решатель SAT, а также использовать / использовать дополнительные знания, которые дает эта связь, для создания более совершенных алгоритмов решения. вот опрос. как уже указывалось, они могут быть гораздо более эффективными, чем комбинирование специального механизма кодирования со стандартными решателями SAT.
Теории удовлетворенности по модулю: закуска / Леонардо де Моура и Николай Бьернер
источник