сейчас внимательно присматриваюсь к Minizinc. Minizinc показывает все допустимые решения моей модели в окне вывода при решении модели. Я немного сбит с толку, потому что я не просил minizinc решить модель как проблему удовлетворения. Есть ли вероятность, что будут показаны только оптимальные решения? Спасибо за ответы.
с уважением
Какое у вас solve заявление? Если это solve satisfy, тогда вы просите все решения. Если это solve minimize x или solve maximize x, то решающая программа покажет прогресс оптимальных решений, причем оптимальное решение будет показано последним.
С помощью OptiMathSAT версии 1.5.1 теперь можно распечатать все оптимальные решения с одинаковой стоимостью для данного FlatZinc формула с использованием опции
-opt.fzn.all_solutions=[BOOL]
например, возьмите следующий test.fzn файл
var 0..3: x ::output_var;
var 0..3: y ::output_var;
var bool: r1 ::output_var;
var bool: r2 ::output_var;
constraint int_lin_le_reif([1, 1, -1], [x, y, 4], 0, r1);
constraint int_lin_le_reif([1, 1, -1], [x, y, 2], 0, r2);
constraint bool_or(r1, r2, true);
solve maximize x;
и решите его следующим образом:
~$ ../bin/optimathsat -input=fzn -opt.fzn.all_solutions=True < test.fzn
% allsat model
x = 3;
y = 0;
r1 = true;
r2 = false;
----------
% allsat model
x = 3;
y = 1;
r1 = true;
r2 = false;
----------
=========
Максимальное значение для x равно 3, поэтому решатель печатает только те модели test.fzn, для которых x равно 3.
Естественно, как упомянул @hakank в своем ответе, кого-то может заинтересовать развитие решений в сторону оптимального. Это также можно сделать в OptiMathSAT, используя параметр
-opt.fzn.partial_solutions=[BOOL]
В приведенном выше примере это даст
~$ ../bin/optimathsat -input=fzn -opt.fzn.partial_solutions=True < test.fzn
% objective: x (model)
x = 2;
y = 0;
r1 = true;
r2 = true;
----------
% objective: x (model)
x = 3;
y = 0;
r1 = true;
r2 = false;
----------
% objective: x (optimal model)
x = 3;
y = 0;
r1 = true;
r2 = false;
----------
=========
Здесь поиск оптимизации находит две разные модели: начальную, в которой x равно 2, и оптимальную, в которой x равно 3. Последняя модель печатается дважды: первый раз, как только она будет найдена, второй раз, когда решатель сможет доказать, что это действительно оптимальное решение проблемы.
