合金中的锁挑战

Question

我想用Alloy解决the following lock challenge。

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

我创建了一个快速草稿：

sig Digit, Position{}

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

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

在这种情况下，请您：

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

谢谢。

Answer 1

我对这个谜题的框架是：

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 2

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

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

在文本视图中寻找答案。

更新我们讨论了合金列表，我想用更易读的版本修改我的解决方案：

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

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

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

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

Answer 4

是的，我认为Alloy适合这类问题。

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

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

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

Answer 5

我喜欢此页面上的 Nomura 解决方案。我对谓词和要解决的事实稍作修改。

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 (https://*.com/a/61022419/5005552) 提出的新难题证明了原始解决方案的一个弱点：它没有考虑代码中数字的多次使用。对“正确”表达式的修改解决了这个问题。将每个猜测的数字与传递代码中的数字的并集相交，并将它们相加以获得真正的基数。我将匹配封装在一个函数中，它会为每个数字返回 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]}