Приращение элементов массива переменных в Minizinc

Я хотел бы выполнить простую операцию приращения для определенных элементов массива:

Пример минимального неработающего:

array[1..2] of var 0..1: a = [0, 0];

constraint forall (i in 1..2) (
    a[i] = a[i] + 1
);

output ["\(a)"];

solve satisfy;

Это дает результат minizinc

  WARNING: model inconsistency detected
  stack.mzn:3:
  in call 'forall'
  in array comprehension expression
    with i = 1
  stack.mzn:4:
  in binary '=' operator expression
=====UNSATISFIABLE=====
% stack.fzn:1: warning: model inconsistency detected before search.

Почему это несоответствие модели - почему я не могу ссылаться на старое значение текущего элемента массива? Есть ли другой способ увеличить текущий элемент массива на 1?

Я новичок в решении ограничений, поэтому надеюсь, что это не такой уж и глупый вопрос.


constraint-programming minizinc
person Pethor    schedule 14.03.2018    source источник
comment
Это похоже на решение уравнения x+1=x   -  person Erwin Kalvelagen    schedule 15.03.2018

Ответы (1)


arrow_upward
11
arrow_downward

Важно знать, что MiniZinc - это декларативный язык. В ограничении вы не формулируете инструкцию, а излагаете «правду», известную решателям.

Это означает, что такая инструкция, как a = a + 1, не будет работать, потому что вы заявляете, что мы ищем значение для a, которое является его собственным значением + 1. Поскольку такого значения не существует, мы называем модель несогласованной, поскольку решения не могут быть найдены.

Идея элементов ограничения состоит в том, чтобы выразить отношения между различными переменными и параметрами. Например, вы можете написать: constraint forall(i in N) (a[i] = a[i-1] + 1). Это будет означать, что мы будем искать значение a[i], которое на 1 больше, чем a[i-1] для всех i in N. (Обратите внимание, что нам, вероятно, следует добавить оператор if, чтобы убедиться, что i-1 остается в заданных пределах)

Как правило: если есть литерал с одной стороны от знака равенства, использование этого литерала с другой стороны создаст противоречивую модель.

Если вы все еще хотите создать модель MiniZinc, которая увеличивает значения данного массива на единицу, вы можете использовать следующую модель:

set of int: N = 1..2
array[N] of int: a = [0,1];
array[N] of var int: b;

constraint forall(i in N) (
    b[i] = a[i] + 1
);

Поскольку переменные a теперь выражаются в терминах b, это не нарушает нашего правила.

person Dekker1    schedule 14.03.2018
comment
Спасибо за подробное объяснение; Думаю, мне нужно больше узнать о том, как решатели ограничений работают внутри :) - person Pethor; 14.03.2018