Ukuqinisekisa okusemthethweni kusetshenziswa isibonelo senkinga yempisi, imbuzi kanye neklabishi

Ngokombono wami, emkhakheni wolimi lwesiRashiya we-Intanethi, isihloko sokuqinisekiswa okusemthethweni asihlanganisiwe ngokwanele, futhi kukhona ikakhulukazi ukuntuleka kwezibonelo ezilula nezicacile.

Ngizokwenza isibonelo ngomthombo wangaphandle, ngifake eyami isixazululo kule nkinga eyaziwayo yokuwela impisi, imbuzi neklabishi ngaphesheya komfula.

Kodwa okokuqala, ngizochaza kafushane ukuthi kuyini ukuqinisekiswa okusemthethweni nokuthi kungani kudingeka.

Ukuqinisekisa okusemthethweni ngokuvamile kusho ukuhlola uhlelo olulodwa noma i-algorithm usebenzisa olunye.

Lokhu kuyadingeka ukuze kuqinisekiswe ukuthi uhlelo luziphatha ngendlela elindelekile futhi nokuqinisekisa ukuphepha kwalo.

Ukuqinisekisa okusemthethweni kuyindlela enamandla kakhulu yokuthola nokuqeda ubungozi: kukuvumela ukuthi uthole zonke izimbobo ezikhona neziphazamisi ohlelweni, noma ufakazele ukuthi azikho.
Kuyaphawuleka ukuthi kwezinye izimo lokhu akunakwenzeka, njengasenkingeni yezindlovukazi eziyi-8 ezinobubanzi bebhodi lezikwele eziyi-1000: konke kwehla kubunzima be-algorithmic noma inkinga yokumisa.

Kodwa-ke, kunoma yikuphi, impendulo eyodwa kwezithathu izotholwa: uhlelo lulungile, alulungile, noma kwakungenakwenzeka ukubala impendulo.

Uma kungenakwenzeka ukuthola impendulo, ngokuvamile kuyenzeka ukuthi kusetshenzwe kabusha izingxenye ezingacacile zohlelo, kuncishiswe ubunkimbinkimbi bazo be-algorithmic, ukuze kutholwe impendulo ethile ethi yebo noma cha.

Futhi ukuqinisekiswa okusemthethweni kusetshenziswa, isibonelo, ku-Windows kernel kanye nezinhlelo zokusebenza ze-Darpa drone, ukuqinisekisa izinga eliphezulu lokuvikela.

Sizosebenzisa i-Z3Prover, ithuluzi elinamandla kakhulu lokufakazela i-theorem ezenzakalelayo kanye nokuxazulula izibalo.

Ngaphezu kwalokho, i-Z3 ixazulula izilinganiso, futhi ayikhethi amanani azo isebenzisa amandla anonya.
Lokhu kusho ukuthi iyakwazi ukuthola impendulo, ngisho nasezimeni lapho kukhona 10^100 inhlanganisela yezinketho zokufaka.

Kodwa lokhu cishe kungama-agumenti okokufaka ayishumi nambili ohlobo lwe-Integer, futhi lokhu kuvame ukuhlangana nakho ekusebenzeni.

Inkinga mayelana nezindlovukazi eziyisi-8 (Kuthathwe esiNgisini imanuwali).

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

Isebenzisa i-Z3, sithola isisombululo:

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

Inkinga yendlovukazi iqhathaniswa nohlelo oluthatha njengokufakiwe izixhumanisi zezindlovukazi ezingu-8 futhi lukhiphe impendulo ukuthi izindlovukazi ziyashayana.

Uma besingaxazulula uhlelo olunjalo sisebenzisa ukuqinisekiswa okusemthethweni, bese uma siqhathaniswa nenkinga, sizomane sithathe isinyathelo esisodwa ngaphezulu ngendlela yokuguqula ikhodi yohlelo ibe isibalo: izofana ncamashi neyethu ( Yebo, uma uhlelo lubhalwe ngendlela efanele).

Cishe kuzokwenzeka into efanayo endabeni yokufuna ubungozi: sivele sibeke izimo zokuphuma esizidingayo, isibonelo, iphasiwedi yomqondisi, siguqule umthombo noma ikhodi ehlukanisiwe ibe izibalo ezihambisana nokuqinisekisa, bese sithola impendulo yokuthi yini. idatha idinga ukuhlinzekwa njengokufakwayo ukuze kuzuzwe umgomo.

Ngokubona kwami, inkinga mayelana nempisi, imbuzi kanye neklabishi iyathakazelisa nakakhulu, ngoba ukuyixazulula kakade kudinga izinyathelo eziningi (7).

Uma inkinga yendlovukazi iqhathaniswa necala lapho ungangena khona kuseva usebenzisa isicelo esisodwa se-GET noma se-POST, khona-ke impisi, imbuzi kanye neklabishi ibonisa isibonelo esivela esigabeni esiyinkimbinkimbi kakhulu nesisabalele, lapho umgomo ungafinyelelwa khona kuphela. ngezicelo eziningi.

Lokhu kuqhathaniswa, isibonelo, nesimo lapho udinga ukuthola umjovo we-SQL, bhala ifayela ngawo, bese uphakamisa amalungelo akho bese uthola igama-mfihlo kuphela.

