Language: cn / en

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?

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

## 分析

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

## 建模

$$X_i \oplus X_{i+1}$$

$$\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}})\\$$

$$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}$$

WolfGOATCABBAGE
TrueTrueFalse
FalseTrueTrue
FalseFalseTrue
TrueFalseFalse

$$(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$$

## 结果

stepwolfgoatcabbage
1FTF
2FTF
3TTF
4TFF
5TFT
6TFT
7TTT

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)
)