我正在尝试从“模仿一只知更鸟”中模拟一个逻辑难题。我正在努力将其翻译成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)
最佳答案
我认为有一个隐含的假设,即花园中代表了所有三种颜色的花朵。考虑到这一点,这就是我将使用Python和Haskell接口与Z3进行编码的方法。因为用这些语言编写代码比直接用SMTLib语言编写更容易。
蟒蛇
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 / SBV中进行相同的编码。请参见以下要点,以获得几乎相同的文字编码:https://gist.github.com/LeventErkok/66594d8e94dc0ab2ebffffe4fdabccc9请注意,Haskell解决方案可以利用SBV的
allSat
构造(返回所有满足的假设),更简单地说明N=3
是唯一的解决方案。