Π€ΠΎΡ€ΠΌΠ°Π»ΡŒΠ½Π°Ρ вСрификация Π½Π° ΠΏΡ€ΠΈΠΌΠ΅Ρ€Π΅ Π·Π°Π΄Π°Ρ‡ΠΈ ΠΎ Π²ΠΎΠ»ΠΊΠ΅, ΠΊΠΎΠ·Π΅ ΠΈ капустС

На ΠΌΠΎΠΉ взгляд, Π² русскоязычном сСкторС ΠΈΠ½Ρ‚Π΅Ρ€Π½Π΅Ρ‚Π° Ρ‚Π΅ΠΌΠ°Ρ‚ΠΈΠΊΠ° Ρ„ΠΎΡ€ΠΌΠ°Π»ΡŒΠ½ΠΎΠΉ Π²Π΅Ρ€ΠΈΡ„ΠΈΠΊΠ°Ρ†ΠΈΠΈ освСщСна нСдостаточно, ΠΈ особСнно Π½Π΅ Ρ…Π²Π°Ρ‚Π°Π΅Ρ‚ простых ΠΈ наглядных ΠΏΡ€ΠΈΠΌΠ΅Ρ€ΠΎΠ².

Π― ΠΏΡ€ΠΈΠ²Π΅Π΄Ρƒ Ρ‚Π°ΠΊΠΎΠΉ ΠΏΡ€ΠΈΠΌΠ΅Ρ€ ΠΈΠ· Π·Π°Ρ€ΡƒΠ±Π΅ΠΆΠ½ΠΎΠ³ΠΎ источника, ΠΈ дополню собствСнным Ρ€Π΅ΡˆΠ΅Π½ΠΈΠ΅ΠΌ извСстной Π·Π°Π΄Π°Ρ‡ΠΈ ΠΎ ΠΏΠ΅Ρ€Π΅ΠΏΡ€Π°Π²Π΅ Π²ΠΎΠ»ΠΊΠ°, ΠΊΠΎΠ·Ρ‹ ΠΈ капусты Π½Π° Π΄Ρ€ΡƒΠ³ΡƒΡŽ сторону Ρ€Π΅ΠΊΠΈ.

Но Π²Π½Π°Ρ‡Π°Π»Π΅ Π²ΠΊΡ€Π°Ρ‚Ρ†Π΅ ΠΎΠΏΠΈΡˆΡƒ, Ρ‡Ρ‚ΠΎ ΠΈΠ· сСбя прСдставляСт Ρ„ΠΎΡ€ΠΌΠ°Π»ΡŒΠ½Π°Ρ вСрификация ΠΈ Π·Π°Ρ‡Π΅ΠΌ ΠΎΠ½Π° Π½ΡƒΠΆΠ½Π°.

Под Ρ„ΠΎΡ€ΠΌΠ°Π»ΡŒΠ½ΠΎΠΉ Π²Π΅Ρ€ΠΈΡ„ΠΈΠΊΠ°Ρ†ΠΈΠ΅ΠΉ ΠΎΠ±Ρ‹Ρ‡Π½ΠΎ ΠΏΠΎΠ½ΠΈΠΌΠ°ΡŽΡ‚ ΠΏΡ€ΠΎΠ²Π΅Ρ€ΠΊΡƒ ΠΎΠ΄Π½ΠΎΠΉ ΠΏΡ€ΠΎΠ³Ρ€Π°ΠΌΠΌΡ‹ Π»ΠΈΠ±ΠΎ Π°Π»Π³ΠΎΡ€ΠΈΡ‚ΠΌΠ° с ΠΏΠΎΠΌΠΎΡ‰ΡŒΡŽ Π΄Ρ€ΡƒΠ³ΠΎΠΉ.

