对逻辑难题进行建模
我正在尝试模拟“模拟一只知更鸟”中的一个逻辑难题。我正在努力把它翻译成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)回答 1
Stack Overflow用户
发布于 2018-12-11 08:29:35
我认为有一种隐含的假设，即花园中所有三种颜色的花都有代表性。考虑到这一点，我将使用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构造(它返回所有令人满意的假设)，更简单地表明N=3是唯一的解决方案。
https://stackoverflow.com/questions/53711168
复制相似问题
腾讯云开发者
