N'uche nke m, na mpaghara asụsụ Russian nke Ịntanetị, isiokwu nke nkwenye nkịtị adịghị ekpuchi nke ọma, na enweghi ihe atụ dị mfe na nke doro anya.
M ga-enye ihe atụ sitere na isi obodo ọzọ, tinyekwa ihe ngwọta nke m na nsogbu a maara nke ọma nke ịgafe anụ ọhịa wolf, ewu na kabeeji n'akụkụ nke ọzọ nke osimiri.
Mana nke mbụ, m ga-akọwa nkenke nkenke ihe nkwenye nkịtị bụ yana ihe kpatara eji chọọ ya.
Nkwenye n'ụdị na-apụtakarị ịlele otu mmemme ma ọ bụ algọridim site na iji ọzọ.
Nke a dị mkpa iji hụ na mmemme ahụ na-akpa àgwà dịka a tụrụ anya ya nakwa iji hụ na nchekwa ya.
Nkwenye n'ụdị bụ ụzọ kachasị ike isi chọta na iwepụ adịghị ike: ọ na-enye gị ohere ịchọta oghere na ahụhụ niile dị na mmemme, ma ọ bụ gosi na ha adịghị.
Ọ dị mma ịmara na n'ọnọdụ ụfọdụ nke a agaghị ekwe omume, dịka na nsogbu nke 8 Queens na obosara osisi nke 1000 squares: ọ niile na-agbadata mgbagwoju anya algorithmic ma ọ bụ nsogbu nkwụsị.
Agbanyeghị, n'ọnọdụ ọ bụla, a ga-enweta otu n'ime azịza atọ: mmemme ahụ ziri ezi, ezighi ezi, ma ọ bụ enweghị ike ịgbakọ azịza ya.
Ọ bụrụ na ọ gaghị ekwe omume ịchọta azịza, ọ na-enwekarị ike ịmegharị akụkụ ndị na-edoghị anya nke mmemme ahụ, na-ebelata mgbagwoju anya algorithmic ha, iji nweta azịza ee ma ọ bụ enweghị.
A na-ejikwa nkwenye nkịtị, dịka ọmụmaatụ, na Windows kernel na Darpa drone sistemụ arụmọrụ, iji hụ na nchebe kachasị elu.
Anyị ga-eji Z3Prover, ngwá ọrụ dị ike nke ukwuu maka igosipụta usoro ahụike akpaaka na idozi nha anya.
Ọzọkwa, Z3 na-edozi nha anya, ọ naghị ahọrọ ụkpụrụ ha site na iji ike dị nro.
Nke a pụtara na ọ nwere ike ịchọta azịza ya, ọbụlagodi n'ọnọdụ ebe enwere 10^100 nchikota nhọrọ ntinye.
Mana nke a bụ naanị ihe dị ka arụmụka ntinye iri na abụọ nke ụdị Integer, na nke a na-ezutekarị na omume.
Nsogbu gbasara 8 Queens (Ewere na Bekee ).
# 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)
Na-agba ọsọ Z3, anyị na-enweta azịza ya:
[Q_5 = 1,
Q_8 = 7,
Q_3 = 8,
Q_2 = 2,
Q_6 = 3,
Q_4 = 6,
Q_7 = 5,
Q_1 = 4]
Nsogbu eze nwanyị dị ka mmemme na-ewere dị ka ntinye aha nhazi nke ndị eze nwanyị 8 wee wepụta azịza ma ndị eze na-eti ibe ha.
Ọ bụrụ na anyị ga-edozi mmemme dị otú ahụ site na iji nkwenye nkịtị, ma e jiri ya tụnyere nsogbu ahụ, anyị ga-achọ ịme otu nzọụkwụ ọzọ n'ụdị ịtụgharị koodu mmemme n'ime nha nha: ọ ga-apụta na ọ bụ nke anyị. n'ezie, ọ bụrụ na e dere mmemme ahụ nke ọma).
Ihe fọrọ nke nta ka ọ bụrụ otu ihe ahụ ga-eme n'ihe banyere ịchọ adịghị ike: anyị na-edozi ọnọdụ mmepụta anyị chọrọ, dịka ọmụmaatụ, paswọọdụ nchịkwa, gbanwee isi iyi ma ọ bụ koodu decompiled n'ime nha anya kwekọrọ na nkwenye, wee nweta azịza maka ihe ọ bụla. ekwesịrị ịnye data dị ka ntinye iji mezuo ebumnuche.
N'uche nke m, nsogbu gbasara anụ ọhịa wolf, ewu na kabeeji na-adọrọ mmasị karị, ebe ọ bụ na edozi ya na-achọrịrị ọtụtụ (7) nzọụkwụ.
Ọ bụrụ na nsogbu eze nwanyị dị ka ikpe ebe ị nwere ike ịbanye na ihe nkesa site na iji otu GET ma ọ bụ POST arịrịọ, mgbe ahụ anụ ọhịa wolf, ewu na kabeeji na-egosipụta ihe atụ sitere na ụdị dị mgbagwoju anya na nke zuru ebe niile, nke nwere ike ime naanị ihe mgbaru ọsọ ahụ. site n'ọtụtụ arịrịọ.
Nke a bụ ihe atụ, dịka ọmụmaatụ, na ọnọdụ ebe ịchọrọ ịchọta ntụtụ SQL, dee faịlụ site na ya, wee bulie ikike gị elu wee nweta paswọọdụ.
Ọnọdụ nsogbu na ngwọta yaOnye ọrụ ugbo kwesịrị ibuga anụ ọhịa wolf, ewu na kabeeji gafee osimiri ahụ. Onye ọrụ ugbo nwere ụgbọ mmiri nke nwere ike iburu naanị otu ihe, ewezuga onye ọrụ ugbo n'onwe ya. Anụ ọhịa wolf ga-eri mkpi, ewu ga-erikwa kabeeji ma ọ bụrụ na onye ọrụ ugbo hapụ ya n'echeghị ya.
Ihe ngwọta ya bụ na na nzọụkwụ 4 onye ọrụ ugbo ga-achọ iburu ewu ahụ azụ.
Ugbu a, ka anyị malite idozi ya na mmemme.
Ka anyị gosi onye ọrụ ugbo, wolf, ewu na kabeeji dị ka 4 variables na-ewere uru naanị 0 ma ọ bụ 1. Zero pụtara na ha nọ n'aka ekpe, otu pụtara na ha nọ n'aka nri.
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
Ọnụọgụ bụ ọnụọgụ usoro achọrọ iji dozie. Nzọụkwụ ọ bụla na-anọchi anya ọnọdụ osimiri, ụgbọ mmiri na ihe niile.
Maka ugbu a, ka anyị họrọ ya na enweghị usoro ma jiri oke, were 10.
A na-anọchi anya ụlọ ọrụ ọ bụla na mbipụta 10 - nke a bụ uru ya na nke ọ bụla n'ime usoro iri.
Ugbu a, ka anyị tọọ ọnọdụ maka mmalite na imecha.
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 ]
Mgbe ahụ, anyị na-edozi ọnọdụ ebe anụ ọhịa wolf na-eri ewu, ma ọ bụ ewu na-eri kabeeji, dịka ihe mgbochi na nha nha.
(In the presence of a farmer, aggression bụ agaghị ekwe omume)
# 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) ]
N'ikpeazụ, anyị ga-akọwapụta ihe niile onye ọrụ ugbo nwere ike ime mgbe ọ na-agafe ebe ahụ ma ọ bụ azụ.
Ọ nwere ike iburu anụ ọhịa wolf, ewu ma ọ bụ kabeeji, ma ọ bụ na ọ gaghị ewere onye ọ bụla, ma ọ bụ ghara ịkwọ ụgbọ mmiri ebe ọ bụla.
N'ezie, ọ dịghị onye nwere ike ịgafe ma ọ bụrụ na onye ọrụ ugbo adịghị.
A ga-egosipụta nke a site n'eziokwu na steeti ọ bụla na-esote nke osimiri, ụgbọ mmiri na ụlọ ọrụ nwere ike ịdị iche na nke gara aga naanị n'ụzọ dị oke oke.
Ọ bụghị ihe karịrị 2 bits, yana ọtụtụ oke ndị ọzọ, ebe ọ bụ na onye ọrụ ugbo nwere ike ibuga otu ihe n'otu oge ma ọ bụghị ha niile nwere ike ịhapụ ọnụ.
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) ]
Ka anyị mee ihe ngwọta.
solve(Side + Start + Finish + Safe + Travel)
Anyị nwetakwara azịza ya!
Z3 chọtara steeti na-agbanwe agbanwe na-eju ọnọdụ niile.
Ụdị nkedo akụkụ anọ nke oghere-oge.
Ka anyị chọpụta ihe merenụ.
Anyị na-ahụ na n'ikpeazụ onye ọ bụla gafere, naanị na mbụ onye ọrụ ugbo anyị kpebiri izu ike, na nke mbụ 2 nzọụkwụ ọ dịghị igwu mmiri n'ebe ọ bụla.
Human_2 = 0
Human_3 = 0
Nke a na-egosi na ọnụ ọgụgụ steeti anyị họọrọ karịrị akarị, na 8 ga-ezu oke.
N'ebe anyị nọ, onye ọrụ ugbo mere nke a: malite, zuru ike, zuru ike, gafee ewu, gaghachi azụ, gafee kabeeji, laghachi na ewu, gafee anụ ọhịa wolf, laghachi azụ naanị ya, nyeghachi ewu ọzọ.
Ma n'ikpeazụ, e doziri nsogbu ahụ.
#Старт.
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
Ugbu a, ka anyị gbalịa ịgbanwe ọnọdụ ma gosi na ọ dịghị ngwọta.
Iji mee nke a, anyị ga-enye anụ ọhịa wolf herbivory, ọ ga-achọkwa iri kabeeji.
Enwere ike iji nke a tụnyere ikpe nke ebumnuche anyị bụ ịchekwa ngwa ahụ yana anyị kwesịrị ijide n'aka na enweghị oghere.
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 nyere anyị nzaghachi ndị a:
no solution
Ọ pụtara na e nweghị ngwọta n'ezie.
Ya mere, anyị ji mmemme gosipụtara na ọ gaghị ekwe omume ịgafe anụ ọhịa wolf na-enweghị ihe efu maka onye ọrụ ugbo.
Ọ bụrụ na ndị na-ege ntị na-ahụ isiokwu a na-akpali mmasị, mgbe ahụ, n'ọdịnihu isiokwu m ga-agwa gị otú e si atụgharị nkịtị omume ma ọ bụ ọrụ n'ime nhata dakọtara na usoro iwu, na-edozi ya, si otú na-ekpughe ma niile ziri ezi ndapụta na vulnerabilities. Nke mbụ, n'otu ọrụ ahụ, ma e gosipụtara n'ụdị mmemme, wee jiri nwayọọ nwayọọ na-agbagwoju anya ma na-aga n'ihu na ihe atụ dị ugbu a site na ụwa nke mmepe ngwanrọ.
Edemede na-esote adịlarị:
N'ime ya, m na-esi na nkwenye nkwenye nke nsogbu gaa na mmemme, ma kọwaa
kedu ka esi agbanwe ha ka ọ bụrụ usoro iwu iwu na-akpaghị aka.
isi: www.habr.com