Π­Ρ‚ΠΎ Π½ΡƒΠΆΠ½ΠΎ для Ρ‚ΠΎΠ³ΠΎ, Ρ‡Ρ‚ΠΎΠ±Ρ‹ ΡƒΠ΄ΠΎΡΡ‚ΠΎΠ²Π΅Ρ€ΠΈΡ‚ΡŒΡΡ, Ρ‡Ρ‚ΠΎ ΠΏΠΎΠ²Π΅Π΄Π΅Π½ΠΈΠ΅ ΠΏΡ€ΠΎΠ³Ρ€Π°ΠΌΠΌΡ‹ соотвСтствуСт ΠΎΠΆΠΈΠ΄Π°Π΅ΠΌΠΎΠΌΡƒ, Π° Ρ‚Π°ΠΊΠΆΠ΅ ΠΎΠ±Π΅ΡΠΏΠ΅Ρ‡ΠΈΡ‚ΡŒ Π΅Ρ‘ Π±Π΅Π·ΠΎΠΏΠ°ΡΠ½ΠΎΡΡ‚ΡŒ.

Π€ΠΎΡ€ΠΌΠ°Π»ΡŒΠ½Π°Ρ вСрификация являСтся самым ΠΌΠΎΡ‰Π½Ρ‹ΠΌ срСдством поиска ΠΈ устранСния уязвимостСй: ΠΎΠ½Π° позволяСт Π½Π°ΠΉΡ‚ΠΈ всС ΡΡƒΡ‰Π΅ΡΡ‚Π²ΡƒΡŽΡ‰ΠΈΠ΅ Π΄Ρ‹Ρ€Ρ‹ ΠΈ Π±Π°Π³ΠΈ Π² ΠΏΡ€ΠΎΠ³Ρ€Π°ΠΌΠΌΠ΅, Π»ΠΈΠ±ΠΎ ΠΆΠ΅ Π΄ΠΎΠΊΠ°Π·Π°Ρ‚ΡŒ, Ρ‡Ρ‚ΠΎ ΠΈΡ… Π½Π΅Ρ‚.
Π‘Ρ‚ΠΎΠΈΡ‚ Π·Π°ΠΌΠ΅Ρ‚ΠΈΡ‚ΡŒ, Ρ‡Ρ‚ΠΎ Π² Π½Π΅ΠΊΠΎΡ‚ΠΎΡ€Ρ‹Ρ… случаях это Π±Ρ‹Π²Π°Π΅Ρ‚ Π½Π΅Π²ΠΎΠ·ΠΌΠΎΠΆΠ½ΠΎ, ΠΊΠ°ΠΊ Π½Π°ΠΏΡ€ΠΈΠΌΠ΅Ρ€, Π² Π·Π°Π΄Π°Ρ‡Π΅ ΠΎ 8 фСрзях с ΡˆΠΈΡ€ΠΈΠ½ΠΎΠΉ доски 1000 ΠΊΠ»Π΅Ρ‚ΠΎΠΊ: всё упираСтся Π² Π°Π»Π³ΠΎΡ€ΠΈΡ‚ΠΌΠΈΡ‡Π΅ΡΠΊΡƒΡŽ ΡΠ»ΠΎΠΆΠ½ΠΎΡΡ‚ΡŒ Π»ΠΈΠ±ΠΎ ΠΏΡ€ΠΎΠ±Π»Π΅ΠΌΡƒ остановки.

Однако Π² любом случаС Π±ΡƒΠ΄Π΅Ρ‚ ΠΏΠΎΠ»ΡƒΡ‡Π΅Π½ ΠΎΠ΄ΠΈΠ½ ΠΈΠ· Ρ‚Ρ€Ρ‘Ρ… ΠΎΡ‚Π²Π΅Ρ‚ΠΎΠ²: ΠΏΡ€ΠΎΠ³Ρ€Π°ΠΌΠΌΠ° ΠΊΠΎΡ€Ρ€Π΅ΠΊΡ‚Π½Π°, Π½Π΅ΠΊΠΎΡ€Ρ€Π΅ΠΊΡ‚Π½Π°, ΠΈΠ»ΠΈ ΠΆΠ΅ β€” Π²Ρ‹Ρ‡ΠΈΡΠ»ΠΈΡ‚ΡŒ ΠΎΡ‚Π²Π΅Ρ‚ Π½Π΅ ΡƒΠ΄Π°Π»ΠΎΡΡŒ.

