منهنجي خيال ۾، انٽرنيٽ جي روسي-ٻولي شعبي ۾، رسمي تصديق جو موضوع ڪافي نه آهي، ۽ خاص طور تي سادي ۽ واضح مثالن جي کوٽ آهي.
مان هڪ غير ملڪي ماخذ کان هڪ مثال ڏيندس، ۽ درياهه جي ٻئي ڪناري تي هڪ بگھڙ، هڪ ٻڪري ۽ هڪ گوبي کي پار ڪرڻ جي چڱي ريت مسئلي جو حل پڻ شامل ڪيو.
پر پهرين، مان مختصر طور تي بيان ڪندس ته رسمي تصديق ڇا آهي ۽ ان جي ضرورت ڇو آهي.
رسمي تصديق جو مطلب عام طور تي هڪ پروگرام يا ٻيو استعمال ڪندي الگورتھم کي جانچڻ جو مطلب آهي.
اهو ضروري آهي ته پروگرام کي توقع جي مطابق عمل ڪيو وڃي ۽ ان جي حفاظت کي يقيني بڻائي سگهجي.
باضابطه تصديق ڪمزورين کي ڳولڻ ۽ ختم ڪرڻ جو سڀ کان وڌيڪ طاقتور وسيلو آهي: اهو توهان کي پروگرام ۾ موجود سڀ سوراخ ۽ بگ ڳولڻ جي اجازت ڏئي ٿو، يا ثابت ڪري ٿو ته اهي موجود نه آهن.
اهو سمجهڻ جي قابل آهي ته ڪجهه حالتن ۾ اهو ناممڪن آهي، جهڙوڪ 8 چوڪن جي بورڊ جي چوٽي سان 1000 راڻين جي مسئلي ۾: اهو سڀ ڪجهه الورورٿمڪ پيچيدگي يا روڪڻ واري مسئلي تي اچي ٿو.
بهرحال، ڪنهن به صورت ۾، ٽن جوابن مان هڪ وصول ڪيو ويندو: پروگرام صحيح آهي، غلط، يا اهو ممڪن ناهي ته جواب جي حساب سان.
جيڪڏهن اهو هڪ جواب ڳولڻ ناممڪن آهي، اهو اڪثر ڪري پروگرام جي غير واضح حصن کي ٻيهر ڪم ڪرڻ ممڪن آهي، انهن جي الگورتھمي پيچيدگي کي گهٽائڻ، هڪ مخصوص ها يا نه جواب حاصل ڪرڻ لاء.
۽ رسمي تصديق استعمال ٿئي ٿي، مثال طور، ونڊوز ڪنيل ۽ ڊارپا ڊرون آپريٽنگ سسٽم ۾، تحفظ جي وڌ کان وڌ سطح کي يقيني بڻائڻ لاءِ.
اسان استعمال ڪنداسين Z3Prover، هڪ تمام طاقتور اوزار خودڪار ٿيل نظريي کي ثابت ڪرڻ ۽ مساوات کي حل ڪرڻ لاء.
ان کان علاوه، Z3 مساوات کي حل ڪري ٿو، ۽ انهن جي قيمتن کي برٽ فورس استعمال ڪندي نه چونڊيو.
هن جو مطلب اهو آهي ته اهو جواب ڳولڻ جي قابل آهي، جيتوڻيڪ ڪيسن ۾ جتي 10^100 ان پٽ اختيارن جا مجموعا آهن.
پر اهو صرف هڪ درجن ان پٽ دليلن جي قسم جي Integer جي باري ۾ آهي، ۽ اهو اڪثر عملي طور تي سامهون اچي ٿو.
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 رياستن جو هڪ جهڙي سيٽ مليو جيڪو سڀني شرطن کي پورو ڪري ٿو.
خلائي وقت جو هڪ قسم جي چار-dimensional ڪاسٽ.
اچو ته سمجهون ته ڇا ٿيو.
اسان ڏسون ٿا ته آخر ۾ هرڪو پار ڪيو، صرف پهرين اسان جي هاريءَ آرام ڪرڻ جو فيصلو ڪيو، ۽ پهرين 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