River crossing puzzle in z3

Question

I've just start learning z3 solver. I've seen some puzzles solved by z3 i.e sudoku and Eight Queens. I'm just wondering if any one solved River crossing problem in z3. z3 seems very good in problem solving.

Regards

Answer 1

Thank Shahab, and here goes the python version inspired by Shahab's code. Some improvements are also added, for example, there is no such a step number as 14. By the way, I treated the man and the boat as one object, not a position.

The two for-loops are just two versions to output the result; choose as you like.

'''
A man has a wolf, a goat and a cabbage.
On the way home he must cross a river.
His boat is small and won't fit more than one of his object.
He cannot leave the goat alone with the cabbage (because the goat would eat it),
nor he can leave the goat alone with the wolf (because the goat would be eaten).
How can the man get everything on the other side in this river crossing puzzle?
'''

from z3 import *
import timeit

s = Then('qe', 'smt').solver() # This strategy improves efficiency

Obj, (Man, Wolf, Goat, Cabbage) = EnumSort('Obj', ['Man', 'Wolf', 'Goat', 'Cabbage'])
Pos, (Left, Right) = EnumSort('Pos', ['Left', 'Right'])
f = Function('f', Obj, IntSort(), Pos) # f(obj, t) returns the position of the object obj at time t (from 0)

# variables for quantifier
i, j, k, x = Ints('i j k x')
a, b = Consts('a b', Obj)

# At time 0, all the objects are at left side
s.add(ForAll([a],
             f(a, 0) == Left))

# At time x (x >= 0), all objects are at right side
# And before that, the duplicated cases are not allowed
s.add(And(x >= 0,
          ForAll([a], f(a, x) == Right),
          ForAll([j, k],
                 Implies(And(j >= 0, j <= x, k >= 0, k <= x, j != k),
                         Exists([b],
                                f(b, j) != f(b, k))))))

# Man will come over and again between two sides until all objects are at right
s.add(ForAll([i],
             Implies(And(i >= 0, i < x),
                     f(Man, i) != f(Man, i + 1))))

# Man is at the same side with the goat, or goat is at a different side with wolf and cabbage
s.add(ForAll([i],
             Implies(And(i >= 0, i <= x),
                     Or(f(Man, i) == f(Goat, i),
                        And(f(Wolf, i) != f(Goat, i),
                            f(Cabbage, i) != f(Goat, i))))))

# All objects except man remain at the same side,
# or only one object moves the same with man while others remain the same side
s.add(ForAll([i],
             Implies(And(i >= 0, i < x),
                     Or(ForAll([a],  # all objects except man remain the same
                               Implies(a != Man,
                                       f(a, i) == f(a, i + 1))),
                        Exists([b],  # or there must one moves the same with man
                               And(b != Man,
                                   f(b, i) == f(Man, i),
                                   f(b, i + 1) == f(Man, i + 1),
                                   ForAll([a],  # and except that one must remain the same
                                          Implies(And(a != b, a != Man),
                                                  f(a, i) == f(a, i + 1)))))))))

print "Time eclipsed:", timeit.timeit(s.check, number=1)
print

if s.check() != sat:
    print "No result!"
    exit()

m = s.model()
total = m[x].as_long() + 1

for t in range(total):
    print "Step:", t
    print "Man", m.eval(f(Man, t)), "\t",
    print "Wolf", m.eval(f(Wolf, t)), "\t",
    print "Goat", m.eval(f(Goat, t)), "\t",
    print "Cabbage", m.eval(f(Cabbage, t))

print

for t in range(total):
    print "Step:", t
    if m.eval(f(Man, t)).eq(Left):
        print "Man",
    if m.eval(f(Wolf, t)).eq(Left):
        print "Wolf",
    if m.eval(f(Goat, t)).eq(Left):
        print "Goat",
    if m.eval(f(Cabbage, t)).eq(Left):
        print "Cabbage",
    print "~~~>",
    if m.eval(f(Man, t)).eq(Right):
        print "Man",
    if m.eval(f(Wolf, t)).eq(Right):
        print "Wolf",
    if m.eval(f(Goat, t)).eq(Right):
        print "Goat",
    if m.eval(f(Cabbage, t)).eq(Right):
        print "Cabbage",
    print