Π’ случаС нСвозмоТности нахоТдСния ΠΎΡ‚Π²Π΅Ρ‚Π°, Π·Π°Ρ‡Π°ΡΡ‚ΡƒΡŽ ΠΌΠΎΠΆΠ½ΠΎ ΠΏΠ΅Ρ€Π΅Ρ€Π°Π±ΠΎΡ‚Π°Ρ‚ΡŒ нСясныС мСста ΠΏΡ€ΠΎΠ³Ρ€Π°ΠΌΠΌΡ‹, ΡƒΠΌΠ΅Π½ΡŒΡˆΠΈΠ² ΠΈΡ… Π°Π»Π³ΠΎΡ€ΠΈΡ‚ΠΌΠΈΡ‡Π΅ΡΠΊΡƒΡŽ ΡΠ»ΠΎΠΆΠ½ΠΎΡΡ‚ΡŒ, для Ρ‚ΠΎΠ³ΠΎ Ρ‡Ρ‚ΠΎΠ±Ρ‹ ΠΏΠΎΠ»ΡƒΡ‡ΠΈΡ‚ΡŒ ΠΊΠΎΠ½ΠΊΡ€Π΅Ρ‚Π½Ρ‹ΠΉ ΠΎΡ‚Π²Π΅Ρ‚ Π΄Π° Π»ΠΈΠ±ΠΎ Π½Π΅Ρ‚.

А примСняСтся Ρ„ΠΎΡ€ΠΌΠ°Π»ΡŒΠ½Π°Ρ вСрификация, Π½Π°ΠΏΡ€ΠΈΠΌΠ΅Ρ€, Π² ядрС Windows ΠΈ ΠΎΠΏΠ΅Ρ€Π°Ρ†ΠΈΠΎΠ½Π½Ρ‹Ρ… систСмах бСспилотников Darpa, для обСспСчСния максимального уровня Π·Π°Ρ‰ΠΈΡ‚Ρ‹.

ΠœΡ‹ Π±ΡƒΠ΄Π΅ΠΌ ΠΈΡΠΏΠΎΠ»ΡŒΠ·ΠΎΠ²Π°Ρ‚ΡŒ Z3Prover, ΠΎΡ‡Π΅Π½ΡŒ ΠΌΠΎΡ‰Π½Ρ‹ΠΉ инструмСнт для Π°Π²Ρ‚ΠΎΠΌΠ°Ρ‚ΠΈΠ·ΠΈΡ€ΠΎΠ²Π°Π½Π½ΠΎΠ³ΠΎ Π΄ΠΎΠΊΠ°Π·Π°Ρ‚Π΅Π»ΡŒΡΡ‚Π²Π° Ρ‚Π΅ΠΎΡ€Π΅ΠΌ ΠΈ Ρ€Π΅ΡˆΠ΅Π½ΠΈΡ уравнСния.

ΠŸΡ€ΠΈΡ‡Ρ‘ΠΌ Z3 ΠΈΠΌΠ΅Π½Π½ΠΎ Ρ€Π΅ΡˆΠ°Π΅Ρ‚ уравнСния, Π° Π½Π΅ ΠΏΠΎΠ΄Π±ΠΈΡ€Π°Π΅Ρ‚ ΠΈΡ… значСния Π³Ρ€ΡƒΠ±Ρ‹ΠΌ брутфорсом.
Π­Ρ‚ΠΎ ΠΎΠ·Π½Π°Ρ‡Π°Π΅Ρ‚, Ρ‡Ρ‚ΠΎ ΠΎΠ½ способСн Π½Π°Ρ…ΠΎΠ΄ΠΈΡ‚ΡŒ ΠΎΡ‚Π²Π΅Ρ‚, Π΄Π°ΠΆΠ΅ Π² случаях ΠΊΠΎΠ³Π΄Π° ΠΊΠΎΠΌΠ±ΠΈΠ½Π°Ρ†ΠΈΠΉ Π²Ρ…ΠΎΠ΄Π½Ρ‹Ρ… Π²Π°Ρ€ΠΈΠ°Π½Ρ‚ΠΎΠ² ΠΈ 10^100.

