I am new to alloy and was trying to pose the following puzzle given to me by a friend in terms of Alloy constraints
- 682 one digit is right and in its right place taken
- 614 one digit is right but in the wrong place taken
- 206 two digits are right but both are in the wrong place
- 738 all digits are wrong
- 380 one digit is right but in the wrong place
The solution is 042
My incomplete solution is the following:
open util/ordering[Key]
enum Numbers{o1,o2,o3,o4,o5,o6,o7,o8,o9,o0}
sig Key{
num: one Numbers
}
fact{
// 682 one digit is right and in its right place
all key: Key-first-last |
(key.prev.num = o6 and key.num != o8 and key.next.num != o2) or
(key.prev.num != o6 and key.num = o8 and key.next.num != o2) or
(key.prev.num != o6 and key.num != o8 and key.next.num = o2)
// 614 one digit is right but in the wrong place
one key: Key-first-last |
((key.prev.num = o1 or key.prev.num = o4) or
(key.num = o6 or key.num = o4) or
(key.next.num = o6 or key.next.num = o1)) and
key.prev.num != o6 and key.num !=o1 and key.next.num != o4
// 206 two digits are right but both are in the wrong place
// Haven't posed this constraint yet
// all 738 digits are wrong
all key: Key |
key.num != o7 and key.num != o3 and key.num != o8
// 380 one digit is right but in the wrong place
one key: Key-first-last |
((key.prev.num = o8 or key.prev.num = o0) or
(key.num = o3 or key.num = o0) or
(key.next.num = o3 or key.next.num = o8)) and
key.prev.num != o3 and key.num !=o8 and key.next.num != o0
}
run {} for exactly 3 Key
Can someone suggest me an optimal way or one of the optimal ways to pose the constraints as defined in the following problem?
I can see that my constraints are not exactly matching the posed problem, for example, constraint one, where my constraint is not strict enough as the problem is saying. But the way I am posing and constraining each Key will make this very verbose. I want to use some more general definitions to pose the constraint.
