ਬਘਿਆੜ, ਬੱਕਰੀ ਅਤੇ ਗੋਭੀ ਸਮੱਸਿਆ ਦੀ ਉਦਾਹਰਨ ਦੀ ਵਰਤੋਂ ਕਰਕੇ ਰਸਮੀ ਤਸਦੀਕ

ਮੇਰੀ ਰਾਏ ਵਿੱਚ, ਇੰਟਰਨੈਟ ਦੇ ਰੂਸੀ-ਭਾਸ਼ਾ ਦੇ ਖੇਤਰ ਵਿੱਚ, ਰਸਮੀ ਤਸਦੀਕ ਦਾ ਵਿਸ਼ਾ ਕਾਫ਼ੀ ਨਹੀਂ ਹੈ, ਅਤੇ ਖਾਸ ਤੌਰ 'ਤੇ ਸਧਾਰਨ ਅਤੇ ਸਪੱਸ਼ਟ ਉਦਾਹਰਣਾਂ ਦੀ ਘਾਟ ਹੈ।

ਮੈਂ ਇੱਕ ਵਿਦੇਸ਼ੀ ਸਰੋਤ ਤੋਂ ਇੱਕ ਉਦਾਹਰਣ ਦੇਵਾਂਗਾ, ਅਤੇ ਇੱਕ ਬਘਿਆੜ, ਇੱਕ ਬੱਕਰੀ ਅਤੇ ਇੱਕ ਗੋਭੀ ਨੂੰ ਦਰਿਆ ਦੇ ਦੂਜੇ ਪਾਸੇ ਪਾਰ ਕਰਨ ਦੀ ਜਾਣੀ-ਪਛਾਣੀ ਸਮੱਸਿਆ ਦਾ ਆਪਣਾ ਹੱਲ ਜੋੜਾਂਗਾ।

ਪਰ ਪਹਿਲਾਂ, ਮੈਂ ਸੰਖੇਪ ਵਿੱਚ ਵਰਣਨ ਕਰਾਂਗਾ ਕਿ ਰਸਮੀ ਤਸਦੀਕ ਕੀ ਹੈ ਅਤੇ ਇਸਦੀ ਲੋੜ ਕਿਉਂ ਹੈ।

ਰਸਮੀ ਤਸਦੀਕ ਦਾ ਆਮ ਤੌਰ 'ਤੇ ਮਤਲਬ ਹੁੰਦਾ ਹੈ ਇੱਕ ਪ੍ਰੋਗਰਾਮ ਜਾਂ ਐਲਗੋਰਿਦਮ ਦੀ ਦੂਜੇ ਦੀ ਵਰਤੋਂ ਕਰਕੇ ਜਾਂਚ ਕਰਨਾ।

ਇਹ ਯਕੀਨੀ ਬਣਾਉਣ ਲਈ ਜ਼ਰੂਰੀ ਹੈ ਕਿ ਪ੍ਰੋਗਰਾਮ ਉਮੀਦ ਅਨੁਸਾਰ ਵਿਵਹਾਰ ਕਰੇ ਅਤੇ ਇਸਦੀ ਸੁਰੱਖਿਆ ਨੂੰ ਵੀ ਯਕੀਨੀ ਬਣਾਇਆ ਜਾਵੇ।

ਰਸਮੀ ਤਸਦੀਕ ਕਮਜ਼ੋਰੀਆਂ ਨੂੰ ਲੱਭਣ ਅਤੇ ਖ਼ਤਮ ਕਰਨ ਦਾ ਸਭ ਤੋਂ ਸ਼ਕਤੀਸ਼ਾਲੀ ਸਾਧਨ ਹੈ: ਇਹ ਤੁਹਾਨੂੰ ਪ੍ਰੋਗਰਾਮ ਵਿੱਚ ਮੌਜੂਦ ਸਾਰੇ ਛੇਕ ਅਤੇ ਬੱਗ ਲੱਭਣ, ਜਾਂ ਇਹ ਸਾਬਤ ਕਰਨ ਦੀ ਇਜਾਜ਼ਤ ਦਿੰਦਾ ਹੈ ਕਿ ਉਹ ਮੌਜੂਦ ਨਹੀਂ ਹਨ।
ਇਹ ਧਿਆਨ ਦੇਣ ਯੋਗ ਹੈ ਕਿ ਕੁਝ ਮਾਮਲਿਆਂ ਵਿੱਚ ਇਹ ਅਸੰਭਵ ਹੈ, ਜਿਵੇਂ ਕਿ 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

