ืืื ืืืื ืืืื ืื ื, ืืื ืื ืจืืกืืฉ-ืฉืคึผืจืึทื ืกืขืงืืึธืจ ืคืื ืืขืจ ืืื ืืขืจื ืขืฅ, ืื ืืขืืข ืคืื โโืคืึธืจืืึทื ืืืขืจืึทืคืึทืงืืืฉืึทื ืืื ื ืืฉื ืืขื ืื ืืืืขืงื, ืืื ืขืก ืืื ืกืคึผืขืฆืืขื ืึท ืคืขืื ืคืื ืคึผืฉืื ืืื ืงืืึธืจ ืืืืฉืคืืื.
ืืื ืืืขื ืืขืื ืึท ืืืืฉืคึผืื ืคืื ืึท ืคืจืขืืื ืืงืืจ, ืืื ืฆืืืขืื ืืืื ืืืืืขื ืข ืืืืืื ื ืฆื ืืขืจ ืืืงืื ืืขืจ ืคึผืจืึธืืืขื ืคืื ืึทืจืืืขืจืืืื ืึท ืืืึธืืฃ, ืึท ืฆืื ืืื ืึท ืงืจืืื ืืืืฃ ืืขืจ ืึทื ืืขืจืขืจ ืืืื ืืืื.
ืืืขืจ ืขืจืฉืืขืจ, ืืื ืืืขื ืืขืงืืฆืขืจ ืืึทืฉืจืืึทืื ืืืึธืก ืคืึธืจืืึทื ืืืขืจืึทืคืึทืงืืืฉืึทื ืืื ืืื ืืืึธืก ืขืก ืืื ืืืจืฃ.
ืคืึธืจืืึทื ืืืขืจืึทืคืึทืงืืืฉืึทื ืืืืฉืึทืืืึทืื ืืืื ืงืึธื ืืจืึธืืืจืื ื ืืืื ืคึผืจืึธืืจืึทื ืึธืืขืจ ืึทืืืขืจืืืึทื ื ืืฆื ืื ืืขืจื.
ืืึธืก ืืื ื ืืืืืง ืฆื ืขื ืฉืืจ ืึทื ืื ืคึผืจืึธืืจืึทื ืืืืืืืื ืืื ืืขืจืืืึทืจื ืืื ืืืื ืฆื ืขื ืฉืืจ ืืืึทื ืืืืขืจืืืื.
ืคืึธืจืืึทื ืืืขืจืึทืคืึทืงืืืฉืึทื ืืื ืื ืืขืจืกื ืฉืืึทืจืง ืืืื ืฆื ืืขืคึฟืื ืขื ืืื ืขืืืืื ืืจื ืืืึทืื ืขืจืึทืืืืืืื: ืขืก ืึทืืึทืื ืืืจ ืฆื ืืขืคึฟืื ืขื ืึทืืข ืืืืืกืืื ื ืืึธืืขืก ืืื ืืึทืื ืืื ืึท ืคึผืจืึธืืจืึทื, ืึธืืขืจ ืืึทืืืืึทืื ืึทื ืืื ืืึธื ื ืื ืขืงืกืืกืืืจื.
ืขืก ืืื ืืืื ืฆื ืืืืขืจืงื ืึทื ืืื ืขืืืขืืข ืงืึทืกืขืก ืืึธืก ืืื ืืืืืขืืืขื, ืึทืืึท ืืื ืืื ืื ืคึผืจืึธืืืขื ืคืื 8 ืงืืืื ืก ืืื ืึท ืืจืขื ืืจืืื ืคืื 1000 ืกืงืืืขืจื: ืขืก ืึทืืข ืงืืื ืึทืจืึธืคึผ ืฆื ืึทืืืขืจืืืึทื ืงืึทืืคึผืืขืงืกืืื ืึธืืขืจ ืกืืึธืคึผืคึผืื ื ืคึผืจืึธืืืขื.
ืึธืืขืจ, ืืื ืงืืื ืคืึทื, ืืืื ืขืจ ืคืื ืืจืืึท ืขื ืืคึฟืขืจืก ืืืขื ืืืื ืืืงืืืขื: ืื ืคึผืจืึธืืจืึทื ืืื ืจืืืืืง, ืคืึทืืฉ, ืึธืืขืจ ืขืก ืืื ื ืื ืืขืืืขื ืฆื ืจืขืืขื ืขื ืื ืขื ืืคืขืจ.
ืืืื ืขืก ืืื ืืืืืขืืืขื ืฆื ืืขืคึฟืื ืขื ืึทื ืขื ืืคืขืจ, ืขืก ืืื ืึธืคื ืืขืืืขื ืฆื ืจืืืืขืจืง ืืืงืืึธืจ ืคึผืึทืจืฅ ืคืื ืื ืคึผืจืึธืืจืึทื, ืจืืืืกืื ื ืืืืขืจ ืึทืืืขืจืืืึทืืืง ืงืึทืืคึผืืขืงืกืืื, ืฆื ืืึทืงืืืขื ืึท ืกืคึผืขืฆืืคืืฉ ืืึธ ืึธืืขืจ ืงืืื ืขื ืืคืขืจ.
ืืื ืคืึธืจืืึทื ืืืขืจืึทืคืึทืงืืืฉืึทื ืืื ืืขื ืืฆื, ืืืฉื, ืืื ืื Windows ืงืขืจื ืืื ืืึทืจืคึผืึท ืืจืึธืื ืึธืคึผืขืจืืืืื ื ืกืืกืืขืืขื, ืฆื ืขื ืฉืืจ ืื ืืึทืงืกืืืื ืฉืืฅ ืืืจืื.
ืืืจ ืืืขืื ื ืืฆื Z3Prover, ืึท ืืืืขืจ ืฉืืึทืจืง ืืขืฆืืึทื ืคึฟืึทืจ ืึธืืึทืืืืืื ืืขืึธืจืขื ืคึผืจืึธืืืขื ืืื ืืงืืืืืืฉืึทื ืกืึทืืืืื ื.
ืืขืจืฆื, Z3 ืกืึทืืืื ืืงืืืืืืฉืึทื ื ืืื ืกืึทืืขืงืฅ ื ืืฉื ืืืืขืจ ืืืึทืืืขืก ืืื ืืจืื ืงืจืึทืคื.
ืืขื ืืืื ืึทื ืขืก ืืื ืืืืืืช ืฆื ืืขืคึฟืื ืขื ืื ืขื ืืคืขืจ, ืืคืืื ืืื ืงืึทืกืขืก ืืื ืขืก ืืขื ืขื 10 ^ 100 ืงืึทืืืึทื ืืืฉืึทื ื ืคืื ืึทืจืืึทื ืฉืจืืึทื ืึธืคึผืฆืืขืก.
ืึธืืขืจ ืืึธืก ืืื ืืืืื ืืืขืื ืึท ืืืฅ ืึทืจืืึทื ืฉืจืืึทื ืึทืจืืืืขื ืื ืคืื ืืืคึผ ืื ืืขืืขืจ, ืืื ืืึธืก ืืื ืึธืคื ืืขืคึผืืึธื ืืขืจื ืืื ืคืืจ.
ืคึผืจืึธืืืขื ืืืขืื 8 ืงืืืื ืก (ืืขื ืืืขื ืคืื ืขื ืืืืฉ ).
# We know each queen must be in a different row.
# So, we represent each queen by a single integer: the column position
Q = [ Int('Q_%i' % (i + 1)) for i in range(8) ]
# Each queen is in a column {1, ... 8 }
val_c = [ And(1 <= Q[i], Q[i] <= 8) for i in range(8) ]
# At most one queen per column
col_c = [ Distinct(Q) ]
# Diagonal constraint
diag_c = [ If(i == j,
True,
And(Q[i] - Q[j] != i - j, Q[i] - Q[j] != j - i))
for i in range(8) for j in range(i) ]
solve(val_c + col_c + diag_c)
ืืื Z3, ืืืจ ืืึทืงืืืขื ืื ืืืืืื ื:
[Q_5 = 1,
Q_8 = 7,
Q_3 = 8,
Q_2 = 2,
Q_6 = 3,
Q_4 = 6,
Q_7 = 5,
Q_1 = 4]
ืื ืืืึผื ืคึผืจืึธืืืขื ืืื ืคืึทืจืืืืึทืืืขื ืฆื ืึท ืคึผืจืึธืืจืึทื ืืืึธืก ื ืขืื ืืื ืึทืจืืึทื ืฉืจืืึทื ืื ืงืึธืืึธืจืืึทื ืึทืฅ ืคืื 8 ืงืืืื ืก ืืื ืึทืืืคึผืืฅ ืื ืขื ืืคืขืจ ืฆื ืื ืงืืืื ืก ืฉืืึธืื ืืขืืขืจ ืื ืืขืจืขืจ.
ืืืื ืืืจ ืืืึธืื ืกืึธืืืืข ืึทืืึท ืึท ืคึผืจืึธืืจืึทื ื ืืฆื ืคืึธืจืืึทื ืืืขืจืึทืคืึทืงืืืฉืึทื, ืงืึทืืคึผืขืจื ืืื ืืขื ืคึผืจืึธืืืขื, ืืืจ ืืืึธืื ื ืึธืจ ืืึทืจืคึฟื ืฆื ื ืขืืขื ื ืึธื ืืืื ืฉืจืื ืืื ืื ืคืึธืจืขื ืคืื ืงืึทื ืืืขืจืืื ื ืื ืคึผืจืึธืืจืึทื ืงืึธื ืืื ืึทื ืืงืืืืืืฉืึทื: ืขืก ืืืึธืื ืืืื ืืกืขื ืฉืึทืื ืืืืขื ืืงืึทื ืฆื ืืื ืืืขืจ ( ืคืื ืงืืจืก, ืืืื ืื ืคึผืจืึธืืจืึทื ืืื ืืขืฉืจืืื ืจืืืืืง).
ืึผืืขื ืื ืืขืืืข ืืึทื ืืืขื ืคึผืึทืกืืจื ืืื ืืขื ืคืึทื ืคืื ืืืื ืคึฟืึทืจ ืืืึทืื ืขืจืึทืืืืืืื: ืืืจ ื ืึธืจ ืฉืืขืื ืื ืจืขืืืืืึทื ืื ืึธืื ืืืึธืก ืืืจ ืืึทืจืคึฟื, ืืืฉื, ืื ืึทืืืื ืืกืืจืึทืืึธืจ ืคึผืึทืจืึธื, ืืืขืจืืึทืื ืื ืืงืืจ ืึธืืขืจ ืืืงืึทืืคึผืืืื ืงืึธื ืืื ืืงืืืืืืฉืึทื ื ืงืึทืืคึผืึทืืึทืืึทื ืืื ืืืขืจืึทืคืึทืงืืืฉืึทื, ืืื ืืขืจื ืึธื ืืึทืงืืืขื ืึทื ืขื ืืคืขืจ ืฆื ืืืึธืก. ืืึทืื ืืึทืจืฃ ืืืื ืกืึทืคึผืืืื ืืื ืึทืจืืึทื ืฉืจืืึทื ืฆื ืืขืจืืจืืืื ืืขื ืฆืื.
ืืื ืืืื ืืืื ืื ื, ืื ืคึผืจืึธืืืขื ืืืขืื ืื ืืืึธืืฃ, ืื ืฆืื ืืื ืื ืงืจืืื ืืื ืืคืืื ืืขืจ ืืฉืืงืึทืืืข, ืืืืึทื ืกืึทืืืืื ื ืขืก ืฉืืื ืจืืงืืืืืขืจื ืคืืืข (7) ืืจืื.
ืืืื ืื ืืืึผื ืคึผืจืึธืืืขื ืืื ืคืึทืจืืืืึทืืืขื ืฆื ืืขื ืคืึทื ืืืขื ืืืจ ืงืขื ืขื ืืืจืื ืขืืขื ืึท ืกืขืจืืืขืจ ืืื ืึท ืืืื GET ืึธืืขืจ POST ืืขืื, ืืขืจ ืืืึธืืฃ, ืฆืื ืืื ืงืจืืื ืืขืืึทื ืกืืจืืืฅ ืึท ืืืืฉืคึผืื ืคืื ืึท ืคืื ืืขืจ ืงืึธืืคึผืืืฆืืจื ืืื ืืืืืืกืคึผืจืขื ืงืึทืืขืืึธืจืืข, ืืื ืืืึธืก ืืขืจ ืฆืื ืงืขื ืขื ืืืื ืึทืืฉืืืื ืืืืื ืืืจื ืขืืืขืืข ืจืืงืืืขืก.
ืืึธืก ืืื ืคืึทืจืืืืึทืืืขื, ืืืฉื, ืฆื ืึท ืกืฆืขื ืึทืจ ืืื ืืืจ ืืึทืจืคึฟื ืฆื ืืขืคึฟืื ืขื ืึท ืกืงื ืื ืืืฉืขืงืฉืึทื, ืฉืจืืึทืื ืึท ืืขืงืข ืืืจื ืขืก, ืืื ืืคืืืืื ืืืื ืจืขืื ืืื ืืืืื ืืขืืึธืื ืืึทืงืืืขื ืึท ืคึผืึทืจืึธื.
ืงืึธื ืืืืืึธื ืก ืคืื ืื ืคึผืจืึธืืืขื ืืื ืืืึทื ืืืืืื ืืืขืจ ืคึผืืืขืจ ืืึทืจืฃ ืึทืจืืืขืจืคืืจื ืึท ืืืึธืืฃ, ืึท ืฆืื ืืื ืงืจืืื ืึทืจืืืขืจ ืื ืืืึทื. ืืขืจ ืคึผืืืขืจ ืืึธื ืึท ืฉืืคื, ืืืึธืก ืงืขื ื ืึธืจ ืึทืงืึทืืึทืืืื ืืืื ืืืืคืขืฅ, ืึทืืืฅ ืืขื ืคึผืืืขืจ ืืื. ืืขืจ ืืืืืฃ ืืืขื ืขืกื ืื ืฆืื ืืื ืื ืฆืื ืืืขื ืขืกื ืื ืงืจืืื ืืืื ืืขืจ ืคึผืืืขืจ ืืึธืื ืืื ืึธื ืืืืื ื.
ืื ืืืืืื ื ืืื ืึทื ืืื ืฉืจืื 4 ืืขืจ ืคึผืืืขืจ ืืืขื ืืึทืจืคึฟื ืฆื ื ืขืืขื ืื ืฆืื ืฆืืจืืง.
ืืืฆื ืืึธืื ืก ืึธื ืืืืื ืกืึธืืืืข ืขืก ืคึผืจืึธืืจืึทืืืึทืืืงืึทืืื.
ืืึธืืืจ ืืึทืฆืืืืขื ืขื ืืขื ืคึผืืืขืจ, ืืืึธืืฃ, ืฆืื ืืื ืงืจืืื ืืื 4 ืืืขืจืืึทืืึทืื ืืืึธืก ื ืขืืขื ืื ืืืขืจื ืืืืื 0 ืึธืืขืจ 1. ื ืื ืืืื ืึทื ืืื ืืขื ืขื ืืืืฃ ืื ืืื ืงืก ืืจืขื, ืืื ืืืื ืขืจ ืืืื ืึทื ืืื ืืขื ืขื ืืืืฃ ืื ืจืขืื.
import json
from z3 import *
s = Solver()
Num= 8
Human = [ Int('Human_%i' % (i + 1)) for i in range(Num) ]
Wolf = [ Int('Wolf_%i' % (i + 1)) for i in range(Num) ]
Goat = [ Int('Goat_%i' % (i + 1)) for i in range(Num) ]
Cabbage = [ Int('Cabbage_%i' % (i + 1)) for i in range(Num) ]
# Each creature can be only on left (0) or right side (1) on every state
HumanSide = [ Or(Human[i] == 0, Human[i] == 1) for i in range(Num) ]
WolfSide = [ Or(Wolf[i] == 0, Wolf[i] == 1) for i in range(Num) ]
GoatSide = [ Or(Goat[i] == 0, Goat[i] == 1) for i in range(Num) ]
CabbageSide = [ Or(Cabbage[i] == 0, Cabbage[i] == 1) for i in range(Num) ]
Side = HumanSide+WolfSide+GoatSide+CabbageSide
ื ืืืขืจ ืืื ืื ื ืืืขืจ ืคืื ืกืืขืคึผืก ืคืืจืืื ืื ืฆื ืกืึธืืืืข. ืืขืืขืจ ืฉืจืื ืจืขืคึผืจืึทืืขื ืฅ ืื ืฉืืึทื ืคืื ืื ืืืึทื, ืื ืฉืืคื ืืื ืึทืืข ืขื ืืืืื.
ืืืฆื, ืืึธืื ืก ืงืืืึทืื ืขืก ืจืึทื ืืึธื ืืื ืืื ืึท ืืจืขื ืขืฅ, ื ืขืืขื 10.
ืืขืืขืจ ืขื ืืืื ืืื ืจืขืคึผืจืืืขื ืืื ืืื 10 ืขืงืืขืืคืืืจื - ืืึธืก ืืื ืืืึทื ืืืขืจื ืืื ืืขืืขืจ ืคืื ืื 10 ืกืืขืคึผืก.
ืืืฆื ืืึธืื ืก ืฉืืขืื ืื ืืืืื ืืื ืืขื ืคึฟืึทืจ ืื ืึธื ืืืื ืืื ืขื ืืืงื.
Start = [ Human[0] == 0, Wolf[0] == 0, Goat[0] == 0, Cabbage[0] == 0 ]
Finish = [ Human[9] == 1, Wolf[9] == 1, Goat[9] == 1, Cabbage[9] == 1 ]
ืืขืจื ืึธื ืืืจ ืฉืืขืื ืื ืืืืื ืืื ืืขื ืืื ืืขืจ ืืืึธืืฃ ืขืกื ืื ืฆืื, ืึธืืขืจ ืื ืฆืื ืขืกื ืื ืงืจืืื, ืืื ืงืึทื ืกืืจืืื ืฅ ืืื ืื ืืงืืืืืืฉืึทื.
(ืืื ืืขื ืืืึทืืืึทื ืคืื ืึท ืคึผืืืขืจ, ืึธื ืคืึทื ืืื ืืืืืขืืืขื)
# Wolf cant stand with goat, and goat with cabbage without human. Not 2, not 0 which means that they are one the same side
Safe = [ And( Or(Wolf[i] != Goat[i], Wolf[i] == Human[i]), Or(Goat[i] != Cabbage[i], Goat[i] == Human[i])) for i in range(Num) ]
ืืื ืฆืื ืกืืฃ, ืืืจ ืืืขืื ืืขืคืื ืืจื ืึทืืข ืืขืืืขื ืึทืงืฉืึทื ื ืคืื ืื ืคึผืืืขืจ ืืืขื ืึทืจืืืขืจ ืึทืืื ืึธืืขืจ ืฆืืจืืง.
ืขืจ ืงืึธื ืึธืืขืจ ื ืขืืขื ืืื ืืื ืึท ืฐืึธืืฃ, ืึท ืฆืื ืึธืืขืจ ืึท ืงืจืืื, ืึธืืขืจ ืงืฒื ืขื ื ืืฉื ื ืขืืขื, ืึธืืขืจ ืืึธืจ ื ืืฉื ืคึฟืึธืจื ืขืจืืขืฅ.
ืคึฟืึทืจืฉืืืื ืืื, ืึทื ืึธื ืึท ืคึผืืืขืจ ืงืึธื ืงืืื ืขืจ ื ืืฉื ืึทืจืืืขืจืืืื.
ืืึธืก ืืืขื ืืืื ืืืืกืืขืืจืืงื ืืืจื ืื ืคืึทืงื ืึทื ืืขืืขืจ ืกืึทืืกืึทืงืืืึทื ื ืฉืืึทื ืคืื ืื ืืืึทื, ืฉืืคื ืืื ืขื ืืืืื ืงืขื ืขื ืืืื ืึทื ืืขืจืฉ ืคืื ืื ืคืจืืขืจืืืงืข ืืืืื ืืื ืึท ืฉืืจืขื ื ืืืืืืขื ืืืขื.
ื ืื ืืขืจ ืืื 2 ืืืื, ืืื ืืื ืคืืืข ืื ืืขืจืข ืืืืึทืฅ, ืืืืึทื ืืขืจ ืคึผืืืขืจ ืงืขื ืขื ืืืืื ืึทืจืืืขืจืคืืจื ืืืื ืขื ืืืื ืืื ืึท ืฆืืึทื ืืื ื ืื ืึทืืข ืงืขื ืขื ืืืื ืืื ืงืก ืฆืืืึทืืขื.
Travel = [ Or(
And(Human[i] == Human[i+1] + 1, Wolf[i] == Wolf[i+1] + 1, Goat[i] == Goat[i+1], Cabbage[i] == Cabbage[i+1]),
And(Human[i] == Human[i+1] + 1, Goat[i] == Goat[i+1] + 1, Wolf[i] == Wolf[i+1], Cabbage[i] == Cabbage[i+1]),
And(Human[i] == Human[i+1] + 1, Cabbage[i] == Cabbage[i+1] + 1, Wolf[i] == Wolf[i+1], Goat[i] == Goat[i+1]),
And(Human[i] == Human[i+1] - 1, Wolf[i] == Wolf[i+1] - 1, Goat[i] == Goat[i+1], Cabbage[i] == Cabbage[i+1]),
And(Human[i] == Human[i+1] - 1, Goat[i] == Goat[i+1] - 1, Wolf[i] == Wolf[i+1], Cabbage[i] == Cabbage[i+1]),
And(Human[i] == Human[i+1] - 1, Cabbage[i] == Cabbage[i+1] - 1, Wolf[i] == Wolf[i+1], Goat[i] == Goat[i+1]),
And(Wolf[i] == Wolf[i+1], Goat[i] == Goat[i+1], Cabbage[i] == Cabbage[i+1])) for i in range(Num-1) ]
ืืื ืก ืืืืคื ืื ืืืืืื ื.
solve(Side + Start + Finish + Safe + Travel)
ืืื ืืืจ ืืึทืงืืืขื ืื ืขื ืืคืขืจ!
Z3 ืืขืคืื ืขื ืึท ืงืึธื ืกืืกืืขื ื ืืึทื ื ืคืื ืฉืืึทืื ืืืึธืก ืกืึทืืืกืคืืื ืึทืืข ืืืืื ืืื ืืขื.
ื ืืื ืคืืจ-ืืืืขื ืฉืึทื ืึทื ืืขืฉืืึทืื ืคืื ืคึผืืึทืฅ-ืฆืืื.
ืืืืืจ ืืืืกืจืขืืขื ืขื ืืืืก ืืื ืืขืฉืขื.
ืื ืจ ืืขืขื , ื ื ืื ื ืกื ืฃ ืืขื ืข ื ืื ืข ืืจืืืขืจ , ื ื ืจ ืื ืืฒ ื ืื ื ืืื ืืืข ืจ ืคืืืข ืจ ืืืฉืืืก ื ืื ื ืฆ ื ืจืืขื , ืื ื ืื ื ื ื ืขืจืฉื ืข 2 ืืจืื ืฉืืืื ื ืข ืจ ื ืืฉ ื ืขืจืืขืฅ .
Human_2 = 0
Human_3 = 0
ืืึธืก ืกืึทืืืืฉืขืกืฅ ืึทื ืื ื ืืืขืจ ืคืื ืฉืืึทืื ืืืจ ืืืืกืืขืจืืืืืื ืืื ืืืขืจืืง, ืืื 8 ืืืขื ืืืื ืืึทื ืฅ ืืขื ืื.
ืื ื ืืื ืืืข ืจ ืคืื , ืื ื ืืข ืจ ืคืืืข ืจ ืื ืก ืืขืื ื : ืื ืืืื ื , ืจื , ืจืื , ืืจืืืขืจืฆืืืฒ ื ื ื ืฆืื , ืืจืืืขืจืฆืืจืฒืก ื ื ื ืงืจืืื , ืฆืืจืืงืงืืืข ื ืื ื ืืข ืจ ืฆืื , ืืจืืืขืจ ึพ ืืจืื ื ืืข ื ืฐืืืฃ , ืื ื ืฆืืจืืง , ืืืฒื , ืืืืขืจืืขืืขื ื ื ื ืฆืื .
ืืืขืจ ืืื ืื ืกืืฃ ืื ืคึผืจืึธืืืขื ืืื ืกืึทืืืื.
#ะกัะฐัั.
Human_1 = 0
Wolf_1 = 0
Goat_1 = 0
Cabbage_1 = 0
#ะคะตัะผะตั ะพัะดัั
ะฐะตั.
Human_2 = 0
Wolf_2 = 0
Goat_2 = 0
Cabbage_2 = 0
#ะคะตัะผะตั ะพัะดัั
ะฐะตั.
Human_3 = 0
Wolf_3 = 0
Goat_3 = 0
Cabbage_3 = 0
#ะคะตัะผะตั ะพัะฒะพะทะธั ะบะพะทั ะฝะฐ ะฝัะถะฝัะน ะฑะตัะตะณ.
Human_4 = 1
Wolf_4 = 0
Goat_4 = 1
Cabbage_4 = 0
#ะคะตัะผะตั ะฒะพะทะฒัะฐัะฐะตััั.
Human_5 = 0
Wolf_5 = 0
Goat_5 = 1
Cabbage_5 = 0
#ะคะตัะผะตั ะพัะฒะพะทะธั ะบะฐะฟัััั ะฝะฐ ะฝัะถะฝัะน ะฑะตัะตะณ.
Human_6 = 1
Wolf_6 = 0
Cabbage_6 = 1
Goat_6 = 1
#ะะปััะตะฒะฐั ัะฐััั ะพะฟะตัะฐัะธะธ: ัะตัะผะตั ะฒะพะทะฒัะฐัะฐะตั ะบะพะทั ะพะฑัะฐัะฝะพ.
Human_7 = 0
Wolf_7 = 0
Goat_7 = 0
Cabbage_7 = 1
#ะคะตัะผะตั ะพัะฒะพะทะธั ะฒะพะปะบะฐ ะฝะฐ ะดััะณะพะน ะฑะตัะตะณ, ะณะดะต ะพะฝ ัะตะฟะตัั ะฝะฐั
ะพะดะธััั ะฒะผะตััะต ั ะบะฐะฟัััะพะน.
Human_8 = 1
Wolf_8 = 1
Goat_8 = 0
Cabbage_8 = 1
#ะคะตัะผะตั ะฒะพะทะฒัะฐัะฐะตััั ะทะฐ ะบะพะทะพะน.
Human_9 = 0
Wolf_9 = 1
Goat_9 = 0
Cabbage_9 = 1
#ะคะตัะผะตั ะฟะพะฒัะพัะฝะพ ะดะพััะฐะฒะปัะตั ะบะพะทั ะฝะฐ ะฝัะถะฝัะน ะฑะตัะตะณ ะธ ะทะฐะฒะตััะฐัั ะฟะตัะตะฟัะฐะฒั.
Human_10 = 1
Wolf_10 = 1
Goat_10 = 1
Cabbage_10 = 1
ืืืฆื ืืึธืืืจ ืคึผืจืืืืจื ืฆื ืืืืฉื ืื ืืืืื ืืื ืืขื ืืื ืืึทืืืืึทืื ืึทื ืขืก ืืขื ืขื ืงืืื ืกืึทืืืฉืึทื ื.
ืฆื ืืึธื ืืึธืก, ืืืจ ืืืขืื ืืขืื ืืื ืืืขืจ ืืืึธืืฃ ืืขืจืืืืืึธืจื, ืืื ืขืจ ืืืขื ืืืขืื ืฆื ืขืกื ืงืจืืื.
ืืึธืก ืงืขื ืืืื ืงืึทืืคึผืขืจื ืืื ืืขื ืคืึทื ืืื ืืืึธืก ืืื ืืืขืจ ืฆืื ืืื ืฆื ืืึทืืืึธืจืขื ืขื ืื ืึทืคึผืืึทืงืืืฉืึทื ืืื ืืืจ ืืึทืจืคึฟื ืฆื ืืึทืื ืืืืขืจ ืึทื ืขืก ืืขื ืขื ืงืืื ืืืคึผืืึธืืื.
Safe = [ And( Or(Wolf[i] != Goat[i], Wolf[i] == Human[i]), Or(Goat[i] != Cabbage[i], Goat[i] == Human[i]), Or(Wolf[i] != Cabbage[i], Goat[i] == Human[i])) for i in range(Num) ]
Z3 ืืื ืืื ืื ืื ืคืืืืขื ืืข ืขื ืืคืขืจ:
no solution
ืขืก ืืืื ืึทื ืขืก ืืึทืงืข ืืขื ืขื ืงืืื ืกืึทืืืฉืึทื ื.
ืืื ื ืืื ื ืื ืจ ืคืจืืืจืืืืืืฉ ืข ืืืฐืืื , ื ื ืืืืืขืืืขืืงืฒื ื ืฆ ื ืืจืืืขืจืฆืืืฒ ื ืื ื ื ื ืืืื ืืฐืขืจ ื ืฐืืืฃ , ื ื ืคืืจืืืกื ื ืคื ืจ ืืข ื ืคืืืขืจ .
ืืืื ืื ืืืืขื ืืขืคืื ื ืืขื ืืขืืข ืืฉืืงืึทืืืข, ืืื ืฆืืงืื ืคึฟื ืึทืจืืืงืืขื ืืื ืืืขื ืืึธืื ืืืจ ืืื ืฆื ืืืขื ืื ืึท ืคึผืจืึธืกื ืคึผืจืึธืืจืึทื ืึธืืขืจ ืคืื ืงืฆืืข ืืื ืึท ืืงืืืืืืฉืึทื ืงืึทืืคึผืึทืืึทืืึทื ืืื ืคืึธืจืืึทื ืืขืืืึธืืก, ืืื ืกืึธืืืืข ืขืก, ืืื ืืขืจืืื ืึทื ืืืขืงื ืึทืืข ืืึทืืืฉืืืึทืืึทื ืกืื ืขืจืืึธืื ืืื ืืืึทืื ืขืจืึทืืืืืืื. ืขืจืฉืืขืจ, ืืืืฃ ืืขืจ ืืขืืืืงืขืจ ืึทืจืืขื, ืึธืืขืจ ืืขืจืืื ืื ืืื ืื ืคืึธืจืขื ืคืื ืึท ืคึผืจืึธืืจืึทื, ืืื ืืขืืึธืื ืืืกืืขืืืืืึทื ืงืึทืืคึผืืึทืงืืืืื ื ืขืก ืืื ืืึทื ืืืืฃ ืฆื ืื ืงืจืึทื ื ืืืืฉืคืืื ืคืื ืืขืจ ืืืขืื ืคืื ืืืืืืืืืจื ืึทื ืืืืืงืืื ื.
ืืขืจ ืืืืึทืืขืจ ืึทืจืืืงื ืืื ืฉืืื ืืจืืื:
ืืื ืขืก ืืื ืืึทื ืคืื ืคืึธืจืืึทื ืืืขืจืึทืคืึทืงืืืฉืึทื ืคืื ืคึผืจืึธืืืขืืก ืฆื ืืืืื, ืืื ืืึทืฉืจืืึทืื
ืืื ืงืขื ืขื ืืื ืืืืืึธืืึทืืืฉ ืงืึธื ืืืขืจืืขื ืืื ืคืึธืจืืึทื ืืขืจืฉื ืกืืกืืขืืขื.
ืืงืืจ: www.habr.com