Ба андешаи ман, дар бахши русизабони интернет мавзӯи санҷиши расмӣ ба қадри кофӣ пӯшонида нашудааст ва махсусан мисолҳои соддаву равшан каманд.
Аз сарчашмаи хоричй мисол меорам ва ба масъалаи маълуми гузаштан аз гург, бузу буз ва карам ба он тарафи дарё халли худро илова мекунам.
Аммо аввал, ман мухтасар шарҳ медиҳам, ки санҷиши расмӣ чист ва чаро он зарур аст.
Санҷиши расмӣ одатан маънои тафтиши як барнома ё алгоритмро бо истифода аз барномаи дигар дорад.
Ин барои он зарур аст, ки барнома тавре ки интизор мерафт, амал кунад ва инчунин амнияти онро таъмин кунад.
Санҷиши расмӣ воситаи пуриқтидортарин барои дарёфт ва рафъи осебпазирӣ мебошад: он ба шумо имкон медиҳад, ки ҳама сӯрохиҳо ва хатогиҳои мавҷударо дар барнома пайдо кунед ё исбот кунед, ки онҳо вуҷуд надоранд.
Қобили зикр аст, ки дар баъзе мавридҳо ин имконнопазир аст, масалан дар масъалаи 8 малика бо паҳнои тахтаи 1000 мураббаъ: ҳамааш ба мураккабии алгоритмӣ ё масъалаи қатъкунӣ рост меояд.
Аммо, дар ҳар сурат, яке аз се ҷавоб гирифта мешавад: барнома дуруст аст, нодуруст аст ё ҷавобро ҳисоб кардан имкон надошт.
Агар ёфтани ҷавоб имконнопазир бошад, аксар вақт қисмҳои норавшани барномаро аз нав кор кардан, мураккабии алгоритмии онҳоро кам кардан мумкин аст, то ҷавоби мушаххаси ҳа ё неро ба даст оред.
Ва санҷиши расмӣ, масалан, дар системаҳои оператсионии ядрои Windows ва Darpa drone барои таъмини сатҳи ҳадди ниҳоии муҳофизат истифода мешавад.
Мо 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 маҷмӯи муттасили давлатҳоро пайдо кард, ки ҳама шароитҳоро қонеъ мекунанд.
Як навъ рехтани чор-ченакаи кайҳон-вақт.
Биёед бифаҳмем, ки чӣ рӯй дод.
Мо мебинем, ки дар охир хама гузаштанд, танхо дар аввал дехкони мо карор дод, ки дам гирад ва дар 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
Ин маънои онро дорад, ки дар ҳақиқат ҳеҷ гуна ҳалли мушкилот вуҷуд надорад.
Хамин тавр, мо ба таври программавй исбот намудем, ки бо гурги хамахур бе талаф гузаштан ба дехкон имконнопазир аст.
Агар шунавандагон ин мавзӯъро ҷолиб пайдо кунанд, пас дар мақолаҳои оянда ман ба шумо мегӯям, ки чӣ гуна як барнома ё функсияи оддиро ба муодилаи бо усулҳои расмӣ мувофиқ табдил додан ва онро ҳал кардан ва ба ин васила ҳам ҳама сенарияҳои қонунӣ ва осебпазириро ошкор кардан лозим аст. Аввалан, аз рӯи ҳамон вазифа, аммо дар шакли барнома пешниҳод карда мешавад ва сипас тадриҷан онро мураккабтар карда, ба мисолҳои кунунӣ аз ҷаҳони таҳияи нармафзор мегузаранд.
Мақолаи навбатӣ аллакай омода аст:
Дар он ман аз санҷиши расмии мушкилот ба барномаҳо мегузарам ва тавсиф мекунам
чӣ тавр онҳо метавонанд ба таври худкор ба системаҳои қоидаҳои расмӣ табдил дода шаванд.
Манбаъ: will.com