ਇਸਦਾ ਮਤਲਬ ਹੈ ਕਿ ਅਸਲ ਵਿੱਚ ਕੋਈ ਹੱਲ ਨਹੀਂ ਹਨ.

ਇਸ ਤਰ੍ਹਾਂ, ਅਸੀਂ ਪ੍ਰੋਗ੍ਰਾਮਿਕ ਤੌਰ 'ਤੇ ਕਿਸਾਨ ਲਈ ਨੁਕਸਾਨ ਤੋਂ ਬਿਨਾਂ ਸਰਵਭੋਗੀ ਬਘਿਆੜ ਨਾਲ ਪਾਰ ਕਰਨ ਦੀ ਅਸੰਭਵਤਾ ਨੂੰ ਸਾਬਤ ਕੀਤਾ ਹੈ।

ਜੇਕਰ ਦਰਸ਼ਕਾਂ ਨੂੰ ਇਹ ਵਿਸ਼ਾ ਦਿਲਚਸਪ ਲੱਗਦਾ ਹੈ, ਤਾਂ ਭਵਿੱਖ ਦੇ ਲੇਖਾਂ ਵਿੱਚ ਮੈਂ ਤੁਹਾਨੂੰ ਦੱਸਾਂਗਾ ਕਿ ਕਿਵੇਂ ਇੱਕ ਆਮ ਪ੍ਰੋਗਰਾਮ ਜਾਂ ਫੰਕਸ਼ਨ ਨੂੰ ਰਸਮੀ ਤਰੀਕਿਆਂ ਦੇ ਅਨੁਕੂਲ ਇੱਕ ਸਮੀਕਰਨ ਵਿੱਚ ਬਦਲਣਾ ਹੈ, ਅਤੇ ਇਸਨੂੰ ਹੱਲ ਕਰਨਾ ਹੈ, ਜਿਸ ਨਾਲ ਸਾਰੇ ਜਾਇਜ਼ ਦ੍ਰਿਸ਼ਾਂ ਅਤੇ ਕਮਜ਼ੋਰੀਆਂ ਦੋਵਾਂ ਨੂੰ ਪ੍ਰਗਟ ਕੀਤਾ ਜਾਵੇਗਾ। ਪਹਿਲਾਂ, ਉਸੇ ਕੰਮ 'ਤੇ, ਪਰ ਇੱਕ ਪ੍ਰੋਗਰਾਮ ਦੇ ਰੂਪ ਵਿੱਚ ਪੇਸ਼ ਕੀਤਾ ਗਿਆ, ਅਤੇ ਫਿਰ ਹੌਲੀ-ਹੌਲੀ ਇਸਨੂੰ ਗੁੰਝਲਦਾਰ ਬਣਾਉਣਾ ਅਤੇ ਸਾਫਟਵੇਅਰ ਵਿਕਾਸ ਦੀ ਦੁਨੀਆ ਤੋਂ ਮੌਜੂਦਾ ਉਦਾਹਰਣਾਂ ਵੱਲ ਵਧਣਾ.

ਅਗਲਾ ਲੇਖ ਪਹਿਲਾਂ ਹੀ ਤਿਆਰ ਹੈ:
ਸ਼ੁਰੂ ਤੋਂ ਇੱਕ ਰਸਮੀ ਤਸਦੀਕ ਸਿਸਟਮ ਬਣਾਉਣਾ: PHP ਅਤੇ ਪਾਈਥਨ ਵਿੱਚ ਇੱਕ ਪ੍ਰਤੀਕ VM ਲਿਖਣਾ

ਇਸ ਵਿੱਚ ਮੈਂ ਸਮੱਸਿਆਵਾਂ ਦੀ ਰਸਮੀ ਤਸਦੀਕ ਤੋਂ ਪ੍ਰੋਗਰਾਮਾਂ ਤੱਕ ਜਾਂਦਾ ਹਾਂ, ਅਤੇ ਵਰਣਨ ਕਰਦਾ ਹਾਂ
ਉਹਨਾਂ ਨੂੰ ਆਪਣੇ ਆਪ ਰਸਮੀ ਨਿਯਮ ਪ੍ਰਣਾਲੀਆਂ ਵਿੱਚ ਕਿਵੇਂ ਬਦਲਿਆ ਜਾ ਸਕਦਾ ਹੈ।

ਸਰੋਤ: www.habr.com