{"id":32689,"date":"2019-10-31T21:48:24","date_gmt":"2019-10-31T18:48:24","guid":{"rendered":"https:\/\/prohoster.info\/blog\/formalnaya-verifikatsiya-na-primere-zadachi-o-volke-koze-i-kapuste\/"},"modified":"2019-10-31T21:48:24","modified_gmt":"2019-10-31T18:48:24","slug":"formalnaya-verifikatsiya-na-primere-zadachi-o-volke-koze-i-kapuste","status":"publish","type":"post","link":"https:\/\/prohoster.info\/de\/blog\/administrirovanie\/formalnaya-verifikatsiya-na-primere-zadachi-o-volke-koze-i-kapuste","title":{"rendered":"Formale Verifikation am Beispiel der Aufgabe mit dem Wolf, der Ziege und dem Kohl.","gt_translate_keys":[{"key":"rendered","format":"text"}]},"content":{"rendered":"

\u041d\u0430 \u043c\u043e\u0439 \u0432\u0437\u0433\u043b\u044f\u0434, \u0432 \u0440\u0443\u0441\u0441\u043a\u043e\u044f\u0437\u044b\u0447\u043d\u043e\u043c \u0441\u0435\u043a\u0442\u043e\u0440\u0435 \u0438\u043d\u0442\u0435\u0440\u043d\u0435\u0442\u0430 \u0442\u0435\u043c\u0430\u0442\u0438\u043a\u0430 \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u043e\u0439 \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438 \u043e\u0441\u0432\u0435\u0449\u0435\u043d\u0430 \u043d\u0435\u0434\u043e\u0441\u0442\u0430\u0442\u043e\u0447\u043d\u043e, \u0438 \u043e\u0441\u043e\u0431\u0435\u043d\u043d\u043e \u043d\u0435 \u0445\u0432\u0430\u0442\u0430\u0435\u0442 \u043f\u0440\u043e\u0441\u0442\u044b\u0445 \u0438 \u043d\u0430\u0433\u043b\u044f\u0434\u043d\u044b\u0445 \u043f\u0440\u0438\u043c\u0435\u0440\u043e\u0432.<\/p>\n

\u042f \u043f\u0440\u0438\u0432\u0435\u0434\u0443 \u0442\u0430\u043a\u043e\u0439 \u043f\u0440\u0438\u043c\u0435\u0440 \u0438\u0437 \u0437\u0430\u0440\u0443\u0431\u0435\u0436\u043d\u043e\u0433\u043e \u0438\u0441\u0442\u043e\u0447\u043d\u0438\u043a\u0430, \u0438 \u0434\u043e\u043f\u043e\u043b\u043d\u044e \u0441\u043e\u0431\u0441\u0442\u0432\u0435\u043d\u043d\u044b\u043c \u0440\u0435\u0448\u0435\u043d\u0438\u0435\u043c \u0438\u0437\u0432\u0435\u0441\u0442\u043d\u043e\u0439 \u0437\u0430\u0434\u0430\u0447\u0438 \u043e \u043f\u0435\u0440\u0435\u043f\u0440\u0430\u0432\u0435 \u0432\u043e\u043b\u043a\u0430, \u043a\u043e\u0437\u044b \u0438 \u043a\u0430\u043f\u0443\u0441\u0442\u044b \u043d\u0430 \u0434\u0440\u0443\u0433\u0443\u044e \u0441\u0442\u043e\u0440\u043e\u043d\u0443 \u0440\u0435\u043a\u0438.<\/p>\n

\u041d\u043e \u0432\u043d\u0430\u0447\u0430\u043b\u0435 \u0432\u043a\u0440\u0430\u0442\u0446\u0435 \u043e\u043f\u0438\u0448\u0443, \u0447\u0442\u043e \u0438\u0437 \u0441\u0435\u0431\u044f \u043f\u0440\u0435\u0434\u0441\u0442\u0430\u0432\u043b\u044f\u0435\u0442 \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u0430\u044f \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u044f \u0438 \u0437\u0430\u0447\u0435\u043c \u043e\u043d\u0430 \u043d\u0443\u0436\u043d\u0430.<\/p>\n

\u041f\u043e\u0434 \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u043e\u0439 \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0435\u0439 \u043e\u0431\u044b\u0447\u043d\u043e \u043f\u043e\u043d\u0438\u043c\u0430\u044e\u0442 \u043f\u0440\u043e\u0432\u0435\u0440\u043a\u0443 \u043e\u0434\u043d\u043e\u0439 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u044b \u043b\u0438\u0431\u043e \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u0430 \u0441 \u043f\u043e\u043c\u043e\u0449\u044c\u044e \u0434\u0440\u0443\u0433\u043e\u0439.<\/p>\n

\u042d\u0442\u043e \u043d\u0443\u0436\u043d\u043e \u0434\u043b\u044f \u0442\u043e\u0433\u043e, \u0447\u0442\u043e\u0431\u044b \u0443\u0434\u043e\u0441\u0442\u043e\u0432\u0435\u0440\u0438\u0442\u044c\u0441\u044f, \u0447\u0442\u043e \u043f\u043e\u0432\u0435\u0434\u0435\u043d\u0438\u0435 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u044b \u0441\u043e\u043e\u0442\u0432\u0435\u0442\u0441\u0442\u0432\u0443\u0435\u0442 \u043e\u0436\u0438\u0434\u0430\u0435\u043c\u043e\u043c\u0443, \u0430 \u0442\u0430\u043a\u0436\u0435 \u043e\u0431\u0435\u0441\u043f\u0435\u0447\u0438\u0442\u044c \u0435\u0451 \u0431\u0435\u0437\u043e\u043f\u0430\u0441\u043d\u043e\u0441\u0442\u044c.<\/p>\n

\u0424\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u0430\u044f \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u044f \u044f\u0432\u043b\u044f\u0435\u0442\u0441\u044f \u0441\u0430\u043c\u044b\u043c \u043c\u043e\u0449\u043d\u044b\u043c \u0441\u0440\u0435\u0434\u0441\u0442\u0432\u043e\u043c \u043f\u043e\u0438\u0441\u043a\u0430 \u0438 \u0443\u0441\u0442\u0440\u0430\u043d\u0435\u043d\u0438\u044f \u0443\u044f\u0437\u0432\u0438\u043c\u043e\u0441\u0442\u0435\u0439: \u043e\u043d\u0430 \u043f\u043e\u0437\u0432\u043e\u043b\u044f\u0435\u0442 \u043d\u0430\u0439\u0442\u0438 \u0432\u0441\u0435 \u0441\u0443\u0449\u0435\u0441\u0442\u0432\u0443\u044e\u0449\u0438\u0435 \u0434\u044b\u0440\u044b \u0438 \u0431\u0430\u0433\u0438 \u0432 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u0435, \u043b\u0438\u0431\u043e \u0436\u0435 \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u044c, \u0447\u0442\u043e \u0438\u0445 \u043d\u0435\u0442.
\n\u0421\u0442\u043e\u0438\u0442 \u0437\u0430\u043c\u0435\u0442\u0438\u0442\u044c, \u0447\u0442\u043e \u0432 \u043d\u0435\u043a\u043e\u0442\u043e\u0440\u044b\u0445 \u0441\u043b\u0443\u0447\u0430\u044f\u0445 \u044d\u0442\u043e \u0431\u044b\u0432\u0430\u0435\u0442 \u043d\u0435\u0432\u043e\u0437\u043c\u043e\u0436\u043d\u043e, \u043a\u0430\u043a \u043d\u0430\u043f\u0440\u0438\u043c\u0435\u0440, \u0432 \u0437\u0430\u0434\u0430\u0447\u0435 \u043e 8 \u0444\u0435\u0440\u0437\u044f\u0445 \u0441 \u0448\u0438\u0440\u0438\u043d\u043e\u0439 \u0434\u043e\u0441\u043a\u0438 1000 \u043a\u043b\u0435\u0442\u043e\u043a: \u0432\u0441\u0451 \u0443\u043f\u0438\u0440\u0430\u0435\u0442\u0441\u044f \u0432 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u0438\u0447\u0435\u0441\u043a\u0443\u044e \u0441\u043b\u043e\u0436\u043d\u043e\u0441\u0442\u044c \u043b\u0438\u0431\u043e \u043f\u0440\u043e\u0431\u043b\u0435\u043c\u0443 \u043e\u0441\u0442\u0430\u043d\u043e\u0432\u043a\u0438.<\/p>\n

\u041e\u0434\u043d\u0430\u043a\u043e \u0432 \u043b\u044e\u0431\u043e\u043c \u0441\u043b\u0443\u0447\u0430\u0435 \u0431\u0443\u0434\u0435\u0442 \u043f\u043e\u043b\u0443\u0447\u0435\u043d \u043e\u0434\u0438\u043d \u0438\u0437 \u0442\u0440\u0451\u0445 \u043e\u0442\u0432\u0435\u0442\u043e\u0432: \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u0430 \u043a\u043e\u0440\u0440\u0435\u043a\u0442\u043d\u0430, \u043d\u0435\u043a\u043e\u0440\u0440\u0435\u043a\u0442\u043d\u0430, \u0438\u043b\u0438 \u0436\u0435 \u2014 \u0432\u044b\u0447\u0438\u0441\u043b\u0438\u0442\u044c \u043e\u0442\u0432\u0435\u0442 \u043d\u0435 \u0443\u0434\u0430\u043b\u043e\u0441\u044c.<\/p>\n

\u0412 \u0441\u043b\u0443\u0447\u0430\u0435 \u043d\u0435\u0432\u043e\u0437\u043c\u043e\u0436\u043d\u043e\u0441\u0442\u0438 \u043d\u0430\u0445\u043e\u0436\u0434\u0435\u043d\u0438\u044f \u043e\u0442\u0432\u0435\u0442\u0430, \u0437\u0430\u0447\u0430\u0441\u0442\u0443\u044e \u043c\u043e\u0436\u043d\u043e \u043f\u0435\u0440\u0435\u0440\u0430\u0431\u043e\u0442\u0430\u0442\u044c \u043d\u0435\u044f\u0441\u043d\u044b\u0435 \u043c\u0435\u0441\u0442\u0430 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u044b, \u0443\u043c\u0435\u043d\u044c\u0448\u0438\u0432 \u0438\u0445 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u0438\u0447\u0435\u0441\u043a\u0443\u044e \u0441\u043b\u043e\u0436\u043d\u043e\u0441\u0442\u044c, \u0434\u043b\u044f \u0442\u043e\u0433\u043e \u0447\u0442\u043e\u0431\u044b \u043f\u043e\u043b\u0443\u0447\u0438\u0442\u044c \u043a\u043e\u043d\u043a\u0440\u0435\u0442\u043d\u044b\u0439 \u043e\u0442\u0432\u0435\u0442 \u0434\u0430 \u043b\u0438\u0431\u043e \u043d\u0435\u0442.<\/p>\n

\u0410 \u043f\u0440\u0438\u043c\u0435\u043d\u044f\u0435\u0442\u0441\u044f \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u0430\u044f \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u044f, \u043d\u0430\u043f\u0440\u0438\u043c\u0435\u0440, \u0432 \u044f\u0434\u0440\u0435 Windows \u0438 \u043e\u043f\u0435\u0440\u0430\u0446\u0438\u043e\u043d\u043d\u044b\u0445 \u0441\u0438\u0441\u0442\u0435\u043c\u0430\u0445 \u0431\u0435\u0441\u043f\u0438\u043b\u043e\u0442\u043d\u0438\u043a\u043e\u0432 Darpa, \u0434\u043b\u044f \u043e\u0431\u0435\u0441\u043f\u0435\u0447\u0435\u043d\u0438\u044f \u043c\u0430\u043a\u0441\u0438\u043c\u0430\u043b\u044c\u043d\u043e\u0433\u043e \u0443\u0440\u043e\u0432\u043d\u044f \u0437\u0430\u0449\u0438\u0442\u044b.<\/p>\n

\u041c\u044b \u0431\u0443\u0434\u0435\u043c \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u0442\u044c Z3Prover, \u043e\u0447\u0435\u043d\u044c \u043c\u043e\u0449\u043d\u044b\u0439 \u0438\u043d\u0441\u0442\u0440\u0443\u043c\u0435\u043d\u0442 \u0434\u043b\u044f \u0430\u0432\u0442\u043e\u043c\u0430\u0442\u0438\u0437\u0438\u0440\u043e\u0432\u0430\u043d\u043d\u043e\u0433\u043e \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u0430 \u0442\u0435\u043e\u0440\u0435\u043c \u0438 \u0440\u0435\u0448\u0435\u043d\u0438\u044f \u0443\u0440\u0430\u0432\u043d\u0435\u043d\u0438\u044f.<\/p>\n

\u041f\u0440\u0438\u0447\u0451\u043c Z3 \u0438\u043c\u0435\u043d\u043d\u043e \u0440\u0435\u0448\u0430\u0435\u0442 \u0443\u0440\u0430\u0432\u043d\u0435\u043d\u0438\u044f, \u0430 \u043d\u0435 \u043f\u043e\u0434\u0431\u0438\u0440\u0430\u0435\u0442 \u0438\u0445 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u044f \u0433\u0440\u0443\u0431\u044b\u043c \u0431\u0440\u0443\u0442\u0444\u043e\u0440\u0441\u043e\u043c.
\n\u042d\u0442\u043e \u043e\u0437\u043d\u0430\u0447\u0430\u0435\u0442, \u0447\u0442\u043e \u043e\u043d \u0441\u043f\u043e\u0441\u043e\u0431\u0435\u043d \u043d\u0430\u0445\u043e\u0434\u0438\u0442\u044c \u043e\u0442\u0432\u0435\u0442, \u0434\u0430\u0436\u0435 \u0432 \u0441\u043b\u0443\u0447\u0430\u044f\u0445 \u043a\u043e\u0433\u0434\u0430 \u043a\u043e\u043c\u0431\u0438\u043d\u0430\u0446\u0438\u0439 \u0432\u0445\u043e\u0434\u043d\u044b\u0445 \u0432\u0430\u0440\u0438\u0430\u043d\u0442\u043e\u0432 \u0438 10^100.<\/p>\n

\u0410 \u0432\u0435\u0434\u044c \u044d\u0442\u043e \u0432\u0441\u0435\u0433\u043e \u043b\u0438\u0448\u044c \u043e\u043a\u043e\u043b\u043e \u0434\u044e\u0436\u0438\u043d\u044b \u0432\u0445\u043e\u0434\u043d\u044b\u0445 \u0430\u0440\u0433\u0443\u043c\u0435\u043d\u0442\u043e\u0432 \u0442\u0438\u043f\u0430 Integer, \u0438 \u043f\u043e\u0434\u043e\u0431\u043d\u043e\u0435 \u0437\u0430\u0447\u0430\u0441\u0442\u0443\u044e \u0432\u0441\u0442\u0440\u0435\u0447\u0430\u0435\u0442\u0441\u044f \u043d\u0430 \u043f\u0440\u0430\u043a\u0442\u0438\u043a\u0435.<\/p>\n

\u0417\u0430\u0434\u0430\u0447\u0430 \u043e 8 \u0444\u0435\u0440\u0437\u044f\u0445 (\u0412\u0437\u044f\u0442\u0430 \u0438\u0437 \u0430\u043d\u0433\u043b\u043e\u044f\u0437\u044b\u0447\u043d\u043e\u0433\u043e \u043c\u0430\u043d\u0443\u0430\u043b\u0430<\/a><\/noindex>).<\/p>\n

\"\u0424\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u0430\u044f
\n<\/a><\/noindex><\/p>\n

# We know each queen must be in a different row.\n# So, we represent each queen by a single integer: the column position\nQ = [ Int('Q_%i' % (i + 1)) for i in range(8) ]\n\n# Each queen is in a column {1, ... 8 }\nval_c = [ And(1 <= Q[i], Q[i] <= 8) for i in range(8) ]\n\n# At most one queen per column\ncol_c = [ Distinct(Q) ]\n\n# Diagonal constraint\ndiag_c = [ If(i == j,\n              True,\n              And(Q[i] - Q[j] != i - j, Q[i] - Q[j] != j - i))\n           for i in range(8) for j in range(i) ]\n\nsolve(val_c + col_c + diag_c)\n<\/code><\/pre>\n
\n\u0417\u0430\u043f\u0443\u0441\u0442\u0438\u0432 Z3, \u043c\u044b \u043f\u043e\u043b\u0443\u0447\u0430\u0435\u043c \u0440\u0435\u0448\u0435\u043d\u0438\u0435: <\/p>\n
[Q_5 = 1,\n Q_8 = 7,\n Q_3 = 8,\n Q_2 = 2,\n Q_6 = 3,\n Q_4 = 6,\n Q_7 = 5,\n Q_1 = 4]\n<\/code><\/pre>\n
\n\u0417\u0430\u0434\u0430\u0447\u0430 \u043e \u0444\u0435\u0440\u0437\u044f\u0445 \u0441\u0440\u0430\u0432\u043d\u0438\u043c\u0430 \u0441 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u043e\u0439, \u043a\u043e\u0442\u043e\u0440\u0430\u044f \u043f\u0440\u0438\u043d\u0438\u043c\u0430\u0435\u0442 \u043d\u0430 \u0432\u0445\u043e\u0434 \u043a\u043e\u043e\u0440\u0434\u0438\u043d\u0430\u0442\u044b 8 \u0444\u0435\u0440\u0437\u0435\u0439 \u0438 \u0432\u044b\u0432\u043e\u0434\u0438\u0442 \u043e\u0442\u0432\u0435\u0442, \u0431\u044c\u044e\u0442 \u043b\u0438 \u0444\u0435\u0440\u0437\u0438 \u0434\u0440\u0443\u0433 \u0434\u0440\u0443\u0433\u0430.<\/p>\n
\u0415\u0441\u043b\u0438 \u0431\u044b \u043c\u044b \u0440\u0435\u0448\u0430\u043b\u0438 \u0442\u0430\u043a\u0443\u044e \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u0443 \u0441 \u043f\u043e\u043c\u043e\u0449\u044c\u044e \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u043e\u0439 \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438, \u0442\u043e \u043f\u043e \u0441\u0440\u0430\u0432\u043d\u0435\u043d\u0438\u044e \u0441 \u0437\u0430\u0434\u0430\u0447\u0435\u0439, \u043d\u0430\u043c \u0431\u044b \u043f\u0440\u043e\u0441\u0442\u043e \u043f\u043e\u043d\u0430\u0434\u043e\u0431\u0438\u043b\u043e\u0441\u044c \u0441\u0434\u0435\u043b\u0430\u0442\u044c \u0435\u0449\u0451 \u043e\u0434\u0438\u043d \u0448\u0430\u0433 \u0432 \u0432\u0438\u0434\u0435 \u043f\u0440\u0435\u043e\u0431\u0440\u0430\u0437\u043e\u0432\u0430\u043d\u0438\u044f \u043a\u043e\u0434\u0430 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u044b \u0432 \u0443\u0440\u0430\u0432\u043d\u0435\u043d\u0438\u0435: \u043e\u043d\u043e \u0431\u044b \u043f\u043e\u043b\u0443\u0447\u0438\u043b\u043e\u0441\u044c \u043f\u043e \u0441\u0432\u043e\u0435\u0439 \u0441\u0443\u0442\u0438 \u0438\u0434\u0435\u043d\u0442\u0438\u0447\u043d\u044b\u043c \u043d\u0430\u0448\u0435\u043c\u0443 (\u0440\u0430\u0437\u0443\u043c\u0435\u0435\u0442\u0441\u044f, \u0435\u0441\u043b\u0438 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u0430 \u043d\u0430\u043f\u0438\u0441\u0430\u043d\u0430 \u0431\u0435\u0437\u043e\u0448\u0438\u0431\u043e\u0447\u043d\u043e).<\/p>\n
\u041f\u0440\u0430\u043a\u0442\u0438\u0447\u0435\u0441\u043a\u0438 \u0442\u043e \u0436\u0435 \u0441\u0430\u043c\u043e\u0435 \u0431\u0443\u0434\u0435\u0442 \u043f\u0440\u043e\u0438\u0441\u0445\u043e\u0434\u0438\u0442\u044c \u0432 \u0441\u043b\u0443\u0447\u0430\u0435 \u043f\u043e\u0438\u0441\u043a\u0430 \u0443\u044f\u0437\u0432\u0438\u043c\u043e\u0441\u0442\u0435\u0439: \u043c\u044b \u043b\u0438\u0448\u044c \u0437\u0430\u0434\u0430\u0435\u043c \u043d\u0443\u0436\u043d\u044b\u0435 \u043d\u0430\u043c \u0432\u044b\u0445\u043e\u0434\u043d\u044b\u0435 \u0443\u0441\u043b\u043e\u0432\u0438\u044f, \u043d\u0430\u043f\u0440\u0438\u043c\u0435\u0440 \u043f\u0430\u0440\u043e\u043b\u044c \u0430\u0434\u043c\u0438\u043d\u0430, \u043f\u0440\u0435\u043e\u0431\u0440\u0430\u0437\u0443\u0435\u043c \u0438\u0441\u0445\u043e\u0434\u043d\u044b\u0439 \u0438\u043b\u0438 \u0434\u0435\u043a\u043e\u043c\u043f\u0438\u043b\u0438\u0440\u043e\u0432\u0430\u043d\u043d\u044b\u0439 \u043a\u043e\u0434 \u0432 \u0441\u043e\u0432\u043c\u0435\u0441\u0442\u0438\u043c\u044b\u0435 \u0441 \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0435\u0439 \u0443\u0440\u0430\u0432\u043d\u0435\u043d\u0438\u044f, \u0438 \u0437\u0430\u0442\u0435\u043c \u043f\u043e\u043b\u0443\u0447\u0430\u0435\u043c \u043e\u0442\u0432\u0435\u0442, \u043a\u0430\u043a\u0438\u0435 \u0434\u0430\u043d\u043d\u044b\u0435 \u043d\u0443\u0436\u043d\u043e \u043f\u043e\u0434\u0430\u0442\u044c \u043d\u0430 \u0432\u0445\u043e\u0434 \u0434\u043b\u044f \u0434\u043e\u0441\u0442\u0438\u0436\u0435\u043d\u0438\u044f \u0446\u0435\u043b\u0438.<\/p>\n
\u041d\u0430 \u043c\u043e\u0439 \u0432\u0437\u0433\u043b\u044f\u0434, \u0437\u0430\u0434\u0430\u0447\u0430 \u043e \u0432\u043e\u043b\u043a\u0435, \u043a\u043e\u0437\u0435 \u0438 \u043a\u0430\u043f\u0443\u0441\u0442\u0435 \u0435\u0449\u0451 \u0438\u043d\u0442\u0435\u0440\u0435\u0441\u043d\u0435\u0439, \u0442\u0430\u043a \u043a\u0430\u043a \u0434\u043b\u044f \u0435\u0451 \u0440\u0435\u0448\u0435\u043d\u0438\u044f \u043d\u0443\u0436\u043d\u043e \u0443\u0436\u0435 \u043c\u043d\u043e\u0433\u043e (7) \u0448\u0430\u0433\u043e\u0432.<\/p>\n
\u0415\u0441\u043b\u0438 \u0437\u0430\u0434\u0430\u0447\u0430 \u043e \u0444\u0435\u0440\u0437\u044f\u0445 \u0441\u0440\u0430\u0432\u043d\u0438\u043c\u0430 \u0441\u043e \u0432\u0430\u0440\u0438\u0430\u043d\u0442\u043e\u043c, \u043a\u043e\u0433\u0434\u0430 \u043c\u043e\u0436\u043d\u043e \u043f\u0440\u043e\u043d\u0438\u043a\u043d\u0443\u0442\u044c \u043d\u0430 \u0441\u0435\u0440\u0432\u0435\u0440 \u0441 \u043f\u043e\u043c\u043e\u0449\u044c\u044e \u043e\u0434\u043d\u043e\u0433\u043e GET \u0438\u043b\u0438 POST \u0437\u0430\u043f\u0440\u043e\u0441\u0430, \u0442\u043e \u0432\u043e\u043b\u043a, \u043a\u043e\u0437\u0430 \u0438 \u043a\u0430\u043f\u0443\u0441\u0442\u0430 \u0434\u0435\u043c\u043e\u043d\u0441\u0442\u0440\u0438\u0440\u0443\u0435\u0442 \u043f\u0440\u0438\u043c\u0435\u0440 \u0438\u0437 \u0433\u043e\u0440\u0430\u0437\u0434\u043e \u0431\u043e\u043b\u0435\u0435 \u0441\u043b\u043e\u0436\u043d\u043e\u0439 \u0438 \u0440\u0430\u0441\u043f\u0440\u043e\u0441\u0442\u0440\u0430\u043d\u0451\u043d\u043d\u043e\u0439 \u043a\u0430\u0442\u0435\u0433\u043e\u0440\u0438\u0438, \u0432 \u043a\u043e\u0442\u043e\u0440\u043e\u0439 \u0446\u0435\u043b\u0438 \u043c\u043e\u0436\u043d\u043e \u0434\u043e\u0441\u0442\u0438\u0447\u044c \u0442\u043e\u043b\u044c\u043a\u043e \u043d\u0435\u0441\u043a\u043e\u043b\u044c\u043a\u0438\u043c\u0438 \u0437\u0430\u043f\u0440\u043e\u0441\u0430\u043c.<\/p>\n
\u042d\u0442\u043e \u0441\u0440\u0430\u0432\u043d\u0438\u043c\u043e, \u043d\u0430\u043f\u0440\u0438\u043c\u0435\u0440, \u0441\u043e \u0441\u0446\u0435\u043d\u0430\u0440\u0438\u0435\u043c, \u0433\u0434\u0435 \u043d\u0443\u0436\u043d\u043e \u043d\u0430\u0439\u0442\u0438 SQL \u0438\u043d\u044c\u0435\u043a\u0446\u0438\u044e, \u0437\u0430\u043f\u0438\u0441\u0430\u0442\u044c \u0447\u0435\u0440\u0435\u0437 \u043d\u0435\u0451 \u0444\u0430\u0439\u043b, \u043f\u043e\u0441\u043b\u0435 \u043f\u043e\u0432\u044b\u0441\u0438\u0442\u044c \u0441\u0432\u043e\u0438 \u043f\u0440\u0430\u0432\u0430 \u0438 \u0442\u043e\u043b\u044c\u043a\u043e \u0437\u0430\u0442\u0435\u043c \u043f\u043e\u043b\u0443\u0447\u0438\u0442\u044c \u043f\u0430\u0440\u043e\u043b\u044c.<\/p>\n
\u0423\u0441\u043b\u043e\u0432\u0438\u044f \u0437\u0430\u0434\u0430\u0447\u0438 \u0438 \u0435\u0451 \u0440\u0430\u0437\u0433\u0430\u0434\u043a\u0430<\/b>\u0424\u0435\u0440\u043c\u0435\u0440\u0443 \u043d\u0443\u0436\u043d\u043e \u043f\u0435\u0440\u0435\u0432\u0435\u0437\u0442\u0438 \u0447\u0435\u0440\u0435\u0437 \u0440\u0435\u043a\u0443 \u0432\u043e\u043b\u043a\u0430, \u043a\u043e\u0437\u0443 \u0438 \u043a\u0430\u043f\u0443\u0441\u0442\u0443. \u0423 \u0444\u0435\u0440\u043c\u0435\u0440\u0430 \u0435\u0441\u0442\u044c \u043b\u043e\u0434\u043a\u0430, \u0432 \u043a\u043e\u0442\u043e\u0440\u043e\u0439 \u043c\u043e\u0436\u0435\u0442 \u043f\u043e\u043c\u0435\u0441\u0442\u0438\u0442\u044c\u0441\u044f, \u043a\u0440\u043e\u043c\u0435 \u0441\u0430\u043c\u043e\u0433\u043e \u043a\u0440\u0435\u0441\u0442\u044c\u044f\u043d\u0438\u043d\u0430, \u0442\u043e\u043b\u044c\u043a\u043e \u043e\u0434\u0438\u043d \u043e\u0431\u044a\u0435\u043a\u0442. \u0412\u043e\u043b\u043a \u0441\u044a\u0435\u0441\u0442 \u043a\u043e\u0437\u0443, \u0430 \u043a\u043e\u0437\u0430 \u0441\u044a\u0435\u0441\u0442 \u043a\u0430\u043f\u0443\u0441\u0442\u0443, \u0435\u0441\u043b\u0438 \u0444\u0435\u0440\u043c\u0435\u0440 \u043e\u0441\u0442\u0430\u0432\u0438\u0442 \u0438\u0445 \u0431\u0435\u0437 \u043f\u0440\u0438\u0441\u043c\u043e\u0442\u0440\u0430.<\/p>\n
\u0420\u0430\u0437\u0433\u0430\u0434\u043a\u0430 \u0432 \u0442\u043e\u043c, \u0447\u0442\u043e \u043d\u0430 4 \u0448\u0430\u0433\u0435 \u0444\u0435\u0440\u043c\u0435\u0440\u0443 \u043d\u0443\u0436\u043d\u043e \u0431\u0443\u0434\u0435\u0442 \u043e\u0442\u0432\u0435\u0437\u0442\u0438 \u043a\u043e\u0437\u0443 \u043e\u0431\u0440\u0430\u0442\u043d\u043e.
\n\u0422\u0435\u043f\u0435\u0440\u044c \u043f\u0440\u0438\u0441\u0442\u0443\u043f\u0438\u043c \u043a \u0440\u0435\u0448\u0435\u043d\u0438\u044e \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u043d\u044b\u043c \u0441\u043f\u043e\u0441\u043e\u0431\u043e\u043c.<\/p>\n
\u041e\u0431\u043e\u0437\u043d\u0430\u0447\u0438\u043c \u0444\u0435\u0440\u043c\u0435\u0440\u0430, \u0432\u043e\u043b\u043a\u0430, \u043a\u043e\u0437\u0443 \u0438 \u043a\u0430\u043f\u0443\u0441\u0442\u0443 \u043a\u0430\u043a 4 \u043f\u0435\u0440\u0435\u043c\u0435\u043d\u043d\u044b\u0435, \u043a\u043e\u0442\u043e\u0440\u044b\u0435 \u043f\u0440\u0438\u043d\u0438\u043c\u0430\u044e\u0442 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0435 \u0442\u043e\u043b\u044c\u043a\u043e 0 \u0438\u043b\u0438 1. \u041d\u043e\u043b\u044c \u043e\u0437\u043d\u0430\u0447\u0430\u0435\u0442 \u0447\u0442\u043e \u043e\u043d\u0438 \u043d\u0430 \u043b\u0435\u0432\u043e\u043c \u0431\u0435\u0440\u0435\u0433\u0443, \u0430 \u0435\u0434\u0438\u043d\u0438\u0446\u0430- \u0447\u0442\u043e \u043d\u0430 \u043f\u0440\u0430\u0432\u043e\u043c.<\/p>\n
import json\nfrom z3 import *\ns = Solver()\nNum= 8\n\nHuman = [ Int('Human_%i' % (i + 1)) for i in range(Num) ]\nWolf = [ Int('Wolf_%i' % (i + 1)) for i in range(Num) ]\nGoat = [ Int('Goat_%i' % (i + 1)) for i in range(Num) ]\nCabbage = [ Int('Cabbage_%i' % (i + 1)) for i in range(Num) ]\n\n# Each creature can be only on left (0) or right side (1) on every state\nHumanSide = [ Or(Human[i] == 0, Human[i] == 1) for i in range(Num) ]\nWolfSide = [ Or(Wolf[i] == 0, Wolf[i] == 1) for i in range(Num) ]\nGoatSide = [ Or(Goat[i] == 0, Goat[i] == 1) for i in range(Num) ]\nCabbageSide = [ Or(Cabbage[i] == 0, Cabbage[i] == 1) for i in range(Num) ]\nSide = HumanSide+WolfSide+GoatSide+CabbageSide\n<\/code><\/pre>\n
\nNum \u2014 \u044d\u0442\u043e \u0447\u0438\u0441\u043b\u043e \u0448\u0430\u0433\u043e\u0432 \u043d\u0435\u043e\u0431\u0445\u043e\u0434\u0438\u043c\u044b\u0445 \u0434\u043b\u044f \u0440\u0435\u0448\u0435\u043d\u0438\u044f. \u041a\u0430\u0436\u0434\u044b\u0439 \u0448\u0430\u0433 \u043f\u0440\u0435\u0434\u0441\u0442\u0430\u0432\u043b\u044f\u0435\u0442 \u0441\u043e\u0431\u043e\u0439 \u0441\u043e\u0441\u0442\u043e\u044f\u043d\u0438\u0435 \u0440\u0435\u0447\u043a\u0438, \u043b\u043e\u0434\u043a\u0438 \u0438 \u0432\u0441\u0435\u0445 \u0441\u0443\u0449\u043d\u043e\u0441\u0442\u0435\u0439.<\/p>\n
\u041f\u043e\u043a\u0430 \u0447\u0442\u043e \u0432\u044b\u0431\u0435\u0440\u0435\u043c \u0435\u0433\u043e \u043d\u0430\u0443\u0433\u0430\u0434 \u0438 \u0441 \u0437\u0430\u043f\u0430\u0441\u043e\u043c, \u0432\u043e\u0437\u044c\u043c\u0451\u043c 10.<\/p>\n
\u041a\u0430\u0436\u0434\u0430\u044f \u0441\u0443\u0449\u043d\u043e\u0441\u0442\u044c \u043f\u0440\u0435\u0434\u0441\u0442\u0430\u0432\u043b\u0435\u043d\u0430 \u0432 10 \u044d\u043a\u0437\u0435\u043c\u043f\u043b\u044f\u0440\u0430\u0445 \u2014 \u044d\u0442\u043e \u0435\u0451 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0435 \u043d\u0430 \u043a\u0430\u0436\u0434\u043e\u043c \u0438\u0437 10 \u0448\u0430\u0433\u043e\u0432.<\/p>\n
\u0422\u0435\u043f\u0435\u0440\u044c \u0437\u0430\u0434\u0430\u0434\u0438\u043c \u0443\u0441\u043b\u043e\u0432\u0438\u044f \u0434\u043b\u044f \u0441\u0442\u0430\u0440\u0442\u0430 \u0438 \u0444\u0438\u043d\u0438\u0448\u0430.<\/p>\n
Start = [ Human[0] == 0, Wolf[0] == 0, Goat[0] == 0, Cabbage[0] == 0 ]\nFinish = [ Human[9] == 1, Wolf[9] == 1, Goat[9] == 1, Cabbage[9] == 1 ]\n<\/code><\/pre>\n
\n\u0417\u0430\u0442\u0435\u043c \u0437\u0430\u0434\u0430\u0434\u0438\u043c \u0443\u0441\u043b\u043e\u0432\u0438\u044f, \u0433\u0434\u0435 \u0432\u043e\u043b\u043a \u0441\u044a\u0435\u0434\u0430\u0435\u0442 \u043a\u043e\u0437\u0443, \u0438\u043b\u0438 \u043a\u043e\u0437\u0430 \u043a\u0430\u043f\u0443\u0441\u0442\u0430, \u043a\u0430\u043a \u043e\u0433\u0440\u0430\u043d\u0438\u0447\u0435\u043d\u0438\u044f \u0432 \u0443\u0440\u0430\u0432\u043d\u0435\u043d\u0438\u0438.
\n(\u0412 \u043f\u0440\u0438\u0441\u0443\u0442\u0441\u0442\u0432\u0438\u0438 \u0444\u0435\u0440\u043c\u0435\u0440\u0430 \u0430\u0433\u0440\u0435\u0441\u0441\u0438\u044f \u043d\u0435\u0432\u043e\u0437\u043c\u043e\u0436\u043d\u0430)<\/p>\n
# Wolf cant stand with goat, and goat with cabbage without human. Not 2, not 0 which means that they are one the same side\nSafe = [ And( Or(Wolf[i] != Goat[i], Wolf[i] == Human[i]), Or(Goat[i] != Cabbage[i], Goat[i] == Human[i])) for i in range(Num) ]\n<\/code><\/pre>\n
\n\u0418 \u043d\u0430\u043a\u043e\u043d\u0435\u0446, \u0437\u0430\u0434\u0430\u0434\u0438\u043c \u0432\u0441\u0435 \u0432\u043e\u0437\u043c\u043e\u0436\u043d\u044b\u0435 \u0434\u0435\u0439\u0441\u0442\u0432\u0438\u044f \u0444\u0435\u0440\u043c\u0435\u0440\u0430 \u043f\u0440\u0438 \u043f\u0435\u0440\u0435\u043f\u0440\u0430\u0432\u0435 \u0442\u0443\u0434\u0430 \u0438\u043b\u0438 \u043e\u0431\u0440\u0430\u0442\u043d\u043e.
\n\u041e\u043d \u043c\u043e\u0436\u0435\u0442 \u043a\u0430\u043a \u0432\u0437\u044f\u0442\u044c \u0441 \u0441\u043e\u0431\u043e\u0439 \u0432\u043e\u043b\u043a\u0430, \u043a\u043e\u0437\u0443 \u0438\u043b\u0438 \u043a\u0430\u043f\u0443\u0441\u0442\u0443, \u0438\u043b\u0438 \u0436\u0435 \u043d\u0438\u043a\u043e\u0433\u043e \u043d\u0435 \u0431\u0440\u0430\u0442\u044c, \u0438\u043b\u0438 \u0436\u0435 \u0432\u043e\u043e\u0431\u0449\u0435 \u043d\u0438\u043a\u0443\u0434\u0430 \u043d\u0435 \u043f\u043b\u044b\u0442\u044c.<\/p>\n
\u0420\u0430\u0437\u0443\u043c\u0435\u0435\u0442\u0441\u044f, \u0431\u0435\u0437 \u0444\u0435\u0440\u043c\u0435\u0440\u0430 \u043d\u0438\u043a\u0442\u043e \u043f\u0435\u0440\u0435\u043f\u0440\u0430\u0432\u0438\u0442\u044c\u0441\u044f \u043d\u0435 \u043c\u043e\u0436\u0435\u0442.<\/p>\n
\u042d\u0442\u043e \u0431\u0443\u0434\u0435\u0442 \u0432\u044b\u0440\u0430\u0436\u0435\u043d\u043e \u0442\u0435\u043c, \u0447\u0442\u043e \u043a\u0430\u0436\u0434\u043e\u0435 \u0441\u043b\u0435\u0434\u0443\u044e\u0449\u0435\u0435 \u0441\u043e\u0441\u0442\u043e\u044f\u043d\u0438\u0435 \u0440\u0435\u0447\u043a\u0438, \u043b\u043e\u0434\u043a\u0438 \u0438 \u0441\u0443\u0449\u043d\u043e\u0441\u0442\u0435\u0439 \u043c\u043e\u0436\u0435\u0442 \u043e\u0442\u043b\u0438\u0447\u0430\u0442\u044c\u0441\u044f \u043e\u0442 \u043f\u0440\u0435\u0434\u044b\u0434\u0443\u0449\u0435\u0433\u043e \u0442\u043e\u043b\u044c\u043a\u043e \u0441\u0442\u0440\u043e\u0433\u043e \u043e\u0433\u0440\u0430\u043d\u0438\u0447\u0435\u043d\u043d\u044b\u043c \u043e\u0431\u0440\u0430\u0437\u043e\u043c.<\/p>\n
\u041d\u0435 \u0431\u043e\u043b\u0435\u0435 \u0447\u0435\u043c \u043d\u0430 2 \u0431\u0438\u0442\u0430, \u0438 \u0441\u043e \u043c\u043d\u043e\u0436\u0435\u0441\u0442\u0432\u043e\u043c \u0434\u0440\u0443\u0433\u0438\u0445 \u043b\u0438\u043c\u0438\u0442\u043e\u0432, \u0442\u0430\u043a \u043a\u0430\u043a \u0444\u0435\u0440\u043c\u0435\u0440 \u043c\u043e\u0436\u0435\u0442 \u043f\u0435\u0440\u0435\u0432\u0435\u0437\u0442\u0438 \u0437\u0430 \u0440\u0430\u0437 \u043b\u0438\u0448\u044c \u043e\u0434\u043d\u0443 \u0441\u0443\u0449\u043d\u043e\u0441\u0442\u044c \u0438 \u043d\u0435 \u0432\u0441\u0435\u0445 \u043c\u043e\u0436\u043d\u043e \u043e\u0441\u0442\u0430\u0432\u0438\u0442\u044c \u0432\u043c\u0435\u0441\u0442\u0435.<\/p>\n
Travel = [ Or(\nAnd(Human[i] == Human[i+1] + 1, Wolf[i] == Wolf[i+1] + 1, Goat[i] == Goat[i+1], Cabbage[i] == Cabbage[i+1]),\nAnd(Human[i] == Human[i+1] + 1, Goat[i] == Goat[i+1] + 1, Wolf[i] == Wolf[i+1], Cabbage[i] == Cabbage[i+1]),\nAnd(Human[i] == Human[i+1] + 1, Cabbage[i] == Cabbage[i+1] + 1, Wolf[i] == Wolf[i+1], Goat[i] == Goat[i+1]),\nAnd(Human[i] == Human[i+1] - 1, Wolf[i] == Wolf[i+1] - 1, Goat[i] == Goat[i+1], Cabbage[i] == Cabbage[i+1]),\nAnd(Human[i] == Human[i+1] - 1, Goat[i] == Goat[i+1] - 1, Wolf[i] == Wolf[i+1], Cabbage[i] == Cabbage[i+1]),\nAnd(Human[i] == Human[i+1] - 1, Cabbage[i] == Cabbage[i+1] - 1, Wolf[i] == Wolf[i+1], Goat[i] == Goat[i+1]),\nAnd(Wolf[i] == Wolf[i+1], Goat[i] == Goat[i+1], Cabbage[i] == Cabbage[i+1])) for i in range(Num-1) ]\n<\/code><\/pre>\n
\n\u0417\u0430\u043f\u0443\u0441\u0442\u0438\u043c \u0440\u0435\u0448\u0435\u043d\u0438\u0435.<\/p>\n
solve(Side + Start + Finish + Safe + Travel)\n<\/code><\/pre>\n
\n\u0418 \u043c\u044b \u043f\u043e\u043b\u0443\u0447\u0430\u0435\u043c \u043e\u0442\u0432\u0435\u0442!<\/p>\n
Z3 \u043d\u0430\u0448\u0451\u043b \u043d\u0435\u043f\u0440\u043e\u0442\u0438\u0432\u043e\u0440\u0435\u0447\u0438\u0432\u0443\u044e, \u0438 \u0443\u0434\u043e\u0432\u043b\u0435\u0442\u0432\u043e\u0440\u044f\u044e\u0449\u0443\u044e \u0432\u0441\u0435\u043c \u0443\u0441\u043b\u043e\u0432\u0438\u044f\u043c \u0441\u043e\u0432\u043e\u043a\u0443\u043f\u043d\u043e\u0441\u0442\u044c \u0441\u043e\u0441\u0442\u043e\u044f\u043d\u0438\u0439.
\n\u042d\u0434\u0430\u043a\u0438\u0439 \u0447\u0435\u0442\u044b\u0440\u0451\u0445\u043c\u0435\u0440\u043d\u044b\u0439 \u0441\u043b\u0435\u043f\u043e\u043a \u043f\u0440\u043e\u0441\u0442\u0440\u0430\u043d\u0441\u0442\u0432\u0430-\u0432\u0440\u0435\u043c\u0435\u043d\u0438.<\/p>\n
\u0414\u0430\u0432\u0430\u0439\u0442\u0435 \u0440\u0430\u0437\u0431\u0435\u0440\u0451\u043c\u0441\u044f, \u0447\u0442\u043e \u0436\u0435 \u043f\u0440\u043e\u0438\u0437\u043e\u0448\u043b\u043e.<\/p>\n
\u041c\u044b \u0432\u0438\u0434\u0438\u043c, \u0447\u0442\u043e \u0432 \u0438\u0442\u043e\u0433\u0435 \u0432\u0441\u0435 \u043f\u0435\u0440\u0435\u043f\u0440\u0430\u0432\u0438\u043b\u0438\u0441\u044c, \u0432\u043e\u0442 \u0442\u043e\u043b\u044c\u043a\u043e \u0432\u043d\u0430\u0447\u0430\u043b\u0435 \u043d\u0430\u0448 \u0444\u0435\u0440\u043c\u0435\u0440 \u0440\u0435\u0448\u0438\u043b \u043e\u0442\u0434\u043e\u0445\u043d\u0443\u0442\u044c, \u0438 \u043d\u0438\u043a\u0443\u0434\u0430 \u043d\u0430 \u043f\u0435\u0440\u0432\u044b\u0445 2 \u0448\u0430\u0433\u0430\u0445 \u043d\u0435 \u043f\u043b\u044b\u0432\u0451\u0442.<\/p>\n
Human_2 = 0\nHuman_3 = 0\n<\/code><\/pre>\n
\n\u042d\u0442\u043e \u0433\u043e\u0432\u043e\u0440\u0438\u0442 \u043e \u0442\u043e\u043c, \u0447\u0442\u043e \u0447\u0438\u0441\u043b\u043e \u0441\u043e\u0441\u0442\u043e\u044f\u043d\u0438\u0439 \u043c\u044b \u0432\u044b\u0431\u0440\u0430\u043b\u0438 \u0438\u0437\u0431\u044b\u0442\u043e\u0447\u043d\u043e\u0435, \u0438 8 \u0431\u0443\u0434\u0435\u0442 \u0432\u043f\u043e\u043b\u043d\u0435 \u0434\u043e\u0441\u0442\u0430\u0442\u043e\u0447\u043d\u043e.<\/p>\n
\u0412 \u043d\u0430\u0448\u0435\u043c \u0441\u043b\u0443\u0447\u0430\u0435 \u0444\u0435\u0440\u043c\u0435\u0440 \u043f\u043e\u0441\u0442\u0443\u043f\u0438\u043b \u0442\u0430\u043a: \u0441\u0442\u0430\u0440\u0442, \u043e\u0442\u0434\u044b\u0445, \u043e\u0442\u0434\u044b\u0445, \u043f\u0435\u0440\u0435\u043f\u0440\u0430\u0432\u0430 \u043a\u043e\u0437\u044b, \u043f\u0435\u0440\u0435\u043f\u0440\u0430\u0432\u0430 \u043e\u0431\u0440\u0430\u0442\u043d\u043e, \u043f\u0435\u0440\u0435\u043f\u0440\u0430\u0432\u0430 \u043a\u0430\u043f\u0443\u0441\u0442\u044b, \u0432\u043e\u0437\u0432\u0440\u0430\u0442 \u0441 \u043a\u043e\u0437\u043e\u0439, \u043f\u0435\u0440\u0435\u043f\u0440\u0430\u0432\u0430 \u0432\u043e\u043b\u043a\u0430, \u0432\u043e\u0437\u0432\u0440\u0430\u0442 \u043e\u0431\u0440\u0430\u0442\u043d\u043e \u0432 \u043e\u0434\u0438\u043d\u043e\u0447\u043a\u0443, \u043f\u043e\u0432\u0442\u043e\u0440\u043d\u0430\u044f \u0434\u043e\u0441\u0442\u0430\u0432\u043a\u0430 \u043a\u043e\u0437\u044b.<\/p>\n
\u041d\u043e \u0432 \u0438\u0442\u043e\u0433\u0435 \u0437\u0430\u0434\u0430\u0447\u0430 \u0440\u0435\u0448\u0435\u043d\u0430.<\/p>\n
#\u0421\u0442\u0430\u0440\u0442.\n Human_1 = 0\n Wolf_1 = 0\n Goat_1 = 0\n Cabbage_1 = 0\n \n #\u0424\u0435\u0440\u043c\u0435\u0440 \u043e\u0442\u0434\u044b\u0445\u0430\u0435\u0442.\n Human_2 = 0\n Wolf_2 = 0\n Goat_2 = 0\n Cabbage_2 = 0\n \n #\u0424\u0435\u0440\u043c\u0435\u0440 \u043e\u0442\u0434\u044b\u0445\u0430\u0435\u0442.\n Human_3 = 0\n Wolf_3 = 0\n Goat_3 = 0\n Cabbage_3 = 0\n \n #\u0424\u0435\u0440\u043c\u0435\u0440 \u043e\u0442\u0432\u043e\u0437\u0438\u0442 \u043a\u043e\u0437\u0443 \u043d\u0430 \u043d\u0443\u0436\u043d\u044b\u0439 \u0431\u0435\u0440\u0435\u0433.\n Human_4 = 1\n Wolf_4 = 0\n Goat_4 = 1\n Cabbage_4 = 0\n \n #\u0424\u0435\u0440\u043c\u0435\u0440 \u0432\u043e\u0437\u0432\u0440\u0430\u0449\u0430\u0435\u0442\u0441\u044f.\n Human_5 = 0\n Wolf_5 = 0\n Goat_5 = 1\n Cabbage_5 = 0\n \n #\u0424\u0435\u0440\u043c\u0435\u0440 \u043e\u0442\u0432\u043e\u0437\u0438\u0442 \u043a\u0430\u043f\u0443\u0441\u0442\u0443 \u043d\u0430 \u043d\u0443\u0436\u043d\u044b\u0439 \u0431\u0435\u0440\u0435\u0433.\n Human_6 = 1\n Wolf_6 = 0\n Cabbage_6 = 1\n Goat_6 = 1\n \n #\u041a\u043b\u044e\u0447\u0435\u0432\u0430\u044f \u0447\u0430\u0441\u0442\u044c \u043e\u043f\u0435\u0440\u0430\u0446\u0438\u0438: \u0444\u0435\u0440\u043c\u0435\u0440 \u0432\u043e\u0437\u0432\u0440\u0430\u0449\u0430\u0435\u0442 \u043a\u043e\u0437\u0443 \u043e\u0431\u0440\u0430\u0442\u043d\u043e.\n Human_7 = 0\n Wolf_7 = 0\n Goat_7 = 0\n Cabbage_7 = 1\n \n #\u0424\u0435\u0440\u043c\u0435\u0440 \u043e\u0442\u0432\u043e\u0437\u0438\u0442 \u0432\u043e\u043b\u043a\u0430 \u043d\u0430 \u0434\u0440\u0443\u0433\u043e\u0439 \u0431\u0435\u0440\u0435\u0433, \u0433\u0434\u0435 \u043e\u043d \u0442\u0435\u043f\u0435\u0440\u044c \u043d\u0430\u0445\u043e\u0434\u0438\u0442\u0441\u044f \u0432\u043c\u0435\u0441\u0442\u0435 \u0441 \u043a\u0430\u043f\u0443\u0441\u0442\u043e\u0439.\n Human_8 = 1\n Wolf_8 = 1\n Goat_8 = 0\n Cabbage_8 = 1\n \n #\u0424\u0435\u0440\u043c\u0435\u0440 \u0432\u043e\u0437\u0432\u0440\u0430\u0449\u0430\u0435\u0442\u0441\u044f \u0437\u0430 \u043a\u043e\u0437\u043e\u0439.\n Human_9 = 0\n Wolf_9 = 1\n Goat_9 = 0\n Cabbage_9 = 1\n \n #\u0424\u0435\u0440\u043c\u0435\u0440 \u043f\u043e\u0432\u0442\u043e\u0440\u043d\u043e \u0434\u043e\u0441\u0442\u0430\u0432\u043b\u044f\u0435\u0442 \u043a\u043e\u0437\u0443 \u043d\u0430 \u043d\u0443\u0436\u043d\u044b\u0439 \u0431\u0435\u0440\u0435\u0433 \u0438 \u0437\u0430\u0432\u0435\u0440\u0448\u0430\u044e\u0442 \u043f\u0435\u0440\u0435\u043f\u0440\u0430\u0432\u0443.\n Human_10 = 1\n Wolf_10 = 1\n Goat_10 = 1\n Cabbage_10 = 1\n<\/code><\/pre>\n
\n \u0422\u0435\u043f\u0435\u0440\u044c \u043f\u043e\u043f\u0440\u043e\u0431\u0443\u0435\u043c \u043f\u043e\u043c\u0435\u043d\u044f\u0442\u044c \u0443\u0441\u043b\u043e\u0432\u0438\u044f \u0438 \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u044c, \u0447\u0442\u043e \u0440\u0435\u0448\u0435\u043d\u0438\u0439 \u043d\u0435\u0442.<\/p>\n
\u0414\u043b\u044f \u044d\u0442\u043e\u0433\u043e \u043c\u044b \u043d\u0430\u0434\u0435\u043b\u0438\u043c \u043d\u0430\u0448\u0435\u0433\u043e \u0432\u043e\u043b\u043a\u0430 \u0442\u0440\u0430\u0432\u043e\u044f\u0434\u043d\u043e\u0441\u0442\u044c\u044e, \u0438 \u043e\u043d \u0437\u0430\u0445\u043e\u0447\u0435\u0442 \u0441\u044a\u0435\u0441\u0442\u044c \u043a\u0430\u043f\u0443\u0441\u0442\u0443.
\n \u042d\u0442\u043e \u043c\u043e\u0436\u043d\u043e \u0441\u0440\u0430\u0432\u043d\u0438\u0442\u044c \u0441\u043e \u0441\u043b\u0443\u0447\u0430\u0435\u043c, \u0432 \u043a\u043e\u0442\u043e\u0440\u043e\u043c \u043d\u0430\u0448\u0430 \u0446\u0435\u043b\u044c \u2014 \u0437\u0430\u0449\u0438\u0442\u0430 \u043f\u0440\u0438\u043b\u043e\u0436\u0435\u043d\u0438\u044f \u0438 \u043c\u044b \u0434\u043e\u043b\u0436\u043d\u044b \u0443\u0434\u043e\u0441\u0442\u043e\u0432\u0435\u0440\u0438\u0442\u044c\u0441\u044f \u0447\u0442\u043e \u043b\u0430\u0437\u0435\u0435\u043a \u043d\u0435\u0442.<\/p>\n
 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) ]\n<\/code><\/pre>\n
