A ra'ayi na, a cikin harshen Rashanci na Intanet, batun tabbatarwa na yau da kullun ba a cika shi sosai ba, kuma musamman ma rashin misalai masu sauƙi da bayyanannu.
Zan ba da misali daga wata majiyar waje, in ƙara da kaina maganin matsalar tsallakawa da kerkeci da akuya da kabeji zuwa wancan gefen kogi.
Amma da farko, zan ɗan bayyana mene ne tabbaci na hukuma da kuma dalilin da ya sa ake buƙata.
Tabbatarwa na yau da kullun yana nufin duba wani shiri ko algorithm ta amfani da wani.
Wannan ya zama dole don tabbatar da cewa shirin ya kasance kamar yadda ake tsammani da kuma tabbatar da tsaro.
Tabbatarwa ta hukuma ita ce hanya mafi ƙarfi ta ganowa da kawar da lahani: yana ba ku damar nemo duk ramuka da kwari a cikin shirin, ko tabbatar da cewa babu su.
Ya kamata a lura da cewa a wasu lokuta wannan ba zai yiwu ba, kamar a cikin matsala na 8 sarauniya tare da girman allo na murabba'in 1000: duk ya zo ne zuwa algorithmic complexity ko matsalar tsayawa.
Koyaya, a kowane hali, ɗaya daga cikin amsoshi uku za a karɓi: shirin daidai ne, ba daidai ba, ko kuma ba a iya ƙididdige amsar ba.
Idan ba zai yiwu a sami amsa ba, sau da yawa yana yiwuwa a sake yin wasu ɓangarori na shirin, rage rikitarwar algorithmic, don samun takamaiman eh ko a'a.
Kuma ana amfani da tabbaci na yau da kullun, alal misali, a cikin Windows kernel da Darpa drone tsarin aiki, don tabbatar da matsakaicin matakin kariya.
Za mu yi amfani da Z3Prover, kayan aiki mai ƙarfi don tabbatar da ka'idar sarrafa kansa da warware daidaito.
Haka kuma, Z3 yana warware ma'auni, kuma baya zaɓar ƙimar su ta amfani da ƙarfi.
Wannan yana nufin cewa yana iya samun amsar, ko da a lokuta inda akwai 10^100 haɗuwa na zaɓin shigarwa.
Amma wannan kusan muhawarar shigarwar dozin goma ce ta nau'in Integer, kuma galibi ana fuskantar wannan a aikace.
Matsala game da sarauniya 8 (An ɗauko daga Turanci ).
# 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)
Gudun Z3, muna samun mafita:
[Q_5 = 1,
Q_8 = 7,
Q_3 = 8,
Q_2 = 2,
Q_6 = 3,
Q_4 = 6,
Q_7 = 5,
Q_1 = 4]
Matsalar sarauniya tana kwatankwacin shirin da ke daukar matakan shigar da sarakuna 8 tare da fitar da amsar ko sarauniyar sun doke juna.
Idan za mu warware irin wannan shirin ta amfani da tabbaci na yau da kullun, to, idan aka kwatanta da matsalar, za mu buƙaci ƙarin mataki ɗaya ta hanyar canza lambar shirin zuwa ma'auni: zai zama ainihin kama da namu. Tabbas, idan an rubuta shirin daidai).
Kusan abu ɗaya zai faru a yanayin neman raunin: kawai muna saita yanayin fitarwa da muke buƙata, alal misali, kalmar sirri ta admin, canza tushen ko lambar da aka lalata zuwa ma'auni masu dacewa da tabbatarwa, sannan mu sami amsar menene. ana buƙatar samar da bayanai azaman shigarwa don cimma burin.
A ganina, matsala game da kerkeci, goat da kabeji ya fi ban sha'awa, tun da yake warware shi ya riga ya buƙaci matakai (7).
Idan matsalar Sarauniya ta yi daidai da yanayin da za ku iya shiga uwar garken ta amfani da buƙatun GET ko POST guda ɗaya, to, kerkeci, akuya da kabeji suna nuna misali daga nau'in da ya fi rikitarwa da yaɗuwa, wanda za a iya cimma burin kawai. ta buƙatun da yawa.
Wannan yana kama da misali, zuwa yanayin da kake buƙatar nemo allurar SQL, rubuta fayil ta ciki, sannan ɗaukaka haƙƙoƙinka sannan kawai sami kalmar sirri.
Yanayin matsalar da maganintaManomin na bukatar ya yi safarar kerkeci, akuya da kabeji ya haye kogin. Manomin yana da kwale-kwalen da zai iya daukar abu daya kawai, ban da shi kansa manomi. Kerkeci zai cinye akuya, akuya kuma za ta cinye kabeji idan manomi ya bar su ba tare da kula da su ba.
Mafita ita ce a mataki na 4 manomi zai bukaci ya mayar da akuya.
Yanzu bari mu fara warware shi ta hanyar shirye-shirye.
Bari mu nuna manomi, kerkeci, akuya da kabeji a matsayin masu canji guda 4 waɗanda suke ɗaukar ƙimar 0 ko 1 kawai. Sifili yana nufin suna gefen hagu, ɗayan yana nufin suna hannun dama.
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
Lambobi shine adadin matakan da ake buƙata don warwarewa. Kowane mataki yana wakiltar yanayin kogin, jirgin ruwa da dukkan abubuwa.
A yanzu, bari mu zaɓi shi bazuwar kuma tare da gefe, ɗauki 10.
Kowane mahalli yana wakilta a cikin kwafi 10 - wannan shine ƙimarsa a kowane matakai 10.
Yanzu bari mu saita yanayin farawa da gamawa.
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 ]
Sa'an nan kuma mu tsara yanayin da kerkeci ke cin akuya, ko akuya ya ci kabeji, a matsayin ƙuntatawa a cikin ƙididdiga.
(A gaban manomi, zalunci ba zai yiwu ba)
# 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) ]
Kuma a ƙarshe, za mu ayyana duk ayyukan da manomi zai yi yayin tsallakawa can ko baya.
Zai iya ɗaukar kerkeci, ko akuya ko kabeji tare da shi, ko kuma ba zai ɗauki kowa ba, ko kuma ba zai yi tafiya a ko'ina ba.
Tabbas, babu wanda zai iya wucewa ba tare da manomi ba.
Za a bayyana hakan ta yadda kowane yanayi na kogi, jirgin ruwa da mahalli na gaba zai iya bambanta da wanda ya gabata kawai ta hanya mai iyaka.
Ba fiye da 2 ragi ba, kuma tare da wasu iyakoki masu yawa, tun da manomi zai iya jigilar kaya ɗaya kawai a lokaci guda kuma ba duka za a iya barin tare ba.
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) ]
Mu gudanar da maganin.
solve(Side + Start + Finish + Safe + Travel)
Kuma mun sami amsar!
Z3 ya sami daidaitattun saitin jahohi waɗanda suka gamsar da kowane yanayi.
Wani nau'in simintin gyare-gyare mai girma huɗu na lokacin sarari.
Bari mu gano abin da ya faru.
Mun ga cewa a ƙarshe kowa ya ketare, kawai da farko manominmu ya yanke shawarar hutawa, kuma a cikin matakai 2 na farko ba ya iyo a ko'ina.
Human_2 = 0
Human_3 = 0
Wannan yana nuna cewa adadin jihohin da muka zaɓa ya wuce kima, kuma 8 za su isa sosai.
A wajenmu, manomi ya yi haka: ya fara, ya huta, ya huta, ya haye akuya, ya tsallaka baya, ya haye kabeji, ya dawo da akuya, ya tsallaka kerkeci, ya dawo shi kadai, ya sake kai akuya.
Amma a karshe an magance matsalar.
#Старт.
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
Yanzu bari mu yi ƙoƙari mu canza yanayin kuma mu tabbatar da cewa babu mafita.
Don yin wannan, za mu ba mu wolf herbivory, kuma zai so ya ci kabeji.
Ana iya kwatanta wannan da yanayin da burinmu shine tabbatar da aikace-aikacen kuma muna buƙatar tabbatar da cewa babu madauki.
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 ya ba mu amsa kamar haka:
no solution
Yana nufin cewa da gaske babu mafita.
Don haka, a cikin tsari mun tabbatar da rashin yiwuwar hayewa da kerkeci ba tare da asara ga manomi ba.
Idan masu sauraro suka sami wannan batu mai ban sha'awa, to a cikin kasidu na gaba zan gaya muku yadda ake juya shirin ko aiki na yau da kullun zuwa ma'auni mai dacewa da hanyoyin yau da kullun, kuma a warware shi, ta yadda za a bayyana duka halaltattun yanayi da lahani. Na farko, akan wannan aiki, amma an gabatar da shi ta hanyar tsari, sannan a hankali ya takura shi da ci gaba zuwa ga misalai na yanzu daga duniyar ci gaban software.
An riga an shirya labari na gaba:
A ciki na matsa daga tabbatar da matsaloli na yau da kullun zuwa shirye-shirye, in bayyana
ta yaya za a iya canza su zuwa tsarin mulki na yau da kullun ta atomatik.
source: www.habr.com