নেকড়ে, ছাগল এবং বাঁধাকপি সমস্যার উদাহরণের আনুষ্ঠানিক যাচাইকরণ

আমার মতে, ইন্টারনেটের রাশিয়ান-ভাষা সেক্টরে, আনুষ্ঠানিক যাচাইকরণের বিষয়টি পর্যাপ্তভাবে কভার করা হয়নি এবং বিশেষ করে সহজ এবং স্পষ্ট উদাহরণের অভাব রয়েছে।

আমি একটি বিদেশী উত্স থেকে একটি উদাহরণ দেব, এবং নদীর অপর পারে একটি নেকড়ে, একটি ছাগল এবং একটি বাঁধাকপি অতিক্রম করার সুপরিচিত সমস্যার আমার নিজস্ব সমাধান যোগ করব।

তবে প্রথমে, আমি সংক্ষেপে বর্ণনা করব আনুষ্ঠানিক যাচাইকরণ কী এবং কেন এটি প্রয়োজন।

আনুষ্ঠানিক যাচাইকরণের অর্থ সাধারণত একটি প্রোগ্রাম বা অ্যালগরিদম ব্যবহার করে অন্যটি পরীক্ষা করা।

এটি নিশ্চিত করার জন্য প্রয়োজনীয় যে প্রোগ্রামটি প্রত্যাশিতভাবে আচরণ করে এবং এর নিরাপত্তা নিশ্চিত করতে।

ফর্মাল ভেরিফিকেশন হল দুর্বলতা খুঁজে বের করার এবং দূর করার সবচেয়ে শক্তিশালী মাধ্যম: এটি আপনাকে একটি প্রোগ্রামে বিদ্যমান সব ছিদ্র এবং বাগ খুঁজে বের করতে বা প্রমাণ করতে দেয় যে সেগুলি বিদ্যমান নেই।
এটি লক্ষণীয় যে কিছু ক্ষেত্রে এটি অসম্ভব, যেমন 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 অনুরোধ ব্যবহার করে একটি সার্ভারে প্রবেশ করতে পারেন, তাহলে নেকড়ে, ছাগল এবং বাঁধাকপি আরও জটিল এবং বিস্তৃত বিভাগ থেকে একটি উদাহরণ প্রদর্শন করে, যেখানে লক্ষ্যটি কেবলমাত্র অর্জন করা যেতে পারে। বেশ কয়েকটি অনুরোধ দ্বারা।

এটি তুলনীয়, উদাহরণস্বরূপ, এমন একটি দৃশ্যের সাথে যেখানে আপনাকে একটি এসকিউএল ইনজেকশন খুঁজে বের করতে হবে, এটির মাধ্যমে একটি ফাইল লিখতে হবে, তারপরে আপনার অধিকারগুলিকে উন্নত করুন এবং শুধুমাত্র তারপর একটি পাসওয়ার্ড পাবেন৷

সমস্যার শর্ত এবং এর সমাধানকৃষককে নদীর ওপারে একটি নেকড়ে, একটি ছাগল এবং বাঁধাকপি পরিবহন করতে হবে। কৃষকের একটি নৌকা আছে যা শুধুমাত্র একটি বস্তুকে মিটমাট করতে পারে, কৃষক নিজে ছাড়াও। নেকড়ে ছাগল খাবে এবং ছাগল বাঁধাকপি খাবে যদি কৃষক তাদের অযত্নে ছেড়ে দেয়।

উত্তর হল ধাপ 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

Num হল সমাধানের জন্য প্রয়োজনীয় ধাপের সংখ্যা। প্রতিটি পদক্ষেপ নদী, নৌকা এবং সমস্ত সত্তার অবস্থার প্রতিনিধিত্ব করে।

আপাতত, র্যান্ডম এবং মার্জিন সহ এটি বেছে নেওয়া যাক, 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