Книга рецептов для спутниковых кодировок?

17

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

Многие такие кодировки кажутся мне очень распространенными, например: утверждение, что конечный набор узлов связан как дерево, или как DAG, или список отсортирован ...

Существует ли репозиторий / книга рецептов общих кодировок для общих проблем с оптимизированными решениями?

Bordaigorl
источник
1. Этот вопрос выглядит очень полезным, но также потенциально заграничным. Я думаю, что может быть лучше, если вы сфокусируете его на одном домене (да, это может включать в себя несколько вопросов, по одному на домен, но обязательно сделайте некоторое исследование, прежде чем спрашивать и показывать нам, что вы сделали).
DW
2. Кроме того, какое исследование вы провели? Вы смотрели на интерфейсы SAT, такие как STP, Alloy и Minion? Вы смотрели на cs.stackexchange.com/q/12087/755 , cs.stackexchange.com/q/13188/755 , cs.stackexchange.com/a/6522/755 , cs.stackexchange.com/a/12153/ 755 ? на вопросы помечены сат-решатели или выполнимость ?
DW
Да, вопрос может быть немного широким. @DW спасибо за ссылки, некоторые из которых имеют прямое отношение. Я должен был упомянуть, что я не заинтересован в решении конкретной проблемы или в общих методах для более эффективного кодирования; Выражение «лучшие практики», которое я использовал, вероятно, вводит в заблуждение, я отредактирую. Я заинтересован в книге рецептов =)
Bordaigorl
Что касается области, я бы сказал (гипер) теория графов, но это, вероятно, все еще очень широко ...
Bordaigorl
См. Также связанный вопрос cs.stackexchange.com/q/12087
Андраш Саламон

Ответы:

9

Несколько лет назад я прочитал обзорную статью Магнуса Бьорка « Успешные методы кодирования SAT ».

Абстрактный:

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

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

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

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

Это всегда хорошая идея, чтобы сначала проверить Руководство по удовлетворенности [1] (я думаю, это не в свободном доступе, извините). Здесь глава 2 называется «Кодировки CNF». По крайней мере, книга содержит литературные ссылки о состоянии дел на момент написания, и вы можете расширить свой поиск по ним.

Кроме того, здесь и здесь есть два недавних слайда по предварительной обработке SAT. На слайдах дан краткий обзор методов предварительной обработки, а также дополнительные ссылки. Идея состоит в том, что вместо того, чтобы пытаться «вручную» моделировать проблему эффективным способом, вы просто моделируете ее самым простым способом, нажимаете кнопку go, и программное обеспечение дает вам эффективное кодирование.


[1] Biere, Armin, Marijn Heule и Hans van Maaren, ред. Справочник удовлетворенности. Том 185. IOS Press, 2009.

Юхо
источник
3

не совсем прямой ответ, но другой, все более тесно связанный аспект: некоторые из них охватываются относительно новой областью исследований, известной как SMT, Satisfiability Modulo Theories . Основная идея состоит в том, чтобы объединить кодировки проблем (например, целочисленную арифметику, графики и т. д.) в решатель SAT, а также использовать / использовать дополнительные знания, которые дает эта связь, для создания более совершенных алгоритмов решения. вот опрос. как уже указывалось, они могут быть гораздо более эффективными, чем комбинирование специального механизма кодирования со стандартными решателями SAT.

  • Теории удовлетворенности по модулю: закуска / Леонардо де Моура и Николай Бьернер

    Теория удовлетворенности по модулю (SMT) - это проверка выполнимости логических формул над одной или несколькими теориями. Эта проблема основана на сочетании некоторых из наиболее фундаментальных областей информатики. Он объединяет проблему булевой выполнимости с областями, такими как те, которые изучаются в выпуклой оптимизации и терминах манипулирования символическими системами. Он также опирается на наиболее плодотворные проблемы символической логики прошлого века: проблему решения, полноту и неполноту логических теорий и, наконец, теорию сложности. Проблема модульного комбинирования алгоритмов специального назначения для каждой области является такой же глубокой и интригующей, как поиск новых алгоритмов, которые особенно хорошо работают в контексте комбинации. SMT также играет очень полезную роль в разработке программного обеспечения. Современное программное обеспечение, Аппаратный анализ и инструменты на основе моделей становятся все более сложными и многогранными программными системами. Однако в их основе всегда лежит компонент, использующий символическую логику для описания состояний и преобразований между ними. Хорошо настроенный решатель SMT, учитывающий новейшие достижения, обычно масштабируется на несколько порядков больше, чем пользовательские специальные решатели.

ВЗН
источник
Это очень хороший момент. Но даже когда вы используете SMT-решатель, есть часть поиска, основанная исключительно на SAT, которая может извлечь выгоду из успешных «рецептов» ...
Bordaigorl
не совсем точно сказать, что это «чисто основанная на SAT часть поиска», потому что (как указано / мое понимание) она использует специальную известную / построенную структуру сгенерированных экземпляров в своей эвристике, которую не решал бы «ванильный» решатель «признают». другими словами, он (т.е. комбинация ) не является «приводимым / разделяемым» для составных частей (т.е. кодер плюс решатель) или просто для другой стандартизированной системы кодирования.
ВЗН
Понимаю. Я буду читать больше об этом, спасибо!
Бордайгорль
конечно. Также обратите внимание на то, что программирование набора ответов несколько похоже.
vzn