වෘකයා, එළුවා සහ ගෝවා ගැටලුවේ උදාහරණය භාවිතා කරමින් විධිමත් සත්‍යාපනය

මගේ මතය අනුව, අන්තර්ජාලයේ රුසියානු භාෂා අංශයේ, විධිමත් සත්‍යාපනය පිළිබඳ මාතෘකාව ප්‍රමාණවත් ලෙස ආවරණය කර නොමැති අතර, විශේෂයෙන් සරල හා පැහැදිලි උදාහරණ හිඟයක් ඇත.

මම විදේශීය මූලාශ්‍රයකින් උදාහරණයක් දෙන්නෙමි, වෘකයෙකු, එළුවෙකු සහ ගෝවා ගඟෙන් එගොඩට යාමේ සුප්‍රසිද්ධ ගැටලුවට මගේම විසඳුමක් එක් කරමි.

නමුත් පළමුව, විධිමත් සත්‍යාපනය යනු කුමක්ද සහ එය අවශ්‍ය වන්නේ මන්දැයි මම කෙටියෙන් විස්තර කරමි.

විධිමත් සත්‍යාපනය යනු සාමාන්‍යයෙන් එක් වැඩසටහනක් හෝ ඇල්ගොරිතමයක් භාවිතා කරමින් පරීක්ෂා කිරීමයි.

වැඩසටහන අපේක්ෂිත පරිදි ක්‍රියා කරන බව සහතික කිරීමට සහ එහි ආරක්ෂාව සහතික කිරීමට මෙය අවශ්‍ය වේ.

විධිමත් සත්‍යාපනය යනු දුර්වලතා සෙවීමේ සහ ඉවත් කිරීමේ ප්‍රබලතම මාධ්‍යයයි: එය ඔබට වැඩසටහනක පවතින සියලුම සිදුරු සහ දෝෂ සොයා ගැනීමට හෝ ඒවා නොපවතින බව ඔප්පු කිරීමට ඉඩ සලසයි.
වර්ග 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ක් ලෙස දක්වමු. Zero යන්නෙන් අදහස් කරන්නේ ඔවුන් වම් ඉවුරේ සිටින බවත්, එකකින් අදහස් කරන්නේ ඒවා දකුණේ බවත්ය.

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

ඒ කියන්නේ ඇත්තටම විසඳුම් නැහැ කියන එක.

මේ අනුව, ගොවියාට පාඩුවක් නොමැතිව සර්ව භක්ෂක වෘකයෙකු සමඟ තරණය කිරීමේ නොහැකියාව අපි ක්‍රමලේඛනගතව ඔප්පු කළෙමු.

ප්‍රේක්ෂකයින්ට මෙම මාතෘකාව සිත්ගන්නාසුළු නම්, සාමාන්‍ය වැඩසටහනක් හෝ ශ්‍රිතයක් විධිමත් ක්‍රමවලට අනුකූල සමීකරණයක් බවට පත් කර එය විසඳන්නේ කෙසේදැයි ඉදිරි ලිපි වලින් මම ඔබට කියමි, එමඟින් සියලු නීත්‍යානුකූල අවස්ථා සහ අවදානම් දෙකම හෙළි කරයි. පළමුව, එකම කාර්යය මත, නමුත් වැඩසටහනක ස්වරූපයෙන් ඉදිරිපත් කර, පසුව ක්රමයෙන් එය සංකීර්ණ කිරීම සහ මෘදුකාංග සංවර්ධන ලෝකයෙන් වත්මන් උදාහරණ වෙත ගමන් කරයි.

ඊළඟ ලිපිය දැනටමත් සූදානම්:
මුල සිට විධිමත් සත්‍යාපන පද්ධතියක් නිර්මාණය කිරීම: PHP සහ Python හි සංකේතාත්මක VM ලිවීම

එය තුළ මම ගැටළු පිළිබඳ විධිමත් සත්‍යාපනයේ සිට වැඩසටහන් වෙත මාරු වන අතර විස්තර කරමි
ඒවා ස්වයංක්‍රීයව විධිමත් රීති පද්ධති බවට පරිවර්තනය කරන්නේ කෙසේද.

මූලාශ්රය: www.habr.com