А вСдь это всСго лишь ΠΎΠΊΠΎΠ»ΠΎ Π΄ΡŽΠΆΠΈΠ½Ρ‹ Π²Ρ…ΠΎΠ΄Π½Ρ‹Ρ… Π°Ρ€Π³ΡƒΠΌΠ΅Π½Ρ‚ΠΎΠ² Ρ‚ΠΈΠΏΠ° Integer, ΠΈ ΠΏΠΎΠ΄ΠΎΠ±Π½ΠΎΠ΅ Π·Π°Ρ‡Π°ΡΡ‚ΡƒΡŽ встрСчаСтся Π½Π° ΠΏΡ€Π°ΠΊΡ‚ΠΈΠΊΠ΅.

Π—Π°Π΄Π°Ρ‡Π° ΠΎ 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

Num β€” это число шагов Π½Π΅ΠΎΠ±Ρ…ΠΎΠ΄ΠΈΠΌΡ‹Ρ… для Ρ€Π΅ΡˆΠ΅Π½ΠΈΡ. ΠšΠ°ΠΆΠ΄Ρ‹ΠΉ шаг прСдставляСт собой состояниС Ρ€Π΅Ρ‡ΠΊΠΈ, Π»ΠΎΠ΄ΠΊΠΈ ΠΈ всСх сущностСй.

Пока Ρ‡Ρ‚ΠΎ Π²Ρ‹Π±Π΅Ρ€Π΅ΠΌ Π΅Π³ΠΎ Π½Π°ΡƒΠ³Π°Π΄ ΠΈ с запасом, Π²ΠΎΠ·ΡŒΠΌΡ‘ΠΌ 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

Он ΠΎΠ·Π½Π°Ρ‡Π°Π΅Ρ‚, Ρ‡Ρ‚ΠΎ Ρ€Π΅ΡˆΠ΅Π½ΠΈΠΉ Π΄Π΅ΠΉΡΡ‚Π²ΠΈΡ‚Π΅Π»ΡŒΠ½ΠΎ Π½Π΅Ρ‚.

Π’Π°ΠΊΠΈΠΌ ΠΎΠ±Ρ€Π°Π·ΠΎΠΌ ΠΌΡ‹ ΠΏΡ€ΠΎΠ³Ρ€Π°ΠΌΠΌΠ½Ρ‹ΠΌ способом Π΄ΠΎΠΊΠ°Π·Π°Π»ΠΈ Π½Π΅Π²ΠΎΠ·ΠΌΠΎΠΆΠ½ΠΎΡΡ‚ΡŒ ΠΏΠ΅Ρ€Π΅ΠΏΡ€Π°Π²Ρ‹ со всСядным Π²ΠΎΠ»ΠΊΠΎΠΌ, Π±Π΅Π· ΠΏΠΎΡ‚Π΅Ρ€ΡŒ для Ρ„Π΅Ρ€ΠΌΠ΅Ρ€Π°.

Если аудитория сочтёт эту Ρ‚Π΅ΠΌΠ°Ρ‚ΠΈΠΊΡƒ интСрСсной, Ρ‚ΠΎ Π² Π΄Π°Π»ΡŒΠ½Π΅ΠΉΡˆΠΈΡ… ΡΡ‚Π°Ρ‚ΡŒΡΡ… я расскаТу, ΠΊΠ°ΠΊ ΠΏΡ€Π΅Π²Ρ€Π°Ρ‚ΠΈΡ‚ΡŒ ΠΎΠ±Ρ‹Ρ‡Π½ΡƒΡŽ ΠΏΡ€ΠΎΠ³Ρ€Π°ΠΌΠΌΡƒ ΠΈΠ»ΠΈ Ρ„ΡƒΠ½ΠΊΡ†ΠΈΡŽ Π² совмСстимоС с Ρ„ΠΎΡ€ΠΌΠ°Π»ΡŒΠ½Ρ‹ΠΌΠΈ ΠΌΠ΅Ρ‚ΠΎΠ΄Π°ΠΌΠΈ ΡƒΡ€Π°Π²Π½Π΅Π½ΠΈΠ΅, ΠΈ Ρ€Π΅ΡˆΠΈΡ‚ΡŒ Π΅Π³ΠΎ, ΠΎΠ±Π½Π°Ρ€ΡƒΠΆΠΈΠ² Ρ‚Π΅ΠΌ самым ΠΊΠ°ΠΊ всС Π»Π΅Π³ΠΈΡ‚ΠΈΠΌΠ½Ρ‹Π΅ сцСнарии, Ρ‚Π°ΠΊ ΠΈ уязвимости. Π‘Π½Π°Ρ‡Π°Π»Π° Π½Π° этой ΠΆΠ΅ Π·Π°Π΄Π°Ρ‡Π΅, Π½ΠΎ прСдставлСнной ΡƒΠΆΠ΅ Π² Π²ΠΈΠ΄Π΅ ΠΏΡ€ΠΎΠ³Ρ€Π°ΠΌΠΌΡ‹, Π° Π·Π°Ρ‚Π΅ΠΌ постСпСнно услоТняя ΠΈ пСрСходя ΠΊ Π°ΠΊΡ‚ΡƒΠ°Π»ΡŒΠ½Ρ‹ΠΌ ΠΏΡ€ΠΈΠΌΠ΅Ρ€Π°ΠΌ ΠΈΠ· ΠΌΠΈΡ€Π° Ρ€Π°Π·Ρ€Π°Π±ΠΎΡ‚ΠΊΠΈ ПО.

Π‘Π»Π΅Π΄ΡƒΡŽΡ‰Π°Ρ ΡΡ‚Π°Ρ‚ΡŒΡ ΡƒΠΆΠ΅ Π³ΠΎΡ‚ΠΎΠ²Π°:
Π‘ΠΎΠ·Π΄Π°Π½ΠΈΠ΅ систСмы Ρ„ΠΎΡ€ΠΌΠ°Π»ΡŒΠ½ΠΎΠΉ Π²Π΅Ρ€ΠΈΡ„ΠΈΠΊΠ°Ρ†ΠΈΠΈ с нуля: ПишСм ΡΠΈΠΌΠ²ΠΎΠ»ΡŒΠ½ΡƒΡŽ VM Π½Π° PHP ΠΈ Python

Π’ Π½Π΅ΠΉ я ΠΏΠ΅Ρ€Π΅Ρ…ΠΎΠΆΡƒ ΠΎΡ‚ Ρ„ΠΎΡ€ΠΌΠ°Π»ΡŒΠ½ΠΎΠΉ Π²Π΅Ρ€ΠΈΡ„ΠΈΠΊΠ°Ρ†ΠΈΠΈ Π·Π°Π΄Π°Ρ‡, ΠΊ ΠΏΡ€ΠΎΠ³Ρ€Π°ΠΌΠΌΠ°ΠΌ, ΠΈ ΠΎΠΏΠΈΡΡ‹Π²Π°ΡŽ,
ΠΊΠ°ΠΊΠΈΠΌ ΠΎΠ±Ρ€Π°Π·ΠΎΠΌ ΠΌΠΎΠΆΠ½ΠΎ ΠΊΠΎΠ½Π²Π΅Ρ€Ρ‚ΠΈΡ€ΠΎΠ²Π°Ρ‚ΡŒ ΠΈΡ… Π² систСмы Ρ„ΠΎΡ€ΠΌΠ°Π»ΡŒΠ½Ρ‹Ρ… ΠΏΡ€Π°Π²ΠΈΠ» автоматичСски.

Π˜ΡΡ‚ΠΎΡ‡Π½ΠΈΠΊ: habr.com