Is cost minimization possible in 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
}

// .. same way items 4 to 10

Is it possible to select n (such that n = 1 to 10) items so that the sum of prices of the selected items is minimum?

For n=3 items the result should be item1, item2 and item3.

If possible how to write this thing in Alloy?

Thanks a lot in Advance for your kind reply.

Answer 1

It is possible to write such a higher-order query (e.g., find me a set of items such that no other set of items has a lower total price), but it is not possible to automatically solve it. There are a few workarounds though.

First, here's how you can rewrite your model so that you don't have to manually write 10 different sigs for prices from 1 to 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] }

Now, you could express the aforementioned query in Alloy like this:

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

but if you try to run it you'll get the following error:

Analysis cannot be performed since it requires higher-order quantification that could not be skolemized.

What you can do instead is to check if there exists a set of items whose total price is lower than a given price, e.g.,

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

In this example, the property to be checked is there is no set of exactly 3 items whose total price is less than 7. If you now ask Alloy to check this property, you'll get a counterexample in which iset contains exactly the 3 lowest-priced items, and therefore its total price is 6. Then if you change the check command above to ask if there is a set of 3 items whose total price is lower than 6, you won't get a counterexample, meaning that 6 is indeed the lowest price possible. As you can see, you can't ask Alloy to tell you that the answer is 6 in a single run, but you can run Alloy iteratively to arrive at the same conclusion.