Nam bheachd-sa, ann an roinn cànan na Ruis den eadar-lìn, chan eil cuspair dearbhadh foirmeil air a chòmhdach gu leòr, agus gu sònraichte tha dìth eisimpleirean sìmplidh agus soilleir.
Bheir mi eisimpleir bho thùs cèin, agus cuiridh mi mo fhuasgladh fhìn ris an duilgheadas ainmeil a thaobh a bhith a 'dol thairis air madadh-allaidh, gobhar agus càl gu taobh eile na h-aibhne.
Ach an toiseach, bheir mi cunntas goirid air dè a th’ ann an dearbhadh foirmeil agus carson a tha feum air.
Mar as trice bidh dearbhadh foirmeil a’ ciallachadh sgrùdadh a dhèanamh air aon phrògram no algairim a’ cleachdadh fear eile.
Tha seo riatanach gus dèanamh cinnteach gun giùlain am prògram mar a bhiodh dùil agus cuideachd gus dèanamh cinnteach à tèarainteachd.
Is e dearbhadh foirmeil an dòigh as cumhachdaiche air so-leòntachd a lorg agus a chuir às: leigidh e leat na tuill agus na mialan a th’ ann mar-thà a lorg ann am prògram, no dearbhadh nach eil iad ann.
Is fhiach a bhith mothachail gu bheil seo do-dhèanta ann an cuid de chùisean, leithid ann an duilgheadas 8 banrighrean le leud bùird de 1000 ceàrnag: tha e uile an urra ri iom-fhillteachd algorithmach no an duilgheadas stad.
Ach, ann an suidheachadh sam bith, gheibhear aon de thrì freagairtean: tha am prògram ceart, ceàrr, no cha robh e comasach am freagairt obrachadh a-mach.
Ma tha e do-dhèanta freagairt a lorg, gu tric bidh e comasach pàirtean neo-shoilleir den phrògram ath-obrachadh, a ’lughdachadh an iom-fhillteachd algorithmach, gus freagairt sònraichte tha no chan eil fhaighinn.
Agus tha dearbhadh foirmeil air a chleachdadh, mar eisimpleir, ann an siostaman obrachaidh drone kernel Windows agus Darpa, gus dèanamh cinnteach gu bheil an ìre dìon as àirde.
Cleachdaidh sinn Z3Prover, inneal fìor chumhachdach airson dearbhadh teòirim fèin-ghluasadach agus fuasgladh co-aontar.
A bharrachd air an sin, bidh Z3 a 'fuasgladh co-aontaran, agus chan eil e a' taghadh an luachan le bhith a 'cleachdadh feachd brùideil.
Tha seo a’ ciallachadh gu bheil e comasach dha am freagairt a lorg, eadhon ann an cùisean far a bheil cothlamadh 10^100 de roghainnean cuir a-steach.
Ach chan eil seo ach mu dhusan argamaid a-steach den t-seòrsa Integer, agus gu tric bidh seo a’ tachairt ann an cleachdadh.
Duilgheadas mu 8 banrighrean (Air a thoirt bhon Bheurla ).
# 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)
A’ ruith Z3, gheibh sinn am fuasgladh:
[Q_5 = 1,
Q_8 = 7,
Q_3 = 8,
Q_2 = 2,
Q_6 = 3,
Q_4 = 6,
Q_7 = 5,
Q_1 = 4]
Tha duilgheadas na banrigh an coimeas ri prògram a bheir a-steach co-chomharran 8 banrighrean agus a bheir a-mach am freagairt an do rinn na banrighrean a’ chùis air a chèile.
Nam biodh sinn gu bhith a’ fuasgladh prògram mar seo a’ cleachdadh dearbhadh foirmeil, an uairsin an taca ris an duilgheadas, cha bhiodh againn ach aon cheum eile a ghabhail ann an cruth còd a’ phrògraim a thionndadh gu co-aontar: bhiodh e gu ìre mhòr co-ionann ris an fheadhainn againne ( gu dearbh, ma chaidh am prògram a sgrìobhadh ceart).
Bidh cha mhòr an aon rud a’ tachairt a thaobh a bhith a’ lorg so-leòntachd: tha sinn dìreach a’ suidheachadh nan suidheachaidhean toraidh a dh’ fheumas sinn, mar eisimpleir, am facal-faire rianachd, atharraich an stòr no an còd dì-chompanaidh gu co-aontaran a tha co-chosmhail ri dearbhadh, agus an uairsin faigh sinn freagairt a thaobh dè feumar dàta a thoirt seachad mar chur-a-steach gus an amas a choileanadh.
Na mo bheachd-sa, tha an duilgheadas mun mhadadh-allaidh, a 'ghobhar agus an càl eadhon nas inntinniche, oir tha feum air mòran cheumannan (7) airson fuasgladh fhaighinn air mar-thà.
Ma tha duilgheadas na banrigh an coimeas ris a 'chùis far an urrainn dhut a dhol a-steach do fhrithealaiche le aon iarrtas GET no POST, tha am madadh-allaidh, gobhar agus càl a' nochdadh eisimpleir bho roinn a tha mòran nas iom-fhillte agus nas fharsainge, anns nach urrainnear an amas a choileanadh a-mhàin le grunn iarrtasan.
Tha seo coimeasach, mar eisimpleir, ri suidheachadh far am feum thu in-stealladh SQL a lorg, faidhle a sgrìobhadh troimhe, an uairsin àrdaich do chòraichean agus dìreach an uairsin faigh facal-faire.
Suidheachadh na trioblaid agus a fuasgladhFeumaidh an tuathanach madadh-allaidh, gobhar agus càl a ghiùlan tarsainn na h-aibhne. Tha bàta aig an tuathanach nach gabh ach aon nì, a bharrachd air an tuathanach fhèin. Ithidh am madadh-allaidh am gobhar agus ithidh am gobhar an càl ma dh'fhàgas an tuathanach iad gun duine.
Is e am fuasgladh ann an ceum 4 gum feum an tuathanach am gobhar a thoirt air ais.
A-nis tòisichidh sinn ga fhuasgladh gu prògramach.
Leig leinn an tuathanach, madadh-allaidh, gobhar agus càl a chomharrachadh mar 4 caochladairean a bheir an luach a-mhàin 0 no 1. Tha Zero a 'ciallachadh gu bheil iad air a' bhruaich chlì, agus tha aon a 'ciallachadh gu bheil iad air an làimh dheis.
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
Is e àireamh an àireamh de cheumannan a tha riatanach airson fuasgladh. Tha gach ceum a’ riochdachadh staid na h-aibhne, a’ bhàta agus gach buidheann.
Airson a-nis, tagh sinn e air thuaiream agus le iomall, gabh 10.
Tha gach eintiteas air a riochdachadh ann an 10 leth-bhreacan - is e seo a luach aig gach aon de na 10 ceumannan.
A-nis leig dhuinn na suidheachaidhean a shuidheachadh airson toiseach is deireadh.
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 ]
An uairsin bidh sinn a 'suidheachadh nan suidheachaidhean far am bi am madadh-allaidh ag ithe a' ghobhar, no a 'ghobhar ag ithe càl, mar chuingealachaidhean anns a' cho-aontar.
(An làthair tuathanach, tha e do-dhèanta ionnsaigheachd)
# 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) ]
Agus mu dheireadh, mìnichidh sinn a h-uile gnìomh a dh’ fhaodadh a bhith aig an tuathanach nuair a thèid sinn thairis air no air ais.
Faodaidh e madadh-allaidh, gobhar no càl a thoirt leis, no duine sam bith a thoirt leis, no seòladh a dhèanamh idir.
Gu dearbh, chan urrainn dha duine a dhol tarsainn às aonais tuathanach.
Bidh seo air a chuir an cèill leis gum faod gach stàit eile den abhainn, bàta agus eintiteas a bhith eadar-dhealaichte bhon fhear roimhe a-mhàin ann an dòigh cuibhrichte.
Gun a bhith nas fhaide na 2 phìos, agus le mòran chrìochan eile, leis nach urrainn don tuathanach ach aon eintiteas a ghiùlan aig an aon àm agus chan urrainnear a h-uile càil fhàgail còmhla.
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) ]
Leig leinn am fuasgladh a ruith.
solve(Side + Start + Finish + Safe + Travel)
Agus gheibh sinn am freagairt!
Lorg Z3 seata cunbhalach de stàitean a tha a’ sàsachadh a h-uile suidheachadh.
Seòrsa de sgioba ceithir-thaobhach de ùine-fànais.
Leig dhuinn a-mach dè thachair.
Tha sinn a 'faicinn sin aig a' cheann thall chaidh a h-uile duine thairis, dìreach an toiseach cho-dhùin an tuathanach againn fois a ghabhail, agus anns a 'chiad 2 cheum chan eil e a' snàmh an àite sam bith.
Human_2 = 0
Human_3 = 0
Tha seo a’ nochdadh gu bheil an àireamh de stàitean a thagh sinn cus, agus bidh 8 gu leòr.
Anns a 'chùis againn, rinn an tuathanach seo: tòisich, fois, gabh fois, cuir tarsainn air a' ghobhar, crois air ais, cuir tarsainn air a 'chàl, till leis a' ghobhar, cuir tarsainn air a 'mhadadh-allaidh, till air ais leis fhèin, ath-lìbhrigeas a' ghobhar.
Ach mu dheireadh chaidh an duilgheadas fhuasgladh.
#Старт.
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
A-nis feuchaidh sinn ris na suidheachaidhean atharrachadh agus dearbhadh nach eil fuasglaidhean ann.
Gus seo a dhèanamh, bheir sinn ar madadh-allaidh luibheach, agus bidh e ag iarraidh càl ithe.
Faodar seo a choimeas ris a’ chùis far a bheil ar n-amas an tagradh a dhèanamh tèarainte agus feumaidh sinn dèanamh cinnteach nach eil beàrnan ann.
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) ]
Thug Z3 am freagairt a leanas dhuinn:
no solution
Tha e a’ ciallachadh nach eil fuasglaidhean ann dha-rìribh.
Mar sin, dhearbh sinn gu prògramach nach robh e comasach a dhol tarsainn le madadh-allaidh omnivorous gun chall don tuathanach.
Ma tha an cuspair seo inntinneach don luchd-èisteachd, an uairsin ann an artaigilean san àm ri teachd innsidh mi dhut mar a thionndaidheas tu prògram àbhaisteach no gnìomh gu co-aontar a tha co-chosmhail ri modhan foirmeil, agus fuasgladh fhaighinn air, agus mar sin a’ nochdadh gach cuid suidheachadh dligheach agus so-leòntachd. An toiseach, air an aon ghnìomh, ach air a thaisbeanadh ann an cruth prògram, agus an uairsin mean air mhean ga dhèanamh duilich agus a 'gluasad air adhart gu eisimpleirean gnàthach bho shaoghal leasachadh bathar-bog.
Tha an ath artaigil deiseil mu thràth:
An sin bidh mi a’ gluasad bho dhearbhadh foirmeil air duilgheadasan gu prògraman, agus a’ toirt cunntas air
ciamar a ghabhas an tionndadh gu siostaman riaghlaidh foirmeil gu fèin-ghluasadach.
Source: www.habr.com