Z3 来解决一个难题（8 块瓷砖）吗？

Question

我试图从以下描述中解决问题，这是我的代码： 我的想法如下。

1. 空的空间表示为1524。
2. 在每一步 s 中，都有一个方块移动到该空白区域中。
3. 搬入的街区有限制。它可以是空白区域的右侧、左侧、顶部或底部。
4. 在下一轮中，值会被交换。

什么不起作用？ 目前，如果我尝试阻止超过 2 个方块移动，z3 不会给我 sat。这是一部分：

(= 2
(+
(ite (distinct (B s 1 1) (B (+ s 1) 1 1)) 1 0)
(ite (distinct (B s 1 2) (B (+ s 1) 1 2)) 1 0)
(ite (distinct (B s 1 3) (B (+ s 1) 1 3)) 1 0)
(ite (distinct (B s 2 1) (B (+ s 1) 2 1)) 1 0)
(ite (distinct (B s 2 2) (B (+ s 1) 2 2)) 1 0)
(ite (distinct (B s 2 3) (B (+ s 1) 2 3)) 1 0)
(ite (distinct (B s 3 1) (B (+ s 1) 3 1)) 1 0)
(ite (distinct (B s 3 2) (B (+ s 1) 3 2)) 1 0)
(ite (distinct (B s 3 3) (B (+ s 1) 3 3)) 1 0)
)
)

但是，例如，如果我删除最后一个 ite (ite (distinct (B s 3 3) (B (+ s 1) 3 3)) 1 0)，则 z3 会给我 sat。但我不希望这样，因为每个步骤都会更改 3 个值。我只想在每个步骤中更改 2 个块（通过交换）。

--------整个代码从这里开始

; (1,1) (1,2) (1,3) (2,1) (2,2) (2,3) (3,1) (3,2) (3,3)
; step, row, column
(declare-fun B (Int Int Int) Int)
(declare-const N Int)

(= 8 (B 0 1 1))
(= 7 (B 0 1 2))
(= 6 (B 0 1 3))
(= 5 (B 0 2 1))
(= 4 (B 0 2 2))
(= 3 (B 0 2 3))
(= 2 (B 0 3 1))
(= 1 (B 0 3 2))
(= 1524 (B 0 3 3))

;final state
(= 1 (B N 1 1))
(= 2 (B N 1 2))
(= 3 (B N 1 3))
(= 4 (B N 2 1))
(= 5 (B N 2 2))
(= 6 (B N 2 3))
(= 7 (B N 3 1))
(= 8 (B N 3 2))
(= 1524 (B N 3 3))

; only two blocks can move at a time
; not working at the moment..
(forall ((s Int))
(implies
(<= 0 s N)
(and 
; in each round, there is an empty block. an empty block...
; x1 and y1 are the coordinates of the block that will move in.
(exists ((x Int) (y Int) (x1 Int) (y1 Int))
(and
(<= 1 x 3)
(<= 1 y 3)
(<= 1 x1 3)
(<= 1 y1 3)
(= 1524 (B s x y))
(= 1
(+ ; it can be only one block out of the following options: top, bottom, right, left
;right
(ite (and (= x1 x) (= y1 (+ y 1))) 1 0)
;left
(ite (and (= x1 x) (= y1 (- y 1))) 1 0)
;top
(ite (and (= y1 y) (= x1 (+ x 1))) 1 0)
;bottom
(ite (and (= y1 y) (= x1 (- x 1))) 1 0)
)
)
(= (B (+ s 1) x y) (B s x1 y1))
(= (B (+ s 1) x1 y1) (B s x y))
))
)))

(forall ((s Int))
(implies
(<= 0 s N)
(= 1
(+
(ite (= 1524 (B s 1 1)) 1 0)
(ite (= 1524 (B s 1 2)) 1 0)
(ite (= 1524 (B s 1 3)) 1 0)
(ite (= 1524 (B s 2 1)) 1 0)
(ite (= 1524 (B s 2 2)) 1 0)
(ite (= 1524 (B s 2 3)) 1 0)
(ite (= 1524 (B s 3 1)) 1 0)
(ite (= 1524 (B s 3 2)) 1 0)
(ite (= 1524 (B s 3 3)) 1 0)
)
)
))

