Kutsimikizira kovomerezeka pogwiritsa ntchito chitsanzo cha vuto la nkhandwe, mbuzi ndi kabichi

M'malingaliro anga, mu gawo la chilankhulo cha Chirasha pa intaneti, mutu wotsimikizika wokhazikika sunaphimbidwe mokwanira, ndipo pali kusowa kwa zitsanzo zosavuta komanso zomveka bwino.

Ndipereka chitsanzo kuchokera ku gwero lachilendo, ndikuwonjezera yankho langa ku vuto lodziwika bwino la kuwoloka nkhandwe, mbuzi ndi kabichi kutsidya lina la mtsinje.

Koma choyamba, ndifotokoza mwachidule chomwe chitsimikiziro chokhazikika ndi chifukwa chake chikufunika.

Kutsimikizira kovomerezeka kumatanthauza kuyang'ana pulogalamu imodzi kapena algorithm pogwiritsa ntchito ina.

Izi ndizofunikira kuwonetsetsa kuti pulogalamuyo ikuchita momwe ikuyembekezeredwa komanso kuonetsetsa chitetezo chake.

Kutsimikizira kovomerezeka ndi njira yamphamvu kwambiri yopezera ndikuchotsa zofooka: kumakupatsani mwayi wopeza mabowo onse omwe alipo mu pulogalamu, kapena kutsimikizira kuti kulibe.
Ndizofunikira kudziwa kuti nthawi zina izi sizingatheke, monga vuto la mfumukazi 8 yokhala ndi mabwalo 1000 m'lifupi mwake: zonse zimatsikira ku zovuta za algorithmic kapena vuto loyimitsa.

Komabe, mulimonsemo, imodzi mwa mayankho atatu idzalandiridwa: pulogalamuyo ndi yolondola, yolakwika, kapena sikunali kotheka kuwerengera yankho.

Ngati n'kosatheka kupeza yankho, nthawi zambiri n'zotheka kukonzanso zigawo zosamveka bwino za pulogalamuyo, kuchepetsa zovuta zawo za algorithmic, kuti mupeze yankho la inde kapena ayi.

Ndipo kutsimikizira kovomerezeka kumagwiritsidwa ntchito, mwachitsanzo, mu Windows kernel ndi machitidwe a Darpa drone, kuti atsimikizire chitetezo chokwanira.

Tigwiritsa ntchito Z3Prover, chida champhamvu kwambiri chotsimikizira ndi kutsimikizira ma equation.

Kuphatikiza apo, Z3 imathetsa ma equation, ndipo samasankha zikhalidwe zawo pogwiritsa ntchito nkhanza.
Izi zikutanthauza kuti imatha kupeza yankho, ngakhale pakakhala 10 ^ 100 kuphatikiza zosankha zolowetsa.

Koma izi ndi pafupifupi mikangano khumi ndi iwiri yokha ya mtundu wa Integer, ndipo izi zimachitika nthawi zambiri.

Vuto la mfumukazi 8 (Zotengedwa kuchokera ku Chingerezi buku).

# 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)

Kuthamanga Z3, timapeza yankho:

[Q_5 = 1,
 Q_8 = 7,
 Q_3 = 8,
 Q_2 = 2,
 Q_6 = 3,
 Q_4 = 6,
 Q_7 = 5,
 Q_1 = 4]

Vuto la mfumukazi ndi lofanana ndi pulogalamu yomwe imatengera ma coordinates a 8 queens ndikupereka yankho ngati mfumukaziyo idagundana.

Ngati titha kuthana ndi pulogalamu yotereyi pogwiritsa ntchito chitsimikiziro chokhazikika, ndiyeno poyerekeza ndi vutolo, tikanangofunika kuchitapo kanthu kenanso mwanjira yosinthira pulogalamuyo kukhala equation: zitha kukhala zofanana ndi zathu ( ndithudi, ngati pulogalamuyo inalembedwa molondola).

Zomwezo zidzachitikanso pakufufuza zofooka: timangoyika zomwe tikufuna, mwachitsanzo, mawu achinsinsi a admin, kusintha gwero kapena code yosokonekera kukhala ma equations omwe amagwirizana ndi chitsimikiziro, ndiyeno tipeze yankho la chiyani. deta iyenera kuperekedwa monga chothandizira kukwaniritsa cholingacho.

Malingaliro anga, vuto la nkhandwe, mbuzi ndi kabichi ndilosangalatsa kwambiri, popeza kulithetsa kumafuna masitepe ambiri (7).

Ngati vuto la mfumukazi likufanana ndi momwe mungalowetse seva pogwiritsa ntchito pempho limodzi la GET kapena POST, ndiye kuti nkhandwe, mbuzi ndi kabichi zimasonyeza chitsanzo kuchokera ku gulu lovuta kwambiri komanso lofalikira, lomwe cholinga chake chikhoza kutheka kokha. mwa zopempha zingapo.

Izi zikufanana, mwachitsanzo, ndi zochitika zomwe muyenera kupeza jekeseni wa SQL, lembani fayilo kupyoleramo, kenaka kwezani ufulu wanu ndikungopeza mawu achinsinsi.

