Z3 解决农夫过河问题

Language: cn / en

今天做到的一道 CS173 Honor 课程的作业，感觉还挺有意思的，用到了一个月来学到的逻辑运算方法并且运用到了实际生活中的问题解决上。问题是这样的：

A farmer went to a market and purchased a wolf, a goat, and a cabbage. On his way
home, the farmer came to the bank of a river and rented a boat. But crossing the river by boat, the farmer could carry only himself and a single one of his purchases: the wolf,the goat, or the cabbage. If left unattended together, the wolf would eat the goat, or the goat would eat the cabbage. The farmer's challenge is to carry himself and his purchases to the far bank of the river, leaving each purchase intact. How can he do it in seven steps?

大概就是说一农夫想把狼 (wolf)，羊 (goat)，卷心菜 (cabbage) 运到河的另外一边，但是有三个限制：

1. 农夫的船一次性只能运三个中的一个东西
2. 狼，羊不能共处
3. 羊，卷心菜不能共处

问，如何用7步解决这个问题。

分析

首先，我们先来分析一下这个问题，题中主要有三个限制

1. 行动 (Movement): 农夫一次只能运一个东西
2. 携带物品 (carry items): 狼&羊以及羊&卷心菜不能共存
3. 成功 (success): 农夫在第7步需要确保所有物品 (items) 全被转移

因为我们试图通过七个步骤来解决这个问题，所以我们可以将每个项目的状态建模为 goat: $g_0 , g_1, g_2....g_7$, cabbage: $c_0, c_1,c_2...c_7$ wolf: $w_0,w_1,w_2...w_7$, 在这里，每个状态都是布尔 (Boolean) 类型，“True” 表示目的地（河的另一边），而“False”表示起点。然后，我们可以使用逻辑符号来表示每个步骤和约束，最后让Z3为我们解决这个问题。

建模

对于每一个移动，这里的限制是，对于任何移动，最多一个的item可以更改其状态，为了模拟“移动”的行为，我们可以使用异或 (XOR):
$$X_i \oplus X_{i+1}$$
为了模拟不移动，取反 (negation) 就行了:
$$\neg(X_i \oplus X_{i+1})$$
因此，结合上述两种说法，我们可以通过以下方式对移动的约束进行建模：
$$A_i \oplus A_{i+1} \to \neg(B_i \oplus B_{i+1}) ∧ {\neg(C_i\oplus C_{i+1}})\\$$
然后再用De 'Morgan进行简化
$$A_i \oplus A_{i+1} \to \neg((B_i \oplus B_{i+1}) ∨{(C_i\oplus C_{i+1}}))$$
还有一个约束条件是，对于之前在另一端的物品，它不能被转移，在逻辑符号中，它可以显示为
目的地 -> 出发地：
$$X_{i+1} \to X_{i}$$
出发地 -> 目的地：
$$X_i \to X_{i+1}$$
结合以上两个约束，我们可以正确地表示移动了。

对于携带物品的限制，我们只需要避免四种情况：

用逻辑符号表示：
$$(W_i = G_i) ∧(C_i = \neg W_i)$$
$$(G_i= C_i) ∧ (W_i = \neg G_i)$$

还需要考虑的是，存在一些例外情况，因为农夫可以通过在下一次运输中运输一个冲突项目来避免这种限制（假设运输同时发生）。因此，我们需要添加一个条件：
$$(W_i = G_i) ∧ (C_i = \neg W_i) ∧ (W_{i+1}=G_{i+1})$$
$$(G_i= C_i) ∧ (W_i = \neg G_i)∧ (G_{i+1}=C_{i+1})$$
对于最后那个约束，即跨越河流的所有三个项目，可以表示为：
$$G_7 ∧ W_7 ∧ C_7$$

结果

通过把逻辑表达式转移到Z3中，我们能得到以下结果：

用人话说，就是：
1.山羊到另一边
2.返回
3.狼到另一边去
4.带着山羊回来
5.把卷心菜放到另一边
6.返回
7.山羊到另一边，完成！

程序

(declare-const w0 Bool)
(declare-const g0 Bool)
(declare-const c0 Bool)
(declare-const w1 Bool)
(declare-const g1 Bool)
(declare-const c1 Bool)
(declare-const w2 Bool)
(declare-const g2 Bool)
(declare-const c2 Bool)
(declare-const w3 Bool)
(declare-const g3 Bool)
(declare-const c3 Bool)
(declare-const w4 Bool)
(declare-const g4 Bool)
(declare-const c4 Bool)
(declare-const w5 Bool)
(declare-const g5 Bool)
(declare-const c5 Bool)
(declare-const w6 Bool)
(declare-const g6 Bool)
(declare-const c6 Bool)
(declare-const w7 Bool)
(declare-const g7 Bool)
(declare-const c7 Bool)

(assert (= w0 false))
(assert (= g0 false))
(assert (= c0 false))

(assert (=> w0 w1))
(assert (=> c0 c1))
(assert (=> g0 g1))
(assert (=> (xor w0 w1) (not(or(xor g0 g1)(xor c0 c1)))))
(assert (=> (xor g0 g1) (not(or(xor w0 w1)(xor c0 c1)))))
(assert (=> (xor c0 c1) (not(or(xor g0 g1)(xor w0 w1)))))

