为逻辑谜题建模

Question

我正在尝试从 To Mock a Mockingbird 中模拟一个逻辑谜题。我正在努力将其翻译成 SMT-LIB。谜题是这样的：

有一个花园，所有的花要么是红色的，要么是黄色的，要么是蓝色的，所有的颜色都代表着。对于您采摘的任何三朵花，至少一朵是红色的，一朵是黄色的。第三朵花永远是蓝色的吗？

我尝试将花园建模为Array Int Flower，但这不起作用，我相信这是因为数组的域固定在所有整数的范围内。 Z3 很有帮助地告诉我这是无法满足的，CVC4 只是立即返回未知。

解决这个难题的唯一方法是在花园里种一朵每种颜色的花，但我如何让解题者告诉我这个？

这是我失败的尝试：

(declare-datatypes () ((Flower R Y B)))
(declare-const garden (Array Int Flower))
(assert (forall ((a Int) (b Int) (c Int))
                (and (or (= (select garden a) R)
                         (= (select garden b) R)
                         (= (select garden c) R))
                     (or (= (select garden a) Y)
                         (= (select garden b) Y)
                         (= (select garden c) Y)))))
(check-sat)

Answer 1

我认为有一个隐含的假设，即所有三种颜色的花朵都出现在花园中。考虑到这一点，这就是我将如何使用 Python 和 Haskell 接口对 Z3 进行编码的方法；因为用这些语言编写代码比直接在 SMTLib 中编写代码更容易。

Python

from z3 import *

# Color enumeration
Color, (R, Y, B) = EnumSort('Color', ('R', 'Y', 'B'))

# An uninterpreted function for color assignment
col = Function('col', IntSort(), Color)

# Number of flowers
N = Int('N')

# Helper function to specify distinct valid choices:
def validPick (i1, i2, i3):
    return And( Distinct(i1, i2, i3)
              , 1 <= i1, 1 <= i2, 1 <= i3
              , i1 <= N, i2 <= N, i3 <= N
              )

# Helper function to count a given color
def count(pickedColor, flowers):
    return Sum([If(col(f) == pickedColor, 1, 0) for f in flowers])

# Get a solver and variables for our assertions:
s = Solver()
f1, f2, f3 = Ints('f1 f2 f3')

# There's at least one flower of each color
s.add(Exists([f1, f2, f3], And(validPick(f1, f2, f3), col(f1) == R, col(f2) == Y, col(f3) == B)))

# You pick three, and at least one of them is red
s.add(ForAll([f1, f2, f3], Implies(validPick(f1, f2, f3), count(R, [f1, f2, f3]) >= 1)))

# You pick three, and at least one of them is yellow
s.add(ForAll([f1, f2, f3], Implies(validPick(f1, f2, f3), count(Y, [f1, f2, f3]) >= 1)))

# For every three flowers you pick, one of them has to be blue
s.add(ForAll([f1, f2, f3], Implies(validPick(f1, f2, f3), count(B, [f1, f2, f3]) == 1)))

# Find a satisfying value of N
print s.check()
print s.model()[N]

# See if there's any other value by outlawing the choice
nVal = s.model()[N]
s.add(N != nVal)
print s.check()

运行时，会打印：

sat
3
unsat

读取这个输出的方式是当N=3时给定的条件确实可以满足；正如你所寻求的那样。此外，如果您还断言N 不是not 3，那么就没有令人满意的模型，即3 的选择是由给定的条件所强制的。我相信这就是你想要建立的。

我希望代码清晰，但请随时要求澄清。如果你在 SMT-Lib 中确实需要这个，你可以随时插入：

print s.sexpr()

在调用s.check() 之前，您可以看到生成的 SMTLib。

哈斯克尔

也可以在 Haskell/SBV 中编写相同的代码。请参阅此要点以获得几乎相同的文字编码：https://gist.github.com/LeventErkok/66594d8e94dc0ab2ebffffe4fdabccc9 请注意，Haskell 解决方案可以利用 SBV 的 allSat 构造（它返回所有令人满意的假设），并且更简单地表明 N=3 是唯一的解决方案。