模拟逻辑谜题

Question

我正在尝试对来自模拟一只知更鸟 的逻辑谜题进行建模。我正在努力将其翻译成 SMT-LIB。谜题是这样的：

There is a garden in which all flowers are either red, yellow or blue, and all colours are represented. For any three flowers you pick, at least one will be red and one will be yellow. Is the third flower always going to be blue?

我尝试将花园建模为 Array Int Flower，但这行不通，我相信是因为数组的域固定在所有整数范围内。 Z3 告诉我这是无法满足的，CVC4 只是 returns 直接未知。

这个谜题的唯一解法是在花园里每种颜色都恰好有一朵花，但我如何让解算器告诉我这个？

这是我失败的尝试：

(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

我认为有一个隐含的假设，即所有三种颜色的花都出现在花园中。考虑到这一点，下面是我将如何使用 Z3 的 Python 和 Haskell 接口对其进行编码；因为用这些语言编写代码比直接在 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 不是 而不是 3，则没有令人满意的模型，即 3 的选择是由给出的条件。我相信这就是你想要建立的。

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

print s.sexpr()

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

Haskell

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

模拟逻辑谜题

Modelling a logic puzzle

python

z3

smt

z3py

cvc4

Python

Haskell