ስለ ተኩላ፣ ፍየል እና ጎመን ችግር ምሳሌ ላይ መደበኛ ማረጋገጫ

በእኔ አስተያየት, በበይነመረብ የሩስያ ቋንቋ ዘርፍ, መደበኛ የማረጋገጫ ርዕስ በበቂ ሁኔታ አልተሸፈነም, እና በተለይም ቀላል እና ግልጽ ምሳሌዎች እጥረት አለ.

ከባዕድ ምንጭ አንድ ምሳሌ እሰጣለሁ እና ተኩላ ፣ ፍየል እና ጎመንን ወደ ወንዝ ማዶ ለመሻገር የራሴን መፍትሄ እጨምራለሁ ።

በመጀመሪያ ግን መደበኛ ማረጋገጫ ምን እንደሆነ እና ለምን እንደሚያስፈልግ በአጭሩ እገልጻለሁ።

መደበኛ ማረጋገጫ አብዛኛውን ጊዜ አንድን ፕሮግራም ወይም አልጎሪዝም በሌላ በመጠቀም ማረጋገጥ ማለት ነው።

ይህ መርሃግብሩ የሚጠበቀው ባህሪ እንዲኖረው እና ደህንነቱን ለማረጋገጥ አስፈላጊ ነው.

መደበኛ ማረጋገጫ ድክመቶችን ለማግኘት እና ለማስወገድ በጣም ኃይለኛው መንገድ ነው-ሁሉንም ነባር ጉድጓዶች እና ስህተቶች በፕሮግራሙ ውስጥ እንዲያገኙ ወይም አለመኖራቸውን ያረጋግጣል።
በአንዳንድ ሁኔታዎች ይህ የማይቻል መሆኑን ልብ ሊባል የሚገባው ነው, ለምሳሌ በ 8 ንግስቶች ችግር ውስጥ በ 1000 ካሬዎች የቦርድ ስፋት: ሁሉም ወደ አልጎሪዝም ውስብስብነት ወይም የማቆም ችግር ይመጣል.

ሆኖም ግን, በማንኛውም ሁኔታ, ከሶስቱ መልሶች አንዱ ይቀበላል-ፕሮግራሙ ትክክል ነው, ትክክል አይደለም, ወይም መልሱን ማስላት አልተቻለም.

መልስ ለማግኘት የማይቻል ከሆነ, ብዙውን ጊዜ ግልጽ ያልሆኑትን የፕሮግራሙ ክፍሎችን እንደገና መሥራት, የአልጎሪዝም ውስብስብነታቸውን በመቀነስ, የተወሰነ አዎ ወይም የለም መልስ ለማግኘት.

እና መደበኛ ማረጋገጫ ከፍተኛውን የጥበቃ ደረጃ ለማረጋገጥ ለምሳሌ በዊንዶውስ ከርነል እና በዳርፓ ድሮን ኦፕሬቲንግ ሲስተሞች ውስጥ ጥቅም ላይ ይውላል።

ለራስ-ሰር ቲዎረም ማረጋገጫ እና እኩልታ መፍታት በጣም ኃይለኛ መሳሪያ የሆነውን Z3Proverን እንጠቀማለን።

በተጨማሪም ፣ Z3 እኩልታዎችን ይፈታል ፣ እና እሴቶቻቸውን በብርቱ ኃይል አይመርጥም ።
ይህ ማለት 10 ^ 100 የግቤት አማራጮች ጥምረት በሚኖርበት ጊዜ እንኳን መልሱን ማግኘት ይችላል ማለት ነው።

ነገር ግን ይህ የኢንቲጀር አይነት ወደ ደርዘን የሚጠጉ ግቤት ነጋሪ እሴቶች ብቻ ነው፣ እና ይሄ በተግባር ብዙ ጊዜ ያጋጥመዋል።

ችግር ወደ 8 ንግስቶች (ከእንግሊዝኛ የተወሰደ መመሪያ).

# 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 ን ስናሄድ መፍትሄውን እናገኛለን፡-

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

የንግሥቲቱ ችግር የ8 ንግሥቶችን መጋጠሚያዎች እንደ ግብአት ወስዶ ንግሥቲቱ እርስበርስ መምታታቸውን መልሱን ከሚሰጥ ፕሮግራም ጋር ሊወዳደር ይችላል።

መደበኛ ማረጋገጫን በመጠቀም እንዲህ ዓይነቱን ፕሮግራም የምንፈታ ከሆነ ፣ ከችግሩ ጋር ሲነፃፀር ፣ የፕሮግራሙን ኮድ ወደ ቀመር በመቀየር አንድ ተጨማሪ እርምጃ ብቻ መውሰድ አለብን ፣ እሱ በመሠረቱ ከእኛ ጋር ተመሳሳይ ይሆናል () በእርግጥ, ፕሮግራሙ በትክክል ከተፃፈ).

ተጋላጭነቶችን በሚፈልጉበት ጊዜ አንድ አይነት ነገር ይከሰታል ማለት ይቻላል: እኛ የምንፈልገውን የውጤት ሁኔታዎችን ብቻ እናዘጋጃለን ፣ ለምሳሌ ፣ የአስተዳዳሪ የይለፍ ቃል ፣ ምንጩን ወይም የተበላሸውን ኮድ ከማረጋገጫ ጋር ወደሚስማሙ እኩልታዎች እንለውጣለን እና ከዚያ ምን መልስ እናገኛለን ግቡን ለማሳካት መረጃን እንደ ግብአት ማቅረብ ያስፈልጋል።

በእኔ አስተያየት ስለ ተኩላ ፣ ፍየል እና ጎመን ያለው ችግር የበለጠ አስደሳች ነው ፣ ምክንያቱም እሱን ለመፍታት ቀድሞውኑ ብዙ (7) እርምጃዎችን ይፈልጋል ።

የንግሥቲቱ ችግር ነጠላ GET ወይም POST ጥያቄን ተጠቅመህ ሰርቨር ውስጥ መግባት ከምትችልበት ጉዳይ ጋር የሚነጻጸር ከሆነ ተኩላ፣ ፍየል እና ጎመን ግቡን ብቻ ማሳካት ከሚቻልበት በጣም ውስብስብ እና ሰፊ ምድብ ምሳሌ ያሳያል። በበርካታ ጥያቄዎች.

ይህ ለምሳሌ የ SQL መርፌን ለማግኘት ከሚፈልጉበት ሁኔታ ጋር ተመሳሳይ ነው ፣ በእሱ ውስጥ ፋይል ይፃፉ ፣ ከዚያ መብቶችዎን ከፍ ያድርጉ እና ከዚያ ብቻ የይለፍ ቃል ያግኙ።

የችግሩ ሁኔታዎች እና መፍትሄውገበሬው ተኩላ፣ ፍየል እና ጎመን ወንዙን ማሻገር አለበት። ገበሬው ከራሱ ከገበሬው በተጨማሪ አንድ ዕቃ ብቻ ማስተናገድ የሚችል ጀልባ አለው። ተኩላው ፍየሉን ይበላል ፍየሉም ጎመንውን ይበላዋል ገበሬው ሳይጠብቅ ቢተውዋቸው።

መፍትሄው በደረጃ 4 ገበሬው ፍየሉን መልሶ መውሰድ ያስፈልገዋል.
አሁን በፕሮግራም መፍታት እንጀምር።

ገበሬውን፣ ተኩላውን፣ ፍየሉን እና ጎመንን 4 ተለዋዋጮች እንጥቀስ እና እሴቱን 0 ወይም 1 ብቻ ይወስዳሉ። ዜሮ ማለት በግራ ባንክ ላይ ናቸው፣ አንደኛው ደግሞ በቀኝ ናቸው ማለት ነው።

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

ቁጥር ለመፍታት የሚያስፈልጉት የእርምጃዎች ብዛት ነው። እያንዳንዱ እርምጃ የወንዙን, የጀልባውን እና ሁሉንም አካላትን ሁኔታ ይወክላል.

ለአሁን፣ በዘፈቀደ እንመርጠው እና በህዳግ 10 ውሰድ።

እያንዳንዱ አካል በ 10 ቅጂዎች ይወከላል - ይህ በእያንዳንዱ 10 ደረጃዎች ውስጥ ያለው ዋጋ ነው.

አሁን ለመጀመር እና ለመጨረስ ሁኔታዎችን እናዘጋጅ።

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 ]

ከዚያም ተኩላው ፍየሉን የሚበላበት ወይም ፍየል ጎመንን የሚበላበትን ሁኔታ እናስቀምጣለን, እንደ እኩልታው ገደቦች.
(በገበሬው ፊት ጠበኝነት የማይቻል ነው)

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

እና በመጨረሻም፣ ወደዚያ ወይም ወደ ኋላ ሲሻገሩ ገበሬው ሊያደርጋቸው የሚችሉትን ሁሉንም ድርጊቶች እንገልጻለን።
አንድም ተኩላ፣ ፍየል ወይም ጎመን ይዞ መሄድ ይችላል፣ ወይም ማንንም አይወስድም፣ ወይም በምንም መንገድ አይርከብም።

በእርግጥ ያለ ገበሬ ማንም ሊሻገር አይችልም።

ይህ የሚገለጸው እያንዳንዱ ተከታይ የወንዙ፣ የጀልባ እና የአካል ክፍሎች ሁኔታ ከቀዳሚው ሊለዩ የሚችሉት በጥብቅ በተገደበ መንገድ ብቻ ነው።

ገበሬው በአንድ ጊዜ አንድ አካል ብቻ ማጓጓዝ ስለሚችል እና ሁሉም በአንድ ላይ መተው ስለማይችሉ ከ 2 ቢት ያልበለጠ እና ከሌሎች ብዙ ገደቦች ጋር።

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

መፍትሄውን እናካሂድ።

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

እና መልሱን እናገኛለን!

Z3 ሁሉንም ሁኔታዎች የሚያረካ ወጥ የሆነ የግዛት ስብስብ አግኝቷል።
የቦታ-ጊዜ ባለአራት-ልኬት ቀረጻ አይነት።

የሆነውን ነገር እንወቅ።

በመጨረሻ ሁሉም ሰው እንደተሻገረ እናያለን, መጀመሪያ ላይ የእኛ ገበሬ ብቻ ለማረፍ ወስኗል, እና በመጀመሪያዎቹ 2 ደረጃዎች ውስጥ የትኛውም ቦታ አይዋኝም.

Human_2 = 0
Human_3 = 0

ይህ የሚያሳየው የመረጥናቸው ግዛቶች ብዛት ከመጠን በላይ ነው, እና 8 በጣም በቂ ይሆናል.

በእኛ ሁኔታ ገበሬው እንዲህ አድርጓል፡ ጀምር፣ አርፈህ፣ አረፍ፣ ፍየሉን ተሻገር፣ ተሻገር፣ ጎመን ተሻገር፣ ከፍየል ጋር ተመለስ፣ ተኩላውን ተሻገር፣ ብቻውን ተመለስ፣ ፍየሏን እንደገና አስረክብ።

ነገር ግን በመጨረሻ ችግሩ ተፈትቷል.

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

አሁን ሁኔታዎችን ለመለወጥ እና ምንም መፍትሄዎች እንደሌሉ ለማረጋገጥ እንሞክር.

ይህንን ለማድረግ የእኛን ተኩላ የእፅዋት ተክል እንሰጣለን, እና ጎመንን መብላት ይፈልጋል.
ይህ ግባችን አፕሊኬሽኑን መጠበቅ ከሆነበት ሁኔታ ጋር ሊመሳሰል ይችላል እና ምንም ክፍተቶች እንደሌሉ ማረጋገጥ አለብን።

 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 የሚከተለውን ምላሽ ሰጠን።

 no solution

በእውነቱ ምንም መፍትሄዎች የሉም ማለት ነው.

ስለዚህም በገበሬው ላይ ያለ ኪሳራ ከሁሉን ቻይ ተኩላ ጋር መሻገር የማይቻል መሆኑን በፕሮግራም አረጋግጠናል።

ተሰብሳቢዎቹ ይህንን ርዕስ አስደሳች ሆኖ ካገኙት ፣ ከዚያ በሚቀጥሉት መጣጥፎች ውስጥ አንድ ተራ ፕሮግራም ወይም ተግባር ከመደበኛ ዘዴዎች ጋር ወደሚስማማ እኩልታ እንዴት እንደሚቀይሩ እነግርዎታለሁ ፣ እና መፍታት ፣ በዚህም ሁለቱንም ህጋዊ ሁኔታዎችን እና ተጋላጭነቶችን ያሳያል ። በመጀመሪያ ፣ በተመሳሳይ ተግባር ላይ ፣ ግን በፕሮግራም መልክ ቀርቧል ፣ እና ከዚያ ቀስ በቀስ ውስብስብ እና ከሶፍትዌር ልማት ዓለም ወደ ወቅታዊ ምሳሌዎች ይሂዱ።

የሚቀጥለው ጽሑፍ አስቀድሞ ዝግጁ ነው፡-
መደበኛ የማረጋገጫ ስርዓት ከባዶ መፍጠር፡ ተምሳሌታዊ ቪኤምን በPHP እና Python መጻፍ

በእሱ ውስጥ የችግሮችን መደበኛ ማረጋገጫ ወደ ፕሮግራሞች እሸጋገር እና እገልጻለሁ
እንዴት እነሱን ወደ መደበኛ ህጎች ስርዓት በራስ-ሰር መቀየር እንደሚችሉ።

ምንጭ: hab.com