Возможна ли минимизация затрат в Alloy?

Question

abstract sig Item {
    price: one Int
}

one sig item1 extends Item {} { 
    price = 1
}

one sig item2 extends Item {} { 
    price = 2
}

one sig item3 extends Item {} { 
    price = 3
}

one sig item4 extends Item {} { 
    price = 4
}

// .. аналогично пунктам с 4 по 10

Можно ли выбрать n (например, от n = 1 до 10) товаров, чтобы сумма цен на выбранные товары была минимальной?

Для n=3 элементов результат должен быть item1, item2 и item3.

Если возможно, как написать эту вещь в Alloy?

Большое спасибо заранее за ваш добрый ответ.

Answer 1

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

Во-первых, вот как вы можете переписать свою модель, чтобы вам не приходилось вручную писать 10 разных сигнатур по ценам от 1 до 10:

sig Item {
  price: one Int
}

pred nItems[n: Int] {
  #Item = n
  all i: Int | (1 <= i && i <= n) => one price.i
}

fact { nItems[10] }

Теперь вы можете выразить вышеупомянутый запрос в Alloy следующим образом:

fun isum[iset: set Item]: Int {
  sum item: iset | item.price
}

run {
  some miniset: set Item | 
    #miniset = 3 and
    no iset: set Item | 
      #iset = #miniset and
      isum[iset] < isum[miniset]
} for 10 but 5 Int

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

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

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

pred lowerThan[iset: set Item, num: Int, min: Int] {
  #iset = num and
  isum[iset] < min
} 

check {
  no iset: set Item |
   iset.lowerThan[3, 7]
} for 10 but 5 Int

В этом примере проверяемое свойство состоит в том, что нет набора точно из 3 предметов, общая стоимость которых меньше 7. Если вы теперь попросите Alloy проверить это свойство, вы получите контрпример, в котором iset содержит ровно 3 наименования с наименьшей ценой, и поэтому его общая цена равна 6. Тогда, если вы измените команду проверки выше, чтобы спросить, есть ли набор из 3 предметов, общая стоимость которых ниже 6, вы не получите контрпример Это означает, что 6 действительно самая низкая цена. Как видите, вы не можете попросить Alloy сказать, что ответом является 6 за один проход, но вы можете запустить Alloy итеративно, чтобы прийти к тому же выводу.