Как я могу выразить проблемы с расписанием в minisat?

Minisat — это инструмент программирования/удовлетворения ограничений. Существует версия Minisat, которая работает в браузере http://www.msoos.org/2013/09/minisat-in-your-browser/

Как я могу выразить проблему планирования с Minisat? Есть ли язык более высокого уровня, который компилируется в Minisat, который позволил бы мне это выразить?

Я имею в виду для решения таких задач, как составление расписания экзаменов. http://docs.jboss.org/drools/release/6.1.0.Final/optaplanner-docs/html_single/#examination

введите здесь описание изображения


constraint-programming sat
person Phil    schedule 16.12.2014    source источник

Ответы (3)


arrow_upward
5
arrow_downward

Еще одним языком моделирования высокого уровня является Picat (http://picat-lang.org/), в котором есть возможность решения/2 для конвертировать в CNF при использовании спутникового модуля, например. "решить([дамп], Vars)". Синтаксис при использовании модуля sat, а также модулей cp и mip аналогичен стандартному синтаксису CLP.

Некоторые примеры Picat см. на моей странице Picat: http://hakank.org/picat/ .

person hakank    schedule 17.12.2014
comment
Я изучаю minizinc, и, на самом деле, ваш сайт - лучший ресурс (как и ваши ответы здесь, на SO)... увы, через несколько дней он не отвечает... В любом случае, ваш репозиторий github по-прежнему доступен. Спасибо - person CapelliC; 22.01.2015
comment
@CapelliC: Спасибо за добрые слова. Мой сайт hakank.org сейчас недоступен, но я делаю все возможное, чтобы исправить это как можно скорее. Здорово, что вы нашли репозиторий GitHub. - person hakank; 22.01.2015

arrow_upward
3
arrow_downward

решатели SAT, такие как Minisat или Cryptominisat обычно считывают набор предложений логических OR выражения в конъюнктивной нормальной форме (CNF). Требуется шаг кодирования, чтобы преобразовать вашу задачу в этот формат CNF.

Решатели Circuit SAT обрабатывают вложенное логическое выражение, а не CNF. Но похоже, что этот тип решателей в настоящее время уступает CNF SAT решателям.

Решатели программ с ограничениями, такие как Minizinc, используют язык высокого уровня, который легче писать и понимать. . В зависимости от используемых функций Minizinc может переводить язык ввода в CNF/DIMACS формат, подходящий для SAT-решателя.

Статья Питера Стаки "Нет проблем с CNF" объясняет эту идею. Его слайды также содержат некоторые сведения о планировании.

Взгляните на примеры Minizinc для планирования, написанные Хакан Кьеллерстранд.

Планирование и SAT — это обширное рассмотрение темы.

person Axel Kemper    schedule 16.12.2014

arrow_upward
0
arrow_downward

Я работал над этим проектом несколько месяцев назад.

Это было действительно интересно сделать.

Чтобы использовать miniSAT (или любой другой решатель SAT), вам придется свести задачу планирования к задаче SAT.

Я могу порекомендовать вам этот вопрос, который я задал в 3-х частях.

Расписание классов для логической выполнимости [сокращение полиномиального времени]< /а>

Планирование классов для логической выполнимости [полиномиально- сокращение времени] часть 2

Планирование классов для логической выполнимости [сокращение полиномиального времени] Final Часть

И вы в основном увидите, шаг за шагом, как преобразовать задачу планирования в задачу SAT, которую MiniSAT может прочитать и решить :).

Еще раз спасибо @amit, который очень помог в этом проекте.

С этим ответом вы сможете решить N комнат с T учителями, которые преподают S предметов G разным группам учеников :), что, я думаю, достаточно для 99% задач планирования.

person Valentin Montmirail    schedule 27.07.2015