என் கருத்துப்படி, இணையத்தின் ரஷ்ய மொழித் துறையில், முறையான சரிபார்ப்பு தலைப்பு போதுமானதாக இல்லை, குறிப்பாக எளிய மற்றும் தெளிவான எடுத்துக்காட்டுகள் இல்லாதது.
நான் ஒரு வெளிநாட்டு மூலத்திலிருந்து ஒரு உதாரணம் தருகிறேன், மேலும் ஒரு ஓநாய், ஒரு ஆடு மற்றும் ஒரு முட்டைக்கோஸ் ஆற்றின் மறுபுறம் கடந்து செல்லும் நன்கு அறியப்பட்ட பிரச்சனைக்கு எனது சொந்த தீர்வைச் சேர்ப்பேன்.
ஆனால் முதலில், முறையான சரிபார்ப்பு என்றால் என்ன, அது ஏன் தேவைப்படுகிறது என்பதை சுருக்கமாக விவரிக்கிறேன்.
முறையான சரிபார்ப்பு என்பது பொதுவாக ஒரு நிரல் அல்லது அல்காரிதத்தை மற்றொன்றைப் பயன்படுத்தி சரிபார்ப்பதைக் குறிக்கிறது.
நிரல் எதிர்பார்த்தபடி செயல்படுவதை உறுதி செய்வதற்கும் அதன் பாதுகாப்பை உறுதி செய்வதற்கும் இது அவசியம்.
முறையான சரிபார்ப்பு என்பது பாதிப்புகளைக் கண்டறிந்து நீக்குவதற்கான மிகவும் சக்திவாய்ந்த வழிமுறையாகும்: இது ஒரு நிரலில் இருக்கும் அனைத்து ஓட்டைகள் மற்றும் பிழைகளைக் கண்டறிய அல்லது அவை இல்லை என்பதை நிரூபிக்க உங்களை அனுமதிக்கிறது.
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