🥇 Kev txheeb xyuas qhov tseeb siv piv txwv ntawm hma, tshis thiab zaub qhwv teeb meem

Nyob rau hauv kuv lub tswv yim, nyob rau hauv lub Lavxias teb sab-lus sector ntawm Internet, lub ntsiab lus ntawm cov ntaub ntawv pov thawj yog tsis txaus them, thiab muaj tshwj xeeb tshaj yog tsis muaj ib tug yooj yim thiab meej piv txwv.

Kuv yuav muab piv txwv los ntawm ib qho chaw txawv teb chaws, thiab ntxiv kuv tus kheej kev daws teeb meem rau qhov kev paub zoo ntawm kev hla tus hma, tshis thiab zaub qhwv mus rau sab nraud ntawm tus dej.

Tab sis ua ntej, kuv yuav piav qhia luv luv txog qhov kev pov thawj raug cai thiab vim li cas nws thiaj li xav tau.

Kev txheeb xyuas qhov tseeb feem ntau txhais tau tias kuaj ib qho kev pab cuam lossis algorithm siv lwm qhov.

Qhov no yog qhov tsim nyog los xyuas kom meej tias qhov kev zov me nyuam coj raws li qhov xav tau thiab tseem ua kom nws ruaj ntseg.

Kev txheeb xyuas qhov tseeb yog qhov tseem ceeb tshaj plaws ntawm kev nrhiav thiab tshem tawm qhov tsis zoo: nws tso cai rau koj pom tag nrho cov qhov uas twb muaj lawm thiab kab hauv ib qho kev pab cuam, lossis ua pov thawj tias lawv tsis muaj.
Nws yog ib nqi sau cia hais tias nyob rau hauv tej rooj plaub qhov no yog tsis yooj yim sua, xws li nyob rau hauv qhov teeb meem ntawm 8 poj huab tais nrog ib tug board dav ntawm 1000 squares: nws tag nrho los mus rau algorithmic complexity los yog cov teeb meem nres.

Txawm li cas los xij, nyob rau hauv txhua rooj plaub, ib qho ntawm peb cov lus teb yuav tau txais: qhov kev pab cuam yog qhov tseeb, tsis raug, lossis nws tsis tuaj yeem suav cov lus teb.

Yog tias nws tsis tuaj yeem nrhiav cov lus teb, nws feem ntau tuaj yeem rov ua haujlwm tsis meej ntawm qhov kev pab cuam, txo lawv cov algorithmic complexity, thiaj li yuav tau txais cov lus teb tshwj xeeb yog lossis tsis muaj.

Thiab cov ntaub ntawv pov thawj raug siv, piv txwv li, hauv Windows kernel thiab Darpa drone operating systems, los xyuas kom meej qhov siab tshaj plaws ntawm kev tiv thaiv.

Peb yuav siv Z3Prover, lub cuab yeej muaj zog heev rau kev siv tshuab theorem ua pov thawj thiab kev sib npaug sib npaug.

Ntxiv mus, Z3 daws qhov sib npaug, thiab tsis xaiv lawv cov txiaj ntsig siv brute force.
Qhov no txhais tau hais tias nws muaj peev xwm nrhiav tau cov lus teb, txawm tias nyob rau hauv rooj plaub uas muaj 10^100 kev sib txuas ntawm cov kev xaiv nkag.

Tab sis qhov no tsuas yog hais txog kaum tawm cov lus sib cav ntawm hom Integer, thiab qhov no feem ntau ntsib hauv kev xyaum.

Teeb meem txog 8 poj huab tais (Nkag los ntawm Lus Askiv phau ntawv).

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

Khiav Z3, peb tau txais cov kev daws teeb meem:

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

Qhov teeb meem huab tais yog piv rau ib qho kev pab cuam uas yuav siv sij hawm raws li kev sib koom ua ke ntawm 8 huab tais thiab tso tawm cov lus teb seb cov poj huab tais yeej ib leeg.

Yog tias peb yuav daws tau qhov kev pab cuam zoo li no siv cov ntaub ntawv pov thawj, tom qab ntawd muab piv rau qhov teeb meem, peb tsuas yog yuav tsum tau ua ib kauj ruam ntxiv rau hauv daim ntawv ntawm kev hloov cov program code rau hauv qhov sib npaug: nws yuav tig mus rau qhov tseem ceeb zoo ib yam rau peb li ( tau kawg, yog tias qhov program sau raug).

Yuav luag tib yam yuav tshwm sim nyob rau hauv cov ntaub ntawv ntawm kev tshawb nrhiav qhov tsis zoo: peb tsuas yog teeb tsa cov xwm txheej uas peb xav tau, piv txwv li, tus password admin, hloov lub hauv paus lossis decompiled code rau hauv qhov sib npaug sib npaug nrog kev txheeb xyuas, thiab tom qab ntawd tau txais cov lus teb li cas. cov ntaub ntawv yuav tsum tau muab los ua cov tswv yim kom ua tiav lub hom phiaj.

Hauv kuv lub tswv yim, qhov teeb meem hais txog hma, tshis thiab zaub qhwv yog qhov nthuav ntau dua, txij li ntau (7) cov kauj ruam twb xav tau los daws nws.

Yog hais tias qhov teeb meem huab tais yog piv rau cov ntaub ntawv uas koj tuaj yeem nkag mus rau ib tus neeg rau zaub mov siv ib qho GET lossis POST thov, ces tus hma, tshis thiab zaub qhwv ua piv txwv los ntawm ntau yam nyuaj thiab dav, uas lub hom phiaj tuaj yeem ua tiav nkaus xwb. los ntawm ntau qhov kev thov.

Qhov no yog qhov sib piv, piv txwv li, rau qhov xwm txheej uas koj yuav tsum nrhiav kev txhaj tshuaj SQL, sau cov ntaub ntawv los ntawm nws, tom qab ntawd tsa koj txoj cai thiab tsuas yog tom qab ntawd tau txais lo lus zais.

Cov xwm txheej ntawm qhov teeb meem thiab nws txoj kev daws teeb meemTus neeg ua teb yuav tsum thauj hma, tshis thiab zaub qhwv hla tus dej. Tus neeg ua liaj ua teb muaj lub nkoj uas tuaj yeem nqa tau ib yam khoom, dua li tus neeg ua liaj ua teb nws tus kheej. Tus hma yuav noj tshis thiab tshis yuav noj zaub qhwv yog tias tus neeg ua liaj ua teb cia lawv tsis tuaj saib.

Qhov kev daws teeb meem yog tias hauv kauj ruam 4 tus neeg ua liaj ua teb yuav tsum tau coj tus tshis rov qab.
Tam sim no cia peb pib daws nws programmatically.

Wb qhia txog tus neeg ua liaj ua teb, hma, tshis thiab zaub qhwv ua 4 qhov sib txawv uas coj tus nqi tsuas yog 0 lossis 1. Zero txhais tau hais tias lawv nyob rau sab laug, thiab ib qho txhais tau tias lawv nyob ntawm sab xis.

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

Tus lej yog tus lej ntawm cov kauj ruam yuav tsum tau daws. Txhua kauj ruam sawv cev rau lub xeev ntawm tus dej, lub nkoj thiab txhua qhov chaw.

Txog tam sim no, cia peb xaiv nws ntawm random thiab nrog cov npoo, coj 10.

Txhua qhov chaw yog sawv cev hauv 10 daim ntawv - qhov no yog nws tus nqi ntawm txhua 10 kauj ruam.

Tam sim no cia peb teem caij rau qhov pib thiab ua tiav.

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 ]

Tom qab ntawd peb teeb tsa cov xwm txheej uas tus hma noj tshis, lossis tshis noj cov zaub qhwv, raws li kev txwv hauv qhov sib npaug.
(Nyob rau hauv lub xub ntiag ntawm ib tug neeg ua teb, aggression yog tsis yooj yim sua)

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

Thiab thaum kawg, peb yuav txhais txhua yam ua tau ntawm tus neeg ua teb thaum hla qhov ntawd lossis rov qab.
Nws tuaj yeem nqa tus hma, tshis lossis ib lub pob tawb nrog nws, lossis tsis nqa leej twg, lossis tsis caij nkoj mus qhov twg los xij.

