Ni ero mi, ni eka-ede Russian ti Intanẹẹti, koko-ọrọ ti ijẹrisi deede ko ni kikun, ati paapaa aini awọn apẹẹrẹ ti o rọrun ati mimọ.
Emi yoo fun apẹẹrẹ lati orisun ajeji, emi o si fi ojutu ti ara mi kun si iṣoro ti o mọye ti o kọja Ikooko, ewurẹ ati eso kabeeji kan si apa keji odo.
Ṣugbọn ni akọkọ, Emi yoo ṣapejuwe ni ṣoki kini ijẹrisi iṣe deede ati idi ti o ṣe nilo.
Ijẹrisi deede nigbagbogbo tumọ si ṣayẹwo eto kan tabi algorithm nipa lilo omiiran.
Eyi jẹ pataki lati rii daju pe eto naa huwa bi o ti ṣe yẹ ati tun lati rii daju aabo rẹ.
Ijẹrisi deede jẹ ọna ti o lagbara julọ fun wiwa ati imukuro awọn ailagbara: o fun ọ laaye lati wa gbogbo awọn iho ati awọn idun ti o wa ninu eto kan, tabi jẹrisi pe wọn ko si.
O ṣe akiyesi pe ni awọn igba miiran eyi ko ṣee ṣe, gẹgẹbi ninu iṣoro ti awọn ayaba 8 pẹlu iwọn igbimọ ti awọn onigun mẹrin 1000: gbogbo rẹ wa si isalẹ lati algorithmic complexity tabi iṣoro idaduro.
Bibẹẹkọ, ni eyikeyi ọran, ọkan ninu awọn idahun mẹta yoo gba: eto naa tọ, ko tọ, tabi ko ṣee ṣe lati ṣe iṣiro idahun naa.
Ti ko ba ṣee ṣe lati wa idahun, o ṣee ṣe nigbagbogbo lati tun ṣiṣẹ awọn apakan ti ko ṣe akiyesi ti eto naa, idinku idiju algorithmic wọn, lati le gba bẹẹni tabi rara kan pato idahun.
Ati pe a lo ijẹrisi deede, fun apẹẹrẹ, ninu ekuro Windows ati awọn ọna ṣiṣe drone Darpa, lati rii daju ipele aabo ti o pọju.
A yoo lo Z3Prover, ohun elo ti o lagbara pupọ fun idasi imọ-jinlẹ adaṣe ati ipinnu idogba.
Pẹlupẹlu, Z3 yanju awọn idogba, ati pe ko yan awọn iye wọn nipa lilo agbara iro.
Eyi tumọ si pe o ni anfani lati wa idahun, paapaa ni awọn ọran nibiti awọn akojọpọ 10^100 wa ti awọn aṣayan titẹ sii.
Ṣugbọn eyi jẹ nipa awọn ariyanjiyan igbewọle mejila ti iru Integer, ati pe eyi ni igbagbogbo pade ni iṣe.
Isoro nipa awọn ayaba 8 (Ti o gba lati Gẹẹsi ).
# 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)
Ṣiṣe Z3, a gba ojutu:
[Q_5 = 1,
Q_8 = 7,
Q_3 = 8,
Q_2 = 2,
Q_6 = 3,
Q_4 = 6,
Q_7 = 5,
Q_1 = 4]
Iṣoro ayaba jẹ afiwera si eto ti o gba bi titẹ sii awọn ipoidojuko ti awọn ayaba 8 ti o ṣe abajade idahun boya awọn ayaba lu ara wọn.
Ti a ba ni lati yanju iru eto yii nipa lilo iṣeduro deede, lẹhinna ni akawe si iṣoro naa, a yoo nilo lati ṣe igbesẹ kan diẹ sii ni ọna ti yiyipada koodu eto naa sinu idogba: yoo yipada lati jẹ aami pataki si tiwa ( dajudaju, ti o ba ti awọn eto ti a ti kọ tọ).
Fere ohun kanna yoo ṣẹlẹ ninu ọran wiwa fun awọn ailagbara: a kan ṣeto awọn ipo iṣelọpọ ti a nilo, fun apẹẹrẹ, ọrọ igbaniwọle abojuto, yi orisun tabi koodu ti a kojọpọ sinu awọn idogba ti o ni ibamu pẹlu ijerisi, ati lẹhinna gba idahun si kini kini data nilo lati pese bi titẹ sii lati ṣaṣeyọri ibi-afẹde naa.
Ni ero mi, iṣoro naa nipa Ikooko, ewurẹ ati eso kabeeji paapaa jẹ ohun ti o nifẹ si, niwon didasilẹ rẹ tẹlẹ nilo ọpọlọpọ awọn igbesẹ (7).
Ti iṣoro ayaba ba jẹ afiwera si ọran nibiti o ti le wọ inu olupin kan nipa lilo GET kan tabi ibeere POST, lẹhinna Ikooko, ewurẹ ati eso kabeeji ṣafihan apẹẹrẹ kan lati eka pupọ diẹ sii ati ẹka ibigbogbo, ninu eyiti ibi-afẹde le ṣee ṣe nikan nipa orisirisi awọn ibeere.
Eyi jẹ afiwera, fun apẹẹrẹ, si oju iṣẹlẹ nibiti o nilo lati wa abẹrẹ SQL kan, kọ faili nipasẹ rẹ, lẹhinna gbe awọn ẹtọ rẹ ga ati lẹhinna gba ọrọ igbaniwọle kan.
Awọn ipo ti iṣoro naa ati ojutu rẹAgbe nilo lati gbe Ikooko, ewurẹ ati eso kabeeji kọja odo naa. Àgbẹ̀ náà ní ọkọ̀ ojú omi tó lè gba nǹkan kan ṣoṣo, yàtọ̀ sí àgbẹ̀ fúnra rẹ̀. Ikooko yoo je ewure, ewurẹ yoo jẹ eso kabeeji ti agbe ba fi wọn silẹ lainidi.
Ojutu ni pe ni igbese 4 agbe yoo nilo lati mu ewurẹ naa pada.
Bayi jẹ ki ká bẹrẹ lohun o programmatically.
Jẹ ki a tọka si agbe, Ikooko, ewurẹ ati eso kabeeji bi awọn oniyipada 4 ti o gba iye nikan 0 tabi 1. Zero tumọ si pe wọn wa ni banki osi, ọkan tumọ si pe wọn wa ni apa ọtun.
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ọmba jẹ nọmba awọn igbesẹ ti o nilo lati yanju. Igbesẹ kọọkan jẹ aṣoju ipo ti odo, ọkọ oju omi ati gbogbo awọn nkan.
Ni bayi, jẹ ki a yan ni laileto ati pẹlu ala kan, mu 10.
Ẹya kọọkan jẹ aṣoju ni awọn ẹda mẹwa 10 - eyi ni iye rẹ ni ọkọọkan awọn igbesẹ mẹwa 10 naa.
Bayi jẹ ki a ṣeto awọn ipo fun ibẹrẹ ati ipari.
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 ]
Lẹhinna a ṣeto awọn ipo nibiti Ikooko ti jẹ ewúrẹ, tabi ewurẹ njẹ eso kabeeji, gẹgẹbi awọn idiwọ ni idogba.
(In the presence of a farm, 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) ]
Ati nikẹhin, a yoo ṣalaye gbogbo awọn iṣe ti o ṣeeṣe ti agbẹ nigbati o ba kọja sibẹ tabi sẹhin.
O le mu Ikooko, ewurẹ tabi eso kabeeji pẹlu rẹ, tabi ko mu ẹnikẹni, tabi ko lọ si ibikibi rara.
Dajudaju, ko si ẹnikan ti o le kọja laisi agbe.
Eyi yoo ṣe afihan nipasẹ otitọ pe ipinlẹ kọọkan ti o tẹle ti odo, ọkọ oju-omi ati awọn nkan le yatọ si ti iṣaaju nikan ni ọna ti o muna.
Ko si ju 2 die-die, ati pẹlu ọpọlọpọ awọn ifilelẹ lọ, niwon agbẹ le gbe nkan kan nikan ni akoko kan ati pe kii ṣe gbogbo wọn ni a le fi silẹ papọ.
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) ]
Jẹ ki a ṣiṣẹ ojutu naa.
solve(Side + Start + Finish + Safe + Travel)
Ati pe a gba idahun!
Z3 ri kan dédé ṣeto ti ipinle ti o satisfies gbogbo awọn ipo.
Iru simẹnti onisẹpo mẹrin ti akoko aaye-aye.
Jẹ ká ro ero jade ohun to sele.
A rii pe ni ipari gbogbo eniyan kọja, nikan ni akọkọ agbẹ wa pinnu lati sinmi, ati ni awọn igbesẹ 2 akọkọ ko wẹ nibikibi.
Human_2 = 0
Human_3 = 0
Eyi ṣe imọran pe nọmba awọn ipinlẹ ti a yan pọ ju, ati pe 8 yoo to.
Ninu oro tiwa, agbe se eleyi: bere, sinmi, sinmi, rekoja ewure, rekoja pada, reko eso eso kabeeji, pada pelu ewure naa, rekoja Ikooko, pada nikan, tun gbe ewure naa pada.
Ṣugbọn ni ipari iṣoro naa ti yanju.
#Старт.
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
Bayi jẹ ki a gbiyanju lati yi awọn ipo pada ki o fihan pe ko si awọn solusan.
Lati ṣe eyi, a yoo fun wa Ikooko herbivory, ati awọn ti o yoo fẹ lati je eso kabeeji.
Eyi le ṣe afiwe si ọran ti ibi-afẹde wa ni lati ni aabo ohun elo ati pe a nilo lati rii daju pe ko si awọn loophos.
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 fun wa ni esi wọnyi:
no solution
O tumọ si pe ko si awọn ojutu gangan.
Nípa bẹ́ẹ̀, a fi ìtòlẹ́sẹẹsẹ fìdí rẹ̀ múlẹ̀ pé kò ṣeé ṣe láti kọjá lọ pẹ̀lú ìkookò omnivorous láìsí àdánù fún àgbẹ̀.
Ti awọn olugbo ba rii koko-ọrọ yii ti o nifẹ, lẹhinna ni awọn nkan iwaju Emi yoo sọ fun ọ bi o ṣe le yi eto lasan tabi iṣẹ sinu idogba ti o ni ibamu pẹlu awọn ọna iṣe, ati yanju rẹ, nitorinaa ṣafihan gbogbo awọn oju iṣẹlẹ ati awọn ailagbara mejeeji. Ni akọkọ, lori iṣẹ-ṣiṣe kanna, ṣugbọn ti a gbekalẹ ni irisi eto kan, ati lẹhinna didiẹ di idiju rẹ ati gbigbe si awọn apẹẹrẹ lọwọlọwọ lati agbaye ti idagbasoke sọfitiwia.
Nkan ti o tẹle ti ṣetan tẹlẹ:
Ninu rẹ Mo gbe lati ijẹrisi deede ti awọn iṣoro si awọn eto, ati ṣapejuwe
bawo ni wọn ṣe le yipada si awọn eto ofin deede laifọwọyi.
orisun: www.habr.com