(not (exists ((s Int))
(implies
(<= 0 s N)
(<= 2
(+
(ite (distinct (B s 1 1) (B (+ s 1) 1 1)) 1 0)
(ite (distinct (B s 1 2) (B (+ s 1) 1 2)) 1 0)
(ite (distinct (B s 1 3) (B (+ s 1) 1 3)) 1 0)
(ite (distinct (B s 2 1) (B (+ s 1) 2 1)) 1 0)
(ite (distinct (B s 2 2) (B (+ s 1) 2 2)) 1 0)
(ite (distinct (B s 2 3) (B (+ s 1) 2 3)) 1 0)
(ite (distinct (B s 3 1) (B (+ s 1) 3 1)) 1 0)
(ite (distinct (B s 3 2) (B (+ s 1) 3 2)) 1 0)
(ite (distinct (B s 3 3) (B (+ s 1) 3 3)) 1 0)
))
)
))


))

请帮忙！

Answer 1

为什么

unsat

你得到

unsat

的原因是你的最后一个限制：

(not (exists ((s Int))
(implies
(<= 0 s N)
(<= 2
(+
(ite (distinct (B s 1 1) (B (+ s 1) 1 1)) 1 0)
(ite (distinct (B s 1 2) (B (+ s 1) 1 2)) 1 0)
(ite (distinct (B s 1 3) (B (+ s 1) 1 3)) 1 0)
(ite (distinct (B s 2 1) (B (+ s 1) 2 1)) 1 0)
(ite (distinct (B s 2 2) (B (+ s 1) 2 2)) 1 0)
(ite (distinct (B s 2 3) (B (+ s 1) 2 3)) 1 0)
(ite (distinct (B s 3 1) (B (+ s 1) 3 1)) 1 0)
(ite (distinct (B s 3 2) (B (+ s 1) 3 2)) 1 0)
(ite (distinct (B s 3 3) (B (+ s 1) 3 3)) 1 0)
))
)
))

如果将否定推入内部，则此约束的形式为：

forall s. not (implies (<= 0 s N) Q)

我用 Q 替换了整个

(<= 2 ...)

部分。

如果将

not (implies a b)

替换为等效的

a && not b

，我们会得到：

forall s. (<= 0 s N) && not Q

要满足这一点，您必须满足两个合取词，特别是以下必须是

sat

：

forall s. (<= 0 s N)

通用量化公式可满足意味着什么？嗯，这一定是真的。但显然，对于任何给定的

s

，并非所有

N

都小于

N

，因为整数是无界的。所以，这个子句本身是不能满足的。

这就是您获得

unsat

的原因。

建模

您没有问，但您的问题隐含的是如何使用 SMT 求解器对此类难题进行建模。当然，可以有多种方法对其进行建模，并且使用

B

将电路板建模为未解释的函数是一种有趣的方法。我并不是说这行不通。但在存在量词的情况下，逻辑必然是半可判定的。添加未解释的函数本身并不一定会使问题变得更加困难。相反，是量词让它做到了这一点。也就是说，即使您要修复约束以正确捕获语义，求解器仍然很难获得令人满意的模型。

此外，诸如此类的问题通常不适合 SMT 求解器。 SMT 求解器的亮点在于

T

部分：模理论。这里没有真正基于理论的推理。 （整数和比较的使用显然是算术，但仅在表面层面。这里实际上没有任何“数学”推理。）因此，除非有人构建可满足性模“滑动8谜题”理论，求解器最终主要依赖于 SAT 推理，而这些类型的约束会导致大量的子句。如果你在故事中添加量词，事情就会变得更加困难。

但是，如果您的目标是仅使用 SMT 求解器（即使它可能不是最好的工具），我建议您使用不同的建模风格。避免使用量词。相反，生成越来越长的“移动”列表。 （从左上下、从左上上等）使这些具有象征意义。根据这些符号移动计算最终棋盘，看看是否可以从第一个棋盘开始匹配最终状态。通过迭代加深这个序列的长度，你最终可以找到解决方案。

请注意，这种策略虽然是可判定的，但不一定有效。如果只需少量步骤（例如 10 个左右）即可找到解决方案，那么您可能可以相当快地生成它。但随着长度的增加，它很可能会遭受组合爆炸。例如，您选择的特定起始状态需要 62 次移动（我认为！），SMT 求解器在短时间内得出这个结果是不合理的。至少对于最先进的水平来说不是。

让我们知道您的探索进展如何；我很想知道您是否可以修复当前的形式化问题并在合理的时间内找到解决方案。