🥇 Fanamarinana ofisialy amin'ny fampiasana ohatry ny olan'ny amboadia, osy ary laisoa

Raha ny hevitro, ao amin'ny sehatry ny Internet amin'ny teny Rosiana, dia tsy voaresaka tsara ny lohahevitra momba ny fanamarinana ofisialy, ary indrindra indrindra ny tsy fahampian'ny ohatra tsotra sy mazava.

Hanome ohatra avy amin'ny loharano vahiny aho, ary ampiako ny vahaolana ho an'ny olana fanta-daza amin'ny fiampitana amboadia, osy ary laisoa ho any ampitan'ny renirano.

Fa aloha, holazaiko fohifohy ny atao hoe fanamarinana ofisialy sy ny antony ilana izany.

Ny fanamarinana ofisialy matetika dia midika hoe manamarina programa iray na algorithm amin'ny fampiasana hafa.

Ilaina izany mba hahazoana antoka fa ny fandaharana dia mandeha araka ny tokony ho izy ary koa mba hiantohana ny fiarovana azy.

Ny fanamarinana ofisialy no fomba mahery vaika indrindra hitadiavana sy hanafoanana ny vulnerability: ahafahanao mahita ny lavaka sy ny bibikely rehetra misy ao anaty programa, na manaporofo fa tsy misy izy ireo.
Tsara ny manamarika fa amin'ny toe-javatra sasany dia tsy azo atao izany, toy ny amin'ny olan'ny mpanjakavavy 8 miaraka amin'ny sakan'ny birao 1000 efamira: izany rehetra izany dia midina amin'ny fahasarotana algorithmika na ny olana miato.

Na izany aza, na izany na tsy izany, ny iray amin'ireo valiny telo dia ho azo: marina ny programa, diso, na tsy azo atao ny mikajy ny valiny.

Raha tsy azo atao ny mahita valiny, dia matetika azo atao ny mamerina ny ampahany tsy mazava amin'ny programa, mampihena ny fahasarotan'ny algorithm, mba hahazoana valiny eny na tsia.

Ary ny fanamarinana ara-dalàna dia ampiasaina, ohatra, ao amin'ny Windows kernel sy ny rafitra fiasan'ny drone Darpa, mba hahazoana antoka ny fiarovana ambony indrindra.

Hampiasa Z3Prover izahay, fitaovana tena matanjaka ho an'ny fanaporofoana teôrema mandeha ho azy sy famahana ny equation.

Ankoatr'izay, ny Z3 dia mamaha ny fitoviana, ary tsy mifidy ny soatoaviny amin'ny fampiasana hery mahery vaika.
Midika izany fa afaka mahita ny valiny, na dia amin'ny tranga misy 10^100 fitambarana safidy fampidirana.

Saingy eo amin'ny tohan-kevitra fampidirana am-polony eo ho eo amin'ny karazana Integer izany, ary matetika no hita amin'ny fampiharana izany.

Olana momba ny mpanjakavavy 8 (Nalaina tamin'ny teny anglisy BOKY).

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

Mihazakazaka Z3, mahazo ny vahaolana:

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

Ny olan'ny mpanjakavavy dia azo ampitahaina amin'ny programa iray izay mandray ny koordinate amin'ny mpanjakavavy 8 ary mamoaka ny valiny raha mifampikapoka ny mpanjakavavy.

Raha mamaha programa toy izany amin'ny alàlan'ny fanamarinana ara-dalàna isika, raha ampitahaina amin'ny olana, dia mila manao dingana iray fotsiny isika amin'ny endrika famadihana ny code program ho toy ny equation: mety ho mitovy amin'ny antsika izany ( mazava ho azy, raha nosoratana tsara ny fandaharana).

Saika mitovy amin'izany koa no hitranga amin'ny fikatsahana ny vulnerabilities: mametraka ny fepetra fivoahana ilaintsika, ohatra, ny tenimiafina admin, manova ny loharano na code decompiled ho equations mifanaraka amin'ny fanamarinana, ary avy eo mahazo valiny momba ny data. mila omena ho fandraisan'anjarana mba hanatratrarana ny tanjona.

Raha ny hevitro dia vao mainka mahaliana ny olana momba ny amboadia sy ny osy ary ny laisoa, satria ny famahana azy dia efa mila dingana maro (7).

Raha ny olan'ny mpanjakavavy dia azo ampitahaina amin'ny tranga izay ahafahanao miditra amin'ny mpizara iray miaraka amin'ny fangatahana GET na POST tokana, dia ny amboadia, osy ary laisoa dia mampiseho ohatra avy amin'ny sokajy sarotra kokoa sy miely patrana, izay ny tanjona dia tsy ho tratra ihany. amin'ny fangatahana maromaro.

Izany dia azo ampitahaina, ohatra, amin'ny scenario iray izay ilanao hahita tsindrona SQL, manorata rakitra amin'ny alàlan'izany, ary atsangano ny zonao ary avy eo mahazo tenimiafina.

Ny toetry ny olana sy ny vahaolanaMila mitondra amboadia, osy ary laisoa eny ampitan'ny renirano ny mpamboly. Ny tantsaha dia manana sambo izay tsy mahazaka afa-tsy zavatra iray, ankoatry ny tantsaha mihitsy. Hohanin’ny amboadia ny osy ary hohanin’ny osy ny laisoa raha mamela azy tsy ho voakarakara ny mpamboly.

Ny vahaolana dia ny dingana faha-4 dia mila mamerina ny osy ny mpamboly.
Andeha isika hanomboka hamaha izany amin'ny programa.

Andeha hojerentsika ny mpamboly, amboadia, osy ary laisoa ho fari-piainana 4 izay mandray ny sandany 0 na 1 ihany. Ny aotra dia midika fa eo amin'ny sisiny ankavia izy ireo, ary ny iray midika hoe eo ankavanana.

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 dia ny isan'ny dingana ilaina hamahana. Ny dingana tsirairay dia maneho ny toetry ny renirano, ny sambo ary ny singa rehetra.

Amin'izao fotoana izao, andao hifidy azy amin'ny kisendrasendra ary miaraka amin'ny sisiny, maka 10.

Ny orinasa tsirairay dia aseho amin'ny dika 10 - izany no sandany isaky ny dingana 10.

Andeha isika hametraka ny fepetra amin'ny fanombohana sy famaranana.

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 ]

