在 Alloy 中锁定挑战

Question

我想解决 using Alloy.

我的主要问题是如何为表示数字键的整数建模。

我创建了一个快速草稿：

sig Digit, Position{}

sig Lock {
 d: Digit one -> lone Position
}

run {} for exactly 1 Lock, exactly 3 Position, 10 Digit

在这种情况下，能否请您：

告诉我 Alloy 你觉得是否适合解决这类问题？
请给我一些关于如何为关键数字建模的指示（不使用 Ints）？

谢谢。

Answer 1

是的，我觉得Alloy适合这种题

关于数字，您根本不需要整数：事实上，如果它们是数字或任何一组 10 个不同的标识符（不对它们执行算术），则与此特定目的有点无关紧要。您可以使用单例签名声明数字，所有扩展签名Digit，应标记为abstract。类似于：

abstract sig Digit {}
one sig Zero, One, ..., Nine extends Digit {}

可以使用类似的策略来声明锁的三个不同位置。顺便说一句，因为你只有一把锁，你也可以将 Lock 声明为单例签名。

Answer 2

一种简单的入门方法，您并不总是需要签名。找到的解决方案可能不是预期的解决方案，但那是因为要求不明确，走了捷径。

pred lock[ a,b,c : Int ] {
    a=6 || b=8 || c= 2
    a in 1+4 || b in 6+4 || c in 6+1
    a in 0+6 || b in 2+6 || c in 2+0
    a != 7 && b != 3 && c != 8
    a = 7 || b=8 || c=0 
}

run lock for 6 int

在文本视图中寻找答案。

upate 我们对 Alloy 列表进行了讨论，我想用更易读的版本修改我的解决方案：

let sq[a,b,c]       = 0->a + 1->b + 2->c
let digit       = { n : Int | n>=0 and n <10 }

fun correct[ lck : seq digit, a, b, c : digit ] : Int    { # (Int.lck & (a+b+c)) }
fun wellPlaced[ lck : seq digit, a, b, c : digit ] : Int { # (lck & sq[a,b,c])   }

pred lock[ a, b, c : digit ] {
    let lck = sq[a,b,c] {
        1 = correct[ lck, 6,8,2] and 1 = wellPlaced[ lck, 6,8,2]        
        1 = correct[ lck, 6,1,4] and 0 = wellPlaced[ lck, 6,1,4]
        2 = correct[ lck, 2,0,6] and 0 = wellPlaced[ lck, 2,0,6]
        0 = correct[ lck, 7,3,8]
        1 = correct[ lck, 7,8,0] and 0 = wellPlaced[ lck, 7,8,0]
    }
}

run lock for 6 Int

Answer 3

我的拼图框架是：

enum Digit { N0,N1,N2,N3,N4,N5,N6,N7,N8,N9 }
one sig Code {a,b,c:Digit}

pred hint(h1,h2,h3:Digit, matched,wellPlaced:Int) {
    matched = #(XXXX)        // fix XXXX
    wellPlaced = #(XXXX)     // fix XXXX
}

fact {
    hint[N6,N8,N2, 1,1]
    hint[N6,N1,N4, 1,0]
    hint[N2,N0,N6, 2,0]
    hint[N7,N3,N8, 0,0]
    hint[N7,N8,N0, 1,0]
}

run {}

Answer 4

当您认为解决方案完成时，让我们检查解决方案是否通用。

这是另一把锁。
如果你不能用同样的形式解决这个问题，你的解决方案可能还不够。

提示 1：(1,2,3) - 没有什么是正确的。
提示 2：(4,5,6) - 没有什么是正确的。
提示 3：(7,8,9) - 一个数字正确但位置错误。
提示 4：(9,0,0) - 所有数字都是正确的，其中一个位置正确。

Answer 5

我喜欢这个页面上的野村解决方案。我对predicate 和fact 做了一点修改就解决了。

enum Digit { N0,N1,N2,N3,N4,N5,N6,N7,N8,N9 }
one sig Code {a,b,c: Digit}

pred hint(code: Code, d1,d2,d3: Digit, correct, wellPlaced:Int) {
    correct = #((code.a + code.b + code.c)&(d1 + d2 + d3))
    wellPlaced = #((0->code.a + 1->code.b + 2->code.c)&(0->d1 + 1->d2 + 2->d3))
}

fact {
    some code: Code | 
    hint[code, N6,N8,N2, 1,1] and
    hint[code, N6,N1,N4, 1,0] and
    hint[code, N2,N0,N6, 2,0] and
    hint[code, N7,N3,N8, 0,0] and
    hint[code, N7,N8,N0, 1,0]
}

run {}

更新（2020-12-29）： Nomura () 提出的新难题展示了原始解决方案中的一个弱点：它没有考虑代码中数字的多次使用。对“正确”表达式的修改解决了这个问题。将每个猜测的数字与来自传递代码的数字的并集相交，并将它们相加以获得真正的基数。我将匹配封装在一个函数中，该函数将为每个数字 return 0 或 1。

enum Digit {N0,N1,N2,N3,N4,N5,N6,N7,N8,N9}

let sequence[a,b,c] = 0->a + 1->b + 2->c

one sig Code {c1, c2, c3: Digit}

fun match[code: Code, d: Digit]: Int { #((code.c1 + code.c2 + code.c3) & d) }

pred hint(code: Code, d1,d2,d3: Digit, correct, wellPlaced:Int) {   
    // The intersection of each guessed digit with the code (unordered) tells us 
    // whether any of the digits match each other and how many
    correct = match[code,d1].plus[match[code,d2]].plus[match[code,d3]]
    // The intersection of the sequences of digits (ordered) tells us whether 
    // any of the digits are correct AND in the right place in the sequence
    wellPlaced = #(sequence[code.c1,code.c2,code.c3] & sequence[d1, d2, d3])
}

pred originalLock {
    some code: Code | 
    hint[code, N6,N8,N2, 1,1] and
    hint[code, N6,N1,N4, 1,0] and
    hint[code, N2,N0,N6, 2,0] and
    hint[code, N7,N3,N8, 0,0] and
    hint[code, N7,N8,N0, 1,0]
}

pred newLock {
    some code: Code | 
    hint[code, N1,N2,N3, 0,0] and 
    hint[code, N4,N5,N6, 0,0] and
    hint[code, N7,N8,N9, 1,0] and
    hint[code, N9,N0,N0, 3,1]
}

run originalLock
run newLock
run test {some code: Code | hint[code, N9,N0,N0, 3,1]}

在 Alloy 中锁定挑战

Lock Challenge in Alloy

alloy