Xaqiijinta rasmiga ah iyadoo la adeegsanayo tusaale ahaan dhibaatada yeyga, riyaha iyo kaabashka

Fikradayda, qaybta luqadda Ruushka ee internetka, mawduuca xaqiijinta rasmiga ah si ku filan looma daboolin, gaar ahaanna waxaa jira la'aanta tusaalooyin fudud oo cad.

Waxa aan tusaale u soo qaadan doonaa il shisheeye, oo aan ku dari doonaa xal u gaar ah dhibaatada la og yahay ee ah in yeey, ari iyo kaabash loo maro dhinaca kale ee webiga.

Laakiin marka hore, waxaan si kooban u qeexi doonaa waxa ay tahay xaqiijinta rasmiga ah iyo sababta loogu baahan yahay.

Xaqiijinta rasmiga ah waxay badanaa ka dhigan tahay hubinta hal barnaamij ama algorithm adoo isticmaalaya mid kale.

Tani waa lagama maarmaan si loo hubiyo in barnaamijku u dhaqmo sidii la filayay iyo sidoo kale si loo xaqiijiyo ammaankiisa.

Xaqiijinta rasmiga ah waa habka ugu awoodda badan ee lagu helo loogana takhaluso dayacanka: waxay kuu ogolaaneysaa inaad hesho dhammaan godadka jira iyo kutaannada barnaamijka, ama caddeyso inaysan jirin.
Waxaa habboon in la ogaado in xaaladaha qaarkood tani ay tahay mid aan macquul ahayn, sida dhibaatada 8 boqorrada oo leh ballac guddiga 1000 oo labajibbaaran: dhammaantood waxay hoos ugu dhacaan kakanaanta algorithmic ama dhibaatada joojinta.

Si kastaba ha ahaatee, xaalad kasta, mid ka mid ah seddexda jawaabood ayaa la heli doonaa: barnaamijku waa sax, khalad, ama ma suurtagalin in la xisaabiyo jawaabta.

Haddii aysan suurtagal ahayn in la helo jawaab, waxaa badanaa suurtagal ah in dib loo shaqeeyo qaybo aan caddayn oo barnaamijka ah, hoos u dhigaya kakanaanta algorithmic, si loo helo jawaab gaar ah oo haa ama maya ah.

Xaqiijinta rasmiga ah ayaa loo isticmaalaa, tusaale ahaan, nidaamyada hawlgalka Windows kernel iyo Darpa drone, si loo hubiyo heerka ugu sarreeya ee ilaalinta.

Waxaan isticmaali doonaa Z3Prover, qalab aad u awood badan oo loogu talagalay caddaynta teorem-ka tooska ah iyo xallinta isla'egta.

Intaa waxaa dheer, Z3 waxay xallisaa isla'egyada, mana doortaan qiyamkooda iyadoo la adeegsanayo xoog aan caqli-gal ahayn.
Tani waxay ka dhigan tahay inay awood u leedahay inay hesho jawaabta, xitaa xaaladaha ay jiraan 10 ^ 100 isku darka ikhtiyaarka wax-gelinta.

Laakin tani waa kaliya ilaa darsin doodood oo soo gelis ah oo ah nooca Integer-ka, tanina inta badan waxa ay la kulantaa ficil ahaan.

Dhibaato ku saabsan 8 boqoradood (waxaa laga soo qaatay Ingiriis buug-gacmeedka).

# 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)

Ku shaqeynta Z3, waxaan helnaa xalka:

[Q_5 = 1,
 Q_8 = 7,
 Q_3 = 8,
 Q_2 = 2,
 Q_6 = 3,
 Q_4 = 6,
 Q_7 = 5,
 Q_1 = 4]

Dhibaatada boqoraddu waxay u dhigantaa barnaamij ka qaata isku-duwidda 8 boqoradood oo soo saara jawaabta haddii boqoradu is garaaceen.

Haddii aan xallino barnaamijkan oo kale annagoo adeegsanayna xaqiijinta rasmiga ah, ka dib marka la barbar dhigo dhibaatada, waxaan si fudud ugu baahan karnaa inaan qaadno hal tallaabo oo kale oo ah qaabka loo beddelo koodhka barnaamijka isla'eg: waxay noqon doontaa mid asal ahaan la mid ah keenna. Dabcan, haddii barnaamijka si sax ah loo qoray).

Ku dhawaad ​​wax la mid ah ayaa ku dhici doona kiiska raadinta nuglaanta: kaliya waxaan dejineynaa shuruudaha wax soo saarka ee aan u baahanahay, tusaale ahaan, erayga sirta ah ee maamulka, u beddelo isha ama koodhka la jajabiyey isla'egyada ku habboon xaqiijinta, ka dibna hel jawaabta waxa xogta ayaa loo baahan yahay in la keeno si ay u noqoto talobixin si loo gaaro yoolka.

Fikradayda, dhibaatada ku saabsan yeyga, riyaha iyo kaabajka ayaa xitaa aad u xiiso badan, tan iyo markii la xalliyo waxay u baahan tahay tallaabooyin badan (7).

Haddii dhibaatada boqoraddu ay la mid tahay kiis aad geli karto server adoo isticmaalaya hal codsi GET ama POST, ka dib yeyga, riyaha iyo kaabajka ayaa muujinaya tusaale ka mid ah qayb aad u adag oo baahsan, kaas oo hadafka lagu gaari karo oo kaliya. dhowr codsi.

Tani waxay la mid tahay tusaale ahaan, xaalad aad u baahan tahay si aad u hesho cirbad SQL ah, ku qor fayl, ka dibna kor u qaad xuquuqdaada oo kaliya ka dibna hel furaha sirta ah.

