Mune maonero angu, mumutauro weRussia-mutauro weInternet, musoro wekusimbiswa kwepamutemo hauna kuvharwa zvakakwana, uye pane kunyanya kushayikwa kwemienzaniso iri nyore uye yakajeka.
Ndichapa muenzaniso kubva kune imwe nyika, uye ndowedzera mhinduro yangu kune dambudziko rinozivikanwa rekuyambuka mhumhi, mbudzi uye kabichi kune rumwe rutivi rwerwizi.
Asi chekutanga, ini ndichatsanangura muchidimbu kuti chii chiri pamutemo verification uye nei ichidikanwa.
Formal verification inowanzoreva kutarisa chirongwa chimwe kana algorithm uchishandisa imwe.
Izvi zvinodiwa kuti ive nechokwadi chekuti chirongwa chinoshanda sezvakatarisirwa uye zvakare kuve nechokwadi chekuchengetedzwa kwayo.
Kuongororwa kwepamutemo ndiyo nzira ine simba kwazvo yekutsvaga uye kubvisa kusakanganiswa: inokutendera iwe kuti uwane ese aripo maburi uye tsikidzi muchirongwa, kana kuratidza kuti haapo.
Zvakakosha kuziva kuti mune dzimwe nguva izvi hazvigoneki, zvakadai sedambudziko re 8 queens nehupamhi hwebhodhi re 1000 squares: zvose zvinosvika kune algorithmic kuoma kana dambudziko rekumisa.
Zvisinei, chero ipi zvayo, imwe yemhinduro nhatu ichagamuchirwa: purogiramu yakarurama, isina kururama, kana kuti zvakanga zvisingakwanisi kuverenga mhinduro.
Kana zvisingabviri kuwana mhinduro, kazhinji zvinogoneka kugadzirisazve zvikamu zvisina kujeka zvechirongwa, kuderedza kuomarara kwavo kwealgorithmic, kuti vawane mhinduro chaiyo hongu kana kwete.
Uye kuongororwa kwepamutemo kunoshandiswa, semuenzaniso, muWindows kernel uye Darpa drone masisitimu anoshanda, kuve nechokwadi chepamusoro mwero wekudzivirira.
Isu tichashandisa Z3Prover, chishandiso chine simba kwazvo che automated theorem kuratidza uye kugadzirisa equation.
Uyezve, Z3 inogadzirisa equations, uye haisarudze hunhu hwavo uchishandisa brute force.
Izvi zvinoreva kuti inokwanisa kuwana mhinduro, kunyangwe kana paine 10 ^100 misanganiswa yesarudzo dzekuisa.
Asi izvi zvingori gumi nembiri zvekupokana zvemhando yeInteger, uye izvi zvinowanzosangana mukuita.
Dambudziko nezve 8 queens (Yakatorwa kubva kuChirungu ).
# 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)
Kumhanya Z3, tinowana mhinduro:
[Q_5 = 1,
Q_8 = 7,
Q_3 = 8,
Q_2 = 2,
Q_6 = 3,
Q_4 = 6,
Q_7 = 5,
Q_1 = 4]
Dambudziko remambokadzi rinofananidzwa nechirongwa chinotora semakonisheni emahosi masere uye chinoburitsa mhinduro kunyangwe vahosi vanorovana.
Dai taizogadzirisa chirongwa chakadaro tichishandisa certification yepamutemo, tozoenzanisa nedambudziko, taingoda kutora rimwe danho muchimiro chekushandura kodhi yepurogiramu kuita equation: yaizove yakangofanana neyedu ( hongu, kana chirongwa chakanyorwa nemazvo).
Zvinenge zvimwe chete zvichaitika munyaya yekutsvaga kusasimba: isu tinongoseta mamiriro ekubuda atinoda, semuenzaniso, password ye admin, shandura iyo sosi kana yakadhirowa kodhi kuita equations inoenderana nekusimbisa, tobva tawana mhinduro yekuti ndeipi data. inoda kupihwa sechipo chekuzadzisa chinangwa.
Mune maonero angu, dambudziko pamusoro pemhumhi, mbudzi uye kabichi inonyanya kufadza, sezvo kurigadzirisa kunotoda matanho akawanda (7).
Kana dambudziko remambokadzi richifananidzwa nenyaya yekuti iwe unogona kupinda musevha uchishandisa imwechete GET kana POST chikumbiro, ipapo mhumhi, mbudzi uye kabichi inoratidza muenzaniso kubva kune yakanyanya kuoma uye yakapararira chikamu, umo chinangwa chinogona kuwanikwa chete. nezvikumbiro zvakawanda.
Izvi zvinofananidzwa, semuenzaniso, kune chiitiko chaunoda kutsvaga jekiseni reSQL, nyora faira kuburikidza nayo, wozosimudza kodzero dzako uye wobva wawana password.
Mamiriro edambudziko uye mhinduro yaroMurimi anoda kutakura mhumhi, mbudzi nekabichi kuyambuka rwizi. Murimi ane igwa rinokwanisa kutakura chinhu chimwe chete, kunze kwemurimi pachake. Mhumhi ichadya mbudzi uye mbudzi ichadya makabheji kana murimi akarisiya.
Mhinduro ndeyekuti padanho rechina murimi anenge otoda kudzosera mbudzi.
Zvino ngatitangei kuzvigadzirisa nemapurogiramu.
Ngatiratidze murimi, mhumhi, mbudzi uye makabheji semimwe 4 inotora kukosha chete 0 kana 1. Zero zvinoreva kuti dziri kuruboshwe, uye imwe inoreva kuti dziri kurudyi.
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 ndiyo nhamba yematanho anodiwa kugadzirisa. Nhanho imwe neimwe inomiririra mamiriro erwizi, chikepe uye masangano ese.
Parizvino, ngatizvisarudzei zvisina tsarukano uye nemuganho, tora gumi.
Chimwe nechimwe chinomiririrwa mumakopi gumi - uku ndiko kukosha kwayo pane imwe neimwe yematanho gumi.
Zvino ngatiisei mamiriro ekutanga uye ekupedzisira.
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 ]
Zvadaro tinoisa mamiriro ezvinhu apo mhumhi inodya mbudzi, kana mbudzi inodya kabichi, sezvipingamupinyi mukuenzanisa.
(In the presence of a farmer, aggression is impossible)
# 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) ]
Uye pakupedzisira, tichatsanangura zvese zvingaitwa nemurimi kana achiyambuka ipapo kana kumashure.
Anogona kutora mhumhi, mbudzi kana kabichi naye, kana kusatora chero munhu, kana kusafamba nechikepe chero kupi zvako.
Chokwadi, hapana anogona kuyambuka asina murimi.
Izvi zvicharatidzwa nenyaya yekuti imwe neimwe inotevera mamiriro erwizi, chikepe uye masangano anogona kusiyana kubva kune yapfuura chete nenzira yakaganhurirwa.
Kwete kupfuura 2 bits, uye nemimwe miganho yakawanda, sezvo murimi anogona kutakura chinhu chimwe chete panguva uye kwete ese anogona kusiiwa pamwechete.
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) ]
Ngatimhanyei mhinduro.
solve(Side + Start + Finish + Safe + Travel)
Uye tinowana mhinduro!
Z3 yakawana seti inowirirana yenyika inogutsa mamiriro ese.
Rudzi rwechina-dimensional cast of space-time.
Ngatione kuti chii chakaitika.
Tinoona kuti pakupedzisira munhu wose akayambuka, pakutanga chete murimi wedu akasarudza kuzorora, uye mumatanho maviri ekutanga haana kushambira chero kupi zvako.
Human_2 = 0
Human_3 = 0
Izvi zvinoratidza kuti nhamba yematunhu atasarudza yakawandisa, uye 8 ichave yakakwana.
Muchiitiko chedu, murimi akaita izvi: kutanga, zorora, zorora, kuyambuka mbudzi, kuyambuka shure, kuyambuka kabichi, kudzoka nembudzi, kuyambuka mhumhi, kudzoka shure kwega, kuendesa zvakare mbudzi.
Asi pakupedzisira dambudziko rakagadziriswa.
#Π‘ΡΠ°ΡΡ.
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
Zvino ngatiedzei kushandura mamiriro uye kuratidza kuti hapana mhinduro.
Kuti tiite izvi, isu tichapa mhumhi yedu herbivory, uye iye achada kudya kabichi.
Izvi zvinogona kufananidzwa nechiitiko icho chinangwa chedu ndechekuchengetedza chikumbiro uye isu tinofanirwa kuve nechokwadi chekuti hapana maburi.
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 yakatipa mhinduro inotevera:
no solution
Zvinoreva kuti hapana mhinduro.
Nekudaro, isu takaratidza nenzira yehurongwa hazvigoneke kuyambuka neomnivorous wolf pasina kurasikirwa kumurimi.
Kana vateereri vakawana ichi chinyorwa chinonakidza, saka mune zvinotevera zvinyorwa ini ndichakuudza nzira yekushandura yakajairwa chirongwa kana basa kuita equation inoenderana neyakagadzirirwa nzira, uye kuigadzirisa, nekudaro kuburitsa zvese zviri pamutemo mamiriro uye kusasimba. Kutanga, pane basa rimwe chete, asi rinoratidzwa muchimiro chechirongwa, uye zvishoma nezvishoma kuchiomesa uye kuenderera kune yazvino mienzaniso kubva munyika yekuvandudza software.
Chinyorwa chinotevera chatogadzirira:
Mariri ini ndinofamba kubva kune yakarongeka yekusimbisa matambudziko kuenda kumapurogiramu, uye ndinotsanangura
vangashandurwa sei kuva hurongwa hwekutonga huri nyore.
Source: www.habr.com