Ukuqinisekisa ngokusesikweni kusetyenziswa umzekelo wengcuka, ingxaki yebhokhwe kunye nekhaphetshu

Ngokombono wam, kwicandelo lolwimi lwesiRashiya kwi-Intanethi, isihloko sokuqinisekiswa okusemthethweni asihlanganiswanga ngokwaneleyo, kwaye kukho ukungabikho kwemizekelo elula kwaye ecacileyo.

Ndizakwenza umzekelo kumthombo wasemzini, ndongeze eyam isisombululo kule ngxaki eyaziwayo yokuwela ingcuka, ibhokhwe nekhaphetshu ukuya kwelinye icala lomlambo.

Kodwa okokuqala, ndiza kuchaza ngokufutshane ukuba yintoni ukuqinisekiswa okusesikweni kwaye kutheni kuyimfuneko.

Ukuqinisekiswa okusesikweni ngokuqhelekileyo kuthetha ukujonga inkqubo enye okanye i-algorithm usebenzisa enye.

Oku kuyimfuneko ukuze kuqinisekiswe ukuba inkqubo iziphatha ngendlela elindelekileyo kunye nokuqinisekisa ukhuseleko lwayo.

Ukuqinisekiswa okusesikweni yeyona ndlela inamandla yokufumana kunye nokuphelisa ubuthathaka: ikuvumela ukuba ufumane yonke imingxuma ekhoyo kunye neebhugi kwinkqubo, okanye ubonise ukuba azikho.
Kuyafaneleka ukuba uqaphele ukuba kwezinye iimeko oku akunakwenzeka, njengengxaki yeendlovukazi ezi-8 ezinobubanzi bebhodi yee-square ze-1000: yonke into ihla kwi-algorithmic complexity okanye ingxaki yokuyeka.

Nangona kunjalo, kuyo nayiphi na imeko, enye yeempendulo ezintathu ziya kufunyanwa: inkqubo ichanekile, ayilunganga, okanye kwakungenakwenzeka ukubala impendulo.

Ukuba akunakwenzeka ukufumana impendulo, kuyenzeka ukuba kusebenze kwakhona iindawo ezingacacanga zeprogram, ukunciphisa ukuntsokotha kwazo kwe-algorithmic, ukuze kufumaneke ewe okanye hayi impendulo ethile.

Kwaye ukuqinisekiswa okusemthethweni kusetyenziswa, umzekelo, kwiinkqubo ze-Windows kernel kunye ne-Darpa drone, ukuqinisekisa umgangatho ophezulu wokukhusela.

Siza kusebenzisa i-Z3Prover, isixhobo esinamandla kakhulu sobungqina bethiyori ezenzekelayo kunye nokusombulula inxaki.

Ngapha koko, i-Z3 isombulula ii-equations, kwaye ayikhethi amaxabiso abo isebenzisa amandla akhohlakeleyo.
Oku kuthetha ukuba iyakwazi ukufumana impendulo, nakwiimeko apho kukho i-10^100 indibaniselwano yokhetho longeniso.

Kodwa oku kumalunga neshumi elinesibini leengxoxo zegalelo zohlobo lwe-Integer, kwaye oku kuhlala kudibana nokusebenza.

Ingxaki malunga neendlovukazi ezi-8 (Ithathwe kwisiNgesi incwadi yesandla).

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

Ukuqhuba i-Z3, sifumana 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]

Ingxaki kakumkanikazi ithelekiseka nenkqubo ethatha njengegalelo ulungelelwaniso lweekumkanikazi ezi-8 kwaye ikhuphe impendulo ukuba ngaba iikumkanikazi ziyabethana.

Ukuba besinokusombulula inkqubo enjalo sisebenzisa ukuqinisekiswa okusesikweni, ngoko xa kuthelekiswa nengxaki, kuya kufuneka sithathe elinye inyathelo ngakumbi ngendlela yokuguqula ikhowudi yenkqubo ibe yinxaki: iya kufana ngokusisiseko neyethu ( kunjalo, ukuba inkqubo yabhalwa ngokuchanekileyo).

Phantse into efanayo iyakwenzeka kwimeko yokukhangela ubuthathaka: sibeka nje iimeko zemveliso esizifunayo, umzekelo, igama eligqithisiweyo lolawulo, siguqule imvelaphi okanye ikhowudi eyohliweyo ibe yiequations ehambelana nokuqinisekisa, kwaye emva koko sifumane impendulo yokuba yintoni na. idatha kufuneka inikezelwe njengegalelo ukufezekisa injongo.

Ngokombono wam, ingxaki malunga nengcuka, ibhokhwe kunye neklabishi inomdla ngakumbi, ekubeni ukuyicombulula sele kufuna amanyathelo amaninzi (7).

Ukuba ingxaki yokumkanikazi ithelekiseka kwimeko apho ungangena kwi-server usebenzisa isicelo esisodwa se-GET okanye se-POST, ngoko ingcuka, ibhokhwe kunye neklabishi ibonisa umzekelo ovela kudidi olunzima kakhulu kunye nolubanzi, apho injongo inokufezekiswa kuphela. ngezicelo ezininzi.

Oku kuthelekiseka, umzekelo, kwimeko apho kufuneka ufumane inaliti yeSQL, bhala ifayile ngayo, emva koko uphakamise amalungelo akho kwaye emva koko ufumane igama eliyimfihlo.

