首页
学习
活动
专区
工具
TVP
发布
社区首页 >问答首页 >对逻辑难题进行建模

对逻辑难题进行建模
EN

Stack Overflow用户
提问于 2018-12-11 01:59:46
回答 1查看 155关注 0票数 2

我正在尝试模拟“模拟一只知更鸟”中的一个逻辑难题。我正在努力把它翻译成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)
EN
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接:

https://stackoverflow.com/questions/53711168

复制
相关文章

相似问题

领券
问题归档专栏文章快讯文章归档关键词归档开发者手册归档开发者手册 Section 归档