\nZ3 \u0412\u044b\u0434\u0430\u043b \u043d\u0430\u043c \u0441\u043b\u0435\u0434\u0443\u044e\u0449\u0438\u0439 \u043e\u0442\u0432\u0435\u0442:<\/p>\n
 no solution\n<\/code><\/pre>\n
\n\u041e\u043d \u043e\u0437\u043d\u0430\u0447\u0430\u0435\u0442, \u0447\u0442\u043e \u0440\u0435\u0448\u0435\u043d\u0438\u0439 \u0434\u0435\u0439\u0441\u0442\u0432\u0438\u0442\u0435\u043b\u044c\u043d\u043e \u043d\u0435\u0442.<\/p>\n
\u0422\u0430\u043a\u0438\u043c \u043e\u0431\u0440\u0430\u0437\u043e\u043c \u043c\u044b \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u043d\u044b\u043c \u0441\u043f\u043e\u0441\u043e\u0431\u043e\u043c \u0434\u043e\u043a\u0430\u0437\u0430\u043b\u0438 \u043d\u0435\u0432\u043e\u0437\u043c\u043e\u0436\u043d\u043e\u0441\u0442\u044c \u043f\u0435\u0440\u0435\u043f\u0440\u0430\u0432\u044b \u0441\u043e \u0432\u0441\u0435\u044f\u0434\u043d\u044b\u043c \u0432\u043e\u043b\u043a\u043e\u043c, \u0431\u0435\u0437 \u043f\u043e\u0442\u0435\u0440\u044c \u0434\u043b\u044f \u0444\u0435\u0440\u043c\u0435\u0440\u0430. <\/p>\n
\u0415\u0441\u043b\u0438 \u0430\u0443\u0434\u0438\u0442\u043e\u0440\u0438\u044f \u0441\u043e\u0447\u0442\u0451\u0442 \u044d\u0442\u0443 \u0442\u0435\u043c\u0430\u0442\u0438\u043a\u0443 \u0438\u043d\u0442\u0435\u0440\u0435\u0441\u043d\u043e\u0439, \u0442\u043e \u0432 \u0434\u0430\u043b\u044c\u043d\u0435\u0439\u0448\u0438\u0445 \u0441\u0442\u0430\u0442\u044c\u044f\u0445 \u044f \u0440\u0430\u0441\u0441\u043a\u0430\u0436\u0443, \u043a\u0430\u043a \u043f\u0440\u0435\u0432\u0440\u0430\u0442\u0438\u0442\u044c \u043e\u0431\u044b\u0447\u043d\u0443\u044e \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u0443 \u0438\u043b\u0438 \u0444\u0443\u043d\u043a\u0446\u0438\u044e \u0432 \u0441\u043e\u0432\u043c\u0435\u0441\u0442\u0438\u043c\u043e\u0435 \u0441 \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u044b\u043c\u0438 \u043c\u0435\u0442\u043e\u0434\u0430\u043c\u0438 \u0443\u0440\u0430\u0432\u043d\u0435\u043d\u0438\u0435, \u0438 \u0440\u0435\u0448\u0438\u0442\u044c \u0435\u0433\u043e, \u043e\u0431\u043d\u0430\u0440\u0443\u0436\u0438\u0432 \u0442\u0435\u043c \u0441\u0430\u043c\u044b\u043c \u043a\u0430\u043a \u0432\u0441\u0435 \u043b\u0435\u0433\u0438\u0442\u0438\u043c\u043d\u044b\u0435 \u0441\u0446\u0435\u043d\u0430\u0440\u0438\u0438, \u0442\u0430\u043a \u0438 \u0443\u044f\u0437\u0432\u0438\u043c\u043e\u0441\u0442\u0438. \u0421\u043d\u0430\u0447\u0430\u043b\u0430 \u043d\u0430 \u044d\u0442\u043e\u0439 \u0436\u0435 \u0437\u0430\u0434\u0430\u0447\u0435, \u043d\u043e \u043f\u0440\u0435\u0434\u0441\u0442\u0430\u0432\u043b\u0435\u043d\u043d\u043e\u0439 \u0443\u0436\u0435 \u0432 \u0432\u0438\u0434\u0435 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u044b, \u0430 \u0437\u0430\u0442\u0435\u043c \u043f\u043e\u0441\u0442\u0435\u043f\u0435\u043d\u043d\u043e \u0443\u0441\u043b\u043e\u0436\u043d\u044f\u044f \u0438 \u043f\u0435\u0440\u0435\u0445\u043e\u0434\u044f \u043a \u0430\u043a\u0442\u0443\u0430\u043b\u044c\u043d\u044b\u043c \u043f\u0440\u0438\u043c\u0435\u0440\u0430\u043c \u0438\u0437 \u043c\u0438\u0440\u0430 \u0440\u0430\u0437\u0440\u0430\u0431\u043e\u0442\u043a\u0438 \u041f\u041e.<\/p>\n
\u0421\u043b\u0435\u0434\u0443\u044e\u0449\u0430\u044f \u0441\u0442\u0430\u0442\u044c\u044f \u0443\u0436\u0435 \u0433\u043e\u0442\u043e\u0432\u0430:
\n\u0421\u043e\u0437\u0434\u0430\u043d\u0438\u0435 \u0441\u0438\u0441\u0442\u0435\u043c\u044b \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u043e\u0439 \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438 \u0441 \u043d\u0443\u043b\u044f: \u041f\u0438\u0448\u0435\u043c \u0441\u0438\u043c\u0432\u043e\u043b\u044c\u043d\u0443\u044e VM \u043d\u0430 PHP \u0438 Python<\/a><\/noindex><\/p>\n
\u0412 \u043d\u0435\u0439 \u044f \u043f\u0435\u0440\u0435\u0445\u043e\u0436\u0443 \u043e\u0442 \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u043e\u0439 \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438 \u0437\u0430\u0434\u0430\u0447, \u043a \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u0430\u043c, \u0438 \u043e\u043f\u0438\u0441\u044b\u0432\u0430\u044e, 
\n\u043a\u0430\u043a\u0438\u043c \u043e\u0431\u0440\u0430\u0437\u043e\u043c \u043c\u043e\u0436\u043d\u043e \u043a\u043e\u043d\u0432\u0435\u0440\u0442\u0438\u0440\u043e\u0432\u0430\u0442\u044c \u0438\u0445 \u0432 \u0441\u0438\u0441\u0442\u0435\u043c\u044b \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u044b\u0445 \u043f\u0440\u0430\u0432\u0438\u043b \u0430\u0432\u0442\u043e\u043c\u0430\u0442\u0438\u0447\u0435\u0441\u043a\u0438.
\n
\u0418\u0441\u0442\u043e\u0447\u043d\u0438\u043a: habr.com<\/a><\/p>\n","protected":false,"gt_translate_keys":[{"key":"rendered","format":"html"}]},"excerpt":{"rendered":"
\u041d\u0430 \u043c\u043e\u0439 \u0432\u0437\u0433\u043b\u044f\u0434, \u0432 \u0440\u0443\u0441\u0441\u043a\u043e\u044f\u0437\u044b\u0447\u043d\u043e\u043c \u0441\u0435\u043a\u0442\u043e\u0440\u0435 \u0438\u043d\u0442\u0435\u0440\u043d\u0435\u0442\u0430 \u0442\u0435\u043c\u0430\u0442\u0438\u043a\u0430 \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u043e\u0439 \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438 \u043e\u0441\u0432\u0435\u0449\u0435\u043d\u0430 \u043d\u0435\u0434\u043e\u0441\u0442\u0430\u0442\u043e\u0447\u043d\u043e, \u0438 \u043e\u0441\u043e\u0431\u0435\u043d\u043d\u043e \u043d\u0435 \u0445\u0432\u0430\u0442\u0430\u0435\u0442 \u043f\u0440\u043e\u0441\u0442\u044b\u0445 \u0438 \u043d\u0430\u0433\u043b\u044f\u0434\u043d\u044b\u0445 \u043f\u0440\u0438\u043c\u0435\u0440\u043e\u0432. \u042f \u043f\u0440\u0438\u0432\u0435\u0434\u0443 \u0442\u0430\u043a\u043e\u0439 \u043f\u0440\u0438\u043c\u0435\u0440 \u0438\u0437 \u0437\u0430\u0440\u0443\u0431\u0435\u0436\u043d\u043e\u0433\u043e \u0438\u0441\u0442\u043e\u0447\u043d\u0438\u043a\u0430, \u0438 \u0434\u043e\u043f\u043e\u043b\u043d\u044e \u0441\u043e\u0431\u0441\u0442\u0432\u0435\u043d\u043d\u044b\u043c \u0440\u0435\u0448\u0435\u043d\u0438\u0435\u043c \u0438\u0437\u0432\u0435\u0441\u0442\u043d\u043e\u0439 \u0437\u0430\u0434\u0430\u0447\u0438 \u043e \u043f\u0435\u0440\u0435\u043f\u0440\u0430\u0432\u0435 \u0432\u043e\u043b\u043a\u0430, \u043a\u043e\u0437\u044b \u0438 \u043a\u0430\u043f\u0443\u0441\u0442\u044b \u043d\u0430 \u0434\u0440\u0443\u0433\u0443\u044e \u0441\u0442\u043e\u0440\u043e\u043d\u0443 \u0440\u0435\u043a\u0438. \u041d\u043e \u0432\u043d\u0430\u0447\u0430\u043b\u0435 \u0432\u043a\u0440\u0430\u0442\u0446\u0435 \u043e\u043f\u0438\u0448\u0443, \u0447\u0442\u043e \u0438\u0437 \u0441\u0435\u0431\u044f \u043f\u0440\u0435\u0434\u0441\u0442\u0430\u0432\u043b\u044f\u0435\u0442 \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u0430\u044f \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u044f \u0438 \u0437\u0430\u0447\u0435\u043c […]<\/p>\n","protected":false,"gt_translate_keys":[{"key":"rendered","format":"html"}]},"author":1,"featured_media":24473,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"footnotes":""},"categories":[688],"tags":[],"class_list":["post-32689","post","type-post","status-publish","format-standard","has-post-thumbnail","hentry","category-administrirovanie"],"aioseo_notices":[],"aioseo_head":"\n\t\t\n\t\n\t\n\t\n\t\n\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\n","aioseo_head_json":{"title":"\ud83e\udd47Formale Verifizierung am Beispiel des Problems mit Wolf, Ziege und Kohl | ProHoster","description":"Meiner Meinung nach ist das Thema der formalen Verifikation im russischsprachigen Internet nicht ausreichend beleuchtet, und es mangelt insbesondere an einfachen und anschaulichen Beispielen. Ich werde ein solches Beispiel aus einer ausl\u00e4ndischen Quelle anf\u00fchren und mit einer eigenen L\u00f6sung der bekannten Aufgabe, einen Wolf, eine Ziege und einen Kohl auf die andere Seite des Flusses zu bringen, erg\u00e4nzen. Zun\u00e4chst werde ich kurz beschreiben, was formale Verifikation ist und warum sie notwendig ist.","canonical_url":"https:\/\/prohoster.info\/de\/blog\/administrirovanie\/formalnaya-verifikatsiya-na-primere-zadachi-o-volke-koze-i-kapuste","robots":"max-image-preview:large","keywords":"","webmasterTools":{"miscellaneous":""},"schema":null,"og:locale":"de_DE","og:site_name":"ProHoster | \u041a\u0443\u043f\u0438\u0442\u044c \u043d\u0430\u0434\u0435\u0436\u043d\u044b\u0439 \u0445\u043e\u0441\u0442\u0438\u043d\u0433 \u0434\u043b\u044f \u0441\u0430\u0439\u0442\u043e\u0432 \u0441 \u0437\u0430\u0449\u0438\u0442\u043e\u0439 \u043e\u0442 DDoS, VPS VDS \u0441\u0435\u0440\u0432\u0435\u0440\u044b","og:type":"article","og:title":"\ud83e\udd47\u0424\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u0430\u044f \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u044f \u043d\u0430 \u043f\u0440\u0438\u043c\u0435\u0440\u0435 \u0437\u0430\u0434\u0430\u0447\u0438 \u043e \u0432\u043e\u043b\u043a\u0435, \u043a\u043e\u0437\u0435 \u0438 \u043a\u0430\u043f\u0443\u0441\u0442\u0435 | ProHoster","og:description":"\u041d\u0430 \u043c\u043e\u0439 \u0432\u0437\u0433\u043b\u044f\u0434, \u0432 \u0440\u0443\u0441\u0441\u043a\u043e\u044f\u0437\u044b\u0447\u043d\u043e\u043c \u0441\u0435\u043a\u0442\u043e\u0440\u0435 \u0438\u043d\u0442\u0435\u0440\u043d\u0435\u0442\u0430 \u0442\u0435\u043c\u0430\u0442\u0438\u043a\u0430 \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u043e\u0439 \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438 \u043e\u0441\u0432\u0435\u0449\u0435\u043d\u0430 \u043d\u0435\u0434\u043e\u0441\u0442\u0430\u0442\u043e\u0447\u043d\u043e, \u0438 \u043e\u0441\u043e\u0431\u0435\u043d\u043d\u043e \u043d\u0435 \u0445\u0432\u0430\u0442\u0430\u0435\u0442 \u043f\u0440\u043e\u0441\u0442\u044b\u0445 \u0438 \u043d\u0430\u0433\u043b\u044f\u0434\u043d\u044b\u0445 \u043f\u0440\u0438\u043c\u0435\u0440\u043e\u0432. \u042f \u043f\u0440\u0438\u0432\u0435\u0434\u0443 \u0442\u0430\u043a\u043e\u0439 \u043f\u0440\u0438\u043c\u0435\u0440 \u0438\u0437 \u0437\u0430\u0440\u0443\u0431\u0435\u0436\u043d\u043e\u0433\u043e \u0438\u0441\u0442\u043e\u0447\u043d\u0438\u043a\u0430, \u0438 \u0434\u043e\u043f\u043e\u043b\u043d\u044e \u0441\u043e\u0431\u0441\u0442\u0432\u0435\u043d\u043d\u044b\u043c \u0440\u0435\u0448\u0435\u043d\u0438\u0435\u043c \u0438\u0437\u0432\u0435\u0441\u0442\u043d\u043e\u0439 \u0437\u0430\u0434\u0430\u0447\u0438 \u043e \u043f\u0435\u0440\u0435\u043f\u0440\u0430\u0432\u0435 \u0432\u043e\u043b\u043a\u0430, \u043a\u043e\u0437\u044b \u0438 \u043a\u0430\u043f\u0443\u0441\u0442\u044b \u043d\u0430 \u0434\u0440\u0443\u0433\u0443\u044e \u0441\u0442\u043e\u0440\u043e\u043d\u0443 \u0440\u0435\u043a\u0438. \u041d\u043e \u0432\u043d\u0430\u0447\u0430\u043b\u0435 \u0432\u043a\u0440\u0430\u0442\u0446\u0435 \u043e\u043f\u0438\u0448\u0443, \u0447\u0442\u043e \u0438\u0437 \u0441\u0435\u0431\u044f \u043f\u0440\u0435\u0434\u0441\u0442\u0430\u0432\u043b\u044f\u0435\u0442 \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u0430\u044f \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u044f \u0438 \u0437\u0430\u0447\u0435\u043c","og:url":"https:\/\/prohoster.info\/de\/blog\/administrirovanie\/formalnaya-verifikatsiya-na-primere-zadachi-o-volke-koze-i-kapuste","og:image":"https:\/\/prohoster.info\/wp-content\/uploads\/2021\/11\/logo-350.jpg","og:image:secure_url":"https:\/\/prohoster.info\/wp-content\/uploads\/2021\/11\/logo-350.jpg","og:image:width":350,"og:image:height":350,"article:published_time":"2019-10-31T18:48:24+00:00","article:modified_time":"2019-10-31T18:48:24+00:00","article:publisher":"https:\/\/www.facebook.com\/prohoster","article:author":"https:\/\/www.facebook.com\/prohoster"},"aioseo_meta_data":{"post_id":"32689","title":null,"description":null,"keywords":null,"keyphrases":null,"primary_term":null,"canonical_url":null,"og_title":null,"og_description":null,"og_object_type":"default","og_image_type":"default","og_image_url":null,"og_image_width":null,"og_image_height":null,"og_image_custom_url":null,"og_image_custom_fields":null,"og_video":null,"og_custom_url":null,"og_article_section":null,"og_article_tags":null,"twitter_use_og":false,"twitter_card":"default","twitter_image_type":"default","twitter_image_url":null,"twitter_image_custom_url":null,"twitter_image_custom_fields":null,"twitter_title":null,"twitter_description":null,"schema":{"blockGraphs":[],"customGraphs":[],"default":{"data":{"Article":[],"Course":[],"Dataset":[],"FAQPage":[],"Movie":[],"Person":[],"Product":[],"ProductReview":[],"Car":[],"Recipe":[],"Service":[],"SoftwareApplication":[],"WebPage":[]},"graphName":"","isEnabled":true},"graphs":[]},"schema_type":null,"schema_type_options":null,"pillar_content":false,"robots_default":true,"robots_noindex":false,"robots_noarchive":false,"robots_nosnippet":false,"robots_nofollow":false,"robots_noimageindex":false,"robots_noodp":false,"robots_notranslate":false,"robots_max_snippet":null,"robots_max_videopreview":null,"robots_max_imagepreview":"large","priority":null,"frequency":null,"local_seo":null,"seo_analyzer_scan_date":"2026-01-21 12:04:21","breadcrumb_settings":null,"limit_modified_date":false,"reviewed_by":null,"ai":null,"created":"2021-03-01 02:54:26","updated":"2026-01-21 12:04:21"},"gt_translate_keys":[{"key":"link","format":"url"}],"_links":{"self":[{"href":"https:\/\/prohoster.info\/de\/wp-json\/wp\/v2\/posts\/32689","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/prohoster.info\/de\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/prohoster.info\/de\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/prohoster.info\/de\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/prohoster.info\/de\/wp-json\/wp\/v2\/comments?post=32689"}],"version-history":[{"count":0,"href":"https:\/\/prohoster.info\/de\/wp-json\/wp\/v2\/posts\/32689\/revisions"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/prohoster.info\/de\/wp-json\/wp\/v2\/media\/24473"}],"wp:attachment":[{"href":"https:\/\/prohoster.info\/de\/wp-json\/wp\/v2\/media?parent=32689"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/prohoster.info\/de\/wp-json\/wp\/v2\/categories?post=32689"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/prohoster.info\/de\/wp-json\/wp\/v2\/tags?post=32689"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}