Solving maximizing problems in Alloy (or other optimization problems)

Question

I've bought and read the Software Abstractions book (great book actually) a couple of months if not 1.5 years ago. I've read online tutorials and slides on Alloy, etc. Of course, I've also done exercises and a few models of my own. I've even preached for Alloy in some confs. Congrats for Alloy btw!

Now, I am wondering if one can model and solve maximizing problems over integers in Alloy. I don't see how it could be done but I thought asking real experts could give me a more definitive answer.

For instance, say you have a model similar to this:

open util/ordering[State] as states

sig State {
  i, j, k: Int
}{
  i >= 0
  j >= 0
  k >= 0
}

pred subi (s, s': State) {
  s'.i = minus[s.i, 2]
  s'.j = s.j
  s'.k = s.k
}

pred subj (s, s': State) {
  s'.i = s.i
  s'.j = minus[s.j, 1]
  s'.k = s.k
}

pred subk (s, s': State) {
  s'.i = s.i
  s'.j = s.j
  s'.k = minus[s.k, 3]
}

pred init (s: State) {
  // one example
  s.i = 10
  s.j = 8
  s.k = 17
}

fact traces {
  init[states/first]
  all s: State - states/last | let s' = states/next[s] |
    subi[s, s'] or subj[s, s'] or subk[s, s']
  let s = states/last | (s.i > 0 => (s.j = 0 and s.k = 0)) and
    (s.j > 0 => (s.i = 0 and s.k = 0)) and
    (s.k > 0 => (s.i = 0 and s.j = 0))
}

run {} for 14 State, 6 Int

I could have used Naturals but let's forget it. What if I want the trace which leads to the maximal i, j or k in the last state? Can I constrain it?

Some intuition is telling me I could do it by trial and error, i.e., find one solution and then manually add a constraint in the model for the variable to be stricly greater than the one value I just found, until it is unsatisfiable. But can it be done more elegantly and efficiently?

Thanks!

Fred

EDIT: I realize that for this particular problem, the maximum is easy to find, of course. Keep the maximal value in the initial state as-is and only decrease the other two and you're good. But my point was to illustrate one simple problem to optimize so that it can be applied to harder problems.

Answer 1

Your intuition is right: trial and error is certainly a possible approach, and I use it regularly in similar situations (e.g. to find minimal sets of axioms that entail the properties I want).

Whether it can be done more directly and elegantly depends, I think, on whether a solution to the problem can be represented by an atom or must be a set or other non-atomic object. Given a problem whose solutions will all be atoms of type T, a predicate Solution which is true of atomic solutions to a problem, and a comparison relation gt which holds over atoms of the appropriate type(s), then you can certainly write

pred Maximum[ a : T ] {
  Solution[a]
  and 
  all s : T | Solution[s] implies
    (gt[a,s] or a = s)
}
run Maximum for 5

Since Alloy is resolutely first-order, you cannot write the equivalent predicate for solutions which involve sets, relations, functions, paths through a graph, etc. (Or rather, you can write them, but the Analyzer cannot analyze them.)

But of course one can also introduce signatures called MySet, MyRelation, etc., so that one has one atom for each set, relation, etc., that one needs in a problem. This sometimes works, but it does run into the difficulty that such problems sometimes need all possible sets, relations, functions, etc., to exist (as in set theory they do), while Alloy will not, in general, create an atom of type MySet for every possible set of objects in univ. Jackson discusses this technique in sections 3.2.3 (see "Is there a loss of expressive power in the restriction to flat relations?"), 5.2.2 "Skolemization", and 5.3 "Unbounded universal quantifiers" of his book, and the discussion has thus far repaid repeated rereadings. (I have penciled in an additional index entry in my copy of the book pointing to these sections, under the heading 'Second-order logic, faking it', so I can find them again when I need them.)

All of that said, however: in section 4.8 of his book, Jackson writes "Integers are not actually very useful. If you think you need them, think again; ... Of course, if you have a heavily numerical problem, you're likely to need integers (and more), but then Alloy is probably not suitable anyway."