Iimeko zengxaki kunye nesisombululo sayoUmfama kufuneka ahambise ingcuka, ibhokhwe kunye nekhaphetshu ukuwela umlambo. Umlimi unephenyane elinokuthwala into enye kuphela, ngaphandle komlimi ngokwakhe. Ingcuka iya kuyitya ibhokhwe kwaye ibhokhwe iya kuyitya ikhaphetshu ukuba umfama uzishiya zingajongwanga.

Isisombululo kukuba kwinyathelo lesi-4 umfama kuya kufuneka ayibuyisele ibhokhwe.
Ngoku masiqale ukuyisombulula ngokwenkqubo.

Masichaze umfama, ingcuka, ibhokhwe kunye nekhaphetshu njengezinto ezi-4 eziguquguqukayo ezithatha ixabiso elingu-0 okanye 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

Num linani lamanyathelo afunekayo ukusombulula. Inyathelo ngalinye limele imeko yomlambo, isikhephe kunye nawo onke amaqumrhu.

Okwangoku, masiyikhethe ngokungakhethiyo kwaye ngomda, sithathe i-10.

Iziko ngalinye limelwe kwiikopi ezili-10 - eli lixabiso layo kwinqanaba ngalinye lamanyathelo ali-10.

Ngoku makhe sibeke iimeko zokuqala nokugqiba.

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 ]

Emva koko sibeka iimeko apho ingcuka idla ibhokhwe, okanye ibhokhwe idla iklabishi, njengemiqobo kwi-equation.
(Phambi komlimi, ugonyamelo 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) ]

Kwaye ekugqibeleni, siya kuchaza zonke izenzo ezinokwenzeka zomfama xa ewela apho okanye emva.
Unokuthatha ingcuka, ibhokhwe okanye ikhaphetshu kunye naye, okanye angathathi nabani na, okanye angahambi ngomkhumbi naphi na.

Kakade ke, akukho mntu unokuwela ngaphandle komlimi.

Oku kuya kubonakaliswa yinyaniso yokuba imeko nganye elandelayo yomlambo, isikhephe kunye nemibutho inokwahluka kuleyo yangaphambili kuphela ngendlela engqongqo.

Akukho ngaphezu kwe-2 bits, kunye neminye imida emininzi, ekubeni umlimi unokuthutha kuphela iqumrhu elinye ngexesha kwaye akusiyo yonke into enokushiywa kunye.

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 isisombululo.

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

Kwaye sifumana impendulo!

I-Z3 ifumene iseti ehambelanayo yeemeko ezanelisa zonke iimeko.
Uhlobo lwe-four-dimensional cast of space-time.

Makhe sibone ukuba kwenzeka ntoni.

Siyabona ukuba ekugqibeleni wonke umntu wawela, kuphela ekuqaleni umlimi wethu wagqiba ekubeni aphumle, kwaye kumanyathelo ama-2 okuqala akaqubha naphi na.

Human_2 = 0
Human_3 = 0

Oku kubonisa ukuba inani lamazwe esiwakhethileyo ligqithise, kwaye i-8 iya kwanela.

Kwimeko yethu, umlimi wenza oku: qalisa, ukuphumla, ukuphumla, ukuwela ibhokhwe, ukuwela umva, ukuwela iklabishi, ukubuya kunye nebhokhwe, ukuwela ingcuka, ukubuyisela umva wedwa, ukuhambisa kwakhona ibhokhwe.

Kodwa ekugqibeleni ingxaki yasonjululwa.

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

Ngoku makhe sizame ukutshintsha iimeko kwaye sibonise ukuba akukho zisombululo.

Ukwenza oku, siya kunika ingcuka yethu i-herbivory, kwaye uya kufuna ukutya ikhaphetshu.
Oku kunokufaniswa kwimeko apho injongo yethu kukukhusela isicelo kwaye kufuneka siqinisekise ukuba akukho zikroba.

 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 le mpendulo ilandelayo:

 no solution

Kuthetha ukuba akukho zisombululo ngenene.

Ke ngoko, siye sangqina ngokwenkqubo ukuba akunakwenzeka ukuwela kunye nengcuka ye-omnivorous ngaphandle kwelahleko kumlimi.

Ukuba abaphulaphuli bafumana esi sihloko sinomdla, ngoko kumanqaku azayo ndiya kukuxelela indlela yokuguqula inkqubo eqhelekileyo okanye umsebenzi kwi-equation ehambelana neendlela ezisemthethweni, kwaye uyisombulule, ngaloo ndlela utyhila zombini iimeko ezisemthethweni kunye nobuthathaka. Okokuqala, kumsebenzi ofanayo, kodwa uboniswe ngendlela yeprogram, kwaye ngokuthe ngcembe unzima kwaye uqhubele phambili kwimizekelo yangoku evela kwihlabathi lophuhliso lwesoftware.

Inqaku elilandelayo sele lilungile:
Ukudala inkqubo yokuqinisekisa esemthethweni ukusuka ekuqaleni: Ukubhala iVM engumfuziselo kwi-PHP kunye nePython

Kuyo ndisuka ekuqinisekiseni okusesikweni kweengxaki ukuya kwiinkqubo, kwaye ndichaze
zingaguqulwa njani zibe ziinkqubo ezisemthethweni ngokuzenzekelayo.

umthombo: www.habr.com