Я только начал изучать решатель z3. Я видел некоторые головоломки, решаемые z3, например, судоку и восемь ферзей. Мне просто интересно, решил ли кто-нибудь проблему пересечения реки в z3. z3 кажется очень хорошим решением проблем.
С Уважением
Я только начал изучать решатель z3. Я видел некоторые головоломки, решаемые z3, например, судоку и восемь ферзей. Мне просто интересно, решил ли кто-нибудь проблему пересечения реки в z3. z3 кажется очень хорошим решением проблем.
С Уважением
Спасибо Shahab, и вот версия Python, вдохновленная кодом Shahab. Также добавлены некоторые улучшения, например, нет такого номера шага, как 14. Кстати, я рассматривал человека и лодку как один объект, а не позицию.
Два цикла for — это всего лишь две версии для вывода результата; выбирайте, как вам нравится.
'''
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"
И вот результат:
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
Я попытался смоделировать его и пришел к следующему. Вы можете запустить его в интерактивной средеrise4fun и увидеть ответ:
(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))
Вы также можете запустить "(get-model)", чтобы увидеть определение функции "objectLocation", но я предупреждаю вас, что это будет очень непонятно.
Вот краткое описание того, что утверждается: