Bi dîtina min, di sektora înternetê ya bi zimanê rûsî de, mijara verastkirina fermî bi têra xwe nayê vegirtin, û bi taybetî jî kêmbûna mînakên sade û zelal heye.
Ez ê ji çavkaniyeke biyanî mînakekê bidim û çareseriya xwe jî li ser pirsgirêka naskirî ya derbasbûna gur, bizin û kelemekê li aliyê din ê çem zêde bikim.
Lê pêşî, ez ê bi kurtasî diyar bikim ka verastkirina fermî çi ye û çima hewce ye.
Verastkirina fermî bi gelemperî tê wateya kontrolkirina bernameyek an algorîtmayek bi karanîna yekî din.
Ev pêdivî ye ku pê ewle bibe ku bername wekî ku tê hêvî kirin tevdigere û di heman demê de ewlehiya wê jî misoger dike.
Verastkirina fermî amûra herî bi hêz e ji bo dîtin û rakirina qelsiyan: ew dihêle hûn hemî qul û xeletiyên heyî di bernameyekê de bibînin, an jî îspat bikin ku ew tune ne.
Hêjayî gotinê ye ku di hin rewşan de ev ne mumkin e, wek mînak di pirsgirêka 8 şahbanûyan de bi firehiya panelê 1000 çargoşe: ew hemî digihîje tevliheviya algorîtmîkî an pirsgirêka rawestandinê.
Lêbelê, di her rewşê de, yek ji sê bersivan dê were wergirtin: bername rast e, xelet e, an jî ne gengaz bû ku bersiv were hesibandin.
Ger ne gengaz be ku bersivek were dîtin, pir caran gengaz e ku meriv beşên nezelal ên bernameyê ji nû ve bixebite, tevliheviya wan a algorîtmîkî kêm bike, da ku bersivek erê an na ya taybetî werbigire.
Û verastkirina fermî, mînakî, di pergalên xebitandinê yên Windows kernel û drone Darpa de tê bikar anîn, da ku asta herî zêde parastinê peyda bike.
Em ê Z3Prover, amûrek pir bi hêz ji bo îsbatkirina teorema otomatîk û çareserkirina hevkêşeyan bikar bînin.
Digel vê yekê, Z3 hevkêşeyan çareser dike, û bi karanîna hêza hov nirxên wan hilnabijêre.
Ev tê vê wateyê ku ew dikare bersivê bibîne, tewra di rewşên ku 10^100 vebijarkên têketinê hene.
Lê ev tenê bi dehan argumanên têketinê yên tîpa Integer e, û ev pir caran di pratîkê de tê dîtin.
Pirsgirêka 8 şahbanûyan (Ji Îngilîzî hatiye girtin ).
# 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)
Z3 dimeşînin, em çareseriyê digirin:
[Q_5 = 1,
Q_8 = 7,
Q_3 = 8,
Q_2 = 2,
Q_6 = 3,
Q_4 = 6,
Q_7 = 5,
Q_1 = 4]
Pirsgirêka şahbanûyê bi bernameyekê re hevaheng e ku kordînatên 8 şahbanûyan wekî têketinê digire û bersivê dide ka şahbanûyan hevdu lêdixin.
Ger em bernameyek weha bi karanîna verastkirina fermî çareser bikin, wê hingê li gorî pirsgirêkê, em ê tenê gavek din bavêjin di forma veguheztina koda bernameyê nav hevokek de: ew ê di bingeh de bi ya me re bibe yek ( bê guman, heke bername rast hatibe nivîsandin).
Hema hema heman tişt dê di doza lêgerîna qelsiyan de jî çêbibe: em tenê şertên derketinê yên ku ji me re hewce ne destnîşan dikin, mînakî şîfreya rêveberiyê, çavkanî an koda veqetandî veguherînin hevkêşeyên ku bi verastkirinê re hevaheng in, û dûv re bersivek werdigirin ka çi pêdivî ye ku data wekî têketinê were peyda kirin da ku bigihîje armancê.
Bi dîtina min, pirsgirêka gur, bizin û kelemê hê balkêştir e, ji ber ku ji bo çareserkirina wê gelek (7) gavan lazim in.
Ger pirsgirêka şahbanûyê bi doza ku hûn dikarin bi karanîna yek daxwazek GET an POST têkevin serverek hevber e, wê hingê gur, bizin û kelem mînakek ji kategoriyek pir tevlihev û berbelavtir nîşan dide, ku tê de armanc tenê dikare were bidestxistin. bi çend daxwazan.
Mînakî, ev bi senaryoyek ku hûn hewce ne ku derziyek SQL bibînin, pelek bi navgîniya wê ve binivîsin, dûv re mafên xwe bilind bikin û tenê dûv re şîfreyek bistînin re hevaheng e.
Şert û mercên pirsgirêkê û çareseriya wêCotkar divê gur, bizin û kelem li ser çem biguhezîne. Cotkar qeyikek heye ku ji bilî cotkar bi xwe, tenê yek tişt tê de heye. Ger cotkar ji wan bêpar bihêle dê gur bizin û bizin jî kelemê bixwe.
Çareserî ew e ku di gava 4an de cotkar dê bizinê paşde vegerîne.
Naha em dest bi çareserkirina wê bi bernameyî bikin.
Ka em cotkar, gur, bizin û kelem wek 4 guherbaran destnîşan bikin ku nirxê wan tenê 0 an 1 digirin. Sifir tê wateya ku ew li rexê çepê ne, û yek tê wateya ku ew li milê rastê ne.
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 hejmara gavên ku ji bo çareseriyê hewce ne. Her gav rewşa çem, qeyikê û hemû pêkhateyan temsîl dike.
Heya nuha, em wê bi rengek rasthatî û bi marjînal hilbijêrin, 10 bigirin.
Her sazî di 10 kopiyan de tê temsîl kirin - ev nirxa wê di her 10 gavan de ye.
Niha em şert û mercên destpêk û qedandinê diyar bikin.
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 ]
Dûv re em şert û mercên ku gur bizinê dixwe, an bizin kelemê dixwe, di hevkêşeyê de wekî astengî destnîşan dikin.
(Di hebûna cotkar de, êrîşkarî ne mimkûn e)
# 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) ]
Û di dawiyê de, em ê hemî kiryarên gengaz ên cotkar dema ku ji wir derbas dibin an vedigerin diyar bikin.
Ew dikare bi xwe re gur, bizinek an kelemek bigire, an jî kesî negire, an jî bi gemiyê ve neçe ti deverekê.
Helbet bêyî cotkar kes nikare derbas bibe.
Ev ê ji hêla vê rastiyê ve were diyar kirin ku her dewleta paşê ya çem, qeyik û saziyan tenê bi rengek hişk bi sînor dikare ji ya berê cûda bibe.
Ji 2 bit zêdetir nîne, û bi gelek sînorên din re, ji ber ku cotkar tenê dikare yek carek saziyek veguhezîne û nekare hemî bi hev re werin hiştin.
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) ]
Werin em çareseriyê bimeşînin.
solve(Side + Start + Finish + Safe + Travel)
Û em bersivê bistînin!
Z3 komek domdar a dewletan dît ku hemî şertan têr dike.
Cûreyek çar-alî ya feza-demê.
Ka em fêhm bikin ka çi bûye.
Em dibînin ku di dawiyê de her kes derbas bû, tenê di destpêkê de cotkarê me biryar da ku bêhna xwe bide, û di 2 gavên pêşîn de ew li her derê avjeniyê nake.
Human_2 = 0
Human_3 = 0
Ev destnîşan dike ku hejmara dewletên ku me hilbijartiye zêde ye, û 8 dê têr be.
Li cem me cotkar wiha kir: dest pê kir, bêhnvedan, bêhnvedan, bizinê derbas kirin, bizinê derbas bikin, bi kelemê re derbas bibin, bi bizinê re vegere, gur derbas bike, bi tenê vegere, bizinê ji nû ve teslîm bike.
Lê di dawiyê de pirsgirêk çareser bû.
#Старт.
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
Niha em hewl bidin ku şert û mercan biguherînin û îspat bikin ku çareserî tune.
Ji bo vê yekê, em ê gîhayê gurê xwe bidin, û ew ê bixwaze kelemê bixwe.
Ev dikare bi doza ku tê de mebesta me ewlekirina serîlêdanê ye re were berhev kirin û pêdivî ye ku em pê ewle bin ku valahiyek tune.
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 bersiva jêrîn da me:
no solution
Ev tê wê wateyê ku bi rastî tu çareserî tune.
Bi vî rengî, me bi bernameyekî nepêkanîna derbasbûna bi gurê omnivor bêyî windahiyan ji cotkar re îspat kir.
Ger temaşevan vê mijarê balkêş bibîne, wê hingê di gotarên pêşerojê de ez ê ji we re vebêjim ka meriv çawa bernameyek an fonksiyonek asayî vediguhezîne hevokek ku bi rêbazên fermî re têkildar e, û wê çareser bike, bi vî rengî hem hemî senaryoyên rewa û lawaziyê eşkere bike. Pêşî, li ser heman peywirê, lê di forma bernameyê de tê pêşkêş kirin, û dûv re hêdî hêdî wê tevlihev dike û berbi mînakên heyî yên ji cîhana pêşkeftina nermalavê ve diçe.
Gotara din jixwe amade ye:
Di wê de ez ji verastkirina fermî ya pirsgirêkan berbi bernameyan ve diçim, û diyar dikim
ew çawa dikarin bixweber veguhezînin pergalên serweriya fermî.
Source: www.habr.com