Avy eo dia mametraka ny fepetra izay ihinan'ny amboadia ny osy, na ny osy mihinana ny laisoa, toy ny teritery ao amin'ny equation.
(Raha misy mpamboly dia tsy azo atao ny manao herisetra)

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

Ary farany, hofaritantsika avokoa izay mety ho fihetsiky ny mpamboly rehefa miampita eo na miverina.
Afaka mitondra amboadia, na osy na laisoa miaraka aminy, na tsy mitondra olona, na tsy mandeha sambo na aiza na aiza.

Mazava ho azy fa tsy misy afaka miampita raha tsy misy mpamboly.

Izany dia haseho amin'ny hoe ny fanjakana tsirairay avy amin'ny renirano, sambo ary sampana dia mety tsy hitovy amin'ny teo aloha raha tsy amin'ny fomba voafetra.

Tsy mihoatra ny 2 bit, ary miaraka amin'ny fetra maro hafa, satria ny mpamboly dia afaka mitondra orinasa iray ihany amin'ny fotoana iray ary tsy ny rehetra no azo avela miaraka.

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

Andao hataontsika ny vahaolana.

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

Ary azontsika ny valiny!

Z3 dia nahita fanjakana tsy miovaova izay mahafeno ny fepetra rehetra.
Karazan-damba efatra amin'ny habakabaka-fotoana.

Andeha hojerentsika izay nitranga.

Hitanay fa niampita daholo ny rehetra, tamin'ny voalohany dia nanapa-kevitra ny hiala sasatra ny mpamboly anay, ary tamin'ny dingana 2 voalohany dia tsy milomano na aiza na aiza.

Human_2 = 0
Human_3 = 0

Midika izany fa be loatra ny isan'ny fanjakana nofidianay, ary 8 dia ampy.

Aminay, ny mpamboly dia nanao izao: manomboka, miala sasatra, miala sasatra, miampita osy, miampita laisoa, miampita laisoa, miverina miaraka amin'ny osy, miampita amboadia, miverina irery, manatitra osy indray.

Nivaha ihany anefa ny olana tamin’ny farany.

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

Andeha isika izao hiezaka hanova ny fepetra ary hanaporofo fa tsy misy vahaolana.

Mba hanaovana izany, dia homentsika herbivory ny amboadia, ary te hihinana laisoa izy.
Izany dia azo ampitahaina amin'ny tranga izay ny tanjontsika dia ny fiarovana ny fampiharana ary mila ataontsika antoka fa tsy misy banga.

 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 dia nanome antsika izao valinteny manaraka izao:

 no solution

Midika izany fa tena tsy misy vahaolana.

Noho izany, noporofoinay tamin'ny programa fa tsy azo atao ny miampita miaraka amin'ny amboadia omnivorous tsy misy fatiantoka ho an'ny mpamboly.

Raha hitan'ny mpanatrika mahaliana ity lohahevitra ity, dia holazaiko aminao amin'ny lahatsoratra ho avy ny fomba hamadihana ny programa mahazatra na ny fiasa ho lasa equation mifanaraka amin'ny fomba ofisialy, ary hamaha azy io, amin'izany dia manambara ny toe-javatra ara-dalàna sy ny fahalemena rehetra. Voalohany, amin'ny asa iray ihany, fa aseho amin'ny endrika programa, ary avy eo manasarotra tsikelikely izany ary miroso amin'ny ohatra amin'izao fotoana izao avy amin'ny tontolon'ny fampivoarana rindrambaiko.

Efa vonona ny lahatsoratra manaraka:
Mamorona rafitra fanamarinana ofisialy hatrany am-boalohany: Manoratra VM an'ohatra amin'ny PHP sy Python

Ao anatin'izany aho dia miala amin'ny fanamarinana ofisialy ny olana mankany amin'ny programa, ary mamaritra
ahoana no ahafahana mamadika azy ireo ho rafitra ara-dalàna ho azy.

Source: www.habr.com

Fanamarinana ofisialy mampiasa ny ohatry ny amboadia, osy ary laisoa olana

Add a comment cancel reply