print "finished"

And here is the output:

Time eclipsed: 0.169998884201

Step: 0
Man Left    Wolf Left   Goat Left   Cabbage Left
Step: 1
Man Right   Wolf Left   Goat Right  Cabbage Left
Step: 2
Man Left    Wolf Left   Goat Right  Cabbage Left
Step: 3
Man Right   Wolf Left   Goat Right  Cabbage Right
Step: 4
Man Left    Wolf Left   Goat Left   Cabbage Right
Step: 5
Man Right   Wolf Right  Goat Left   Cabbage Right
Step: 6
Man Left    Wolf Right  Goat Left   Cabbage Right
Step: 7
Man Right   Wolf Right  Goat Right  Cabbage Right

Step: 0
Man Wolf Goat Cabbage ~~~>
Step: 1
Wolf Cabbage ~~~> Man Goat
Step: 2
Man Wolf Cabbage ~~~> Goat
Step: 3
Wolf ~~~> Man Goat Cabbage
Step: 4
Man Wolf Goat ~~~> Cabbage
Step: 5
Goat ~~~> Man Wolf Cabbage
Step: 6
Man Goat ~~~> Wolf Cabbage
Step: 7
~~~> Man Wolf Goat Cabbage
finished

Answer 2

I tried to model it and I came up with the following. You can run it in the interactive rise4fun environment and see the answer:

(declare-datatypes () ((Object Human Fox Rabbit Cabbage)))
(declare-datatypes () ((Location Left Right OnBoat)))
(declare-const n Int)
(declare-fun objectLocation (Int Object) Location)

(assert (= n 14))

(assert (forall ((x Object) (t Int)) (=> (= t 0) (= (objectLocation t x) Left))))
(assert (forall ((x Object) (t Int)) (=> (= t n) (= (objectLocation t x) Right))))
(assert
  (forall
    ((t Int))
    (=>
      (and (>= t 0) (<= t n))
      (<=
        (+
          (ite (= (objectLocation t Human) OnBoat) 1 0)
          (ite (= (objectLocation t Fox) OnBoat) 1 0)
          (ite (= (objectLocation t Rabbit) OnBoat) 1 0)
          (ite (= (objectLocation t Cabbage) OnBoat) 1 0)
        )
        2
      )
    )
  )
)
(assert
  (forall
    ((x Object) (t Int))
    (=>
      (and (>= t 1) (<= t (- n 1)))
      (iff
        (= (objectLocation t x) OnBoat)
        (and
          (not (= (objectLocation (+ t 1) x) OnBoat))
          (not (= (objectLocation (- t 1) x) OnBoat))
          (not (= (objectLocation (+ t 1) x) (objectLocation (- t 1) x)))
        )
      )
    )
  )
)
(assert
  (forall
    ((x Object) (t Int))
    (=>
      (and (>= t 1) (<= t n))
      (=>
        (not (= (objectLocation t x) (objectLocation (- t 1) x)))
        (or
          (= (objectLocation t x) OnBoat)
          (= (objectLocation (- t 1) x) OnBoat)
        )
      )
    )
  )
)
(assert
  (forall
    ((x Object) (y Object) (t Int))
    (=>
      (and (>= t 1) (<= t n))
      (=>
        (and (= (objectLocation t x) OnBoat) (= (objectLocation t y) OnBoat))
        (= (objectLocation (- t 1) x) (objectLocation (- t 1) y))
      )
    )
  )
)
(assert
  (forall
    ((x Object) (t Int))
    (=>
      (and (>= t 0) (<= t n))
      (=>
        (= (objectLocation t x) OnBoat)
        (= (objectLocation t Human) OnBoat)
      )
    )
  )
)
(assert
  (forall
    ((t Int))
    (=>
      (and (>= t 0) (<= t n))
      (=>
        (= (objectLocation t Fox) (objectLocation t Rabbit))
        (= (objectLocation t Human) (objectLocation t Rabbit))
      )
    )
  )
)
(assert
  (forall
    ((t Int))
    (=>
      (and (>= t 0) (<= t n))
      (=>
        (= (objectLocation t Cabbage) (objectLocation t Rabbit))
        (= (objectLocation t Human) (objectLocation t Rabbit))
      )
    )
  )
)

