میری رائے میں، انٹرنیٹ کے روسی زبان کے شعبے میں، رسمی تصدیق کے موضوع کا کافی احاطہ نہیں کیا گیا ہے، اور خاص طور پر سادہ اور واضح مثالوں کی کمی ہے۔
میں ایک غیر ملکی ماخذ سے ایک مثال دوں گا، اور بھیڑیے، بکرے اور گوبھی کو دریا کے دوسری طرف کراس کرنے کے معروف مسئلے کا اپنا حل شامل کروں گا۔
لیکن پہلے، میں مختصراً بیان کروں گا کہ رسمی تصدیق کیا ہے اور اس کی ضرورت کیوں ہے۔
رسمی تصدیق کا مطلب عام طور پر ایک پروگرام یا الگورتھم کو دوسرے کا استعمال کرتے ہوئے چیک کرنا ہوتا ہے۔
یہ یقینی بنانے کے لیے ضروری ہے کہ پروگرام توقع کے مطابق برتاؤ کرے اور اس کی حفاظت کو بھی یقینی بنائے۔
باضابطہ تصدیق کمزوریوں کو تلاش کرنے اور ختم کرنے کا سب سے طاقتور ذریعہ ہے: یہ آپ کو پروگرام میں موجود تمام سوراخوں اور کیڑے تلاش کرنے، یا یہ ثابت کرنے کی اجازت دیتا ہے کہ وہ موجود نہیں ہیں۔
یہ بات قابل غور ہے کہ بعض صورتوں میں یہ ناممکن ہے، جیسے کہ 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