Ka maikutlo a ka, lefapheng la puo ea Serussia ea Inthanete, taba ea ho netefatsa ka molao ha e e-s'o koaheloe ka ho lekaneng, 'me ho na le ho haella ka ho khetheha ha mehlala e bonolo le e hlakileng.
Ke tla fana ka mohlala ho tsoa mohloling osele, ’me ke kenye tharollo ea ka bothateng bo tsebahalang ba ho tšela phiri, poli le khabeche ka mose ho noka.
Empa pele, ke tla hlalosa ka bokhutšoanyane hore na netefatso ea semmuso ke efe le hore na ke hobane'ng ha e hlokahala.
Netefatso ea semmuso hangata e bolela ho hlahloba lenaneo le leng kapa algorithm u sebelisa e 'ngoe.
Sena sea hlokahala ho netefatsa hore lenaneo le sebetsa ka mokhoa o lebelletsoeng le ho netefatsa ts'ireletso ea lona.
Netefatso ea semmuso ke mokhoa o matla ka ho fetesisa oa ho fumana le ho felisa bofokoli: e o lumella ho fumana masoba le litšitšili tse teng lenaneong, kapa ho paka hore ha li eo.
Ke habohlokoa ho hlokomela hore maemong a mang sena ha se khonehe, joalo ka bothateng ba mafumahali a 8 a nang le bophara ba boto ea lisekoere tse 1000: tsohle li theohela ho rarahano ea algorithm kapa bothata ba ho emisa.
Leha ho le joalo, ho sa tsotellehe boemo leha e le bofe, e 'ngoe ea likarabo tse tharo e tla amoheloa: lenaneo le nepahetse, le fosahetse, kapa ho ne ho sa khonehe ho bala karabo.
Haeba ho ke ke ha khoneha ho fumana karabo, hangata hoa khoneha ho tsosolosa likarolo tse sa hlakang tsa lenaneo, ho fokotsa ho rarahana ha tsona ka mokhoa oa algorithm, e le hore u fumane karabo e tobileng ea e kapa che.
'Me ho sebelisoa ho netefatsa ka molao, ka mohlala, tsamaisong ea Windows kernel le ea Darpa drone, ho netefatsa boemo bo phahameng ba tšireletso.
Re tla sebelisa Z3Prover, sesebelisoa se matla haholo bakeng sa ho paka ka boiketsetso le ho rarolla equation.
Ho feta moo, Z3 e rarolla li-equations, 'me ha e khethe boleng ba eona e sebelisa matla a sehlōhō.
Sena se bolela hore e khona ho fumana karabo, esita le maemong ao ho nang le 10^100 motsoako oa likhetho tsa ho kenya.
Empa sena ke likhang tse ka bang leshome le metso e 'meli feela tsa tlhahiso ea mofuta oa Integer, 'me hangata sena se kopana le ts'ebetso.
Bothata ka mafumahali a 8 (E nkuoe ho Senyesemane ).
# 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)
Ho matha Z3, re fumana tharollo:
[Q_5 = 1,
Q_8 = 7,
Q_3 = 8,
Q_2 = 2,
Q_6 = 3,
Q_4 = 6,
Q_7 = 5,
Q_1 = 4]
Bothata ba mofumahali bo ka bapisoa le lenaneo le nkang likhokahanyo tsa mafumahali a 8 e le ho fana ka karabo hore na mafumahali a otlana.
Haeba re ne re ka rarolla lenaneo le joalo re sebelisa netefatso e hlophisitsoeng, ebe ha e bapisoa le bothata, re tla hloka feela ho nka mohato o mong hape ka mokhoa oa ho fetolela khoutu ea lenaneo hore e be equation: e ne e tla tšoana hantle le ea rona ( ha e le hantle, haeba lenaneo le ngotsoe ka nepo).
Hoo e batlang e le ntho e tšoanang e tla etsahala tabeng ea ho batla bofokoli: re mpa re beha maemo ao re a hlokang, mohlala, password ea admin, fetola mohloli kapa khoutu e senyehileng hore e be li-equations tse lumellanang le netefatso, ebe re fumana karabo ea hore na data e hloka ho fanoa e le ho kenya letsoho ho fihlela sepheo.
Ka maikutlo a ka, bothata ba phiri, pōli le k'habeche bo thahasellisa le ho feta, kaha ho bo rarolla ho se ho hloka mehato e mengata (7).
Haeba bothata ba mofumahali bo bapisoa le nyeoe eo u ka kenang ho eona ka har'a seva u sebelisa kopo e le 'ngoe ea GET kapa POST, joale phiri, pōli le k'habeche li bontša mohlala ho tsoa sehlopheng se rarahaneng haholo le se atileng, moo sepheo se ka finyelloang feela. ka likopo tse 'maloa.
Sena se ka bapisoa, ka mohlala, le boemo boo u hlokang ho fumana ente ea SQL, ngola faele ka eona, ebe u phahamisa litokelo tsa hau ebe u fumana password.
Maemo a bothata le tharollo ea bonaSehoai se hloka ho tsamaisa phiri, poli le k'habeche ho tšela noka. Sehoai se na le seketsoana se khonang ho nka ntho e le 'ngoe feela, ntle le molemi ka boeena. Phiri e tla ja pōli ’me pōli e tla ja k’habeche haeba sehoai se li siea li sa li lebela.
Tharollo ke hore mohatong oa 4 sehoai se tla hloka ho khutlisa poli.
Joale a re qaleng ho e rarolla ka lenaneo.
Ha re bolele sehoai, phiri, poli le khabeche e le mefuta e 4 e nkang boleng feela 0 kapa 1. Zero e bolela hore li ka lehlakoreng le letšehali, 'me e' ngoe e bolela hore e ka ho le letona.
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 ke palo ea mehato e hlokahalang ho rarolloa. Mohato o mong le o mong o emela boemo ba noka, sekepe le mekhatlo eohle.
Hajoale, a re e khetheng ka tšohanyetso, 'me ka moeli, nka 10.
Setsi se seng le se seng se emetsoe ka likopi tse 10 - bona ke boleng ba eona mohatong o mong le o mong oa mehato e 10.
Joale ha re beheng maemo a ho qala le ho qetela.
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 ]
Ebe re beha maemo moo phiri e jang pōli, kapa pōli e ja k'habeche, e le lithibelo ho equation.
(Ka pel'a sehoai, ho ba mabifi ha ho khonehe)
# 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) ]
'Me qetellong, re tla hlalosa liketso tsohle tse ka khonehang tsa sehoai ha li tšela moo kapa morao.
A ka nka phiri, poli kapa k'habeche le eena, kapa a se ke a nka mang kapa mang, kapa a se ke a tsamaea ka sekepe ho hang.
Ke ’nete hore ha ho motho ea ka tšelang ntle le sehoai.
Sena se tla bontšoa ke taba ea hore boemo bo bong le bo bong bo latelang ba nōka, sekepe le mekhatlo e ka fapana le e fetileng feela ka tsela e fokolang haholo.
Ha ho li-bits tse fetang 2, 'me ka meeli e meng e mengata, kaha sehoai se ka tsamaisa mokhatlo o le mong ka nako' me ha se bohle ba ka siuoang hammoho.
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) ]
Ha re sebetseng tharollo.
solve(Side + Start + Finish + Safe + Travel)
Mme re fumana karabo!
Z3 e fumane sehlopha se tsitsitseng sa linaha tse khotsofatsang maemo ohle.
Mofuta oa nako ea sebaka-nne-dimensional.
A re bone hore na ho ile ha etsahala’ng.
Rea bona hore qetellong bohle ba ile ba tšela, feela qalong sehoai sa rona se ile sa etsa qeto ea ho phomola, 'me mehatong ea pele ea 2 ha a sese kae kapa kae.
Human_2 = 0
Human_3 = 0
Sena se fana ka maikutlo a hore palo ea linaha tseo re li khethileng li fetelletse, 'me tse 8 li tla lekana.
Tabeng ea rona, sehoai se ile sa etsa sena: qala, phomola, phomola, tšela poli, tšela morao, tšela k'habeche, khutla le pōli, tšela phiri, khutlela morao u le mong, khutlisetsa pōli.
Empa qetellong bothata bo ile ba rarolloa.
#Старт.
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
Joale a re lekeng ho fetola maemo le ho paka hore ha ho na tharollo.
Ho etsa sena, re tla fa wolf herbivory ea rona, 'me o tla batla ho ja k'habeche.
Sena se ka bapisoa le taba eo ho eona sepheo sa rona e leng ho tiisa kopo mme re hloka ho etsa bonnete ba hore ha ho na masoba.
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 e re file karabo e latelang:
no solution
Ho bolela hore ha e le hantle ha ho na tharollo.
Kahoo, re ile ra paka ka lenaneo hore ha ho khonehe ho tšela le phiri ea omnivorous ntle le tahlehelo bakeng sa sehoai.
Haeba bamameli ba fumana sehlooho sena se thahasellisa, joale lihloohong tse tlang ke tla u bolella mokhoa oa ho fetola lenaneo le tloaelehileng kapa ts'ebetso hore e be equation e lumellanang le mekhoa e hlophisitsoeng, 'me u e rarolle, ka ho etsa joalo u senole maemo ohle a nepahetseng le bofokoli. Ntlha ea pele, ka mosebetsi o le mong, empa o hlahisoa ka mokhoa oa lenaneo, ebe butle-butle o o thatafatsa le ho fetela mehlala ea morao-rao e tsoang lefats'eng la nts'etsopele ea software.
Sengoliloeng se latelang se se se lokile:
Ho eona ke tloha ho netefatso ea molao ea mathata ho ea ho mananeo, le ho hlalosa
li ka fetoloa joang hore e be litsamaiso tsa molao tse hlophisitsoeng ka bo eona.
Source: www.habr.com