Use Z3 to solve Wolf-Goat-Cabbage puzzle

Language cn / en

Analysis

There are three main constraints in this problem:

1. Movement: the farmer can only carry at most one item per travel
2. Carry item: goat&wolf and goat&cabbage cannot exist at the same time
3. Success: our goal is to ensure every item can safely pass through the river

Because we try to solve this problem in seven steps, we can model each items' status into 7 parts. i.e. each status for goat can be represented by: $g_0 , g_1, g_2....g_7$, cabbage to: $c_0, c_1,c_2...c_7$ and wolf to $w_0,w_1,w_2...w_7$, whereas each status is Boolean type and True means on destination (other side of the river) and False means in starting point. Then, we can use logical notation to represent each step and constraint to make Z3 solve this problem for us.

Modeling

For each movement, the constrain here is that for any approach status, at most one item in three can change its status, for example, to model the behavior of move, we can use exclusive or.

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

To represent not move, it is just the negation of move

$$ \neg(X_i \oplus X_{i+1}) $$

Therefore, combining the two statements above, we can model the constrain of the move by:

$$ A_i \oplus A_{i+1} \to \neg(B_i \oplus B_{i+1}) ∧ \neg(C_i\oplus C_{i+1})\\ $$

We can simplify it by using De 'Morgan's law

$$ A_i \oplus A_{i+1} \to \neg((B_i \oplus B_{i+1}) ∨ (C_i\oplus C_{i+1})) $$

there is also a constrain that for the item previously on the other side, it cannot be shipped, in logical notation, it can be shown as

right to left:

$$ X_{i+1} \to X_{i} $$

left to right:

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

Combine with two above constraints, we can correctly represent movement.

For the constrain of carry item, we just need to avoid four situations:

which can be simply represent by:

$$ (W_i = G_i) ∧ (C_i = \neg W_i) $$

$$ (G_i= C_i) ∧ (W_i = \neg G_i) $$

What also need to to considered is that there are some exceptions because the farmer can avoid this constrain by shipping one of the conflict item in the next shipping (assume shipping happens simultaneously). Hence, we need to add a condition:

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

For the final constrain, which is all three item cross the river, it can be illustrate to:

$$ G_7 ∧ W_7 ∧ C_7 $$

Result

By translate the logics into Z3 code, we can get the output shown below:

In readable word, it means that:

1. goat to other side
2. return
3. wolf to other side
4. return with goat
5. cabbage to other side
6. return
7. goat to the other side, COMPLETE!

Coding

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

OUTPUT:

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