MiniZinc: показывать точки выбора, когда они неудовлетворительны

При запуске программ в MiniZinc флаг -s позволяет мне видеть количество точек выбора, изученных при поиске решения. Однако, если условия невыполнимы, количество исследованных точек выбора не отображается.

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


person Mossmyr    schedule 27.04.2016    source источник
comment
Я не думаю, что какой-либо решатель FlatZinc имеет эту функцию. (И я не уверен, что это будет означать: если модель неудовлетворительна, есть ли какие-либо варианты отчета?)   -  person hakank    schedule 28.04.2016
comment
@hakank Я очень новичок в MiniZinc (на самом деле всего несколько дней), но, насколько я понимаю, точки выбора - это количество вариантов, изученных до того, как решение было найдено. Так что, если нет решения, удовлетворяющего условиям, разве MiniZinc не должен хотя бы сказать, сколько вариантов было изучено? Опять же, я могу быть совершенно неправ в этом.   -  person Mossmyr    schedule 29.04.2016
comment
Теперь я понимаю, что вы имеете в виду. Некоторые решатели FlatZinc могут отображать статистику (при использовании флага -s) даже для неудовлетворительных моделей, но некоторые этого не делают. А иногда первый процесс выравнивания может дать UNSATISFIABLE (Предупреждение: обнаружена несогласованность модели) без какой-либо статистики. Так что, похоже, это зависит от решателя и от того, как был достигнут UNSAT.   -  person hakank    schedule 29.04.2016
comment
@hakank Хорошо. Я думаю, что на этом мой вопрос получит ответ.   -  person Mossmyr    schedule 29.04.2016


Ответы (1)


Используя fzn-gecode, вы можете визуализировать дерево поиска, используя их функциональность Gist. Много документации по gist можно найти в Руководстве по моделированию Gecode. Однако предполагается, что вы пишете код C++.

Чтобы использовать его из модели MiniZinc, выполните следующие команды:

  1. mzn2fzn -G gecode [model].mzn (data.dzn)
  2. fzn-gecode -mode gist [model].fzn
person Dekker1    schedule 13.10.2016