Tau kawg, tsis muaj leej twg tuaj yeem hla yam tsis muaj neeg ua liaj ua teb.

Qhov no yuav raug qhia los ntawm qhov tseeb tias txhua lub xeev tom ntej ntawm tus dej, lub nkoj thiab cov chaw tuaj yeem txawv ntawm qhov dhau los tsuas yog hauv txoj kev txwv nruj heev.

Tsis pub ntau tshaj 2 khoom, thiab nrog rau ntau yam kev txwv, vim tias tus neeg ua liaj ua teb tsuas tuaj yeem thauj tau ib qho chaw ntawm ib lub sijhawm thiab tsis yog txhua tus tuaj yeem tso ua ke.

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

Cia peb khiav txoj kev daws teeb meem.

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

Thiab peb tau txais cov lus teb!

Z3 pom ib qho kev sib koom ua ke ntawm cov xeev uas txaus siab rau txhua yam xwm txheej.
Ib hom plaub-dimensional cam khwb cia ntawm qhov chaw-lub sij hawm.

Cia peb xav txog qhov tshwm sim.

Peb pom tias thaum kawg txhua tus hla, tsuas yog thaum xub thawj peb cov neeg ua liaj ua teb txiav txim siab so, thiab thawj 2 kauj ruam nws tsis ua luam dej nyob qhov twg.

Human_2 = 0
Human_3 = 0

Qhov no qhia tau hais tias tus naj npawb ntawm lub xeev peb xaiv ntau dhau, thiab 8 yuav txaus txaus.

Hauv peb qhov xwm txheej, tus neeg ua liaj ua teb tau ua li no: pib, so, so, hla tus tshis, hla rov qab, hla lub cabbage, rov qab nrog tshis, hla hma, rov qab ib leeg, rov xa cov tshis.

Tab sis thaum kawg qhov teeb meem tau daws.

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

Tam sim no cia sim hloov cov xwm txheej thiab ua pov thawj tias tsis muaj kev daws teeb meem.

Ua li no, peb yuav muab peb tus hma herbivory, thiab nws yuav xav noj zaub qhwv.
Qhov no tuaj yeem muab piv rau cov ntaub ntawv uas peb lub hom phiaj yog kom ruaj ntseg daim ntawv thov thiab peb yuav tsum xyuas kom meej tias tsis muaj qhov khoob.

 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 muab peb cov lus teb hauv qab no:

 no solution

Nws txhais tau tias yeej tsis muaj kev daws teeb meem.

Yog li, peb programmatically ua pov thawj qhov tsis tuaj yeem hla nrog tus hma omnivorous yam tsis muaj kev poob rau tus neeg ua teb.

Yog tias cov neeg tuaj saib pom cov ncauj lus no nthuav, tom qab ntawd hauv cov ntawv yav tom ntej kuv yuav qhia koj yuav ua li cas tig ib qho kev pab cuam zoo tib yam lossis ua haujlwm rau hauv kev sib npaug sib npaug nrog cov txheej txheem raug cai, thiab daws nws, yog li nthuav tawm txhua qhov xwm txheej raug cai thiab qhov tsis zoo. Ua ntej, ntawm tib txoj haujlwm, tab sis nthuav tawm nyob rau hauv daim ntawv ntawm ib qho kev pab cuam, thiab tom qab ntawd maj mam ua rau nws nyuaj thiab txav mus rau cov piv txwv tam sim no los ntawm lub ntiaj teb ntawm kev txhim kho software.

Kab lus txuas ntxiv yog npaj txhij lawm:
Tsim kom muaj kev pov thawj tseeb los ntawm kos: Sau cov cim VM hauv PHP thiab Python

Hauv nws kuv txav los ntawm kev txheeb xyuas qhov teeb meem rau cov kev pab cuam, thiab piav qhia
yuav ua li cas lawv yuav tsum tau hloov dua siab tshiab rau hauv txoj cai txoj cai txiav.

Tau qhov twg los: www.hab.com

Kev txheeb xyuas qhov tseeb siv qhov piv txwv ntawm qhov teeb meem hma, tshis thiab zaub qhwv

Ntxiv ib saib Отменить ответ