ನನ್ನ ಅಭಿಪ್ರಾಯದಲ್ಲಿ, ಇಂಟರ್ನೆಟ್‌ನ ರಷ್ಯನ್ ಭಾಷೆಯ ವಲಯದಲ್ಲಿ, ಔಪಚಾರಿಕ ಪರಿಶೀಲನೆಯ ವಿಷಯವು ಸಾಕಷ್ಟು ಆವರಿಸಲ್ಪಟ್ಟಿಲ್ಲ ಮತ್ತು ವಿಶೇಷವಾಗಿ ಸರಳ ಮತ್ತು ಸ್ಪಷ್ಟ ಉದಾಹರಣೆಗಳ ಕೊರತೆಯಿದೆ.
ನಾನು ವಿದೇಶಿ ಮೂಲದಿಂದ ಒಂದು ಉದಾಹರಣೆಯನ್ನು ನೀಡುತ್ತೇನೆ ಮತ್ತು ನದಿಯ ಇನ್ನೊಂದು ಬದಿಗೆ ತೋಳ, ಮೇಕೆ ಮತ್ತು ಎಲೆಕೋಸು ದಾಟುವ ಪ್ರಸಿದ್ಧ ಸಮಸ್ಯೆಗೆ ನನ್ನದೇ ಆದ ಪರಿಹಾರವನ್ನು ಸೇರಿಸುತ್ತೇನೆ.
ಆದರೆ ಮೊದಲು, ಔಪಚಾರಿಕ ಪರಿಶೀಲನೆ ಏನು ಮತ್ತು ಅದು ಏಕೆ ಬೇಕು ಎಂದು ನಾನು ಸಂಕ್ಷಿಪ್ತವಾಗಿ ವಿವರಿಸುತ್ತೇನೆ.
ಔಪಚಾರಿಕ ಪರಿಶೀಲನೆಯು ಸಾಮಾನ್ಯವಾಗಿ ಒಂದು ಪ್ರೋಗ್ರಾಂ ಅಥವಾ ಅಲ್ಗಾರಿದಮ್ ಅನ್ನು ಇನ್ನೊಂದನ್ನು ಬಳಸಿಕೊಂಡು ಪರಿಶೀಲಿಸುವುದು ಎಂದರ್ಥ.
ಪ್ರೋಗ್ರಾಂ ನಿರೀಕ್ಷೆಯಂತೆ ವರ್ತಿಸುತ್ತದೆ ಮತ್ತು ಅದರ ಸುರಕ್ಷತೆಯನ್ನು ಖಚಿತಪಡಿಸಿಕೊಳ್ಳಲು ಇದು ಅವಶ್ಯಕವಾಗಿದೆ.
ಔಪಚಾರಿಕ ಪರಿಶೀಲನೆಯು ದೋಷಗಳನ್ನು ಕಂಡುಹಿಡಿಯುವ ಮತ್ತು ತೆಗೆದುಹಾಕುವ ಅತ್ಯಂತ ಶಕ್ತಿಶಾಲಿ ವಿಧಾನವಾಗಿದೆ: ಇದು ಪ್ರೋಗ್ರಾಂನಲ್ಲಿ ಅಸ್ತಿತ್ವದಲ್ಲಿರುವ ಎಲ್ಲಾ ರಂಧ್ರಗಳು ಮತ್ತು ದೋಷಗಳನ್ನು ಹುಡುಕಲು ಅಥವಾ ಅವು ಅಸ್ತಿತ್ವದಲ್ಲಿಲ್ಲ ಎಂದು ಸಾಬೀತುಪಡಿಸಲು ನಿಮಗೆ ಅನುಮತಿಸುತ್ತದೆ.
8 ಚೌಕಗಳ ಬೋರ್ಡ್ ಅಗಲವನ್ನು ಹೊಂದಿರುವ 1000 ರಾಣಿಗಳ ಸಮಸ್ಯೆಯಂತಹ ಕೆಲವು ಸಂದರ್ಭಗಳಲ್ಲಿ ಇದು ಅಸಾಧ್ಯವೆಂದು ಗಮನಿಸಬೇಕಾದ ಅಂಶವಾಗಿದೆ: ಇದು ಅಲ್ಗಾರಿದಮಿಕ್ ಸಂಕೀರ್ಣತೆ ಅಥವಾ ನಿಲ್ಲಿಸುವ ಸಮಸ್ಯೆಗೆ ಬರುತ್ತದೆ.
ಆದಾಗ್ಯೂ, ಯಾವುದೇ ಸಂದರ್ಭದಲ್ಲಿ, ಮೂರು ಉತ್ತರಗಳಲ್ಲಿ ಒಂದನ್ನು ಸ್ವೀಕರಿಸಲಾಗುತ್ತದೆ: ಪ್ರೋಗ್ರಾಂ ಸರಿಯಾಗಿದೆ, ತಪ್ಪಾಗಿದೆ ಅಥವಾ ಉತ್ತರವನ್ನು ಲೆಕ್ಕಾಚಾರ ಮಾಡಲು ಸಾಧ್ಯವಾಗಲಿಲ್ಲ.
ಉತ್ತರವನ್ನು ಕಂಡುಹಿಡಿಯುವುದು ಅಸಾಧ್ಯವಾದರೆ, ನಿರ್ದಿಷ್ಟ ಹೌದು ಅಥವಾ ಇಲ್ಲ ಎಂಬ ಉತ್ತರವನ್ನು ಪಡೆಯುವ ಸಲುವಾಗಿ ಪ್ರೋಗ್ರಾಂನ ಅಸ್ಪಷ್ಟ ಭಾಗಗಳನ್ನು ಪುನಃ ಕೆಲಸ ಮಾಡಲು, ಅವುಗಳ ಅಲ್ಗಾರಿದಮಿಕ್ ಸಂಕೀರ್ಣತೆಯನ್ನು ಕಡಿಮೆ ಮಾಡಲು ಸಾಧ್ಯವಿದೆ.
ಮತ್ತು ಔಪಚಾರಿಕ ಪರಿಶೀಲನೆಯನ್ನು ಬಳಸಲಾಗುತ್ತದೆ, ಉದಾಹರಣೆಗೆ, ವಿಂಡೋಸ್ ಕರ್ನಲ್ ಮತ್ತು ಡರ್ಪಾ ಡ್ರೋನ್ ಆಪರೇಟಿಂಗ್ ಸಿಸ್ಟಮ್‌ಗಳಲ್ಲಿ, ಗರಿಷ್ಠ ಮಟ್ಟದ ರಕ್ಷಣೆಯನ್ನು ಖಚಿತಪಡಿಸಿಕೊಳ್ಳಲು.
ನಾವು 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 ವಿನಂತಿಯನ್ನು ಬಳಸಿಕೊಂಡು ಸರ್ವರ್ ಅನ್ನು ಭೇದಿಸಬಹುದಾದ ಪ್ರಕರಣಕ್ಕೆ ಹೋಲಿಸಬಹುದಾದರೆ, ತೋಳ, ಮೇಕೆ ಮತ್ತು ಎಲೆಕೋಸು ಹೆಚ್ಚು ಸಂಕೀರ್ಣವಾದ ಮತ್ತು ವ್ಯಾಪಕವಾದ ವರ್ಗದಿಂದ ಒಂದು ಉದಾಹರಣೆಯನ್ನು ಪ್ರದರ್ಶಿಸುತ್ತದೆ, ಇದರಲ್ಲಿ ಗುರಿಯನ್ನು ಮಾತ್ರ ಸಾಧಿಸಬಹುದು. ಹಲವಾರು ವಿನಂತಿಗಳಿಂದ.
ಇದನ್ನು ಹೋಲಿಸಬಹುದಾಗಿದೆ, ಉದಾಹರಣೆಗೆ, ನೀವು SQL ಇಂಜೆಕ್ಷನ್ ಅನ್ನು ಕಂಡುಹಿಡಿಯಬೇಕಾದ ಸನ್ನಿವೇಶಕ್ಕೆ, ಅದರ ಮೂಲಕ ಫೈಲ್ ಅನ್ನು ಬರೆಯಿರಿ, ನಂತರ ನಿಮ್ಮ ಹಕ್ಕುಗಳನ್ನು ಹೆಚ್ಚಿಸಿ ಮತ್ತು ನಂತರ ಮಾತ್ರ ಪಾಸ್ವರ್ಡ್ ಪಡೆಯಿರಿ.
ಸಮಸ್ಯೆಯ ಪರಿಸ್ಥಿತಿಗಳು ಮತ್ತು ಅದರ ಪರಿಹಾರರೈತನು ತೋಳ, ಮೇಕೆ ಮತ್ತು ಎಲೆಕೋಸುಗಳನ್ನು ನದಿಯಾದ್ಯಂತ ಸಾಗಿಸಬೇಕಾಗಿದೆ. ರೈತನ ಬಳಿ ದೋಣಿ ಇದೆ, ಅದು ರೈತನ ಹೊರತಾಗಿ ಒಂದು ವಸ್ತುವನ್ನು ಮಾತ್ರ ಇರಿಸಬಹುದು. ತೋಳವು ಮೇಕೆಯನ್ನು ತಿನ್ನುತ್ತದೆ ಮತ್ತು ಮೇಕೆ ಎಲೆಕೋಸನ್ನು ರೈತರು ಗಮನಿಸದೆ ಬಿಟ್ಟರೆ ಮೇಕೆ ತಿನ್ನುತ್ತದೆ.
ಪರಿಹಾರವೆಂದರೆ ಹಂತ 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