Xaaladaha dhibaatada iyo xalkeedaBeeralaydu waxa ay u baahan yihiin in ay wabiga ka gudbaan yeyda, ari iyo kaabash. Beeralayda waxa uu haystaa doon keliya oo qaadi karta hal shay, marka laga reebo beeralayda laftiisa. Yeyga ayaa cuni doonta riyaha, riguna wuxuu cuni doonaa kaabashka haddii beeralaydu ka tago iyaga oo aan la ilaalin.

Xalku wuxuu yahay in tallaabada 4-aad uu beeralaydu u baahan doono inuu orgiga dib u qaato.
Hadda aan bilowno xallinta barnaamij ahaan.

Aynu ku tilmaamno beeralayda, yeyda, riyaha iyo kaabashka inay yihiin 4 doorsoome oo qiimeeya 0 ama 1 kaliya. Zero waxay ka dhigan tahay inay ku yaalaan bangiga bidix, midna waxay ka dhigan tahay inay midigta yihiin.

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

Lambarku waa tirada tillaabooyinka loo baahan yahay si loo xalliyo. Tallaabo kastaa waxay ka dhigan tahay xaaladda webiga, doonta iyo dhammaan qaybaha.

Hadda, aynu ku doorano si bakhtiyaa nasiib ah oo aan xad lahayn, qaado 10.

Qayb kastaa waxay u taagan tahay 10 nuqul - tani waa qiimaheeda mid kasta oo ka mid ah 10ka tallaabo.

Hadda aynu dejinno shuruudaha bilowga iyo dhammaystirka.

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 ]

Ka dib waxaan dejineynaa shuruudaha uu yeeygu ariga cunayo, ama rigu cunayo kaabajka, taasoo ah caqabadaha ku jira isla'egta.
( Beeralayda marka uu joogo, gardarada waa wax aan macquul ahayn)

# 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) ]

Ugu dambeyntiina, waxaan qeexi doonaa dhammaan ficillada suurtagalka ah ee beeralayda marka uu ka gudbayo halkaas ama dib u noqoshada.
Wuxuu qaadan karaa yeey, ari ama kaabash, ama qofna ma kaxaysan karo, ama meelna kuma dhoofin karo.

Dabcan, qofna ma gudbi karo beeralay la'aanteed.

Tan waxaa lagu muujin doonaa xaqiiqda ah in xaalad kasta oo soo socota ee webiga, doonta iyo hay'adaha ay ka duwanaan karaan tii hore oo kaliya si xaddidan.

Wax ka badan 2-bit, iyo xad kale oo badan, maadaama beeralayda uu qaadi karo hal qayb markiiba oo aan dhammaan laga tegi karin.

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) ]

Xalka aan wadno.

solve(Side + Start + Finish + Safe + Travel)

Anaguna jawaabta waan helnaa!

Z3 waxay heshay go'an dawlado joogto ah oo qanciya dhammaan shuruudaha.
Nooc ka mid ah kabka afar-geesoodka ah ee wakhtiga-space-time.

Aynu ogaano waxa dhacay.

Waxaan aragnaa in ugu dambeyntii qof kastaa ka gudbay, kaliya markii ugu horeysay ee beeralayda ayaa go'aansaday inuu nasto, 2dii tillaabo ee horena meelna kuma dabaalan.

Human_2 = 0
Human_3 = 0

Tani waxay soo jeedinaysaa in tirada gobolada aan dooranay ay xad dhaaf tahay, 8-na ay noqon doonto mid ku filan.

Anaga, ninkii beeralayda ahaa sidaan buu yeelay: bilow, naso, naso, orgiga ka gudba, dib u gudba, ka gudubka kaabashka, ridii la soo noqo, yeeyga ka gudba, ka gudba yeeyga, soo noqo kaligiis, dib u soo celi orgiga.

Laakin ugu danbeyn dhibkii waa la xaliyay.

#Старт.
 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

Hadda aan isku dayno inaan bedelno shuruudaha oo aan caddayno inaysan jirin xalal.

Si arrintan loo sameeyo, waxaan siin doonaa geedo yeeyga our, oo wuxuu doonayaa inuu cuno kaabash.
Tan waxaa la barbar dhigi karaa kiis kaas oo hadafkeenu yahay in la sugo codsiga waxaanan u baahanahay inaan hubinno inaysan jirin daldaloolo.

 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 wuxuu na siiyay jawaabta soo socota:

 no solution

Waxay la macno tahay in runtii aysan jirin wax xal ah.

Sidaa awgeed, waxaanu si barnaamij ah u caddaynay in aanay suurtogal ahayn in lagaga gudbo yeyga wax walba oo aan khasaare u geysan beeralayda.

Haddii dhagaystayaashu mawduucan u arkaan mid xiiso leh, markaa maqaallada mustaqbalka waxaan kuu sheegi doonaa sida loo beddelo barnaamijka caadiga ah ama shaqada loo beddelo isla'egta ku habboon hababka rasmiga ah, oo loo xalliyo, taas oo muujinaysa dhammaan xaaladaha sharciga ah iyo dayacanka labadaba. Marka hore, isla hawl isku mid ah, laakiin lagu soo bandhigay qaab barnaamij ah, ka dibna si tartiib tartiib ah u adkeynaya oo u gudubta tusaalooyinka hadda jira ee adduunka horumarinta software.

Maqaalka xiga ayaa durba diyaar ah:
Abuuritaanka nidaam xaqiijin rasmi ah oo xoq ah: Qorista VM calaamad ah PHP iyo Python

Dhexdeeda waxaan uga guuraa xaqiijinta rasmiga ah ee dhibaatooyinka una guuro barnaamijyada, oo aan sharaxo
sidee loogu rogi karaa nidaam sharci oo toos ah.

Source: www.habr.com