(check-sat)

(echo "step 0")
(eval (objectLocation 0 Human))
(eval (objectLocation 0 Fox))
(eval (objectLocation 0 Rabbit))
(eval (objectLocation 0 Cabbage))

(echo "step 1")
(eval (objectLocation 1 Human))
(eval (objectLocation 1 Fox))
(eval (objectLocation 1 Rabbit))
(eval (objectLocation 1 Cabbage))

(echo "step 2")
(eval (objectLocation 2 Human))
(eval (objectLocation 2 Fox))
(eval (objectLocation 2 Rabbit))
(eval (objectLocation 2 Cabbage))

(echo "step 3")
(eval (objectLocation 3 Human))
(eval (objectLocation 3 Fox))
(eval (objectLocation 3 Rabbit))
(eval (objectLocation 3 Cabbage))

(echo "step 4")
(eval (objectLocation 4 Human))
(eval (objectLocation 4 Fox))
(eval (objectLocation 4 Rabbit))
(eval (objectLocation 4 Cabbage))

(echo "step 5")
(eval (objectLocation 5 Human))
(eval (objectLocation 5 Fox))
(eval (objectLocation 5 Rabbit))
(eval (objectLocation 5 Cabbage))

(echo "step 6")
(eval (objectLocation 6 Human))
(eval (objectLocation 6 Fox))
(eval (objectLocation 6 Rabbit))
(eval (objectLocation 6 Cabbage))

(echo "step 7")
(eval (objectLocation 7 Human))
(eval (objectLocation 7 Fox))
(eval (objectLocation 7 Rabbit))
(eval (objectLocation 7 Cabbage))

(echo "step 8")
(eval (objectLocation 8 Human))
(eval (objectLocation 8 Fox))
(eval (objectLocation 8 Rabbit))
(eval (objectLocation 8 Cabbage))

(echo "step 9")
(eval (objectLocation 9 Human))
(eval (objectLocation 9 Fox))
(eval (objectLocation 9 Rabbit))
(eval (objectLocation 9 Cabbage))

(echo "step 10")
(eval (objectLocation 10 Human))
(eval (objectLocation 10 Fox))
(eval (objectLocation 10 Rabbit))
(eval (objectLocation 10 Cabbage))

(echo "step 11")
(eval (objectLocation 11 Human))
(eval (objectLocation 11 Fox))
(eval (objectLocation 11 Rabbit))
(eval (objectLocation 11 Cabbage))

(echo "step 12")
(eval (objectLocation 12 Human))
(eval (objectLocation 12 Fox))
(eval (objectLocation 12 Rabbit))
(eval (objectLocation 12 Cabbage))

(echo "step 13")
(eval (objectLocation 13 Human))
(eval (objectLocation 13 Fox))
(eval (objectLocation 13 Rabbit))
(eval (objectLocation 13 Cabbage))

(echo "step 14")
(eval (objectLocation 14 Human))
(eval (objectLocation 14 Fox))
(eval (objectLocation 14 Rabbit))
(eval (objectLocation 14 Cabbage))

You can also run "(get-model)" to see a definition of the function "objectLocation" but I warn you that it will be very unintelligible.

Here is a short description of what is asserted:

1. There can be at most 14 steps.
2. At step 0, all objects are on the left.
3. At step n, all objects should be on the right.
4. At each step, there can be at most two objects in the boat.
5. An object is on the boat at step t if and only if it is on different sides of the river at steps t-1 and t+1.
6. If an object changes location from step t-1 to step t then one of these locations should be the boat.
7. If two objects are on the boat at step t they should have been on the same side of the river at step t-1.
8. If something is on the boat then the human should also be on the boat.
9. If fox and rabbit are in the same location then human should also be there.
10. If rabbit and cabbage are in the same location then human should also be there.