(assert (=> w2 w1))
(assert (=> c2 c1))
(assert (=> g2 g1))
(assert (=> (xor w1 w2) (not(or(xor g1 g2)(xor c1 c2) ))))
(assert (=> (xor g1 g2) (not(or(xor w1 w2)(xor c1 c2)))))
(assert (=> (xor c1 c2) (not(or(xor g1 g2)(xor w1 w2)))))

(assert (=> w2 w3))
(assert (=> c2 c3))
(assert (=> g2 g3))
(assert (=> (xor w2 w3) (not(or(xor g2 g3)(xor c2 c3)))))
(assert (=> (xor g2 g3) (not(or(xor w2 w3)(xor c2 c3)))))
(assert (=> (xor c2 c3) (not(or(xor g2 g3)(xor w2 w3)))))

(assert (=> w4 w3))
(assert (=> c4 c3))
(assert (=> g4 g3))
(assert (=> (xor w3 w4) (not(or(xor g3 g4)(xor c3 c4)))))
(assert (=> (xor g3 g4) (not(or(xor w3 w4)(xor c3 c4)))))
(assert (=> (xor c3 c4) (not(or(xor g3 g4)(xor w3 w4)))))

(assert (=> w4 w5))
(assert (=> c4 c5))
(assert (=> g4 g5))
(assert (=> (xor w4 w5) (not(or(xor g4 g5)(xor c4 c5)))))
(assert (=> (xor g4 g5) (not(or(xor w4 w5)(xor c4 c5)))))
(assert (=> (xor c4 c5) (not(or(xor g4 g5)(xor w4 w5)))))

(assert (=> w6 w5))
(assert (=> c6 c5))
(assert (=> g6 g5))
(assert (=> (xor w5 w6) (not(or(xor g5 g6)(xor c5 c6)))))
(assert (=> (xor g5 g6) (not(or(xor w5 w6)(xor c5 c6)))))
(assert (=> (xor c5 c6) (not(or(xor g5 g6)(xor w5 w6)))))

(assert (=> w6 w7))
(assert (=> c6 c7))
(assert (=> g6 g7))
(assert (=> (xor w6 w7) (not(or(xor g6 g7)(xor c6 c7)))))
(assert (=> (xor g6 g7) (not(or(xor w6 w7)(xor c6 c7)))))
(assert (=> (xor c6 c7) (not(or(xor g6 g7)(xor w6 w7)))))

(assert (not(and (= g0 w0) (= c0 (not g0)) (= g1 w1))))
(assert (not(and (= g1 w1) (= c1 (not g1)) (= g2 w2))))
(assert (not(and (= g2 w2) (= c2 (not g2)) (= g3 w3))))
(assert (not(and (= g3 w3) (= c3 (not g3)) (= g4 w4))))
(assert (not(and (= g4 w4) (= c4 (not g4)) (= g5 w5))))
(assert (not(and (= g5 w5) (= c5 (not g5)) (= g6 w6))))
(assert (not(and (= g6 w6) (= c6 (not g6)) (= g7 w7))))
(assert (not(and (= g7 w7) (= c7 (not g7)))))

(assert (not(and (= g0 c0) (= c0 (not w0)) (= g1 c1))))
(assert (not(and (= g1 c1) (= c1 (not w1)) (= g2 c2))))
(assert (not(and (= g2 c2) (= c2 (not w2)) (= g3 c3))))
(assert (not(and (= g3 c3) (= c3 (not w3)) (= g4 c4))))
(assert (not(and (= g4 c4) (= c4 (not w4)) (= g5 c5))))
(assert (not(and (= g5 c5) (= c5 (not w5)) (= g6 c6))))
(assert (not(and (= g6 c6) (= c6 (not w6)) (= g7 c7))))
(assert (not(and (= g7 c7) (= c7 (not w7)))))

(assert (and c7 g7 w7))


(check-sat)
(get-model)

输出：

sat
(model 
  (define-fun w3 () Bool
    true)
  (define-fun g2 () Bool
    true)
  (define-fun c3 () Bool
    false)
  (define-fun g4 () Bool
    false)
  (define-fun c5 () Bool
    true)
  (define-fun c6 () Bool
    true)
  (define-fun w5 () Bool
    true)
  (define-fun g1 () Bool
    true)
  (define-fun g5 () Bool
    false)
  (define-fun w6 () Bool
    true)
  (define-fun c2 () Bool
    false)
  (define-fun g3 () Bool
    true)
  (define-fun w4 () Bool
    true)
  (define-fun c4 () Bool
    false)
  (define-fun g6 () Bool
    false)
  (define-fun w2 () Bool
    false)
  (define-fun c1 () Bool
    false)
  (define-fun w1 () Bool
    false)
  (define-fun w7 () Bool
    true)
  (define-fun g7 () Bool
    true)
  (define-fun c7 () Bool
    true)
  (define-fun c0 () Bool
    false)
  (define-fun g0 () Bool
    false)
  (define-fun w0 () Bool
    false)
)