Izimo zenkinga nesixazululo sayoUmlimi udinga ukuthutha impisi, imbuzi kanye neklabishi ngaphesheya komfula. Umlimi unesikebhe esithwala into eyodwa kuphela, ngaphandle komlimi ngokwakhe. Impisi iyodla imbuzi kanti imbuzi izodla iklabishi uma umlimi ebashiya bengagadiwe.

Impendulo ithi esinyathelweni sesi-4 umlimi uzodinga ukuthi abuyisele imbuzi.
Manje ake siqale ukuyixazulula ngokohlelo.

Masichaze umlimi, impisi, imbuzi kanye neklabishi njengeziguquguquko ezi-4 ezithatha inani elingu-0 noma u-1 kuphela.

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

I-Num inombolo yezinyathelo ezidingekayo ukuze zixazululwe. Isinyathelo ngasinye simelela isimo somfula, isikebhe kanye nazo zonke izinhlangano.

Okwamanje, asiyikhethe ngokungahleliwe futhi ngemajini, sithathe u-10.

Ibhizinisi ngalinye limelwe ngamakhophi angu-10 - leli inani lalo esinyathelweni ngasinye kwezingu-10.

Manje ake sibeke izimo zokuqala nokuqeda.

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 ]

Bese sibeka izimo lapho impisi idla khona imbuzi, noma imbuzi idla iklabishi, njengemingcele ku-equation.
(Ebukhoneni bomlimi, ulaka alunakwenzeka)

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

Futhi ekugcineni, sizochaza zonke izenzo ezingenzeka zomlimi lapho ewela lapho noma ebuyela emuva.
Angathatha impisi, imbuzi noma iklabishi, noma angathathi muntu, noma angahambi nhlobo ngomkhumbi.

Yebo, akekho ongawela ngaphandle komlimi.

Lokhu kuzovezwa yiqiniso lokuthi isimo ngasinye esilandelayo somfula, isikebhe kanye nezinhlangano zingahluka kunedlule kuphela ngendlela elinganiselwe.

Angabi ngaphezu kwamabhithi angu-2, kanye neminye imikhawulo eminingi, njengoba umlimi angakwazi ukuthutha inhlangano eyodwa kuphela ngesikhathi futhi akuzona zonke ezingashiywa ndawonye.

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

Masiqhube isixazululo.

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

Futhi sithola impendulo!

I-Z3 ithole isethi yezifunda ezingaguquki ezenelisa zonke izimo.
Uhlobo lwabalingisi abanezinhlangothi ezine besikhathi sesikhathi.

Ake sithole ukuthi kwenzekani.

Siyabona ukuthi ekugcineni wonke umuntu wawela, kuphela ekuqaleni umlimi wethu wanquma ukuphumula, futhi ezinyathelweni zokuqala ezi-2 akabhukudi noma kuphi.

Human_2 = 0
Human_3 = 0

Lokhu kuphakamisa ukuthi inani lezifundazwe esizikhethile lidlulele, futhi u-8 uzokwanela impela.

Esimweni sethu, umlimi wenza lokhu: qala, phumula, uphumule, uwele imbuzi, uwele emuva, uwele iklabishi, ubuyele nembuzi, uwele impisi, ubuyele emuva wedwa, uphinde uhambise imbuzi.

Kodwa ekugcineni inkinga yaxazululeka.

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

Manje ake sizame ukushintsha izimo futhi sibonise ukuthi azikho izixazululo.

Ukwenza lokhu, sizonikeza i-wolf herbivory, futhi uzofuna ukudla iklabishi.
Lokhu kungafaniswa necala lapho inhloso yethu kuwukuvikela isicelo futhi sidinga ukwenza isiqiniseko sokuthi azikho izintuba.

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

I-Z3 isinike impendulo elandelayo:

 no solution

Kusho ukuthi azikho ngempela izixazululo.

Ngakho-ke, ngokohlelo sakufakazela ukuthi akunakwenzeka ukuwela nempisi ye-omnivorous ngaphandle kokulahlekelwa komlimi.

Uma izethameli zithola lesi sihloko sithakazelisa, khona-ke ezihlokweni ezizayo ngizokutshela ukuthi ungaluguqula kanjani uhlelo olujwayelekile noma umsebenzi ube i-equation ehambisana nezindlela ezisemthethweni, futhi uyixazulule, ngaleyo ndlela ngidalule zombili izimo ezisemthethweni kanye nokuba sengozini. Okokuqala, emsebenzini ofanayo, kodwa owethulwe ngendlela yohlelo, bese kancane kancane unzima futhi uqhubekele ezibonelweni zamanje ezivela emhlabeni wokuthuthukiswa kwesofthiwe.

Isihloko esilandelayo sesivele silungile:
Ukudala uhlelo lokuqinisekisa olusemthethweni kusukela ekuqaleni: Ukubhala i-VM engokomfanekiso ku-PHP nePython

Kuyo ngisuka ekuqinisekiseni okusemthethweni kwezinkinga ngiye ezinhlelweni, futhi ngichaze
zingaguqulwa kanjani zibe yizimiso ezisemthethweni ngokuzenzakalelayo.

Source: www.habr.com