Mikhalidwe ya vuto ndi njira yakeMlimi ayenera kunyamula nkhandwe, mbuzi ndi kabichi kuwoloka mtsinjewo. Mlimi ali ndi bwato lomwe limatha kunyamula chinthu chimodzi chokha, kupatula mlimi mwiniyo. Nkhandwe idzadya mbuzi ndipo mbuzi idzadya kabichi ngati mlimi akuwasiya osawayang’anira.

Yankho lake ndiloti mu gawo 4 mlimi akuyenera kubweza mbuziyo.
Tsopano tiyeni tiyambe kuthetsa izo mwadongosolo.

Tiyeni titchule mlimi, nkhandwe, mbuzi ndi kabichi ngati 4 zosintha zomwe zimangotenga mtengo wa 0 kapena 1. Ziro zikutanthauza kuti zili kumanzere, ndipo chimodzi kutanthauza kuti zili kumanja.

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 ndi chiwerengero cha masitepe ofunikira kuthetsa. Gawo lirilonse likuyimira dziko la mtsinje, bwato ndi mabungwe onse.

Pakadali pano, tiyeni tisankhe mwachisawawa ndipo ndi malire, tengani 10.

Gulu lililonse likuimiridwa m'makope 10 - uwu ndi mtengo wake pamasitepe 10 aliwonse.

Tsopano tiyeni tiyike zikhalidwe zoyambira ndi zomaliza.

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 ]

Kenako timayika mikhalidwe yomwe nkhandwe imadya mbuzi, kapena mbuzi imadya kabichi, monga zopinga mu equation.
(Pamaso pa mlimi, nkhanza sizingatheke)

# 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) ]

Ndipo potsiriza, tidzafotokozera zonse zomwe mlimi angachite podutsa kumeneko kapena kubwerera.
Atha kutenga nkhandwe, mbuzi kapena kabichi ndi iye, kapena osatenga aliyense, kapena osayenda kulikonse.

Inde, palibe amene angathe kuwoloka popanda mlimi.

Izi zidzafotokozedwa ndi mfundo yakuti dera lililonse lotsatira la mtsinje, bwato ndi mabungwe akhoza kusiyana ndi m'mbuyomo mwa njira yochepa.

Osapitirira 2 bits, komanso ndi malire ena ambiri, popeza mlimi amatha kunyamula chinthu chimodzi panthawi imodzi ndipo si onse omwe angasiyidwe palimodzi.

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) ]

Tiyeni tiyendetse yankho.

solve(Side + Start + Finish + Safe + Travel)

Ndipo timapeza yankho!

Z3 idapeza zigawo zofananira zomwe zimakwaniritsa mikhalidwe yonse.
Mtundu wa mawonekedwe anayi a nthawi ya danga.

Tiye tione zimene zinachitika.

Tikuwona kuti pamapeto pake aliyense adawoloka, poyamba mlimi wathu adaganiza zopumula, ndipo m'masitepe awiri oyambirira sasambira kulikonse.

Human_2 = 0
Human_3 = 0

Izi zikusonyeza kuti chiwerengero cha mayiko omwe tasankha ndi ochuluka, ndipo 8 adzakhala okwanira.

Kwa ife, mlimi anachita izi: yambani, kupumula, kupumula, kuwoloka mbuzi, kuwoloka mmbuyo, kuwoloka kabichi, kubwerera ndi mbuzi, kuwoloka Nkhandwe, kubwereranso nokha, kubweretsanso mbuzi.

Koma pamapeto pake vutolo linathetsedwa.

#Старт.
 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

Tsopano tiyeni tiyese kusintha mikhalidwe ndi kutsimikizira kuti palibe njira zothetsera.

Kuti tichite izi, tidzapatsa nkhandwe yathu herbivory, ndipo iye adzafuna kudya kabichi.
Izi zitha kufananizidwa ndi zomwe cholinga chathu ndikuteteza pulogalamuyo ndipo tiyenera kuonetsetsa kuti palibe zopinga.

 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 idatipatsa yankho ili:

 no solution

Zikutanthauza kuti palibe njira zothetsera.

Chifukwa chake, tidatsimikizira mwadongosolo kuti sizingatheke kuwoloka ndi nkhandwe ya omnivorous popanda kutayika kwa mlimi.

Ngati omvera apeza kuti mutuwu ndi wosangalatsa, ndiye kuti m'nkhani zamtsogolo ndikuuzani momwe mungasinthire pulogalamu wamba kapena ntchito kukhala equation yogwirizana ndi njira zovomerezeka, ndikuyithetsa, potero ndikuwulula zonse zovomerezeka ndi zofooka. Choyamba, pa ntchito yomweyi, koma yoperekedwa mu mawonekedwe a pulogalamu, ndiyeno pang'onopang'ono kuisokoneza ndikupita ku zitsanzo zamakono kuchokera ku dziko la chitukuko cha mapulogalamu.

Nkhani yotsatira yakonzeka kale:
Kupanga dongosolo lotsimikizira kuyambira poyambira: Kulemba VM yophiphiritsa mu PHP ndi Python

M'menemo ndimachoka ku chitsimikizo chovomerezeka cha mavuto kupita ku mapulogalamu, ndikufotokozera
angasinthidwe bwanji kukhala machitidwe ovomerezeka okha.

Source: www.habr.com