{"id":207112,"date":"2014-01-04T17:34:03","date_gmt":"2014-01-04T13:34:03","guid":{"rendered":"http:\/\/savepearlharbor.com\/?p=207112"},"modified":"-0001-11-30T00:00:00","modified_gmt":"-0001-11-29T21:00:00","slug":"","status":"publish","type":"post","link":"https:\/\/savepearlharbor.com\/?p=207112","title":{"rendered":"<span class=\"post_title\">\u0417\u0430\u0447\u0435\u043c \u043d\u0430\u043c \u0432\u0441\u0435\u043c \u043d\u0443\u0436\u0435\u043d SAT \u0438 \u0432\u0441\u0435 \u044d\u0442\u0438 P-NP (\u0447\u0430\u0441\u0442\u044c \u043f\u0435\u0440\u0432\u0430\u044f)<\/span>"},"content":{"rendered":"<div class=\"content html_format\">\n<blockquote><p>SAT \u0443\u0436\u0435 \u0442\u0435\u043c \u0445\u043e\u0440\u043e\u0448, \u0447\u0442\u043e \u043e\u043d \u0443\u043c \u0432 \u043f\u043e\u0440\u044f\u0434\u043e\u043a \u043f\u0440\u0438\u0432\u043e\u0434\u0438\u0442 <br \/>  \u041b\u043e\u043c\u043e\u043d\u043e\u0441\u043e\u0432 (<a href=\"http:\/\/i.imgur.com\/2nQ8VcA.jpg\">\u043e\u0440\u0438\u0433\u0438\u043d\u0430\u043b<\/a>)  <\/p><\/blockquote>\n<p>  <\/p>\n<h4>\u0412\u0432\u0435\u0434\u0435\u043d\u0438\u0435<\/h4>\n<p>  \u041d\u0430 \u0445\u0430\u0431\u0440\u0435 \u0443\u0436\u0435 \u043d\u0435\u043c\u0430\u043b\u043e \u0441\u0442\u0430\u0442\u0435\u0439, \u043f\u043e\u0441\u0432\u044f\u0449\u0435\u043d\u043d\u044b\u0445 \u043f\u0440\u043e\u0431\u043b\u0435\u043c\u0435 P vs. NP \u0438 \u0437\u0430\u0434\u0430\u0447\u0435 \u043e \u0432\u044b\u043f\u043e\u043b\u043d\u0438\u043c\u043e\u0441\u0442\u0438 \u043b\u043e\u0433\u0438\u0447\u0435\u0441\u043a\u0438\u0445 \u0444\u043e\u0440\u043c\u0443\u043b (SATisfiability problem). \u041e\u0434\u043d\u0430\u043a\u043e, \u0431\u043e\u043b\u044c\u0448\u0438\u043d\u0441\u0442\u0432\u043e \u0438\u0437 \u043d\u0438\u0445 \u043d\u0435 \u043e\u0442\u0432\u0435\u0447\u0430\u0435\u0442 \u043d\u0430 \u043d\u0435\u0441\u043a\u043e\u043b\u044c\u043a\u043e \u0441\u0430\u043c\u044b\u0445 \u0432\u0430\u0436\u043d\u044b\u0445 \u0432\u043e\u043f\u0440\u043e\u0441\u043e\u0432. \u041f\u043e\u0447\u0435\u043c\u0443 \u044d\u0442\u0430 \u043f\u0440\u043e\u0431\u043b\u0435\u043c\u0430 \u0434\u0435\u0439\u0441\u0442\u0432\u0438\u0442\u0435\u043b\u044c\u043d\u0430 \u0432\u0430\u0436\u043d\u0430 \u0434\u043b\u044f \u043d\u0430\u0441? \u0427\u0442\u043e \u0431\u0443\u0434\u0435\u0442, \u0435\u0441\u043b\u0438 \u0435\u0451 \u0440\u0435\u0448\u0430\u0442? \u0413\u0434\u0435 \u044d\u0442\u043e \u0432\u0441\u0435 \u0432\u043e\u043e\u0431\u0449\u0435 \u043f\u0440\u0438\u043c\u0435\u043d\u044f\u0435\u0442\u0441\u044f? \u0418 \u043f\u043e\u0447\u0435\u043c\u0443 \u043d\u0435\u043e\u0431\u0445\u043e\u0434\u0438\u043c\u043e \u0438\u043c\u0435\u0442\u044c \u0445\u043e\u0442\u044f \u0431\u044b \u043e\u0431\u0449\u0435\u0435 \u043f\u0440\u0435\u0434\u0441\u0442\u0430\u0432\u043b\u0435\u043d\u0438\u0435, \u043e \u0447\u0435\u043c \u0442\u0430\u043c \u0438\u0434\u0435\u0442 \u0440\u0435\u0447\u044c?<\/p>\n<p>  <img decoding=\"async\" src=\"http:\/\/habr.habrastorage.org\/post_images\/854\/10f\/e5e\/85410fe5e72138afd3136ec955a16af1.gif\" alt=\"image\"\/><\/p>\n<p>  \u0415\u0441\u043b\u0438 \u043c\u044b \u0434\u0435\u0442\u0430\u043b\u044c\u043d\u043e \u043f\u0440\u043e\u0430\u043d\u0430\u043b\u0438\u0437\u0438\u0440\u0443\u0435\u043c \u043d\u0430\u0438\u0431\u043e\u043b\u0435\u0435 \u0437\u0430\u043c\u0435\u0442\u043d\u044b\u0435 \u0440\u0430\u0431\u043e\u0442\u044b \u043d\u0430 \u0445\u0430\u0431\u0440\u0435 \u043f\u043e \u0434\u0430\u043d\u043d\u043e\u0439 \u0442\u0435\u043c\u0435 [<a href=\"http:\/\/habrahabr.ru\/post\/112305\/\">1<\/a>, <a href=\"http:\/\/habrahabr.ru\/post\/132127\/\">2<\/a>, <a href=\"http:\/\/habrahabr.ru\/post\/112161\/\">3<\/a>, <a href=\"http:\/\/habrahabr.ru\/post\/101271\/\">4<\/a>, <a href=\"http:\/\/habrahabr.ru\/post\/43224\/\">5<\/a>, <a href=\"http:\/\/habrahabr.ru\/post\/175113\/\">6<\/a>, <a href=\"http:\/\/habrahabr.ru\/post\/164557\/\">7<\/a>], \u0442\u043e \u0437\u0430\u043c\u0435\u0442\u0438\u043c, \u0447\u0442\u043e \u0441 \u043e\u0434\u043d\u043e\u0439 \u0441\u0442\u043e\u0440\u043e\u043d\u044b, \u043b\u044e\u0434\u0438 \u043e\u0431\u043b\u0430\u0434\u0430\u044e\u0449\u0438\u0435 \u0437\u043d\u0430\u043d\u0438\u044f\u043c\u0438 \u0432 \u043e\u0431\u043b\u0430\u0441\u0442\u0438 \u0432\u044b\u0447\u0438\u0441\u043b\u0438\u0442\u0435\u043b\u044c\u043d\u043e\u0439 \u0441\u043b\u043e\u0436\u043d\u043e\u0441\u0442\u0438 \u043d\u0435 c\u043c\u043e\u0433\u0443\u0442 \u043f\u043e\u0447\u0435\u0440\u043f\u043d\u0443\u0442\u044c \u043d\u0438\u0447\u0435\u0433\u043e \u043f\u0440\u0438\u043d\u0446\u0438\u043f\u0438\u0430\u043b\u044c\u043d\u043e \u043d\u043e\u0432\u043e\u0433\u043e \u0432 \u0434\u0430\u043d\u043d\u044b\u0445 \u0441\u0442\u0430\u0442\u044c\u044f\u0445. \u0421 \u0434\u0440\u0443\u0433\u043e\u0439 \u0441\u0442\u043e\u0440\u043e\u043d\u044b, \u0434\u0430\u043d\u043d\u044b\u0435 \u0441\u0442\u0430\u0442\u044c\u0438 \u043f\u043e-\u043f\u0440\u0435\u0436\u043d\u0435\u043c\u0443 \u043d\u0435 \u044f\u0432\u043b\u044f\u044e\u0442\u0441\u044f \u043e\u0431\u0449\u0435\u0434\u043e\u0441\u0442\u0443\u043f\u043d\u044b\u043c\u0438. \u0418\u043b\u043b\u044e\u0441\u0442\u0440\u0430\u0446\u0438\u044f \u0438\u0437 \u0437\u0430\u0433\u043e\u043b\u043e\u0432\u043a\u0430 \u043d\u0430\u0433\u043b\u044f\u0434\u043d\u043e \u0434\u0435\u043c\u043e\u043d\u0441\u0442\u0440\u0438\u0440\u0443\u0435\u0442 \u043f\u0440\u043e\u0431\u043b\u0435\u043c\u0443: \u0442\u0435\u043c, \u043a\u043e\u043c\u0443 \u0431\u044b\u043b\u043e \u043d\u0435 \u043f\u043e\u043d\u044f\u0442\u043d\u043e, \u0438\u0437 \u043d\u0435\u0451 \u043d\u0438\u0447\u0435\u0433\u043e \u043d\u0435 \u044f\u0441\u043d\u043e, \u0430 \u0442\u0435, \u043a\u0442\u043e \u043e\u0431 \u044d\u0442\u043e\u043c \u0443\u0436\u0435 \u0441\u043b\u044b\u0448\u0430\u043b, \u0432 \u043d\u0435\u0439 \u043d\u0435 \u043d\u0443\u0436\u0434\u0430\u044e\u0442\u0441\u044f.<\/p>\n<p>  \u0414\u0430\u043d\u043d\u0430\u044f \u0441\u0442\u0430\u0442\u044c\u044f \u043f\u0440\u0435\u0441\u043b\u0435\u0434\u0443\u0435\u0442 \u0434\u0432\u0435 \u0446\u0435\u043b\u0438: \u043f\u0435\u0440\u0432\u043e\u0435 \u2014 \u0434\u0430\u0442\u044c \u043e\u0431\u0449\u0435\u0435 \u043f\u0440\u0435\u0434\u0441\u0442\u0430\u0432\u043b\u0435\u043d\u0438\u0435 \u043e \u043f\u0440\u043e\u0431\u043b\u0435\u043c\u0435 \u0438 \u043e\u0442\u0432\u0435\u0442\u0438\u0442\u044c \u043d\u0430 \u0432\u043e\u043f\u0440\u043e\u0441, \u043f\u043e\u0447\u0435\u043c\u0443 \u0436\u0435 \u043d\u0430\u043c \u0441\u0442\u043e\u0438\u0442\u044c \u0437\u043d\u0430\u0442\u044c \u043e\u0431 \u044d\u0442\u043e\u0439 \u0437\u0430\u0434\u0430\u0447\u0435 (\u043f\u0435\u0440\u0432\u0430\u044f \u0447\u0430\u0441\u0442\u044c), \u0432\u0442\u043e\u0440\u043e\u0435 \u2014 \u043f\u0440\u0435\u0434\u043e\u0441\u0442\u0430\u0432\u0438\u0442\u044c \u043c\u0430\u0442\u0435\u0440\u0438\u0430\u043b \u00ab\u043d\u0430 \u0432\u044b\u0440\u043e\u0441\u0442\u00bb, \u043a\u043e\u0442\u043e\u0440\u044b\u0439 \u0431\u0443\u0434\u0435\u0442 \u0438\u043d\u0442\u0435\u0440\u0435\u0441\u0435\u043d \u043b\u044e\u0434\u044f\u043c \u0438\u043d\u0442\u0435\u0440\u0435\u0441\u0443\u044e\u0449\u0438\u043c\u0441\u044f \u0442\u0435\u043c\u0430\u0442\u0438\u043a\u043e\u0439, \u0430 \u0442\u0430\u043a \u0436\u0435 \u043c\u043e\u0436\u0435\u0442 \u0431\u044b\u0442\u044c \u043f\u043e\u043b\u0435\u0437\u0435\u043d \u0434\u043b\u044f \u0438\u0437\u0443\u0447\u0435\u043d\u0438\u044f \u0442\u0435\u043c\u044b \u0432 \u0434\u0430\u043b\u044c\u043d\u0435\u0439\u0448\u0435\u043c (\u0432\u0442\u043e\u0440\u0430\u044f \u0447\u0430\u0441\u0442\u044c).<\/p>\n<p>  <a name=\"habracut\"><\/a>  <\/p>\n<h4> \u0421\u0442\u0440\u0443\u043a\u0442\u0443\u0440\u0430 \u0441\u0442\u0430\u0442\u044c\u0438<\/h4>\n<p>  \u0414\u043b\u044f \u0443\u0434\u043e\u0431\u0441\u0442\u0432\u0430 \u043f\u0440\u043e\u0447\u0442\u0435\u043d\u0438\u044f \u0438 \u043d\u0430\u0432\u0438\u0433\u0430\u0446\u0438\u0438 \u043f\u0440\u0435\u0434\u043e\u0441\u0442\u0430\u0432\u043b\u044f\u0435\u043c \u043a\u0440\u0430\u0442\u043a\u0438\u0439 \u043e\u0431\u0437\u043e\u0440 \u0441\u043e\u0434\u0435\u0440\u0436\u0438\u043c\u043e\u0433\u043e \u0441\u0442\u0430\u0442\u044c\u0438.<\/p>\n<ul>\n<li>\u041e\u0431\u0449\u0435\u0434\u043e\u0441\u0442\u0443\u043f\u043d\u044b\u0439 \u043c\u0430\u0442\u0435\u0440\u0438\u0430\u043b<br \/> \n<ol>\n<li>\u041f\u043e\u0447\u0435\u043c\u0443 SAT \u0432\u0430\u0436\u0435\u043d \u0434\u043b\u044f \u043d\u0430\u0441 \u0432\u0441\u0435\u0445? \u041f\u0440\u0438\u043b\u043e\u0436\u0435\u043d\u0438\u044f\/\u0418\u043d\u0442\u0435\u0440\u0435\u0441\u043d\u044b\u0435 NP \u0437\u0430\u0434\u0430\u0447\u0438 \u0438 SAT <\/li>\n<li>\u0418\u0441\u0442\u043e\u0440\u0438\u044f SAT \u0438 NP-\u043f\u043e\u043b\u043d\u043e\u0442\u044b <\/li>\n<li>\u00ab\u0418\u043d\u0442\u0443\u0438\u0442\u0438\u0432\u043d\u043e\u0435 \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u0435\u043d\u0438\u0435\u00bb SAT, NP \u0438 P<\/li>\n<li>\u0427\u0442\u043e \u0431\u0443\u0434\u0435\u0442, \u0435\u0441\u043b\u0438\u2026 P != NP, P = NP <\/li>\n<li>2-SAT \u043f\u043e\u043b\u0438\u043d\u043e\u043c\u0438\u0430\u043b\u0435\u043d: \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c \u0438 \u0438\u043d\u0442\u0443\u0438\u0446\u0438\u044f<\/li>\n<li>\u0417\u0430\u0434\u0430\u0447\u043a\u0430 \u043d\u0430 \u043f\u043e\u0434\u0443\u043c\u0430\u0442\u044c<\/li>\n<\/ol>\n<p>   <\/li>\n<li>\u0421\u043f\u0435\u0446\u0438\u0430\u043b\u0438\u0437\u0438\u0440\u043e\u0432\u0430\u043d\u043d\u044b\u0439 \u043c\u0430\u0442\u0435\u0440\u0438\u0430\u043b (\u0441\u043c\u043e\u0442\u0440\u0438\u0442\u0435 \u0432 \u0441\u043b\u0435\u0434\u0443\u044e\u0449\u0438\u0445 \u0441\u0435\u0440\u0438\u044f\u0445)<br \/> \n<ol>\n<li>\u0424\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u043e\u0435 \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u0435\u043d\u0438\u0435. \u041d\u0435\u0441\u0438\u043c\u043c\u0435\u0442\u0440\u0438\u0447\u043d\u043e\u0441\u0442\u044c \u043f\u0440\u043e\u0431\u043b\u0435\u043c\u044b \u0440\u0430\u0437\u0440\u0435\u0448\u0438\u043c\u043e\u0441\u0442\u0438 \u0434\u043b\u044f NP \u0438 CoNP<\/li>\n<li>2+p-SAT \u043f\u043e\u043b\u0438\u043d\u043e\u043c\u0438\u0430\u043b\u0435\u043d? <\/li>\n<li>\u0417\u0430\u0432\u0438\u0441\u0438\u043c\u043e\u0441\u0442\u044c \u0441\u043b\u043e\u0436\u043d\u043e\u0441\u0442\u0438 \u043e\u0442 \u0447\u0438\u0441\u043b\u0430 \u043f\u0435\u0440\u0435\u043c\u0435\u043d\u043d\u044b\u0445 <\/li>\n<li> \u042f \u0440\u0435\u0448\u0438\u043b P vs. NP, \u0447\u0442\u043e \u043c\u043d\u0435 \u0434\u0435\u043b\u0430\u0442\u044c? \u041a\u0443\u0434\u0430 \u043f\u0438\u0441\u0430\u0442\u044c?<\/li>\n<li>\u0422\u0435\u043e\u0440\u0435\u043c\u044b \u043e \u043d\u0435\u0432\u044b\u0440\u0430\u0437\u0438\u043c\u043e\u0441\u0442\u0438: \u043f\u043e\u0447\u0435\u043c\u0443 \u0441\u0442\u0430\u0442\u044c\u044e \u0420\u043e\u043c\u0430\u043d\u043e\u0432\u0430 [<a href=\"http:\/\/habrahabr.ru\/post\/112161\/\">3<\/a>] \u043e\u0436\u0438\u0434\u0430\u0435\u0442 reject<\/li>\n<li>\u041e \u0441\u043e\u0432\u0440\u0435\u043c\u0435\u043d\u043d\u044b\u0445 SAT solver&#8217;\u0430\u0445<\/li>\n<li> \u0427\u0442\u043e \u043f\u043e\u0447\u0438\u0442\u0430\u0442\u044c?<\/li>\n<li>\u0417\u0430\u0434\u0430\u0447\u043a\u0430 \u043d\u0430 \u043f\u043e\u0434\u0443\u043c\u0430\u0442\u044c<\/li>\n<\/ol>\n<p>  <\/li>\n<\/ul>\n<p>  <\/p>\n<h5>Disclaimer<\/h5>\n<p>  \u0414\u0430\u043d\u043d\u0430\u044f \u0440\u0430\u0431\u043e\u0442\u0430 \u044f\u0432\u043b\u044f\u0435\u0442\u0441\u044f \u043e\u0431\u0449\u0435\u043e\u0431\u0440\u0430\u0437\u043e\u0432\u0430\u0442\u0435\u043b\u044c\u043d\u044b\u043c \u043c\u0430\u0442\u0435\u0440\u0438\u0430\u043b\u043e\u043c \u0438 \u043f\u0440\u0435\u0434\u043d\u0430\u0437\u043d\u0430\u0447\u0435\u043d\u0430 \u0438\u0441\u043a\u043b\u044e\u0447\u0438\u0442\u0435\u043b\u044c\u043d\u043e \u0434\u043b\u044f \u043e\u0437\u043d\u0430\u043a\u043e\u043c\u043b\u0435\u043d\u0438\u044f \u0441 \u043f\u0440\u043e\u0431\u043b\u0435\u043c\u0430\u0442\u0438\u043a\u043e\u0439 SAT. \u0412\u044b\u0447\u0438\u0441\u043b\u0438\u0442\u0435\u043b\u044c\u043d\u0430\u044f \u0441\u043b\u043e\u0436\u043d\u043e\u0441\u0442\u044c \u0438 SAT \u043d\u0435 \u044f\u0432\u043b\u044f\u0435\u0442\u0441\u044f \u043e\u0441\u043d\u043e\u0432\u043d\u044b\u043c\u0438 \u043d\u0430\u043f\u0440\u0430\u0432\u043b\u0435\u043d\u0438\u044f\u043c\u0438 \u043c\u043e\u0438\u0445 \u0438\u0441\u0441\u043b\u0435\u0434\u043e\u0432\u0430\u043d\u0438\u0439, \u0430 \u043b\u0435\u0436\u0430\u0442 \u0432 \u0441\u043c\u0435\u0436\u043d\u043e\u0439 \u043d\u0430\u0443\u0447\u043d\u043e\u0439 \u043e\u0431\u043b\u0430\u0441\u0442\u0438, \u043f\u043e\u044d\u0442\u043e\u043c\u0443 \u0432 \u0441\u043b\u0443\u0447\u0430\u0435 \u0441\u043e\u043c\u043d\u0435\u043d\u0438\u044f \u0432\u0441\u0435\u0433\u0434\u0430 \u043e\u0431\u0440\u0430\u0449\u0430\u0439\u0442\u0435\u0441\u044c \u043a \u0443\u043a\u0430\u0437\u0430\u043d\u043d\u043e\u043c\u0443 \u043f\u0435\u0440\u0432\u043e\u0438\u0441\u0442\u043e\u0447\u043d\u0438\u043a\u0443.<\/p>\n<h4>\u041e\u0431\u0449\u0435\u0434\u043e\u0441\u0442\u0443\u043f\u043d\u044b\u0439 \u043c\u0430\u0442\u0435\u0440\u0438\u0430\u043b<\/h4>\n<p>  <\/p>\n<h5>\u041f\u043e\u0447\u0435\u043c\u0443 SAT \u0432\u0430\u0436\u0435\u043d \u0434\u043b\u044f \u043d\u0430\u0441 \u0432\u0441\u0435\u0445? \u041f\u0440\u0438\u043b\u043e\u0436\u0435\u043d\u0438\u044f <\/h5>\n<p>  \u0414\u043b\u044f \u0442\u043e\u0433\u043e, \u0447\u0442\u043e\u0431\u044b \u043e\u0442\u0432\u0435\u0442\u0438\u0442\u044c \u043d\u0430 \u044d\u0442\u043e\u0442 \u0432\u043e\u043f\u0440\u043e\u0441 \u043d\u0443\u0436\u043d\u043e \u043f\u0440\u0435\u0436\u0434\u0435 \u0432\u0441\u0435\u0433\u043e \u043f\u043e\u043d\u044f\u0442\u044c \u043a\u0430\u043a\u0438\u0435 \u043c\u0430\u0442\u0435\u043c\u0430\u0442\u0438\u0447\u0435\u0441\u043a\u0438\u0435 \u0437\u0430\u0434\u0430\u0447\u0438 \u0437\u0430\u0442\u0440\u0430\u0433\u0438\u0432\u0430\u044e\u0442 \u043d\u0430\u0448\u0443 \u043a\u0430\u0436\u0434\u043e\u0434\u043d\u0435\u0432\u043d\u0443\u044e \u0436\u0438\u0437\u043d\u044c \u0444\u0430\u043a\u0442\u0438\u0447\u0435\u0441\u043a\u043e\u0433\u043e \u0431\u0435\u0437 \u043d\u0430\u0448\u0435\u0433\u043e \u0432\u0435\u0434\u043e\u043c\u0430 \u0438 \u043a\u0430\u043a \u044d\u0442\u0438 \u0437\u0430\u0434\u0430\u0447\u0438 \u0441\u0432\u044f\u0437\u0430\u043d\u044b \u0441 SAT.<\/p>\n<p>  \u041f\u0440\u0438\u0432\u0435\u0434\u0435\u043c \u0441\u043f\u0438\u0441\u043e\u043a \u0437\u0430\u0434\u0430\u0447, \u043a\u043e\u0442\u043e\u0440\u044b\u0435 \u0432\u0441\u0442\u0440\u0435\u0447\u0430\u044e\u0442\u0441\u044f \u0432\u043e\u043a\u0440\u0443\u0433 \u043d\u0430\u0441 \u0438 \u0441\u043a\u0430\u0436\u0435\u043c, \u043a\u0430\u043a \u043e\u043d\u0438 \u0441\u0432\u044f\u0437\u0430\u043d\u044b \u0441 SAT.  <\/p>\n<ul>\n<li> \u041f\u0440\u0435\u0436\u0434\u0435 \u0432\u0441\u0435\u0433\u043e \u0443\u043f\u043e\u043c\u044f\u043d\u0435\u043c <a href=\"http:\/\/ru.wikipedia.org\/wiki\/RSA\">\u043a\u0440\u0438\u043f\u0442\u043e\u0433\u0440\u0430\u0444\u0438\u0447\u0435\u0441\u043a\u0438\u0439 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c RSA<\/a>, \u043a\u043e\u0442\u043e\u0440\u044b\u0435 \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u0435\u0442\u0441\u044f \u0434\u043b\u044f \u043e\u0431\u0435\u0441\u043f\u0435\u0447\u0435\u043d\u0438\u044f \u0431\u0435\u0437\u043e\u043f\u0430\u0441\u043d\u043e\u0441\u0442\u0438 \u0431\u0430\u043d\u043a\u043e\u0432\u0441\u043a\u0438\u0445 \u0442\u0440\u0430\u043d\u0437\u0430\u043a\u0446\u0438\u0439, \u0430 \u0442\u0430\u043a \u0436\u0435 \u0434\u043b\u044f \u0441\u043e\u0437\u0434\u0430\u043d\u0438\u044f \u0431\u0435\u0437\u043e\u043f\u0430\u0441\u043d\u043e\u0433\u043e \u0441\u043e\u0435\u0434\u0438\u043d\u0435\u043d\u0438\u044f. \u0410\u043b\u0433\u043e\u0440\u0438\u0442\u043c RSA \u043c\u043e\u0436\u0435\u0442 \u0431\u044b\u0442\u044c \u00ab\u0432\u0437\u043b\u043e\u043c\u0430\u043d\u00bb \u0441 \u043f\u043e\u043c\u043e\u0449\u044c\u044e SAT.<\/li>\n<li>\u041c\u043d\u043e\u0433\u0438\u0435 \u0440\u0435\u043a\u043e\u043c\u0435\u043d\u0434\u0430\u0442\u0435\u043b\u044c\u043d\u044b\u0435 \u0441\u0438\u0441\u0442\u0435\u043c\u044b (\u043d\u0430\u043f\u0440\u0438\u043c\u0435\u0440, \u0432 \u0441\u043e\u0441\u0442\u0430\u0432\u0435 Netflix) \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u044e\u0442 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c \u0440\u0430\u0437\u043b\u043e\u0436\u0435\u043d\u0438\u044f \u0431\u0443\u043b\u0435\u0432\u044b\u0445 \u043c\u0430\u0442\u0440\u0438\u0446 \u0434\u043b\u044f \u0440\u0435\u043a\u043e\u043c\u0435\u043d\u0434\u0430\u0446\u0438\u0438 \u043a\u043e\u043d\u0442\u0435\u043d\u0442\u0430. \u041e\u043f\u0442\u0438\u043c\u0430\u043b\u044c\u043d\u043e\u0435 \u0440\u0430\u0437\u043b\u043e\u0436\u0435\u043d\u0438\u0435 \u0442\u0430\u043a\u0438\u0445 \u043c\u0430\u0442\u0440\u0438\u0446 \u043c\u043e\u0436\u0435\u0442 \u0431\u044b\u0442\u044c \u043d\u0430\u0439\u0434\u0435\u043d\u043e \u0441 \u043f\u043e\u043c\u043e\u0449\u044c\u044e SAT.<\/li>\n<li>\u0417\u0430\u0434\u0430\u0447\u0430 \u043e\u043f\u0442\u0438\u043c\u0430\u043b\u044c\u043d\u043e\u0433\u043e \u0440\u0430\u0441\u043f\u0440\u0435\u0434\u0435\u043b\u0435\u043d\u0438\u044f \u0437\u0430\u0434\u0430\u0447 \u043f\u043e \u043f\u0440\u043e\u0446\u0435\u0441\u0441\u043e\u0440\u0430\u043c \u043c\u043e\u0436\u0435\u0442 \u0431\u044b\u0442\u044c \u0440\u0435\u0448\u0435\u043d\u0430 \u0441 \u043f\u043e\u043c\u043e\u0449\u044c\u044e SAT. \u0411\u043e\u043b\u044c\u0448\u043e\u0435 \u0447\u0438\u0441\u043b\u043e \u0437\u0430\u0434\u0430\u0447 \u043f\u043b\u0430\u043d\u0438\u0440\u043e\u0432\u0430\u043d\u0438\u044f \u0441\u0432\u043e\u0434\u0438\u0442\u0441\u044f \u043a SAT, \u043d\u0430\u043f\u0440\u0438\u043c\u0435\u0440, <a href=\"http:\/\/en.wikipedia.org\/wiki\/Open_shop_scheduling\">open shop scheduling<\/a>, \u0433\u0434\u0435 \u0437\u0430\u0434\u0430\u0447\u0438 (jobs) \u0434\u043e\u043b\u0436\u043d\u044b \u043f\u0440\u043e\u0439\u0442\u0438 \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u0435\u043d\u043d\u044b\u0435 \u0441\u0442\u0430\u0434\u0438\u0438 (\u0432\u044b\u043f\u043e\u043b\u043d\u0435\u043d\u043d\u044b\u043c\u0438 \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u0435\u043d\u043d\u044b\u043c\u0438 \u0440\u0430\u0431\u043e\u0447\u0438\u043c\u0438) \u0438 \u043d\u0435\u043e\u0431\u0445\u043e\u0434\u0438\u043c\u043e \u043c\u0438\u043d\u0438\u043c\u0438\u0437\u0438\u0440\u043e\u0432\u0430\u0442\u044c \u043e\u0431\u0449\u0443\u044e \u043f\u0440\u043e\u0434\u043e\u043b\u0436\u0438\u0442\u0435\u043b\u044c\u043d\u043e\u0441\u0442\u044c \u043e\u0431\u0440\u0430\u0431\u043e\u0442\u043a\u0438 \u0432\u0441\u0435\u0445 \u0437\u0430\u0434\u0430\u0447.<\/li>\n<li>NASA \u043f\u0440\u043e\u0432\u0435\u0440\u044f\u0435\u0442 \u0441\u043f\u0435\u0446\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438 \u0441\u0432\u043e\u0435\u0433\u043e <a href=\"http:\/\/babelfish.arc.nasa.gov\/trac\/jpf\/wiki\/intro\/testing_vs_model_checking\">\u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u043d\u043e\u0433\u043e \u043e\u0431\u0435\u0441\u043f\u0435\u0447\u0435\u043d\u0438\u044f<\/a> \u0438 <a href=\"http:\/\/shemesh.larc.nasa.gov\/fm\/fm-collins-formal-methods.html\">\u043c\u043e\u0434\u0435\u043b\u0435\u0439 <\/a>\u0441\u0432\u043e\u0435\u0433\u043e \u0442\u0435\u0445\u043d\u0438\u0447\u0435\u0441\u043a\u043e\u0433\u043e \u043e\u0431\u0435\u0441\u043f\u0435\u0447\u0435\u043d\u0438\u044f \u0441 \u043f\u043e\u043c\u043e\u0449\u044c\u044e \u043c\u0435\u0442\u043e\u0434\u043e\u0432 <a href=\"http:\/\/ru.wikipedia.org\/wiki\/%D0%9F%D1%80%D0%BE%D0%B2%D0%B5%D1%80%D0%BA%D0%B0_%D0%BC%D0%BE%D0%B4%D0%B5%D0%BB%D0%B5%D0%B9\">model checking<\/a>, \u043d\u0430\u043f\u0440\u044f\u043c\u0443\u044e \u0441\u0432\u044f\u0437\u0430\u043d\u043d\u043e\u0433\u043e \u0441 SAT.<\/li>\n<li>\u041f\u043e\u043f\u0443\u043b\u044f\u0440\u043d\u044b\u0439 \u043c\u0435\u0442\u043e\u0434 \u043a\u043b\u0430\u0441\u0442\u0435\u0440\u0438\u0437\u0430\u0446\u0438\u0438 <a href=\"http:\/\/en.wikipedia.org\/wiki\/K-means_clustering\">k-means<\/a> (\u043c\u0435\u0442\u043e\u0434 \u043a-\u0441\u0440\u0435\u0434\u043d\u0438\u0445) \u043c\u043e\u0436\u0435\u0442 \u0431\u044b\u0442\u044c \u0440\u0435\u0448\u0435\u043d \u0441 \u043f\u043e\u043c\u043e\u0449\u044c\u044e SAT.<\/li>\n<li>\u0411\u043e\u043b\u044c\u0448\u0438\u043d\u0441\u0442\u0432\u043e \u0438\u043d\u0442\u0435\u0440\u0435\u0441\u043d\u044b\u0445 \u0437\u0430\u0434\u0430\u0447 \u0441\u0432\u044f\u0437\u0430\u043d\u043d\u044b\u0445 \u0441 \u0433\u0440\u0430\u0444\u0430\u043c\u0438 (\u043d\u0430\u043f\u0440\u0438\u043c\u0435\u0440, \u0432 \u0441\u043e\u0446\u0438\u0430\u043b\u044c\u043d\u044b\u0445 \u0441\u0435\u0442\u044f\u0445, \u0433\u0440\u0430\u0444 \u2014 \u044d\u0442\u043e \u043e\u0442\u043d\u043e\u0448\u0435\u043d\u0438\u0435 \u0434\u0440\u0443\u0436\u0431\u044b \u043c\u0435\u0436\u0434\u0443 \u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u0442\u0435\u043b\u044f\u043c\u0438) \u2014 \u043f\u043e\u0438\u0441\u043a \u043d\u0430\u0438\u0431\u043e\u043b\u044c\u0448\u0435\u0433\u043e \u0441\u043e\u043e\u0431\u0449\u0435\u0441\u0442\u0432\u0430, \u0433\u0434\u0435 \u043a\u0430\u0436\u0434\u044b\u0439 \u0434\u0440\u0443\u0436\u0438\u0442 \u0441 \u043a\u0430\u0436\u0434\u044b\u043c, \u043f\u043e\u0438\u0441\u043a \u0441\u0430\u043c\u043e\u0433\u043e \u0434\u043b\u0438\u043d\u043d\u043e\u0433\u043e \u043f\u0443\u0442\u0438 \u0438 \u043c\u043d\u043e\u0433\u0438\u0435 \u0434\u0440\u0443\u0433\u0438\u0435 \u0437\u0430\u0434\u0430\u0447\u0438 \u043d\u0430 \u0433\u0440\u0430\u0444\u0430\u0445 \u043c\u043e\u0433\u0443\u0442 \u0431\u044b\u0442\u044c \u0440\u0435\u0448\u0435\u043d\u044b \u0441 \u043f\u043e\u043c\u043e\u0449\u044c\u044e SAT. \u0417\u0430\u0434\u0430\u0447\u0430 \u0438\u0437 \u0436\u0438\u0437\u043d\u0438 \u043c\u043e\u0441\u043a\u043e\u0432\u0441\u043a\u043e\u0439 \u043e\u0431\u043b\u0430\u0441\u0442\u0438 (\u0438 \u043d\u0435 \u0442\u043e\u043b\u044c\u043a\u043e): \u0441\u043e\u0441\u0442\u0430\u0432\u0438\u0442\u044c \u0440\u0430\u0441\u043f\u0438\u0441\u0430\u043d\u0438\u0435 \u043c\u0443\u0441\u043e\u0440\u043e\u0432\u043e\u0437\u043e\u0432 \u0442\u0430\u043a\u0438\u043c \u043e\u0431\u0440\u0430\u0437\u043e\u043c, \u0447\u0442\u043e\u0431\u044b \u043e\u043d\u0438 \u043e\u0431\u044a\u0435\u0445\u0430\u043b\u0438 \u0432\u0441\u0435 \u043f\u0443\u043d\u043a\u0442\u044b \u0441\u0431\u043e\u0440\u0430 \u043c\u0443\u0441\u043e\u0440\u0430 \u043f\u043e \u043e\u0434\u043d\u043e\u043c\u0443 \u0440\u0430\u0437\u0443 \u0437\u0430 \u043c\u0438\u043d\u0438\u043c\u0430\u043b\u044c\u043d\u043e\u0435 \u0432\u0440\u0435\u043c\u044f. \u0411\u043e\u043b\u044c\u0448\u043e\u0435 \u0447\u0438\u0441\u043b\u043e \u0437\u0430\u0434\u0430\u0447 \u0432 \u043b\u043e\u0433\u0438\u0441\u0442\u0438\u043a\u0435 \u0441\u0432\u043e\u0434\u0438\u0442\u0441\u044f \u043a \u0437\u0430\u0434\u0430\u0447\u0435 SAT.<\/li>\n<li>\u0414\u0430\u0436\u0435 <a href=\"http:\/\/ru.wikipedia.org\/wiki\/%D0%97%D0%B0%D0%B4%D0%B0%D1%87%D0%B0_%D0%BE_%D1%80%D0%B0%D0%BD%D1%86%D0%B5\">\u0437\u0430\u0434\u0430\u0447\u0430 \u043e \u0440\u0430\u043d\u0446\u0435 <\/a> \u043c\u043e\u0436\u0435\u0442 \u0431\u044b\u0442\u044c \u0440\u0435\u0448\u0435\u043d\u0430 \u0441 \u043f\u043e\u043c\u043e\u0449\u044c\u044e SAT. \u0417\u0430\u0434\u0430\u0447\u0430 \u0441\u043e\u0441\u0442\u043e\u0438\u0442 \u0432 \u0442\u043e\u043c, \u0447\u0442\u043e\u0431\u044b \u0438\u043c\u0435\u044f \u0440\u0430\u043d\u0435\u0446 \u0444\u0438\u043a\u0441\u0438\u0440\u043e\u0432\u0430\u043d\u043d\u043e\u0433\u043e \u0440\u0430\u0437\u043c\u0435\u0440\u0430, \u043d\u0430\u0431\u0440\u0430\u0442\u044c \u0432 \u043d\u0435\u0433\u043e \u043f\u0440\u0435\u0434\u043c\u0435\u0442\u043e\u0432 \u043d\u0430\u0438\u0431\u043e\u043b\u044c\u0448\u0435\u0439 \u0446\u0435\u043d\u043d\u043e\u0441\u0442\u0438 (\u0437\u043d\u0430\u044f \u0440\u0430\u0437\u043c\u0435\u0440\u044b \u0432\u0441\u0435\u0445 \u043f\u0440\u0435\u0434\u043c\u0435\u0442\u043e\u0432 \u0437\u0430\u0440\u0430\u043d\u0435\u0435).<\/li>\n<li>\u041c\u043d\u043e\u0433\u0438\u0435 \u0432\u0438\u0434\u0435\u043e \u0438\u0433\u0440\u044b \u043c\u043e\u0433\u0443\u0442 \u0431\u044b\u0442\u044c \u0440\u0435\u0448\u0435\u043d\u044b \u0441 \u043f\u043e\u043c\u043e\u0449\u044c\u044e SAT (\u0438 \u0434\u0430\u0436\u0435 <a href=\"http:\/\/habrahabr.ru\/post\/139993\/&amp;post=1203984_258\/\">\u041c\u0430\u0440\u0438\u043e<\/a>!) \u0422\u0430\u043a \u0436\u0435 \u043f\u0430\u0437\u043b <a href=\"http:\/\/www-imai.is.s.u-tokyo.ac.jp\/~yato\/data2\/SIGAL87-2.pdf\">\u0421\u0443\u0434\u043e\u043a\u0443<\/a> \u0438, \u0432\u043d\u0438\u043c\u0430\u043d\u0438\u0435, <a href=\"http:\/\/web.mat.bham.ac.uk\/R.W.Kaye\/minesw\/\">\u0421\u0430\u043f\u0435\u0440<\/a> \u043c\u043e\u0433\u0443\u0442 \u0431\u044b\u0442\u044c \u0440\u0435\u0448\u0435\u043d\u044b \u0441 \u043f\u043e\u043c\u043e\u0449\u044c\u044e SAT!<\/li>\n<li>\u0417\u0430\u0434\u0430\u0447\u0438 \u043e <a href=\"https:\/\/www.google.ru\/url?sa=t&amp;rct=j&amp;q=&amp;esrc=s&amp;source=web&amp;cd=5&amp;ved=0CFgQFjAE&amp;url=http%3A%2F%2Fwebcourse.cs.technion.ac.il%2F236825%2FSpring2013%2Fho%2FWCFiles%2FThe%2520Serializability%2520of%2520Concurrent%2520Database%2520Updates.pptx&amp;ei=GcW4UqHaNMWI4ASF2oGIAQ&amp;usg=AFQjCNHwtnWzinXu5qvjMlkNfb_kX4pBww&amp;sig2=U07eTRZb-qmapyHZ5IJLBw&amp;bvm=bv.58187178,d.bGE&amp;cad=rjt\">\u0441\u0435\u0440\u0438\u0430\u043b\u0438\u0437\u0430\u0446\u0438\u0438 \u0438\u0441\u0442\u043e\u0440\u0438\u0438 \u0442\u0440\u0430\u043d\u0437\u0430\u043a\u0446\u0438\u0439 <\/a>\u0432 \u0431\u0430\u0437\u0430\u0445 \u0434\u0430\u043d\u043d\u044b\u0445 \u043c\u043e\u0436\u0435\u0442 \u0431\u044b\u0442\u044c \u0440\u0435\u0448\u0435\u043d\u0430 \u0441 \u043f\u043e\u043c\u043e\u0449\u044c\u044e SAT.<\/li>\n<\/ul>\n<p>  \u0412\u0438\u0437\u0443\u0430\u043b\u0438\u0437\u0430\u0446\u0438\u044f \u0437\u0430\u0434\u0430\u0447, \u0440\u0435\u0448\u0430\u0435\u043c\u044b\u0445 \u0441 \u043f\u043e\u043c\u043e\u0449\u044c\u044e SAT (due to Bart Selman, \u0432\u0437\u044f\u0442\u043e <a href=\"https:\/\/courses.cs.washington.edu\/courses\/...\/10_17_phase_transition.ppt\u200e\">\u043e\u0442\u0441\u044e\u0434\u0430<\/a>)<br \/>  <img decoding=\"async\" src=\"http:\/\/habr.habrastorage.org\/post_images\/59d\/919\/610\/59d91961001799774470d6afa2bf1b5d.png\"\/><\/p>\n<h5>\u0427\u0442\u043e \u0437\u043d\u0430\u0447\u0438\u0442 \u00ab\u043c\u043e\u0433\u0443\u0442 \u0431\u044b\u0442\u044c \u0440\u0435\u0448\u0435\u043d\u044b\u00bb \u0438 \u043f\u0440\u0438 \u0447\u0435\u043c \u0442\u0443\u0442 NP<\/h5>\n<p>  \u0423\u043f\u0440\u043e\u0449\u0435\u043d\u043d\u043e \u0433\u043e\u0432\u043e\u0440\u044f, \u0435\u0441\u043b\u0438 \u0443 \u043d\u0430\u0441 \u0435\u0441\u0442\u044c \u044d\u0444\u0444\u0435\u043a\u0442\u0438\u0432\u043d\u043e\u0435 \u0440\u0435\u0448\u0435\u043d\u0438\u0435 \u0437\u0430\u0434\u0430\u0447\u0438 SAT, \u0442\u043e \u043c\u044b \u043c\u043e\u0436\u0435\u043c \u044d\u0444\u0444\u0435\u043a\u0442\u0438\u0432\u043d\u043e \u0440\u0435\u0448\u0430\u0442\u044c \u0432\u0441\u0435 \u0443\u043a\u0430\u0437\u0430\u043d\u043d\u044b\u0435 \u0437\u0430\u0434\u0430\u0447\u0438. \u0427\u0442\u043e \u043a\u043e\u043d\u043a\u0440\u0435\u0442\u043d\u043e \u043f\u043e\u0434\u0440\u0430\u0437\u0443\u043c\u0435\u0432\u0430\u0435\u0442\u0441\u044f \u043f\u043e\u0434 \u044d\u0444\u0444\u0435\u043a\u0442\u0438\u0432\u043d\u043e\u0441\u0442\u044c\u044e \u0437\u0430\u0432\u0438\u0441\u0438\u0442 \u043e\u0442 \u043a\u043e\u043d\u043a\u0440\u0435\u0442\u043d\u043e\u0439 \u0437\u0430\u0434\u0430\u0447\u0438, \u043d\u043e \u0437\u0434\u0435\u0441\u044c \u0431\u0443\u0434\u0435\u043c \u0441\u0447\u0438\u0442\u0430\u0442\u044c, \u0447\u0442\u043e \u0432\u0440\u0435\u043c\u044f \u0440\u0430\u0431\u043e\u0442\u044b \u044f\u0432\u043b\u044f\u0435\u0442\u0441\u044f \u043f\u0440\u0438\u0435\u043c\u043b\u0435\u043c\u044b\u043c \u0434\u043b\u044f \u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u0442\u0435\u043b\u044f (\u0434\u043b\u044f \u0441\u043e\u0441\u0442\u0430\u0432\u043b\u0435\u043d\u0438\u044f \u0440\u0430\u0441\u043f\u0438\u0441\u0430\u043d\u0438\u044f \u0448\u043a\u043e\u043b\u044b \u043d\u0430 \u0441\u0435\u043c\u0435\u0441\u0442\u0440, \u043c\u044b \u043c\u043e\u0436\u0435\u043c \u043f\u043e\u0441\u0432\u044f\u0442\u0438\u0442\u044c \u043f\u0430\u0440\u0443 \u0434\u043d\u0435\u0439 \u0432\u044b\u0447\u0438\u0441\u043b\u0435\u043d\u0438\u044f\u043c, \u0430 \u0434\u043b\u044f \u043c\u0435\u0442\u043e\u0434\u0430 \u043a\u043b\u0430\u0441\u0442\u0435\u0440\u0438\u0437\u0430\u0446\u0438\u0438, \u043c\u044b \u0431\u044b \u0445\u043e\u0442\u0435\u043b\u0438 \u043f\u043e\u043b\u0443\u0447\u0438\u0442\u044c \u0440\u0435\u0437\u0443\u043b\u044c\u0442\u0430\u0442 \u0432 \u0438\u043d\u0442\u0435\u0440\u0430\u043a\u0442\u0438\u0432\u043d\u043e\u043c \u0440\u0435\u0436\u0438\u043c\u0435). \u0410 \u0434\u043b\u044f \u043c\u043d\u043e\u0433\u0438\u0445 \u0438\u0437 \u0443\u043a\u0430\u0437\u0430\u043d\u043d\u044b\u0445 \u0432\u044b\u0448\u0435 \u0437\u0430\u0434\u0430\u0447 \u0432\u0435\u0440\u043d\u043e \u0438 \u043e\u0431\u0440\u0430\u0442\u043d\u043e\u0435, \u0435\u0441\u043b\u0438 \u043c\u044b \u0443\u043c\u0435\u0435\u043c \u044d\u0444\u0444\u0435\u043a\u0442\u0438\u0432\u043d\u043e \u0440\u0435\u0448\u0430\u0442\u044c \u0438\u0445, \u0442\u043e \u043c\u044b \u0443\u043c\u0435\u0435\u0442 \u044d\u0444\u0444\u0435\u043a\u0442\u0438\u0432\u043d\u043e \u0440\u0435\u0448\u0430\u0442\u044c SAT (\u044d\u0442\u043e \u0438 \u043d\u0430\u0437\u044b\u0432\u0430\u0435\u0442\u0441\u044f NP-\u043f\u043e\u043b\u043d\u043e\u0442\u043e\u0439 \u2014 \u0434\u0430\u043d\u043d\u043e\u0435 \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u0435\u043d\u0438\u0435 \u043d\u0435\u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u043e, \u043d\u043e \u0434\u043e\u0441\u0442\u0430\u0442\u043e\u0447\u043d\u043e \u0434\u043b\u044f \u043e\u0431\u0449\u0435\u0433\u043e \u043f\u043e\u043d\u0438\u043c\u0430\u043d\u0438\u044f).<\/p>\n<p>  \u0412\u0441\u0435 \u044d\u0442\u0438 \u0437\u0430\u0434\u0430\u0447\u0438 \u043b\u0435\u0436\u0430\u0442 \u0432 \u043a\u043b\u0430\u0441\u0441\u0435 NP \u2014 \u043f\u043e\u0437\u0434\u043d\u0435\u0435 \u043c\u044b \u043e\u043f\u0438\u0448\u0435\u043c \u043a\u043b\u0430\u0441\u0441 \u0434\u0435\u0442\u0430\u043b\u044c\u043d\u0435\u0435, \u0441\u0435\u0439\u0447\u0430\u0441 \u0436\u0435 \u043d\u0430\u043c \u0441\u0442\u043e\u0438\u0442 \u043e\u0442\u043c\u0435\u0442\u0438\u0442\u044c, \u0447\u0442\u043e, \u0435\u0441\u043b\u0438 \u0438\u0437\u0432\u0435\u0441\u0442\u043d\u043e \u044d\u0444\u0444\u0435\u043a\u0442\u0438\u0432\u043d\u043e\u0435 \u0440\u0435\u0448\u0435\u043d\u0438\u0435 \u0437\u0430\u0434\u0430\u0447\u0438 SAT, \u0442\u043e \u043c\u044b \u043c\u043e\u0436\u0435\u043c \u044d\u0444\u0444\u0435\u043a\u0442\u0438\u0432\u043d\u043e \u0440\u0435\u0448\u0430\u0442\u044c <b>\u043b\u044e\u0431\u0443\u044e<\/b> \u0437\u0430\u0434\u0430\u0447\u0443 \u0432 \u043a\u043b\u0430\u0441\u0441\u0435 NP. \u0418\u043d\u0430\u0447\u0435 \u0433\u043e\u0432\u043e\u0440\u044f, SAT \u2014 \u044d\u0442\u043e \u0437\u0430\u0434\u0430\u0447\u0430 \u043f\u0440\u0435\u0434\u0441\u0442\u0430\u0432\u0438\u0442\u0435\u043b\u044c \u043a\u043b\u0430\u0441\u0441\u0430, \u043e\u043d\u0430 \u044f\u0432\u043b\u044f\u0435\u0442\u0441\u044f \u00ab\u0441\u043b\u043e\u0436\u043d\u0435\u0439\u0448\u0435\u0439\u00bb \u0432 \u0441\u0432\u043e\u0435\u043c \u043a\u043b\u0430\u0441\u0441\u0435 \u0438 \u043f\u043e\u0437\u0432\u043e\u043b\u044f\u0435\u0442 \u0440\u0435\u0448\u0438\u0442\u044c \u0432\u0441\u0435 \u0434\u0440\u0443\u0433\u0438\u0435 \u0437\u0430\u0434\u0430\u0447\u0438 \u0432 NP.<\/p>\n<h5>\u0418\u0441\u0442\u043e\u0440\u0438\u044f SAT \u0438 NP-\u043f\u043e\u043b\u043d\u043e\u0442\u044b <\/h5>\n<p>  <\/p>\n<h6>NP-\u043f\u043e\u043b\u043d\u043e\u0442\u0430<\/h6>\n<p>  <a href=\"http:\/\/en.wikipedia.org\/wiki\/Computational_complexity_theory\">\u0422\u0435\u043e\u0440\u0438\u044f \u0432\u044b\u0447\u0438\u0441\u043b\u0438\u0442\u0435\u043b\u044c\u043d\u043e\u0439 \u0441\u043b\u043e\u0436\u043d\u043e\u0441\u0442\u0438<\/a>, \u0432 \u043a\u043e\u0442\u043e\u0440\u043e\u0439 \u044f\u0437\u044b\u043a\u0438 \u0438 \u0444\u0443\u043d\u043a\u0446\u0438\u0438 \u0432\u044b\u0434\u0435\u043b\u044f\u044e\u0442 \u0432 \u0440\u0430\u0437\u043d\u044b\u0435 \u043a\u043b\u0430\u0441\u0441\u044b \u043f\u043e \u043a\u043e\u043b\u0438\u0447\u0435\u0441\u0442\u0432\u0443 \u0432\u0440\u0435\u043c\u0435\u043d\u0438 \u0438 \u043f\u0430\u043c\u044f\u0442\u0438 \u043d\u0435\u043e\u0431\u0445\u043e\u0434\u0438\u043c\u044b\u0435 \u0434\u043b\u044f \u0438\u0445 \u0432\u044b\u0447\u0438\u0441\u043b\u0435\u043d\u0438\u0439, \u0440\u043e\u0434\u0438\u043b\u0430\u0441\u044c \u0438\u0437 <a href=\"http:\/\/en.wikipedia.org\/wiki\/Theory_of_computation\">\u0442\u0435\u043e\u0440\u0438\u0438 \u0432\u044b\u0447\u0438\u0441\u043b\u0438\u043c\u043e\u0441\u0442\u0438 <\/a>(\u0442.\u0435. <a href=\"http:\/\/en.wikipedia.org\/wiki\/History_of_the_Church%E2%80%93Turing_thesis\">\u0440\u0430\u0431\u043e\u0442<\/a> 30\u044b\u0445 \u0433\u043e\u0434\u043e\u0432 \u0413\u0451\u0434\u0435\u043b\u044f, \u0427\u0451\u0440\u0447\u0430 \u0438 \u0422\u044c\u044e\u0440\u0438\u043d\u0433\u0430), \u043a\u043e\u0433\u0434\u0430 \u0425\u0430\u0440\u0442\u043c\u0430\u043d\u0438\u0441, \u0428\u0442\u0435\u0440\u043dc, \u041b\u0435\u0432\u0438\u0441 (1965) \u043f\u0440\u0435\u0434\u043b\u043e\u0436\u0438\u043b\u0438 \u043e\u0434\u043d\u0443 \u0438\u0437 \u043f\u0435\u0440\u0432\u044b\u0445 \u043f\u043e\u0434\u043e\u0431\u043d\u044b\u0445 \u043a\u043b\u0430\u0441\u0441\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0439 \u0444\u0443\u043d\u043a\u0446\u0438\u0439 (\u043e\u0440\u0438\u0433\u0438\u043d\u0430\u043b\u044c\u043d\u044b\u0435 \u0440\u0430\u0431\u043e\u0442\u044b: <a href=\"http:\/\/www.ams.org\/journals\/tran\/1965-117-00\/S0002-9947-1965-0170805-7\/S0002-9947-1965-0170805-7.pdf\">\u0442\u0443\u0442<\/a> \u0438 <a href=\"http:\/\/www.cs.albany.edu\/~res\/space.pdf\">\u0442\u0443\u0442<\/a>).<\/p>\n<p>  \u041a\u043e\u043d\u0446\u0435\u043f\u0446\u0438\u044f NP-\u043f\u043e\u043b\u043d\u043e\u0442\u044b \u0440\u0430\u0437\u0432\u0438\u0432\u0430\u043b\u0430\u0441\u044c \u0432 1960\u0445-1970\u0445 \u0433\u043e\u0434\u0430\u0445 \u043d\u0435\u0437\u0430\u0432\u0438\u0441\u0438\u043c\u043e \u0432 \u0421\u0421\u0421\u0420 \u0438 C\u0428\u0410 (\u042d\u0434\u043c\u043e\u043d\u0434\u0441, \u041b\u0435\u0432\u0438\u043d, \u042f\u0431\u043b\u043e\u043d\u0441\u043a\u0438\u0439 et al.). \u0412 1971 \u0433\u043e\u0434\u0443 \u0421\u0442\u0438\u0432\u0435\u043d \u041a\u0443\u043a \u0441\u0444\u043e\u0440\u043c\u0443\u043b\u0438\u0440\u043e\u0432\u0430\u043b \u0433\u0438\u043f\u043e\u0442\u0435\u0437\u0443 \u043e P vs. NP. \u0422\u0435\u043e\u0440\u0435\u043c\u0443 \u043e \u0442\u043e\u043c, \u0447\u0442\u043e SAT \u044f\u0432\u043b\u044f\u0435\u0442\u0441\u044f \u00ab\u0443\u043d\u0438\u0432\u0435\u0440\u0441\u0430\u043b\u044c\u043d\u043e\u0439 \u0437\u0430\u0434\u0430\u0447\u0435\u0439\u00bb \u0434\u043b\u044f \u043a\u043b\u0430\u0441\u0441\u0430 NP \u0438 \u043f\u043e\u0437\u0432\u043e\u043b\u044f\u0435\u0442 \u0440\u0435\u0448\u0438\u0442\u044c \u043b\u044e\u0431\u0443\u044e \u0437\u0430\u0434\u0430\u0447\u0443 \u0432 \u044d\u0442\u043e\u043c \u043a\u043b\u0430\u0441\u0441\u0435 (NP-\u043f\u043e\u043b\u043d\u043e\u0442\u0430) \u043d\u0435\u0437\u0430\u0432\u0438\u0441\u0438\u043c\u043e \u0434\u043e\u043a\u0430\u0437\u0430\u043b\u0438 \u041b\u0435\u043e\u043d\u0438\u0434 \u041b\u0435\u0432\u0438\u043d (1973) \u0438 \u0421\u0442\u0438\u0432\u0435\u043d \u041a\u0443\u043a, \u0438 \u043d\u0430\u0437\u044b\u0432\u0430\u0435\u0442\u0441\u044f <a href=\"http:\/\/en.wikipedia.org\/wiki\/Cook-Levin_theorem\">\u0442\u0435\u043e\u0440\u0435\u043c\u043e\u0439 \u041b\u0435\u0432\u0438\u043d\u0430-\u041a\u0443\u043a\u0430<\/a>. \u0412 1982\u043e\u043c \u041a\u0443\u043a \u043f\u043e\u043b\u0443\u0447\u0438\u0442 \u0437\u0430 \u044d\u0442\u0443 \u0440\u0430\u0431\u043e\u0442\u0443 \u043f\u0440\u0435\u043c\u0438\u044e \u0422\u044c\u044e\u0440\u0438\u043d\u0433\u0430.<\/p>\n<p>  \u0412 1972\u043e\u043c \u041a\u0430\u0440\u043f \u043f\u0443\u0431\u043b\u0438\u043a\u0443\u0435\u0442 <a href=\"http:\/\/www.win.tue.nl\/~gwoegi\/AC\/karp-1971.pdf\">Reducibility among combinatorial problems<\/a>, \u0441\u043f\u0438\u0441\u043e\u043a \u043f\u043e\u043a\u0430\u0437\u044b\u0432\u0430\u044e\u0449\u0438\u0439, \u0447\u0442\u043e SAT \u0434\u0430\u043b\u0435\u043a\u043e \u043d\u0435 \u0435\u0434\u0438\u043d\u0441\u0442\u0432\u0435\u043d\u043d\u0430\u044f \u0438\u043d\u0442\u0435\u0440\u0435\u0441\u043d\u0430\u044f \u0437\u0430\u0434\u0430\u0447\u0430 \u0432 NP \u0438 \u043e\u0433\u0440\u043e\u043c\u043d\u043e\u0435 \u043a\u043e\u043b\u0438\u0447\u0435\u0441\u0442\u0432\u043e \u0437\u0430\u0434\u0430\u0447 \u043b\u0435\u0436\u0438\u0442 \u0432 NP \u0438 \u044d\u043a\u0432\u0438\u0432\u0430\u043b\u0435\u043d\u0442\u043d\u043e SAT. \u0412 1985\u043e\u043c \u041a\u0430\u0440\u043f \u043f\u043e\u043b\u0443\u0447\u0438\u0442 \u0437\u0430 \u044d\u0442\u0443 \u0440\u0430\u0431\u043e\u0442\u0443 \u043f\u0440\u0435\u043c\u0438\u044e \u0422\u044c\u044e\u0440\u0438\u043d\u0433\u0430.<\/p>\n<p>  \u0412 1974\u043e\u043c \u0424\u0430\u0433\u0438\u043d \u043f\u043e\u043a\u0430\u0436\u0435\u0442, \u0447\u0442\u043e NP \u0442\u0435\u0441\u043d\u043e \u0441\u0432\u044f\u0437\u0430\u043d \u0441 \u043a\u043b\u0430\u0441\u0441\u0438\u0447\u0435\u0441\u043a\u043e\u0439 \u043b\u043e\u0433\u0438\u043a\u043e\u0439, \u0430 \u0438\u043c\u0435\u043d\u043d\u043e, \u0447\u0442\u043e NP \u044d\u043a\u0432\u0438\u0432\u0430\u043b\u0435\u043d\u0442\u0435\u043d \u044d\u043a\u0437\u0438\u0441\u0442\u0435\u043d\u0446\u0438\u0430\u043b\u044c\u043d\u044b\u043c \u043b\u043e\u0433\u0438\u0447\u0435\u0441\u043a\u0438\u043c \u0441\u0442\u0440\u0443\u043a\u0442\u0443\u0440\u0430\u043c \u0432\u0442\u043e\u0440\u043e\u0433\u043e \u043f\u043e\u0440\u044f\u0434\u043a\u0430 (<a href=\"http:\/\/en.wikipedia.org\/wiki\/Fagin&#39;s_theorem\">\u0442\u0435\u043e\u0440\u0435\u043c\u0430 \u0424\u0430\u0433\u0438\u043d\u0430<\/a>). <\/p>\n<p>  \u0412 1975\u043e\u043c \u0433\u043e\u0434\u0443 \u0411\u0435\u0439\u043a\u0435\u0440, \u0414\u0436\u0438\u043b, \u0421\u043e\u043b\u043e\u0432\u044d\u0439 \u043f\u043e\u043b\u0443\u0447\u0438\u043b\u0438 \u043f\u0435\u0440\u0432\u044b\u0439 \u0444\u0443\u043d\u0434\u0430\u043c\u0435\u043d\u0442\u0430\u043b\u044c\u043d\u044b\u0439 \u043c\u0435\u0442\u0430-\u0440\u0435\u0437\u0443\u043b\u044c\u0442\u0430\u0442 \u043e \u043d\u0435\u0440\u0430\u0437\u0440\u0435\u0448\u0438\u043c\u043e\u0441\u0442\u0438 \u0437\u0430\u0434\u0430\u0447\u0438 P vs. NP \u0441 \u043f\u043e\u043c\u043e\u0449\u044c\u044e \u0440\u0435\u0433\u0443\u043b\u044f\u0440\u0438\u0437\u0438\u0440\u0443\u0435\u043c\u044b\u0445 \u043c\u0435\u0442\u043e\u0434\u043e\u0432 \u0442.\u0435. \u044d\u0442\u043e \u043f\u0435\u0440\u0432\u044b\u0439 \u0440\u0435\u0437\u0443\u043b\u044c\u0442\u0430\u0442, \u043f\u043e\u043a\u0430\u0437\u044b\u0432\u0430\u044e\u0449\u0438\u0439, \u0447\u0442\u043e \u0446\u0435\u043b\u044b\u0439 \u043a\u043b\u0430\u0441\u0441 \u043c\u0435\u0442\u043e\u0434\u043e\u0432 \u043d\u0435 \u043c\u043e\u0436\u0435\u0442 \u043e\u0442\u0432\u0435\u0442\u0438\u0442\u044c \u043d\u0430 \u0432\u043e\u043f\u0440\u043e\u0441 \u0440\u0430\u0432\u0435\u043d\u0441\u0442\u0432\u0430 P vs. NP (\u043f\u043e\u0434\u0440\u043e\u0431\u043d\u0435\u0435 \u043e\u0431 \u044d\u0442\u043e\u043c \u043d\u0430\u043f\u0438\u0441\u0430\u043d\u043e <a href=\"http:\/\/www.scottaaronson.com\/papers\/alg.pdf\">\u0437\u0434\u0435\u0441\u044c<\/a>).<\/p>\n<p>  \u0412 1979\u043e\u043c \u0433\u043e\u0434\u0443 \u0413\u044d\u0440\u0438 \u0438 \u0414\u0436\u043e\u043d\u0441\u043e\u043d \u043d\u0430\u043f\u0438\u0448\u0443\u0442 &quot;<a href=\"http:\/\/en.wikipedia.org\/wiki\/Computers_and_Intractability:_A_Guide_to_the_Theory_of_NP-Completeness\">\u0412\u044b\u0447\u0438\u0441\u043b\u0438\u0442\u0435\u043b\u044c\u043d\u044b\u0435 \u043c\u0430\u0448\u0438\u043d\u044b \u0438 \u0442\u0440\u0443\u0434\u043d\u043e\u0440\u0435\u0448\u0430\u0435\u043c\u044b\u0435 \u0437\u0430\u0434\u0430\u0447\u0438<\/a>&quot;, \u043e\u0434\u0438\u043d \u0438\u0437 \u043d\u0430\u0438\u0431\u043e\u043b\u0435\u0435 \u043f\u043e\u043b\u043d\u044b\u0445 \u0438\u0441\u0442\u043e\u0447\u043d\u0438\u043a\u043e\u0432 \u0438\u043d\u0444\u043e\u0440\u043c\u0430\u0446\u0438\u0438 \u043f\u043e NP-\u043f\u043e\u043b\u043d\u043e\u0442\u0435 \u0438 \u043f\u043e\u0434\u0440\u043e\u0431\u043d\u044b\u0439 \u043a\u0430\u0442\u0430\u043b\u043e\u0433 \u0437\u0430\u0434\u0430\u0447. \u041d\u0435\u0441\u043c\u043e\u0442\u0440\u044f \u043d\u0430 \u0442\u043e, \u0447\u0442\u043e \u043d\u0435\u043a\u043e\u0442\u043e\u0440\u044b\u0435 \u0442\u0435\u043e\u0440\u0435\u0442\u0438\u0447\u0435\u0441\u043a\u0438\u0435 \u0440\u0435\u0437\u0443\u043b\u044c\u0442\u0430\u0442\u044b \u0432 \u0434\u0430\u043d\u043d\u044b\u0439 \u043c\u043e\u043c\u0435\u043d\u0442 \u0441\u0447\u0438\u0442\u0430\u044e\u0442\u0441\u044f \u0443\u0441\u0442\u0430\u0440\u0435\u0432\u0448\u0438\u043c\u0438, \u044d\u0442\u043e \u043e\u0434\u0438\u043d \u0438\u0437 \u043d\u0430\u0438\u0431\u043e\u043b\u0435\u0435 \u0444\u0443\u043d\u0434\u0430\u043c\u0435\u043d\u0442\u0430\u043b\u044c\u043d\u044b\u0445 \u0442\u0440\u0443\u0434\u043e\u0432 \u0432 \u043e\u0431\u043b\u0430\u0441\u0442\u0438 \u0432\u044b\u0447\u0438\u0441\u043b\u0438\u0442\u0435\u043b\u044c\u043d\u043e\u0439 \u0441\u043b\u043e\u0436\u043d\u043e\u0441\u0442\u0438.<\/p>\n<p>  \u0412\u0438\u0437\u0443\u0430\u043b\u0438\u0437\u0430\u0446\u0438\u044f \u043e\u0442\u043d\u043e\u0448\u0435\u043d\u0438\u0439 \u043c\u0435\u0436\u0434\u0443 \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u044b\u043c\u0438 \u044f\u0437\u044b\u043a\u0430, \u0442\u0435\u043e\u0440\u0438\u0439 \u0432\u044b\u0447\u0438\u0441\u043b\u0438\u0442\u0435\u043b\u044c\u043d\u043e\u0439 \u0441\u043b\u043e\u0436\u043d\u043e\u0441\u0442\u0438 \u0438 \u0442\u0435\u043e\u0440\u0438\u0438 \u0432\u044b\u0447\u0438\u0441\u043b\u0435\u043d\u0438\u0439 (<a href=\"http:\/\/en.wikipedia.org\/wiki\/Computational_complexity_theory#History\">\u043e\u0442\u0441\u044e\u0434\u0430<\/a>):<br \/>  <img decoding=\"async\" src=\"http:\/\/habr.habrastorage.org\/post_images\/8da\/c1a\/fd5\/8dac1afd550b814bf49a36f2fba1cd54.png\"\/><\/p>\n<h6>\u041e\u0447\u0435\u043d\u044c \u043a\u0440\u0430\u0442\u043a\u0430\u044f \u0438\u0441\u0442\u043e\u0440\u0438\u044f SAT-solvers<\/h6>\n<p>  \u0412 1960\u0445 \u0414\u044d\u0432\u0438\u0441 \u0438 \u041f\u0443\u0442\u043c\u0430\u043d \u043d\u0430\u0447\u0430\u043b\u0438 \u043f\u0440\u0438\u043c\u0435\u043d\u044f\u0442\u044c \u043a\u043b\u0430\u0441\u0441\u0438\u0447\u0435\u0441\u043a\u0438 \u0434\u0435\u0434\u0443\u043a\u0442\u0438\u0432\u043d\u044b\u0435 (\u0433\u043e\u0432\u043e\u0440\u044f \u0443\u043f\u0440\u043e\u0449\u0435\u043d\u043d\u044b\u043c\u0438 \u044f\u0437\u044b\u043a\u043e\u043c, \u043c\u0435\u0442\u043e\u0434\u044b \u0434\u043b\u044f \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u0430 \u0442\u0435\u043e\u0440\u0435\u043c) \u043c\u0435\u0442\u043e\u0434\u044b \u0434\u043b\u044f \u0440\u0435\u0448\u0435\u043d\u0438\u044f SAT (<a href=\"http:\/\/www.ensiie.fr\/~blazy\/ipr\/article1.pdf\">\u043e\u0440\u0438\u0433\u0438\u043d\u0430\u043b\u044c\u043d\u0430\u044f \u0440\u0430\u0431\u043e\u0442\u0430<\/a>). <\/p>\n<p>  \u0412 1962\u043e\u043c \u0433\u043e\u0434\u0443 \u0414\u044d\u0432\u0438\u0441, \u041f\u0430\u0442\u043d\u0435\u043c, \u041b\u043e\u0433\u0435\u043c\u0430\u043d, \u041b\u0430\u0432\u043b\u0435\u043d\u0434 \u043f\u0440\u0435\u0434\u043b\u043e\u0436\u0438\u043b\u0438 <a href=\"http:\/\/en.wikipedia.org\/wiki\/DPLL_algorithm\">DPLL \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c<\/a>, \u043e\u0441\u043d\u043e\u0432\u0430\u043d\u043d\u044b\u0439 \u043d\u0430 \u043f\u043e\u0438\u0441\u043a\u0435 \u0441 \u0432\u043e\u0437\u0432\u0440\u0430\u0442\u043e\u043c \u0438 \u0440\u0430\u0441\u043f\u0440\u043e\u0441\u0442\u0440\u0430\u043d\u0435\u043d\u0438\u0438 \u0434\u0435\u0442\u0435\u0440\u043c\u0438\u043d\u0438\u0440\u043e\u0432\u0430\u043d\u043d\u044b\u0445 \u0432\u044b\u0447\u0438\u0441\u043b\u0435\u043d\u0438\u0439 (unit-propagation). \u0413\u043e\u0432\u043e\u0440\u044f \u0443\u043f\u0440\u043e\u0449\u0435\u043d\u043d\u043e, \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c \u043f\u0440\u0435\u0434\u043f\u043e\u043b\u0430\u0433\u0430\u043b \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0435 \u043d\u0435\u043a\u043e\u0442\u043e\u0440\u043e\u0439 \u043f\u0435\u0440\u0435\u043c\u0435\u043d\u043d\u043e\u0439 \u0440\u0430\u0432\u043d\u043e\u0439 \u0438\u0441\u0442\u0438\u043d\u0435 \u0438 \u0432\u044b\u0447\u0438\u0441\u043b\u044f\u043b \u0432\u0441\u0435 \u0434\u0435\u0442\u0435\u0440\u043c\u0438\u043d\u0438\u0440\u043e\u0432\u0430\u043d\u043d\u044b\u0435 \u0441\u043b\u0435\u0434\u0441\u0442\u0432\u0438\u044f \u043f\u043e\u0434\u043e\u0431\u043d\u043e\u0433\u043e \u0440\u0435\u0448\u0435\u043d\u0438\u044f \u0438 \u043f\u043e\u0432\u0442\u043e\u0440\u044f\u043b, \u043f\u043e\u043a\u0430 \u043d\u0435 \u043d\u0430\u0439\u0434\u0435\u0442 \u0440\u0435\u0448\u0435\u043d\u0438\u044f. \u0414\u0430\u043d\u043d\u044b\u0435 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c \u0441\u043b\u0443\u0436\u0438\u043b \u043e\u0441\u043d\u043e\u0432\u043e\u0439 \u043c\u043d\u043e\u0433\u0438\u0445 SAT solver&#8217;\u043e\u0432 \u043d\u0430 \u043f\u0440\u043e\u0442\u044f\u0436\u0435\u043d\u0438\u0438 \u0434\u0435\u0441\u044f\u0442\u0438\u043b\u0435\u0442\u0438\u0439.<\/p>\n<p>  \u0412 1992\u043e\u043c \u0421\u0435\u043b\u043c\u0430\u043d, \u041b\u0435\u0432\u0435\u0441\u043a\u044c\u044e \u0438 \u041c\u0438\u0442\u0447\u0435\u043b\u043b \u043f\u0440\u0435\u0434\u043b\u043e\u0436\u0438\u043b\u0438 \u043c\u0435\u0442\u043e\u0434 \u043b\u043e\u043a\u0430\u043b\u044c\u043d\u043e\u0433\u043e \u043f\u043e\u0438\u0441\u043a\u0430 \u0432<a href=\"http:\/\/www.cfdvs.iitb.ac.in\/download\/Docs\/verification\/papers\/sat\/original-papers\/gsat.pdf\"> \u0441\u0442\u0430\u0442\u044c\u0435 GSAT.<\/a> GSAT \u2014 \u043e\u0437\u043d\u0430\u0447\u0430\u0435\u0442 Greedy SAT, \u043b\u043e\u043a\u0430\u043b\u044c\u043d\u044b\u0439 \u0442\u0430\u043a \u043a\u0430\u043a \u043f\u0440\u0438\u043d\u0438\u043c\u0430\u0435\u0442 \u0440\u0435\u0448\u0435\u043d\u0438\u0435 \u043e \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0438 \u043f\u0435\u0440\u0435\u043c\u0435\u043d\u043d\u044b\u0445 \u043d\u0430 \u043e\u0441\u043d\u043e\u0432\u0435 \u0442\u043e\u043b\u044c\u043a\u043e \u043b\u043e\u043a\u0430\u043b\u044c\u043d\u043e\u0439 \u0438\u043d\u0444\u043e\u0440\u043c\u0430\u0446\u0438\u0438. \u0410\u043b\u0433\u043e\u0440\u0438\u0442\u043c \u043d\u0430\u0447\u0438\u043d\u0430\u043b \u0441 \u043f\u0440\u043e\u0438\u0437\u0432\u043e\u043b\u044c\u043d\u043e\u0433\u043e \u043d\u0430\u0437\u043d\u0430\u0447\u0435\u043d\u0438\u044f \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0439 \u043f\u0435\u0440\u0435\u043c\u0435\u043d\u043d\u044b\u0445 \u0438 \u0438\u0437\u043c\u0435\u043d\u044f\u043b \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0435 \u043f\u0435\u0440\u0435\u043c\u0435\u043d\u043d\u043e\u0439, \u0435\u0441\u043b\u0438 \u043e\u043d\u0430 \u0434\u0430\u0432\u0430\u043b\u0430 \u043d\u0430\u0438\u0431\u043e\u043b\u044c\u0448\u0438\u0439 \u043f\u0440\u0438\u0440\u043e\u0441\u0442 \u0432\u044b\u043f\u043e\u043b\u043d\u0435\u043d\u043d\u044b\u0445 \u043f\u0440\u0435\u0434\u043b\u043e\u0436\u0435\u043d\u0438\u0439. \u0412\u043f\u043e\u0441\u043b\u0435\u0434\u0441\u0442\u0432\u0438\u0438 \u043c\u0435\u0442\u043e\u0434\u044b \u043b\u043e\u043a\u0430\u043b\u044c\u043d\u043e\u0433\u043e \u043f\u043e\u0438\u0441\u043a\u0430 \u0432 \u0441\u0430\u043c\u044b\u0445 \u0440\u0430\u0437\u043b\u0438\u0447\u043d\u044b\u0445 \u0432\u0430\u0440\u0438\u0430\u0446\u0438\u044f\u0445 \u0431\u044b\u043b\u0438 \u0438\u043d\u0442\u0435\u0433\u0440\u0438\u0440\u043e\u0432\u0430\u043d\u044b \u0432 \u0431\u043e\u043b\u044c\u0448\u0438\u043d\u0441\u0442\u0432\u043e SAT solver&#8217;\u043e\u0432 \u2014 \u0432 1999 \u0425\u0435\u0433\u043b\u0435\u0440 \u0425\u0443\u0441 \u0432 \u0441\u0432\u043e\u0435\u0439 PhD \u0434\u0438\u0441\u0441\u0435\u0440\u0442\u0430\u0446\u0438\u0438 \u043f\u0440\u0438\u0432\u043e\u0434\u0438\u0442 \u043e\u0431\u0448\u0438\u0440\u043d\u043e\u0435 \u0438\u0441\u0441\u043b\u0435\u0434\u043e\u0432\u0430\u043d\u0438\u0435 \u043f\u043e \u0441\u0442\u043e\u0445\u0430\u0441\u0442\u0438\u0447\u0435\u0441\u043a\u043e\u043c\u0443 \u043b\u043e\u043a\u0430\u043b\u044c\u043d\u043e\u043c\u0443 \u043f\u043e\u0438\u0441\u043a\u0443 \u0438 \u0435\u0433\u043e \u043f\u0440\u0438\u043c\u0435\u043d\u0435\u043d\u0438\u044f\u043c (\u0440\u0430\u0431\u043e\u0442\u0430 \u0434\u043e\u0441\u0442\u0443\u043f\u043d\u0430 <a href=\"http:\/\/www.cs.ubc.ca\/~hoos\/ps\/phd-thesis.pdf\">\u0437\u0434\u0435\u0441\u044c<\/a>).<\/p>\n<p>  \u0412 1996\u043e\u043c \u041c\u0430\u0440\u043a\u0435\u0441-\u0421\u0438\u043b\u0432\u0430 (Marques-Silva) \u0438 \u0421\u0430\u043a\u0430\u043b\u0430\u0445 \u043f\u0440\u0435\u0434\u043b\u043e\u0436\u0438\u043b\u0438 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c Conflict-Driven-Clause-Learning (<a href=\"http:\/\/en.wikipedia.org\/wiki\/Conflict_Driven_Clause_Learning\">CDCL<\/a>), \u043f\u043e\u0434\u043e\u0431\u043d\u043e DPLL \u043e\u043d \u043f\u0440\u0438\u043d\u0438\u043c\u0430\u0435\u0442 \u0440\u0435\u0448\u0435\u043d\u0438\u044f \u043e \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0438 \u043f\u0435\u0440\u0435\u043c\u0435\u043d\u043d\u044b\u0445 \u0438 \u043f\u0440\u043e\u0432\u043e\u0434\u0438\u043b \u0434\u0435\u0442\u0435\u0440\u043c\u0438\u043d\u0438\u0440\u043e\u0432\u0430\u043d\u043d\u044b\u0435 \u0432\u044b\u0447\u0438\u0441\u043b\u0435\u043d\u0438\u044f, \u0441 \u0434\u0440\u0443\u0433\u043e\u0439 \u0441\u0442\u043e\u0440\u043e\u043d\u044b \u043e\u043d \u0445\u0440\u0430\u043d\u0438\u0442 \u0432 \u043f\u0430\u043c\u044f\u0442\u0438 \u0433\u0440\u0430\u0444 \u0438\u043c\u043b\u0438\u043a\u0430\u0446\u0438\u0439 \u0438 \u0437\u0430\u043f\u043e\u043c\u0438\u043d\u0430\u0435\u0442 \u043d\u0435\u043a\u043e\u0442\u043e\u0440\u044b\u0435 \u043a\u043e\u043c\u0431\u0438\u043d\u0430\u0446\u0438\u0438, \u043a\u043e\u0442\u043e\u0440\u044b\u0435 \u043d\u0435 \u0432\u0435\u0434\u0443\u0442 \u043a \u0440\u0435\u0448\u0435\u043d\u0438\u044e \u0438 \u043c\u043e\u0436\u0435\u0442 \u044d\u0444\u0444\u0435\u043a\u0442\u0438\u0432\u043d\u043e \u0438\u0437\u0431\u0435\u0433\u0430\u0442\u044c \u00ab\u0431\u0435\u0441\u043f\u043e\u043b\u0435\u0437\u043d\u044b\u0445\u00bb \u0440\u0435\u0448\u0435\u043d\u0438\u0439 \u0438 \u044d\u0444\u0444\u0435\u043a\u0442\u0438\u0432\u043d\u043e \u043e\u0442\u0441\u0435\u043a\u0430\u0442\u044c \u043f\u0440\u043e\u0441\u0442\u0440\u0430\u043d\u0441\u0442\u0432\u043e \u0440\u0435\u0448\u0435\u043d\u0438\u0439 \u0441\u043e\u0434\u0435\u0440\u0436\u0430\u0449\u0435\u0435 \u043a\u043e\u043d\u0444\u043b\u0438\u043a\u0442 \u0443\u0441\u0442\u0430\u043d\u043e\u0432\u043b\u0435\u043d\u043d\u044b\u0439 \u0440\u0430\u043d\u0435\u0435.<\/p>\n<p>  C 2001\u0433\u043e \u043d\u0430\u0447\u0430\u043b\u0438 \u043f\u043e\u044f\u0432\u043b\u044f\u0442\u044c\u0441\u044f Locality Based Search SAT-solver&#8217;\u044b, \u044d\u0444\u0444\u0435\u043a\u0442\u0438\u0432\u043d\u043e \u0432\u044b\u0431\u0438\u0440\u0430\u044e\u0449\u0438\u0435 \u043f\u043e\u0434\u043f\u0440\u043e\u0441\u0442\u0440\u0430\u043d\u0441\u0442\u0432\u0430 \u0434\u043b\u044f \u043f\u043e\u043b\u043d\u043e\u0433\u043e \u043f\u043e\u0438\u0441\u043a\u0430 \u043d\u0430 \u043e\u0441\u043d\u043e\u0432\u0435 \u043b\u043e\u043a\u0430\u043b\u044c\u043d\u043e\u0439 \u0438\u043d\u0444\u043e\u0440\u043c\u0430\u0446\u0438\u0438, \u0442\u0430\u043a\u0438\u0435 \u043a\u0430\u043a <a href=\"http:\/\/eigold.tripod.com\/BerkMin.html\">BerkMin<\/a> (Berkley-Minsk) \u0438 \u043c\u043d\u043e\u0433\u0438\u0435 \u0434\u0440\u0443\u0433\u0438\u0435.<\/p>\n<h4>\u00ab\u0418\u043d\u0442\u0443\u0438\u0442\u0438\u0432\u043d\u043e\u0435 \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u0435\u043d\u0438\u0435\u00bb SAT, NP \u0438 P<\/h4>\n<p>  <\/p>\n<h5> SAT <\/h5>\n<p>  \u041d\u0430\u0447\u043d\u0451\u043c \u0441 \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u0435\u043d\u0438\u044f, \u0447\u0442\u043e \u0436\u0435 \u0442\u0430\u043a\u043e\u0435 <a href=\"http:\/\/ru.wikipedia.org\/wiki\/%D0%9B%D0%BE%D0%B3%D0%B8%D0%BA%D0%B0_%D0%B2%D1%8B%D1%81%D0%BA%D0%B0%D0%B7%D1%8B%D0%B2%D0%B0%D0%BD%D0%B8%D0%B9\">\u043f\u0440\u043e\u043f\u043e\u0437\u0438\u0446\u0438\u043e\u043d\u043d\u0430\u044f \u043b\u043e\u0433\u0438\u043a\u0430<\/a>: \u044d\u0442\u043e \u043d\u0430\u0431\u043e\u0440 \u043f\u0435\u0440\u0435\u043c\u0435\u043d\u043d\u044b\u0445 { x, y, z,\u2026 } \u0438 \u043d\u0430\u0431\u043e\u0440 \u043a\u043e\u043d\u043d\u0435\u043a\u0442\u043e\u0440\u043e\u0432 { and, or, \u2014 (not), \u2192}. \u041a\u0430\u0436\u0434\u0430\u044f \u043f\u0435\u0440\u0435\u043c\u0435\u043d\u043d\u0430\u044f \u043c\u043e\u0436\u0435\u0442 \u0431\u044b\u0442\u044c \u043b\u0438\u0431\u043e \u00ab\u043b\u043e\u0436\u043d\u0430\u00bb, \u043b\u0438\u0431\u043e \u00ab\u0438\u0441\u0442\u0438\u043d\u043d\u0430\u00bb. \u041a\u043e\u043d\u043d\u0435\u043a\u0442\u043e\u0440\u044b \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u0435\u043d\u044b \u0441\u0442\u0430\u043d\u0434\u0430\u0440\u0442\u043d\u043e:  <\/p>\n<ul>\n<li>x and y \u0438\u0441\u0442\u0438\u043d\u043d\u043e \u0442\u043e\u0433\u0434\u0430 \u0438 \u0442\u043e\u043b\u044c\u043a\u043e \u0442\u043e\u0433\u0434\u0430, \u043a\u043e\u0433\u0434\u0430 (\u0434\u043b\u044f \u043a\u0440\u0430\u0442\u043a\u043e\u0441\u0442\u0438 \u0431\u0443\u0434\u0435\u043c \u043f\u0438\u0441\u0430\u0442\u044c iff \u2013 if and only if) x \u0438\u0441\u0442\u0438\u043d\u043d\u043e \u0438 y \u0438\u0441\u0442\u0438\u043d\u043d\u043e, \u043a\u043b\u0430\u0441\u0441\u0438\u0447\u0435\u0441\u043a\u0438\u0439 \u00ab\u0418\u00bb<\/li>\n<li>x or y \u0438\u0441\u0442\u0438\u043d\u043d\u043e iff \u043f\u043e \u043a\u0440\u0430\u0439\u043d\u0435\u0439 \u043c\u0435\u0440\u0435 \u043e\u0434\u043d\u0430 \u0438\u0437 \u043f\u0435\u0440\u0435\u043c\u0435\u043d\u043d\u044b\u0445 x\\y \u0438\u0441\u0442\u0438\u043d\u043d\u0430, \u043a\u043b\u0430\u0441\u0441\u0438\u0447\u0435\u0441\u043a\u0438\u0439 \u00ab\u0418\u041b\u0418\u00bb<\/li>\n<li>-x \u0438\u0441\u0442\u0438\u043d\u043d\u043e iff x \u043b\u043e\u0436\u043d\u043e, \u043a\u043b\u0430\u0441\u0441\u0438\u0447\u0435\u0441\u043a\u043e\u0435 \u043e\u0442\u0440\u0438\u0446\u0430\u043d\u0438\u0435 <\/li>\n<li>x \u2192 y \u043b\u043e\u0436\u043d\u043e iff x \u0438\u0441\u0442\u0438\u043d\u043d\u043e, \u0430 y \u043b\u043e\u0436\u043d\u043e \u2013 \u0440\u0430\u0441\u0441\u043c\u043e\u0442\u0440\u0438\u043c \u043d\u0430 \u043f\u0440\u0438\u043c\u0435\u0440\u0435:<br \/>  \u00ab\u0415\u0441\u043b\u0438 \u0431\u044b\u043b \u0434\u043e\u0436\u0434\u044c, \u0442\u043e \u0442\u0440\u0430\u0432\u0430 \u043c\u043e\u043a\u0440\u0430\u044f\u00bb<br \/>  \u0423\u0442\u0432\u0435\u0440\u0436\u0434\u0435\u043d\u0438\u0435 \u043d\u0435\u0432\u0435\u0440\u043d\u043e, \u0442\u043e\u0433\u0434\u0430 \u0438 \u0442\u043e\u043b\u044c\u043a\u043e \u0442\u043e\u0433\u0434\u0430, \u043a\u043e\u0433\u0434\u0430 \u0434\u043e\u0436\u0434\u044c \u0431\u044b\u043b (x \u0432\u0435\u0440\u043d\u043e), \u0430 \u0442\u0440\u0430\u0432\u0430 \u043f\u043e-\u043f\u0440\u0435\u0436\u043d\u0435\u043c\u0443 \u0441\u0443\u0445\u0430\u044f (y \u043b\u043e\u0436\u043d\u043e).<\/li>\n<\/ul>\n<p>  \u0424\u043e\u0440\u043c\u0443\u043b\u0430 F \u2013 \u044d\u0442\u043e \u0441\u0438\u043d\u0442\u0430\u043a\u0441\u0438\u0447\u0435\u0441\u043a\u0438 \u043f\u0440\u0430\u0432\u0438\u043b\u044c\u043d\u044b\u0439 \u043d\u0430\u0431\u043e\u0440 \u043f\u0435\u0440\u0435\u043c\u0435\u043d\u043d\u044b\u0445 \u0438 \u043a\u043e\u043d\u043d\u0435\u043a\u0442\u043e\u0440\u043e\u0432, \u0442.\u00a0\u0435. \u2192, and, or \u0441\u043e\u0435\u0434\u0438\u043d\u044f\u044e\u0442 \u043f\u0435\u0440\u0435\u043c\u0435\u043d\u043d\u044b\u0435 \u0438\u043b\u0438 \u0434\u0440\u0443\u0433\u0438\u0435 \u0444\u043e\u0440\u043c\u0443\u043b\u044b, -(not) \u0441\u0442\u043e\u0438\u0442 \u043f\u0435\u0440\u0435\u0434 \u043f\u0435\u0440\u0435\u043c\u0435\u043d\u043d\u043e\u0439 \u0438\u043b\u0438 \u0444\u043e\u0440\u043c\u0443\u043b\u043e\u0439. \u041f\u0440\u0438\u043c\u0435\u0440, F = (x \u2192 (y or z)) and (z \u2192 -x). <\/p>\n<p>  \u0413\u043e\u0432\u043e\u0440\u044f\u0442, \u0447\u0442\u043e \u0444\u043e\u0440\u043c\u0443\u043b\u0430 F \u0432\u044b\u043f\u043e\u043b\u043d\u0438\u043c\u0430 (SAT), iff \u0435\u0451 \u043f\u0435\u0440\u0435\u043c\u0435\u043d\u043d\u044b\u043c \u043c\u043e\u0436\u043d\u043e \u043f\u0440\u0438\u043f\u0438\u0441\u0430\u0442\u044c \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u044f \u00ab\u0438\u0441\u0442\u0438\u043d\u0430\u00bb\\\u00ab\u043b\u043e\u0436\u044c\u00bb (\u043c\u044b \u043d\u0430\u0437\u044b\u0432\u0430\u0435\u043c \u0442\u0430\u043a\u0443\u044e \u0444\u0443\u043d\u043a\u0446\u0438\u044e <b>I <\/b>\u043e\u0442 \u0430\u043d\u0433\u043b\u0438\u0439\u0441\u043a\u043e\u0433\u043e <b>I<\/b>nterpretation), \u0442\u0430\u043a\u0438\u043c \u043e\u0431\u0440\u0430\u0437\u043e\u043c, \u0447\u0442\u043e F \u0438\u0441\u0442\u0438\u043d\u043d\u0430. \u0414\u043b\u044f \u043a\u0440\u0430\u0442\u043a\u043e\u0441\u0442\u0438 \u043f\u0438\u0448\u0435\u043c <b>I<\/b>(F) = \u00ab\u0438\u0441\u0442\u0438\u043d\u0430\u00bb.<\/p>\n<p>  \u041b\u044e\u0431\u0430\u044f \u043f\u0440\u043e\u043f\u043e\u0437\u0438\u0446\u0438\u043e\u043d\u043d\u0430\u044f \u0444\u043e\u0440\u043c\u0443\u043b\u0430 F \u043c\u043e\u0436\u0435\u0442 \u0431\u044b\u0442\u044c \u043f\u0440\u0438\u0432\u0435\u0434\u0435\u043d\u0430 \u043a \u0432\u0438\u0434\u0443 CNF (conjunctive normal form) \u0442.\u00a0\u0435. \u0431\u044b\u0442\u044c \u043f\u0440\u0435\u0434\u0441\u0442\u0430\u0432\u043b\u0435\u043d\u0430 \u0432 \u0432\u0438\u0434\u0435 <br \/>  F&#8217; = c<sub>1<\/sub> and c<sub>2<\/sub> and \u2026 c<sub>n<\/sub><br \/>   \u0433\u0434\u0435 c<sub>i<\/sub> \u2013 \u044d\u0442\u043e (x or y or z), \u0430 x, y, z \u2013 \u044d\u0442\u043e \u043f\u0435\u0440\u0435\u043c\u0435\u043d\u043d\u044b\u0435 \u0438\u043b\u0438 \u0438\u0445 \u043e\u0442\u0440\u0438\u0446\u0430\u043d\u0438\u044f.<\/p>\n<p>  \u041f\u0440\u0438\u043c\u0435\u0440 F = (x or -y or -z) and (-x or -y or h) and (z or h).<\/p>\n<p>  \u041f\u043e\u0434\u0440\u043e\u0431\u043d\u0435\u0435 \u043e \u0434\u0430\u043d\u043d\u043e\u043c \u043f\u0440\u0435\u043e\u0431\u0440\u0430\u0437\u043e\u0432\u0430\u043d\u0438\u0438 \u043d\u0430\u043f\u0438\u0441\u0430\u043d\u043e <a href=\"http:\/\/en.wikipedia.org\/wiki\/Conjunctive_normal_form#Conversion_into_CNF\">\u0437\u0434\u0435\u0441\u044c<\/a> (\u0434\u043b\u044f \u0442\u043e\u0433\u043e, \u0447\u0442\u043e\u0431\u044b \u043a\u0430\u0436\u0434\u043e\u0435 \u043f\u0440\u0435\u0434\u043b\u043e\u0436\u0435\u043d\u0438\u0435 \u0441\u043e\u0434\u0435\u0440\u0436\u0430\u043b\u043e \u043d\u0435 \u0431\u043e\u043b\u0435\u0435 \u0442\u0440\u0435\u0445 \u043f\u0435\u0440\u0435\u043c\u0435\u043d\u043d\u044b\u0445, \u043f\u043e\u0442\u0440\u0435\u0431\u0443\u0435\u0442\u0441\u044f \u0432\u0432\u0435\u0441\u0442\u0438 \u0434\u043e\u043f\u043e\u043b\u043d\u0438\u0442\u0435\u043b\u044c\u043d\u044b\u0435 \u043f\u0435\u0440\u0435\u043c\u0435\u043d\u043d\u044b\u0435, \u043d\u043e \u044d\u0442\u043e \u0438\u0441\u043a\u043b\u044e\u0447\u0438\u0442\u0435\u043b\u044c\u043d\u043e \u0442\u0435\u0445\u043d\u0438\u0447\u0435\u0441\u043a\u0438\u0435 \u0434\u0435\u0442\u0430\u043b\u0438). <\/p>\n<p>  \u0412 \u0442\u0430\u043a\u043e\u043c \u0432\u0438\u0434\u0435, \u043a\u043e\u0433\u0434\u0430 \u0444\u043e\u0440\u043c\u0443\u043b\u0430 \u0438\u043c\u0435\u0435\u0442 \u0432\u0438\u0434 \u043e\u043f\u0438\u0441\u0430\u043d\u043d\u044b\u0439 \u0432\u044b\u0448\u0435 \u0437\u0430\u0434\u0430\u0447\u0430 \u043d\u043e\u0441\u0438\u0442 \u043d\u0430\u0437\u0432\u0430\u043d\u0438\u0435 3-SAT, \u043f\u043e\u0434\u0447\u0451\u0440\u043a\u0438\u0432\u0430\u044f \u0442\u043e\u0442 \u0444\u0430\u043a\u0442, \u043a\u0442\u043e \u043a\u0430\u0436\u0434\u043e\u0435 \u043f\u0440\u0435\u0434\u043b\u043e\u0436\u0435\u043d\u0438\u0435 c<sub>i<\/sub> \u0441\u043e\u0434\u0435\u0440\u0436\u0438\u0442 \u043d\u0435 \u0431\u043e\u043b\u0435\u0435 \u0442\u0440\u0435\u0445 \u043f\u0435\u0440\u0435\u043c\u0435\u043d\u043d\u044b\u0445 \u0438\u043b\u0438 \u0438\u0445 \u043e\u0442\u0440\u0438\u0446\u0430\u043d\u0438\u0439. <\/p>\n<p>  \u041f\u043e\u0441\u0442\u0430\u043d\u043e\u0432\u043a\u0430 \u0437\u0430\u0434\u0430\u0447\u0438 3-SAT \u0437\u0432\u0443\u0447\u0438\u0442 \u0441\u043b\u0435\u0434\u0443\u044e\u0449\u0438\u043c \u043e\u0431\u0440\u0430\u0437\u043e\u043c:<br \/>  <b>\u0414\u0430\u043d\u043e:<\/b> \u043f\u0440\u043e\u043f\u043e\u0437\u0438\u0446\u0438\u043e\u043d\u043d\u0430\u044f \u0444\u043e\u0440\u043c\u0443\u043b\u0430 F \u0432 \u0432\u0438\u0434\u0435 3-CNF<br \/>  <b>\u041d\u0430\u0439\u0442\u0438:<\/b>: \u0444\u0443\u043d\u043a\u0446\u0438\u044e <b>I<\/b>, \u043f\u0440\u0438\u043f\u0438\u0441\u044b\u0432\u0430\u044e\u0449\u0443\u044e \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0435 \u00ab\u0438\u0441\u0442\u0438\u043d\u0430\u00bb\\\u00ab\u043b\u043e\u0436\u044c\u00bb \u0432\u0441\u0435\u043c \u043f\u0435\u0440\u0435\u043c\u0435\u043d\u043d\u044b\u043c, \u0442\u0430\u043a\u0443\u044e \u0447\u0442\u043e <b>I<\/b>(F) = \u00ab\u0438\u0441\u0442\u0438\u043d\u0430\u00bb<\/p>\n<h5>\u043a\u043b\u0430\u0441\u0441 P <\/h5>\n<p>  P \u043e\u043d \u0436\u0435 PTIME \u2013 \u0437\u0430\u0434\u0430\u0447\u0438 \u0440\u0430\u0437\u0440\u0435\u0448\u0438\u043c\u044b\u0435 \u0437\u0430 \u043f\u043e\u043b\u0438\u043d\u043e\u043c\u0438\u0430\u043b\u044c\u043d\u043e\u0435 \u0432\u0440\u0435\u043c\u044f, \u044d\u0442\u043e \u0437\u043d\u0430\u0447\u0438\u0442, \u0447\u0442\u043e \u0447\u0438\u0441\u043b\u043e \u0448\u0430\u0433\u043e\u0432 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u0430 \u0432 \u0434\u0430\u043d\u043d\u043e\u043c \u043a\u043b\u0430\u0441\u0441\u0435 \u0440\u0430\u0441\u0442\u0451\u0442 \u043d\u0435 \u0431\u043e\u043b\u0435\u0435, \u0447\u0435\u043c \u043d\u0435\u043a\u043e\u0442\u043e\u0440\u044b\u0439 \u043f\u043e\u043b\u0438\u043d\u043e\u043c \u043e\u0442 \u0432\u0445\u043e\u0434\u043d\u044b\u0445 \u0434\u0430\u043d\u043d\u044b\u0445. \u041f\u043e\u0434\u0440\u043e\u0431\u043d\u0435\u0435 \u043e \u0440\u0430\u0437\u043b\u0438\u0447\u043d\u044b\u0445 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u0430\u0445 \u0438 \u0430\u043d\u0430\u043b\u0438\u0437\u0435 \u0441\u043b\u043e\u0436\u043d\u043e\u0441\u0442\u0438 \u0432 PTIME \u0443\u0436\u0435 \u0431\u044b\u043b\u043e \u043d\u0430\u043f\u0438\u0441\u0430\u043d\u043e \u043d\u0430 \u0445\u0430\u0431\u0440\u0435 [<a href=\"http:\/\/habrahabr.ru\/post\/196560\/\">9<\/a>, <a href=\"http:\/\/habrahabr.ru\/post\/195482\/\">10<\/a>, <a href=\"http:\/\/habrahabr.ru\/post\/195996\/\">11<\/a>, <a href=\"http:\/\/habrahabr.ru\/post\/196226\/\">12<\/a>, <a href=\"http:\/\/habrahabr.ru\/post\/188010\/\">13<\/a>].<\/p>\n<p>  \u0414\u043b\u044f \u0438\u043b\u043b\u044e\u0441\u0442\u0440\u0430\u0446\u0438\u0438 \u043f\u0440\u0438\u0432\u0435\u0434\u0435\u043c \u043f\u0440\u043e\u0441\u0442\u043e\u0439 \u043f\u0440\u0438\u043c\u0435\u0440: \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c \u0441\u043e\u0440\u0442\u0438\u0440\u043e\u0432\u043a\u0438 \u043f\u0443\u0437\u044b\u0440\u044c\u043a\u043e\u043c (<a href=\"http:\/\/en.wikipedia.org\/wiki\/Bubble_sort#Optimizing_bubble_sort\">\u043f\u0441\u0435\u0432\u0434\u043e\u043a\u043e\u0434<\/a> \u0438\u0437 \u0432\u0438\u043a\u0438)  <\/p>\n<pre><code class=\"matlab\">procedure bubbleSort( A : list of sortable items )     n = length(A)     repeat        swapped = false        for i = 1 to n-1 inclusive do           if A[i-1] &gt; A[i] then              swap(A[i-1], A[i])              swapped = true           end if        end for        n = n - 1     until not swapped end procedure <\/code><\/pre>\n<p>  \u0412\u0445\u043e\u0434\u043d\u044b\u043c \u043f\u0430\u0440\u0430\u043c\u0435\u0442\u0440\u043e\u043c \u044f\u0432\u043b\u044f\u0435\u0442\u0441\u044f \u043c\u0430\u0441\u0441\u0438\u0432 \u0447\u0438\u0441\u0435\u043b \u0434\u043b\u044f \u0441\u043e\u0440\u0442\u0438\u0440\u043e\u0432\u043a\u0438. \u041d\u0430\u0441 \u0438\u043d\u0442\u0435\u0440\u0435\u0441\u0443\u0435\u0442 \u0440\u043e\u0441\u0442 \u0432\u0440\u0435\u043c\u0435\u043d\u0438 \u0432 \u0437\u0430\u0432\u0438\u0441\u0438\u043c\u043e\u0441\u0442\u0438 \u043e\u0442 \u0440\u043e\u0441\u0442\u0430 \u0434\u043b\u0438\u043d\u044b \u043c\u0430\u0441\u0441\u0438\u0432\u0430 \u0442.\u0435. \u0437\u0430\u0432\u0438\u0441\u0438\u043c\u043e\u0441\u0442\u044c \u0432\u0440\u0435\u043c\u0435\u043d\u0438 TIME \u043e\u0442 n. \u0417\u0430\u043c\u0435\u0442\u0438\u043c, \u0447\u0442\u043e \u043a\u0430\u0436\u0434\u0430\u044f \u0438\u0442\u0435\u0440\u0430\u0446\u0438\u044f \u0446\u0438\u043a\u043b\u0430 repeat \u0432\u044b\u043f\u043e\u043b\u043d\u044f\u0435\u0442 \u043d\u0435 \u0431\u043e\u043b\u0435\u0435 3*n \u0448\u0430\u0433\u043e\u0432 \u0438 \u0443\u0441\u0442\u0430\u043d\u0430\u0432\u043b\u0438\u0432\u0430\u0435\u0442 \u043f\u043e \u043a\u0440\u0430\u0439\u043d\u0435\u0439 \u043c\u0435\u0440\u0435 \u043e\u0434\u0438\u043d \u044d\u043b\u0435\u043c\u0435\u043d\u0442 \u043c\u0430\u0441\u0441\u0438\u0432\u0430 \u043d\u0430 \u043d\u0443\u0436\u043d\u043e\u0435 \u043c\u0435\u0441\u0442\u043e. \u0417\u043d\u0430\u0447\u0438\u0442, \u0447\u0442\u043e \u0446\u0438\u043a\u043b repeat \u0432\u044b\u043f\u043e\u043b\u043d\u044f\u0435\u0442\u0441\u044f \u043d\u0435 \u0431\u043e\u043b\u0435\u0435, \u0447\u0435\u043c n \u0440\u0430\u0437. \u042d\u0442\u043e \u0437\u043d\u0430\u0447\u0438\u0442, \u0447\u0442\u043e \u043a\u043e\u043b\u0438\u0447\u0435\u0441\u0442\u0432\u043e \u043e\u043f\u0435\u0440\u0430\u0446\u0438\u0439 (\u043e\u043d\u043e \u0436\u0435 TIME) \u0440\u0430\u0441\u0442\u0435\u0442 \u043a\u0430\u043a \u043d\u0435\u043a\u043e\u0442\u043e\u0440\u044b\u0439 \u043a\u0432\u0430\u0434\u0440\u0430\u0442 \u043e\u0442 \u0434\u043b\u0438\u043d\u044b \u043c\u0430\u0441\u0441\u0438\u0432\u0430 (\u0438 \u043b\u0438\u043d\u0435\u0439\u043d\u044b\u0439 \u0447\u043b\u0435\u043d \u0438\u0437 \u00abn = length(A)\u00bb ) \u0442.\u0435.<\/p>\n<p>  TIME(n) = a * n<sup>2<\/sup> + b * n + C<\/p>\n<p>  \u0418\u043d\u0430\u0447\u0435 \u0433\u043e\u0432\u043e\u0440\u044f, \u0432\u0440\u0435\u043c\u044f \u0440\u0430\u0431\u043e\u0442\u044b \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u0430 \u043e\u0433\u0440\u0430\u043d\u0438\u0447\u0435\u043d\u043e \u043d\u0435\u043a\u043e\u0442\u043e\u0440\u044b\u043c \u043f\u043e\u043b\u0438\u043d\u043e\u043c\u043e\u043c \u043e\u0442 n, \u0432 \u0434\u0430\u043d\u043d\u043e\u043c \u0441\u043b\u0443\u0447\u0430\u0435 \u043c\u044b \u0433\u043e\u0432\u043e\u0440\u0438\u043c, \u0447\u0442\u043e \u0432\u0440\u0435\u043c\u044f \u0440\u0430\u0431\u043e\u0442\u044b \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u0430 \u0440\u0430\u0441\u0442\u0435\u0442 \u043d\u0435 \u0431\u044b\u0441\u0442\u0440\u0435\u0435 \u043a\u0432\u0430\u0434\u0440\u0430\u0442\u0430 \u0447\u0438\u0441\u043b\u0430 \u044d\u043b\u0435\u043c\u0435\u043d\u0442\u043e\u0432 \u0438 \u0437\u0430\u043f\u0438\u0441\u044b\u0432\u0430\u0435\u043c \u044d\u0442\u043e \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u044f <a href=\"http:\/\/en.wikipedia.org\/wiki\/Big_O_notation\">Big-O<\/a> \u0437\u0430\u043f\u0438\u0441\u044c<\/p>\n<p>  <img decoding=\"async\" src=\"http:\/\/habr.habrastorage.org\/post_images\/416\/666\/c7a\/416666c7aa781615ea954d1d123d692b.png\"\/><\/p>\n<h5>\u043a\u043b\u0430\u0441\u0441 NP <\/h5>\n<p>  NP \u043e\u0431\u043e\u0437\u043d\u0430\u0447\u0430\u0435\u0442 nondeterministic polynomial time. \u041e\u0447\u0435\u043d\u044c \u0447\u0430\u0441\u0442\u043e \u0435\u0433\u043e \u043e\u0448\u0438\u0431\u043e\u0447\u043d\u043e \u043d\u0430\u0437\u044b\u0432\u0430\u044e\u0442\u0441\u044f non-polynomial time, \u043f\u043e \u044d\u0442\u043e\u043c\u0443 \u043f\u043e\u0432\u043e\u0434\u0443 \u0440\u043e\u0434\u0438\u043b\u0430\u0441\u044c \u0448\u0443\u0442\u043a\u0430: <\/p>\n<blockquote><p>\u0414\u0435\u043b\u0438\u0442\u044c \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u044b \u043d\u0430 \u043f\u043e\u043b\u0438\u043d\u043e\u043c\u0438\u0430\u043b\u044c\u043d\u044b\u0435 \u0438 \u043d\u0435-\u043f\u043e\u043b\u0438\u043d\u043e\u043c\u0438\u0430\u043b\u044c\u043d\u044b\u0435, \u044d\u0442\u043e \u043f\u0440\u0438\u043c\u0435\u0440\u043d\u043e \u043a\u0430\u043a \u0434\u0435\u043b\u0438\u0442\u044c \u0432\u0441\u0435\u043b\u0435\u043d\u043d\u0443\u044e \u043d\u0430 \u0431\u0430\u043d\u0430\u043d\u044b \u0438 \u043d\u0435-\u0431\u0430\u043d\u0430\u043d\u044b.<\/p><\/blockquote>\n<p>  \u0412 \u0434\u0430\u043d\u043d\u043e\u0439 \u0441\u0442\u0430\u0442\u044c\u0435 \u043d\u0430\u0441 \u043d\u0435 \u0438\u043d\u0442\u0435\u0440\u0435\u0441\u0443\u0435\u0442 \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u043e\u0435 \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u0435\u043d\u0438\u0435 NP (\u044d\u0442\u043e \u0431\u0443\u0434\u0435\u0442 \u0432 \u0441\u043f\u0435\u0446\u0438\u0430\u043b\u0438\u0437\u0438\u0440\u043e\u0432\u0430\u043d\u043d\u043e\u043c \u043c\u0430\u0442\u0435\u0440\u0438\u0430\u043b\u0435), \u043d\u043e \u0440\u0430\u0441\u0441\u043c\u043e\u0442\u0440\u0438\u043c \u0438\u043d\u0442\u0443\u0438\u0442\u0438\u0432\u043d\u043e\u0435 \u043f\u0440\u0435\u0434\u0441\u0442\u0430\u0432\u043b\u0435\u043d\u0438\u0435 \u043a\u043b\u0430\u0441\u0441\u0430 NP. \u0421\u0430\u043c\u0430 \u043f\u0440\u0438\u0440\u043e\u0434\u0430 \u0438 \u0432\u043d\u0443\u0442\u0440\u0435\u043d\u043d\u0438\u0435 \u043c\u0435\u0445\u0430\u043d\u0438\u0437\u043c\u044b NP \u0441\u043b\u0435\u0434\u0443\u044e\u0442 \u0442\u0430\u043a \u043d\u0430\u0437\u044b\u0432\u0430\u0435\u043c\u043e\u043c\u0443 guess-and-check \u043c\u0435\u0442\u043e\u0434\u0443. \u0422.\u0435. \u043f\u0440\u043e\u0441\u0442\u0440\u0430\u043d\u0441\u0442\u0432\u043e \u043f\u043e\u0438\u0441\u043a\u0430 \u0440\u0435\u0448\u0435\u043d\u0438\u0439 \u044d\u043a\u0441\u043f\u043e\u043d\u0435\u043d\u0446\u0438\u0430\u043b\u044c\u043d\u043e (\u0434\u043e\u0441\u0442\u0430\u0442\u043e\u0447\u043d\u043e \u0431\u043e\u043b\u044c\u0448\u043e\u0435, \u0447\u0442\u043e\u0431\u044b \u0438\u0441\u043a\u043b\u044e\u0447\u0438\u0442\u044c \u0432\u043e\u0437\u043c\u043e\u0436\u043d\u043e\u0441\u0442\u044c \u043f\u0435\u0440\u0435\u0431\u043e\u0440\u0430), \u0430 \u043f\u0440\u043e\u0432\u0435\u0440\u043a\u0430 \u0440\u0435\u0448\u0435\u043d\u0438\u044f \u044f\u0432\u043b\u044f\u0435\u0442\u0441\u044f \u043f\u0440\u043e\u0441\u0442\u043e\u0439 \u0437\u0430\u0434\u0430\u0447\u0435\u0439. \u041c\u043e\u0436\u043d\u043e \u0440\u0430\u0441\u0441\u043c\u0430\u0442\u0440\u0438\u0432\u0430\u0442\u044c NP, \u043a\u0430\u043a \u043a\u043b\u0430\u0441\u0441 \u0437\u0430\u0434\u0430\u0447, \u0432 \u043a\u043e\u0442\u043e\u0440\u043e\u043c \u043d\u0443\u0436\u043d\u043e \u043d\u0430\u0439\u0442\u0438 \u0440\u0435\u0448\u0435\u043d\u0438\u0435 (\u00ab\u0443\u0433\u0430\u0434\u0430\u0442\u044c\u00bb \u2014 guess \u0447\u0430\u0441\u0442\u044c) \u0441\u0440\u0435\u0434\u0438 \u0431\u043e\u043b\u044c\u0448\u043e\u0433\u043e \u043a\u043e\u043b\u0438\u0447\u0435\u0441\u0442\u0432\u0430 \u0432\u0430\u0440\u0438\u0430\u043d\u0442\u043e\u0432, \u0430 \u043f\u043e\u0442\u043e\u043c \u043f\u0440\u043e\u0432\u0435\u0440\u0438\u0442\u044c \u0435\u0433\u043e \u043a\u043e\u0440\u0440\u0435\u043a\u0442\u043d\u043e\u0441\u0442\u044c (check \u0447\u0430\u0441\u0442\u044c).<\/p>\n<p>  \u0421 \u0442\u043e\u0447\u043a\u0438 \u0437\u0440\u0435\u043d\u0438\u044f SAT, \u043f\u0440\u043e\u0441\u0442\u0440\u0430\u043d\u0441\u0442\u0432\u043e \u0440\u0435\u0448\u0435\u043d\u0438\u0439 \u044d\u0442\u043e \u0432\u0441\u0435\u0432\u043e\u0437\u043c\u043e\u0436\u043d\u044b\u0435 \u043d\u0430\u0431\u043e\u0440\u044b \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0439 \u043f\u0435\u0440\u0435\u043c\u0435\u043d\u043d\u044b\u0445, \u0435\u0441\u043b\u0438 \u0443 \u043d\u0430\u0441 k \u0440\u0430\u0437\u043b\u0438\u0447\u043d\u044b\u0445 \u043f\u0435\u0440\u0435\u043c\u0435\u043d\u043d\u044b\u0445 \u0432 \u0444\u043e\u0440\u043c\u0443\u043b\u0435, \u0442\u043e \u0443 \u043d\u0430\u0441 2<sup>k<\/sup> \u0432\u043e\u0437\u043c\u043e\u0436\u043d\u044b\u0445 \u00ab\u0438\u043d\u0442\u0435\u0440\u043f\u0440\u0435\u0442\u0430\u0446\u0438\u0439\u00bb \u0444\u043e\u0440\u043c\u0443\u043b\u044b, \u0442.\u0435. \u043f\u0440\u043e\u0441\u0442\u0440\u0430\u043d\u0441\u0442\u0432\u043e \u043f\u043e\u0438\u0441\u043a\u0430 <b>I<\/b> \u044d\u043a\u0441\u043f\u043e\u043d\u0435\u043d\u0446\u0438\u0430\u043b\u044c\u043d\u043e. \u041e\u0434\u043d\u0430\u043a\u043e, \u0435\u0441\u043b\u0438 \u043c\u044b \u00ab\u0443\u0433\u0430\u0434\u0430\u043b\u0438\u00bb <b>I<\/b>, \u0442\u043e \u043c\u044b \u043c\u043e\u0436\u0435\u043c \u0437\u0430 \u043f\u043e\u043b\u0438\u043d\u043e\u043c\u0438\u0430\u043b\u044c\u043d\u043e\u0435 \u0432\u0440\u0435\u043c\u044f \u043f\u0440\u043e\u0432\u0435\u0440\u0438\u0442\u044c \u0438\u0441\u0442\u0438\u043d\u043d\u043e\u0441\u0442\u044c \u0444\u043e\u0440\u043c\u0443\u043b\u044b.<\/p>\n<h5>\u0427\u0442\u043e \u0431\u0443\u0434\u0435\u0442 \u0435\u0441\u043b\u0438 P != NP<\/h5>\n<p>  \u041d\u0438\u0447\u0435\u0433\u043e \u043d\u0435 \u0431\u0443\u0434\u0435\u0442, \u0442\u043e\u043b\u044c\u043a\u043e \u043a\u0442\u043e-\u0442\u043e <a href=\"http:\/\/en.wikipedia.org\/wiki\/Millennium_Prize_Problems\">\u043f\u043e\u043b\u0443\u0447\u0438\u0442 \u043c\u0438\u043b\u043b\u0438\u043e\u043d \u0434\u043e\u043b\u043b\u0430\u0440\u043e\u0432<\/a>.<\/p>\n<h5>\u0427\u0442\u043e \u0431\u0443\u0434\u0435\u0442 \u0435\u0441\u043b\u0438 P = NP <\/h5>\n<p>  \u0422\u0443\u0442 \u0434\u0432\u0435 \u043d\u043e\u0432\u043e\u0441\u0442\u0438: \u0445\u043e\u0440\u043e\u0448\u0430\u044f \u0438 \u043f\u043b\u043e\u0445\u0430\u044f.<\/p>\n<p>  <i>\u0425\u043e\u0440\u043e\u0448\u0438\u0435.<\/i> \u041c\u044b \u0431\u0443\u0434\u0435\u043c \u043e\u0447\u0435\u043d\u044c \u0431\u044b\u0441\u0442\u0440\u043e \u0440\u0435\u0448\u0430\u0442\u044c \u043a\u0443\u0447\u0443 \u0437\u0430\u0434\u0430\u0447 \u043e\u043f\u0442\u0438\u043c\u0438\u0437\u0430\u0446\u0438\u0438, \u0437\u0430\u0434\u0430\u0447\u0438 \u043d\u0430 \u0433\u0440\u0430\u0444\u044b, \u0441\u043e\u0441\u0442\u0430\u0432\u043b\u044f\u0442\u044c \u0440\u0430\u0441\u043f\u0438\u0441\u0430\u043d\u0438\u044f, \u0441\u043e\u0431\u0438\u0440\u0430\u0442\u044c \u043f\u0430\u0437\u043b\u044b, \u043f\u0440\u043e\u0432\u0435\u0440\u044f\u0442\u044c \u0440\u0430\u0437\u043b\u0438\u0447\u043d\u044b\u0435 \u0441\u0432\u043e\u0439\u0441\u0442\u0432\u0430 \u0431\u0430\u0437 \u0434\u0430\u043d\u043d\u044b\u0445, \u0430 \u0442\u0430\u043a \u0436\u0435 \u044d\u0444\u0444\u0435\u043a\u0442\u043d\u043e \u043f\u0440\u043e\u0432\u0435\u0440\u044f\u0442\u044c \u0440\u0430\u0431\u043e\u0442\u043e\u0441\u043f\u043e\u0441\u043e\u0431\u043d\u043e\u0441\u0442\u044c \u0441\u043f\u0435\u0446\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0439 NASA.<\/p>\n<p>  <i>\u041f\u043b\u043e\u0445\u0438\u0435.<\/i> \u0420\u0443\u0448\u0438\u0442\u0441\u044f \u0432\u0441\u044f \u0441\u043e\u0432\u0440\u0435\u043c\u0435\u043d\u043d\u0430\u044f \u043a\u0440\u0438\u043f\u0442\u043e\u0433\u0440\u0430\u0444\u0438\u044f, \u0430 \u0432\u043c\u0435\u0441\u0442\u0435 \u0441 \u043d\u0435\u0439 \u043f\u043e \u0443\u0434\u0430\u0440 \u043f\u043e\u043f\u0430\u0434\u0430\u0435\u0442 \u0431\u0430\u043d\u043a\u043e\u0432\u0441\u043a\u0430\u044f \u0441\u0438\u0441\u0442\u0435\u043c\u0430. \u041b\u044e\u0434\u0438 \u043d\u0430\u0447\u043d\u0443\u0442 \u043f\u0438\u0441\u0430\u0442\u044c \u0431\u043e\u0442\u043e\u0432 \u0434\u043b\u044f \u041c\u0430\u0440\u0438\u043e.<\/p>\n<h4>2-SAT in P.<\/h4>\n<p>  \u0420\u0430\u0441\u0441\u043c\u043e\u0442\u0440\u0438\u043c \u0438\u043d\u0442\u0435\u0440\u0435\u0441\u043d\u0443\u044e \u0432\u0430\u0440\u0438\u0430\u0446\u0438\u044e SAT, \u0432 \u043a\u043e\u0442\u043e\u0440\u043e\u0439 \u043a\u0430\u0436\u0434\u043e\u0435 \u043f\u0440\u0435\u0434\u043b\u043e\u0436\u0435\u043d\u0438\u0435 (clause) \u043e\u0433\u0440\u0430\u043d\u0438\u0447\u0435\u043d \u0434\u0432\u0443\u043c\u044f \u043f\u0435\u0440\u0435\u043c\u0435\u043d\u043d\u044b\u043c\u0438. \u0417\u0434\u0435\u0441\u044c \u0438 \u0434\u0430\u043b\u0435\u0435, \u0430\u0432\u0442\u043e\u0440 \u0432\u0441\u0451 \u0441\u0443\u0449\u0435\u0441\u0442\u0432\u0435\u043d\u043d\u043e \u0443\u043f\u0440\u043e\u0449\u0430\u0435\u0442 \u0434\u043b\u044f \u043e\u0431\u043b\u0435\u0433\u0447\u0435\u043d\u0438\u044f \u0432\u043e\u0441\u043f\u0440\u0438\u044f\u0442\u0438\u044f \u043c\u0430\u0442\u0435\u0440\u0438\u0430\u043b\u0430. <\/p>\n<p>  <b>\u0414\u0430\u043d\u043e<\/b>: F \u2013 \u0444\u043e\u0440\u043c\u0443\u043b\u0430 \u0432\u0438\u0434\u0430 c<sub>1<\/sub> and c<sub>2<\/sub> and c<sub>3<\/sub> \u2026 and c<sub>n<\/sub>, <br \/>  \u0433\u0434\u0435 \u0441<sub>i<\/sub> \u0438\u043c\u0435\u0435\u0442 \u0432\u0438\u0434 (x or y) \u0438 x, y \u2013 \u044d\u0442\u043e \u043f\u0435\u0440\u0435\u043c\u0435\u043d\u043d\u044b\u0435 \u0438\u043b\u0438 \u0438\u0445 \u043e\u0442\u0440\u0438\u0446\u0430\u043d\u0438\u044f, \u0442.\u00a0\u0435. x \u044d\u0442\u043e \u043d\u0435\u043a\u043e\u0442\u043e\u0440\u0430\u044f \u043f\u0435\u0440\u0435\u043c\u0435\u043d\u043d\u0430\u044f v \u0438\u043b\u0438 -v.<br \/>  <b>\u041d\u0430\u0439\u0442\u0438<\/b>: \u0444\u0443\u043d\u043a\u0446\u0438\u044e <b>I<\/b>, \u043f\u0440\u0438\u043f\u0438\u0441\u044b\u0432\u0430\u044e\u0449\u0443\u044e \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0435 \u00ab\u0438\u0441\u0442\u0438\u043d\u0430\u00bb\\\u00ab\u043b\u043e\u0436\u044c\u00bb \u0432\u0441\u0435\u043c \u043f\u0435\u0440\u0435\u043c\u0435\u043d\u043d\u044b\u043c, \u0442\u0430\u043a\u0443\u044e \u0447\u0442\u043e <b>I<\/b>(F) = \u00ab\u0438\u0441\u0442\u0438\u043d\u0430\u00bb<br \/>  <b>\u0423\u0442\u0432\u0435\u0440\u0436\u0434\u0435\u043d\u0438\u0435<\/b>: \u0421\u0443\u0449\u0435\u0441\u0442\u0432\u0443\u044e \u043f\u043e\u043b\u0438\u043d\u043e\u043c\u0438\u0430\u043b\u044c\u043d\u044b\u0439 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c P, \u0442\u0430\u043a\u043e\u0439 \u0447\u0442\u043e, \u0435\u0441\u043b\u0438 \u0444\u0443\u043d\u043a\u0446\u0438\u044f <b>I<\/b> \u0441\u0443\u0449\u0435\u0441\u0442\u0432\u0443\u0435\u0442, \u0442\u043e P(F) = <b>I<\/b>, \u0430 \u0438\u043d\u0430\u0447\u0435, P(F) = {}.<\/p>\n<p>  (*) \u0444\u0443\u043d\u043a\u0446\u0438\u044f <b>I<\/b> \u043d\u0435 \u0435\u0434\u0438\u043d\u0441\u0442\u0432\u0435\u043d\u043d\u0430, \u0435\u0441\u043b\u0438 \u043e\u043d\u0430 \u0441\u0443\u0449\u0435\u0441\u0442\u0432\u0443\u0435\u0442 \u0438 P \u0432\u043e\u0437\u0432\u0440\u0430\u0449\u0430\u0435\u0442 \u043d\u0435\u043a\u043e\u0442\u043e\u0440\u0443\u044e \u0444\u0443\u043d\u043a\u0446\u0438\u044e <b>I<\/b> (\u0432 \u043a\u043d\u0438\u0433\u0430\u0445 \u043f\u043e \u0442\u0435\u043e\u0440\u0438\u0438 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u043e\u0432 \u0438 \u0441\u043b\u043e\u0436\u043d\u043e\u0441\u0442\u0438, \u0432\u0441\u0435 \u0442\u043e\u0436\u0435 \u0441\u0430\u043c\u043e\u0435 \u0431\u0443\u0434\u0435\u0442 \u043d\u0430\u043f\u0438\u0441\u0430\u043d\u043e \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u044b\u043c \u044f\u0437\u044b\u043a\u043e\u043c, \u043d\u043e \u044d\u0442\u0438 \u0434\u0435\u0442\u0430\u043b\u0438 \u043d\u0435\u0441\u0443\u0449\u0435\u0441\u0442\u0432\u0435\u043d\u043d\u044b \u0434\u043b\u044f \u0432\u043e\u0441\u043f\u0440\u0438\u044f\u0442\u0438\u044f \u043e\u0431\u0449\u0435\u0439 \u0438\u0434\u0435\u0438 \u043e \u0442\u043e\u043c, \u043f\u043e\u0447\u0435\u043c\u0443 2-SAT \u043f\u043e\u043b\u0438\u043d\u043e\u043c\u0438\u0430\u043b\u0435\u043d)<\/p>\n<h5>\u041d\u0430\u0431\u0440\u043e\u0441\u043e\u043a \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u0430:<br \/>  <\/h5>\n<p>  \u0414\u043b\u044f \u043d\u0430\u0447\u0430\u043b\u0430 \u043f\u0440\u0435\u043e\u0431\u0440\u0430\u0437\u0443\u0435\u043c \u0438\u0441\u0445\u043e\u0434\u043d\u0443\u044e \u0444\u043e\u0440\u043c\u0443\u043b\u0443, \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u044f \u0441\u043b\u0435\u0434\u0443\u044e\u0449\u0438\u0435 \u0440\u0430\u0432\u0435\u043d\u0441\u0442\u0432\u043e:<br \/>  <img decoding=\"async\" src=\"http:\/\/habr.habrastorage.org\/post_images\/cfa\/e60\/418\/cfae60418e09a7896e3ac33ade0b5bd5.png\"\/><br \/>  \u041c\u043e\u0436\u0435\u0442\u0435 \u043f\u0440\u043e\u0432\u0435\u0440\u0438\u0442\u044c \u0435\u0433\u043e \u0441 \u043f\u043e\u043c\u043e\u0449\u044c\u044e \u0442\u0430\u0431\u043b\u0438\u0446\u044b \u0438\u0441\u0442\u0438\u043d\u043d\u043e\u0441\u0442\u0438. \u0418\u043d\u0442\u0443\u0438\u0446\u0438\u044f \u0437\u0430 \u044d\u0442\u0438\u043c \u043f\u0440\u0430\u0432\u0438\u043b\u043e\u043c \u0441\u043b\u0435\u0434\u0443\u044e\u0449\u0430\u044f:<br \/>  \u00ab\u0415\u0441\u043b\u0438 \u0431\u044b\u043b \u0434\u043e\u0436\u0434\u044c, \u0442\u043e \u0442\u0440\u0430\u0432\u0430 \u043c\u043e\u043a\u0440\u0430\u044f\u00bb (x \u2192 y, x \u2014 \u0431\u044b\u043b \u0434\u043e\u0436\u0434\u044c, y \u2013 \u0442\u0440\u0430\u0432\u0430 \u043c\u043e\u043a\u0440\u0430\u044f)<br \/>  \u042d\u0442\u043e \u0437\u043d\u0430\u0447\u0438\u0442, \u0447\u0442\u043e \u0435\u0441\u043b\u0438 \u0442\u0440\u0430\u0432\u0430 \u0441\u0443\u0445\u0430\u044f (\u043d\u0435 \u043c\u043e\u043a\u0440\u0430\u044f: y \u043b\u043e\u0436\u043d\u043e), \u0442\u043e \u0434\u043e\u0436\u0434\u044f \u0442\u043e\u0447\u043d\u043e \u043d\u0435 \u0431\u044b\u043b\u043e (x \u043b\u043e\u0436\u043d\u043e).<br \/>  \u0415\u0441\u043b\u0438 \u0442\u0440\u0430\u0432\u0430 \u043c\u043e\u043a\u0440\u0430\u044f, \u0442\u043e \u043b\u0438\u0431\u043e \u0434\u043e\u0436\u0434\u044c \u0431\u044b\u043b (x \u0438\u0441\u0442\u0438\u043d\u043d\u043e, \u0432 \u043d\u0435\u043a\u043e\u0442\u043e\u0440\u043e\u043c \u0441\u043c\u044b\u0441\u043b\u0435, x \u00ab\u043e\u0431\u044a\u044f\u0441\u043d\u044f\u0435\u0442\u00bb \u043f\u043e\u0447\u0435\u043c\u0443 y \u0438\u0441\u0442\u0438\u043d\u043d\u043e), \u043b\u0438\u0431\u043e \u0434\u043e\u0436\u0434\u044f \u043d\u0435 \u0431\u044b\u043b\u043e (\u0445 \u043b\u043e\u0436\u043d\u043e), \u043d\u0430 \u0438\u043d\u0442\u0443\u0438\u0442\u0438\u0432\u043d\u043e\u043c \u0443\u0440\u043e\u0432\u043d\u0435 \u043c\u044b \u043f\u043e\u0434\u0440\u0430\u0437\u0443\u043c\u0435\u0432\u0430\u0435\u043c, \u0447\u0442\u043e \u0441\u0443\u0449\u0435\u0441\u0442\u0432\u0443\u0435\u0442 \u0434\u0440\u0443\u0433\u0430\u044f \u043f\u0440\u0438\u0447\u0438\u043d\u0430, \u0438\u0437-\u0437\u0430 \u043a\u043e\u0442\u043e\u0440\u043e\u0439 y \u0438\u0441\u0442\u0438\u043d\u043d\u043e (z \u2013 \u0441\u043e\u0441\u0435\u0434 \u043f\u043e\u043b\u0438\u043b \u0433\u0430\u0437\u043e\u043d \u0438 \u043f\u043e\u044d\u0442\u043e\u043c\u0443 \u0442\u0440\u0430\u0432\u0430 \u043c\u043e\u043a\u0440\u0430\u044f).<\/p>\n<p>  \u041f\u0440\u0435\u043e\u0431\u0440\u0430\u0437\u0443\u0435\u043c F \u0441 \u043f\u043e\u043c\u043e\u0449\u044c\u044e (*) \u043a \u0432\u0438\u0434\u0443 c&#8217;<sub>1<\/sub> and c&#8217;<sub>2<\/sub> \u2026 and c&#8217;<sub>n<\/sub> \u0433\u0434\u0435 \u0441&#8217;<sub>i<\/sub> \u0438\u043c\u0435\u0435\u0442 \u0432\u0438\u0434 (x \u2192 y), x,y \u2013 \u043f\u0435\u0440\u0435\u043c\u0435\u043d\u043d\u044b\u0435 \u0438\u043b\u0438 \u0438\u0445 \u043e\u0442\u0440\u0438\u0446\u0430\u043d\u0438\u044f. \u0412 \u0440\u0435\u0437\u0443\u043b\u044c\u0442\u0430\u0442\u0435 F \u2013 \u044d\u0442\u043e \u0433\u0440\u0430\u0444 \u0438\u043c\u043f\u043b\u0438\u043a\u0430\u0446\u0438\u0439. \u041f\u0440\u0438\u043c\u0435\u0440, \u043f\u043e\u0434\u043e\u0431\u043d\u043e\u0433\u043e \u0433\u0440\u0430\u0444\u0430 \u043d\u0438\u0436\u0435:<br \/>  \u0441<sub>1<\/sub> = \u0415\u0441\u043b\u0438 \u0431\u044b\u043b \u0434\u043e\u0436\u0434\u044c, \u0442\u043e \u0442\u0440\u0430\u0432\u0430 \u043c\u043e\u043a\u0440\u0430\u044f.<br \/>  \u0441<sub>2<\/sub> = \u0415\u0441\u043b\u0438 \u0441\u043e\u0441\u0435\u0434 \u043f\u043e\u043b\u0438\u043b \u0433\u0430\u0437\u043e\u043d, \u0442\u043e \u0442\u0440\u0430\u0432\u0430 \u043c\u043e\u043a\u0440\u0430\u044f.<br \/>  \u0441<sub>3<\/sub> = \u0415\u0441\u043b\u0438 \u0442\u0440\u0430\u0432\u0430 \u043c\u043e\u043a\u0440\u0430\u044f, \u0442\u043e \u0445\u043e\u0440\u043e\u0448\u043e \u0440\u0430\u0441\u0442\u0443\u0442 \u0441\u043e\u0440\u043d\u044f\u043a\u0438.<br \/>  <img decoding=\"async\" src=\"http:\/\/habr.habrastorage.org\/post_images\/6a8\/d9e\/1bf\/6a8d9e1bfdaf88360658eb5096f0e9e2.png\"\/><\/p>\n<p>  \u041c\u044b \u0432\u0438\u0434\u0438\u043c, \u0447\u0442\u043e \u0435\u0441\u043b\u0438 \u0432 \u0433\u0440\u0430\u0444\u0435 \u0438\u043c\u043f\u043b\u0438\u043a\u0430\u0446\u0438\u0439 \u0432\u044b\u0439\u0434\u044f \u0438\u0437 \u043d\u0435\u043a\u043e\u0442\u043e\u0440\u043e\u0439 \u0432\u0435\u0440\u0448\u0438\u043d\u044b v (\u043d\u0430\u043f\u0440\u0438\u043c\u0435\u0440, \u0431\u044b\u043b \u0434\u043e\u0436\u0434\u044c), \u043d\u0435\u043b\u044c\u0437\u044f \u0434\u043e\u0441\u0442\u0438\u0447\u044c \u0432\u0435\u0440\u0448\u0438\u043d\u044b -v (\u0434\u043e\u0436\u0434\u044f \u043d\u0435 \u0431\u044b\u043b\u043e), \u0442\u043e \u0441\u0438\u0441\u0442\u0435\u043c\u0430 \u0438\u043c\u043f\u043b\u0438\u043a\u0430\u0446\u0438\u0439 \u043d\u0435\u043f\u0440\u043e\u0442\u0438\u0432\u043e\u0440\u0435\u0447\u0438\u0432\u0430. \u0418\u043d\u0442\u0443\u0438\u0446\u0438\u044f \u0441\u043b\u0435\u0434\u0443\u044e\u0449\u0430\u044f: \u0435\u0441\u043b\u0438 \u043c\u044b \u0441\u0434\u0435\u043b\u0430\u0435\u043c \u043d\u0435\u043a\u043e\u0442\u043e\u0440\u043e\u0435 \u043f\u0440\u0435\u0434\u043f\u043e\u043b\u043e\u0436\u0435\u043d\u0438\u0435, \u043d\u0430\u043f\u0440\u0438\u043c\u0435\u0440, \u0447\u0442\u043e \u0434\u043e\u0436\u0434\u044c \u0431\u044b\u043b, \u0442\u043e \u043c\u044b \u0441\u0440\u0430\u0437\u0443 \u0437\u0430\u043a\u043b\u044e\u0447\u0430\u0435\u043c, \u0447\u0442\u043e \u0442\u0440\u0430\u0432\u0430 \u043c\u043e\u043a\u0440\u0430\u044f \u0438 \u0440\u0430\u0441\u0442\u0443\u0442 \u0441\u043e\u0440\u043d\u044f\u043a\u0438 (\u043e\u0441\u0442\u0430\u043b\u043e\u0441\u044c \u0442\u043e\u043b\u044c\u043a\u043e \u0432\u044b\u0431\u0440\u0430\u0442\u044c \u043f\u043e\u043b\u0438\u0432\u0430\u043b \u043b\u0438 \u0433\u0430\u0437\u043e\u043d \u0441\u043e\u0441\u0435\u0434) \u0438 \u043d\u0435 \u043f\u043e\u043b\u0443\u0447\u0430\u0435\u043c \u043f\u0440\u043e\u0442\u0438\u0432\u043e\u0440\u0435\u0447\u0438\u044f, \u0442\u043e \u0443 \u043d\u0430\u0441 \u0435\u0441\u0442\u044c \u0447\u0430\u0441\u0442\u044c \u0444\u0443\u043d\u043a\u0446\u0438\u0438 <b>I<\/b>, \u0432 \u0447\u0430\u0441\u0442\u043d\u043e\u0441\u0442\u0438 \u043f\u0440\u0438\u043d\u044f\u0432 \u0440\u0435\u0448\u0435\u043d\u0438\u0435, \u0447\u0442\u043e \u0434\u043e\u0436\u0434\u044c \u0431\u044b\u043b, \u043c\u044b \u043f\u043e\u043b\u0443\u0447\u0438\u043b\u0438 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u044f \u0434\u043b\u044f \u00ab\u0442\u0440\u0430\u0432\u0430 \u043c\u043e\u043a\u0440\u0430\u044f\u00bb \u0438 \u00ab\u0445\u043e\u0440\u043e\u0448\u043e \u0440\u0430\u0441\u0442\u0443\u0442 \u0441\u043e\u0440\u043d\u044f\u043a\u0438\u00bb, \u043d\u0430\u043c \u043e\u0441\u0442\u0430\u043b\u043e\u0441\u044c \u043f\u0440\u0438\u043d\u044f\u0442\u044c \u0440\u0435\u0448\u0435\u043d\u0438\u0435 \u043e \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0435 \u00ab\u0441\u043e\u0441\u0435\u0434 \u043f\u043e\u043b\u0438\u043b \u0433\u0430\u0437\u043e\u043d\u00bb. <\/p>\n<p>  \u0421\u043a\u043e\u043b\u044c\u043a\u043e \u0432\u0441\u0435\u0433\u043e \u0442\u0430\u043a\u0438\u0445 \u0440\u0435\u0448\u0435\u043d\u0438\u0439 \u043d\u0443\u0436\u043d\u043e \u043f\u0440\u0438\u043d\u044f\u0442\u044c? \u041d\u0435 \u0431\u043e\u043b\u0435\u0435 \u0447\u0435\u043c n \u2013 \u0447\u0438\u0441\u043b\u043e \u043f\u0440\u0435\u0434\u043b\u043e\u0436\u0435\u043d\u0438\u0439. \u0421\u043a\u043e\u043b\u044c\u043a\u043e \u043e\u043f\u0435\u0440\u0430\u0446\u0438\u0439 \u043d\u0443\u0436\u043d\u043e \u0441\u043e\u0432\u0435\u0440\u0448\u0438\u0442\u044c \u043f\u0440\u0438 \u043f\u0440\u0438\u043d\u044f\u0442\u0438\u0438 \u043e\u0434\u043d\u043e\u0433\u043e \u0440\u0435\u0448\u0435\u043d\u0438\u044f? \u0414\u043b\u044f \u043a\u0430\u0436\u0434\u043e\u0433\u043e \u0440\u0435\u0448\u0435\u043d\u0438\u044f \u043d\u0430\u043c \u043d\u0443\u0436\u043d\u043e \u043e\u0431\u043e\u0439\u0442\u0438 \u0440\u0435\u0431\u0440\u0430 \u0433\u0440\u0430\u0444\u0430 \u043d\u0435 \u0431\u043e\u043b\u0435\u0435 \u043e\u0434\u043d\u043e\u0433\u043e \u0440\u0430\u0437\u0430, \u0442.\u00a0\u0435. \u0441\u043e\u0432\u0435\u0440\u0448\u0438\u0442\u044c \u043d\u0435 \u0431\u043e\u043b\u0435\u0435 n \u043e\u043f\u0435\u0440\u0430\u0446\u0438\u0439 \u043d\u0430 \u043e\u0434\u043d\u043e \u0440\u0435\u0448\u0435\u043d\u0438\u0435. \u0417\u043d\u0430\u0447\u0438\u0442, \u0447\u0442\u043e \u043d\u0443\u0436\u043d\u043e \u0441\u043e\u0432\u0435\u0440\u0448\u0438\u0442\u044c \u043d\u0435 \u0431\u043e\u043b\u0435\u0435 \u0447\u0435\u043c n<sup>2<\/sup> \u043e\u043f\u0435\u0440\u0430\u0446\u0438\u0439 \u0434\u043b\u044f \u043d\u0430\u0445\u043e\u0436\u0434\u0435\u043d\u0438\u044f <b>I<\/b>. \u25a0<\/p>\n<h4>\u0417\u0430\u0434\u0430\u0447\u0430 \u00ab\u043d\u0430 \u043f\u043e\u0434\u0443\u043c\u0430\u0442\u044c\u00bb<\/h4>\n<p>  \u0414\u0430\u043d\u043d\u0430\u044f \u0437\u0430\u0434\u0430\u0447\u0430 \u043c\u043e\u0436\u0435\u0442 \u043f\u043e\u0442\u0440\u0435\u0431\u043e\u0432\u0430\u0442\u044c \u0434\u043e\u043f\u043e\u043b\u043d\u0438\u0442\u0435\u043b\u044c\u043d\u043e\u0433\u043e \u0438\u0437\u0443\u0447\u0435\u043d\u0438\u044f \u0438 \u043f\u043e\u0438\u0441\u043a\u0430 \u043b\u0438\u0442\u0435\u0440\u0430\u0442\u0443\u0440\u044b.   <\/p>\n<h5>\u0422\u0440\u0438\u0432\u0438\u0430\u043b\u044c\u043d\u043e\u0435 \u0440\u0435\u0448\u0435\u043d\u0438\u0435 SAT<br \/>  <\/h5>\n<p><b>\u0423\u0441\u043b\u043e\u0432\u0438\u0435<\/b><br \/>  \u041a\u0430\u0436\u0434\u0443\u044e \u043f\u0440\u043e\u043f\u043e\u0437\u0438\u0446\u0438\u043e\u043d\u043d\u0443\u044e \u0444\u043e\u0440\u043c\u0443\u043b\u0443 F = c<sub>1<\/sub> and c<sub>2<\/sub> and c<sub>3<\/sub> and c<sub>n<\/sub> \u043c\u043e\u0436\u043d\u043e \u043f\u0440\u0438\u0432\u0435\u0437\u0442\u0438 \u043a \u0434\u0438\u0437\u044a\u044e\u043d\u043a\u0442\u0438\u0432\u043d\u043e\u0439 \u043d\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u043e\u0439 \u0444\u043e\u0440\u043c\u0435 (DNF) \u0442.\u00a0\u0435. \u043a \u0432\u0438\u0434\u0443 F&#8217; = c&#8217;<sub>1<\/sub> or c&#8217;<sub>2<\/sub> \u2026 or c&#8217;<sub>k<\/sub>, \u0433\u0434\u0435 \u0441&#8217;<sub>i<\/sub> \u0438\u043c\u0435\u0435\u0442 \u0432\u0438\u0434 (x and y and z), x, y, z \u2013 \u043f\u0435\u0440\u0435\u043c\u0435\u043d\u043d\u044b\u0435 \u0438\u043b\u0438 \u0438\u0445 \u043e\u0442\u0440\u0438\u0446\u0430\u043d\u0438\u044f. \u041d\u0430\u043f\u0440\u0438\u043c\u0435\u0440, \u0441 \u043f\u043e\u043c\u043e\u0449\u044c\u044e \u043f\u043e\u0441\u043b\u0435\u0434\u043e\u0432\u0430\u0442\u0435\u043b\u044c\u043d\u043e\u0433\u043e \u043f\u0440\u0438\u043c\u0435\u043d\u0435\u043d\u0438\u044f \u043f\u0440\u0430\u0432\u0438\u043b \u0414\u0435 \u041c\u043e\u0440\u0433\u0430\u043d\u0430 (\u0441\u0441\u044b\u043b\u043a\u0430) \u0438 \u0440\u0430\u0441\u043a\u0440\u044b\u0442\u0438\u044f \u0441\u043a\u043e\u0431\u043e\u043a.<br \/>  \u0414\u043b\u044f F&#8217; \u0441\u0443\u0449\u0435\u0441\u0442\u0432\u0443\u0435\u0442 \u0442\u0440\u0438\u0432\u0438\u0430\u043b\u044c\u043d\u044b\u0439 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c \u043f\u043e\u0438\u0441\u043a\u0430 \u0444\u0443\u043d\u043a\u0446\u0438\u0438 I. \u041d\u0435\u043e\u0431\u0445\u043e\u0434\u0438\u043c\u043e, \u0447\u0442\u043e\u0431\u044b \u043f\u043e \u043a\u0440\u0430\u0439\u043d\u0435\u0439 \u043c\u0435\u0440\u0435 \u043e\u0434\u0438\u043d \u0438\u0437 c&#8217;<sub>i<\/sub> \u0431\u044b\u043b \u0438\u0441\u0442\u0438\u043d\u043d\u044b\u043c. \u041d\u0430\u043f\u0438\u0448\u0435\u043c \u043f\u0440\u043e\u0441\u0442\u043e\u0439 \u043f\u0441\u0435\u0432\u0434\u043e\u043a\u043e\u0434 \u0440\u0435\u0448\u0430\u044e\u0449\u0438\u0439 \u0437\u0430\u0434\u0430\u0447\u0443:  <\/p>\n<pre><code class=\"python\">#Input: F \u2014 propositional formula in disjunctive normal form (DNF) #Output: {SAT, UNSAT} for each c in F do     if c is SAT:         return SAT return UNSAT <\/code><\/pre>\n<p>  \u0414\u043b\u044f \u043a\u0430\u0436\u0434\u043e\u0433\u043e \u043f\u0440\u0435\u0434\u043b\u043e\u0436\u0435\u043d\u0438\u044f (\u0441lause) c<sub>i<\/sub> \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c \u043f\u043e\u0438\u0441\u043a\u0430 <b>I<\/b> \u0442\u0430\u043a \u0436\u0435 \u0442\u0440\u0438\u0432\u0438\u0430\u043b\u044c\u043d\u044b\u0439, \u0435\u0441\u043b\u0438 \u043f\u0440\u0435\u0434\u043b\u043e\u0436\u0435\u043d\u0438\u0435 c<sub>i<\/sub> \u043d\u0435 \u0441\u043e\u0434\u0435\u0440\u0436\u0438\u0442 \u043d\u0435\u043a\u043e\u0442\u043e\u0440\u043e\u0439 \u043f\u0435\u0440\u0435\u043c\u0435\u043d\u043d\u043e\u0439 v \u0438 \u0435\u0451 \u043e\u0442\u0440\u0438\u0446\u0430\u043d\u0438\u044f \u043e\u0434\u043d\u043e\u0432\u0440\u0435\u043c\u0435\u043d\u043d\u043e, \u0442\u043e c<sub>i<\/sub> \u0432\u044b\u043f\u043e\u043b\u043d\u0438\u043c\u043e (SAT).<br \/>  <b>\u0418\u0442\u043e\u0433\u043e<\/b>: \u043f\u043e\u043b\u0443\u0447\u0430\u0435\u043c \u0442\u0440\u0438\u0432\u0438\u0430\u043b\u044c\u043d\u044b\u0439 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c \u043f\u0440\u043e\u0432\u0435\u0440\u043a\u0438 \u0444\u043e\u0440\u043c\u0443\u043b\u044b \u043d\u0430 \u0432\u044b\u043f\u043e\u043b\u043d\u0438\u043c\u043e\u0441\u0442\u044c<br \/>  <b>\u041d\u0430\u0439\u0442\u0438<\/b>: \u0433\u0434\u0435 \u043e\u0448\u0438\u0431\u043a\u0430?<\/p>\n<h4>\u0421\u0441\u044b\u043b\u043a\u0438 \u0438 \u0438\u0441\u0442\u043e\u0447\u043d\u0438\u043a\u0438<\/h4>\n<p>  \u041a\u0430\u0440\u0442\u0438\u043d\u043a\u0430 \u0432\u043e \u0432\u0432\u0435\u0434\u0435\u043d\u0438\u0438 \u0432\u0437\u044f\u0442\u0430 \u0438\u0437 <br \/>  <a href=\"http:\/\/www.scottaaronson.com\/talks\/anthropic.html\">Computational Complexity and the Anthropic Principle Scott Aaronson<\/a><\/p>\n<p>  \u0421\u043b\u0430\u0439\u0434\u044b<br \/>  <a href=\"https:\/\/courses.cs.washington.edu\/courses\/...\/10_17_phase_transition.ppt\u200e\">Why SAT Scales: Phase Transition Phenomena &#038; Back Doors to Complexity<\/a> slides courtesy of Bart Selman Cornell University.<br \/>  \u0421\u043b\u0430\u0439\u0434\u044b \u043e\u0441\u043d\u043e\u0432\u0430\u043d\u044b \u043d\u0430 \u0441\u0442\u0430\u0442\u044c\u0435:<br \/>  <a href=\"http:\/\/www.cs.cornell.edu\/selman\/papers\/pdf\/99.random.typical.pdf\">2+P-SAT: Relation of typical-case complexity to the nature of the phase transition<\/a> (Monasson, Remi; Zecchina, Riccardo; Kirkpatrick, Scott; Selman, Bart; and Troyansky, Lidror.)<br \/>  \u041e\u0441\u0442\u0430\u043b\u044c\u043d\u044b\u0435 \u0441\u0442\u0430\u0442\u044c\u0438 \u043c\u043e\u0436\u043d\u043e \u043d\u0430\u0439\u0442\u0438 <a href=\"http:\/\/www.cs.cornell.edu\/selman\/papers\/\">\u0437\u0434\u0435\u0441\u044c<\/a><\/p>\n<p>  \u041f\u043e\u0434\u0440\u043e\u0431\u043d\u0435\u0435 \u043e\u0431 \u0438\u0441\u0442\u043e\u0440\u0438\u0438 NP \u043c\u043e\u0436\u043d\u043e \u043f\u0440\u043e\u0447\u0438\u0442\u0430\u0442\u044c \u0437\u0434\u0435\u0441\u044c:<br \/>  <a href=\"http:\/\/www.cs.princeton.edu\/courses\/archive\/spr07\/cos522\/SipserNP.pdf\">The History and Status of the P versus NP Question by Michael Sipser<\/a><br \/>  <a href=\"http:\/\/www.unizar.es\/acz\/05Publicaciones\/Monografias\/MonografiasPublicadas\/Monografia26\/057Mayordomo.pdf\">P versus NP by Elvira Mayordomo<\/a><\/p>\n<p>  \u041f\u043e\u0434\u0440\u043e\u0431\u043d\u0435\u0435 \u043e SAT-solver&#8217;\u0430\u0445:<br \/>  <a href=\"http:\/\/www.cs.princeton.edu\/courses\/archive\/spring10\/cos598D\/SharadMalikCOS598d.pdf\">SAT Solvers: A Condensed History <\/a><br \/>  <a href=\"http:\/\/www.mpi-inf.mpg.de\/vtsa12\/slides\/biere\/Biere-VTSA12-talk.pdf\">Understanding Modern SAT Solvers <\/a> \u2014 \u0430\u0432\u0442\u043e\u0440 Armin Biere, \u043f\u043e\u0436\u0430\u043b\u0443\u0439, \u0441\u0430\u043c\u044b\u0439 \u0438\u0437\u0432\u0435\u0441\u0442\u043d\u044b\u0439 \u0440\u0430\u0437\u0440\u0430\u0431\u043e\u0442\u0447\u0438\u043a SAT Solver&#8217;\u043e\u0432 \u0432 \u043c\u0438\u0440\u0435. \u0414\u043e\u043d\u0430\u043b\u044c\u0434 \u041a\u043d\u0443\u0442, \u043a\u043e\u0442\u043e\u0440\u044b\u0439 \u0441\u0435\u0439\u0447\u0430\u0441 \u043f\u0438\u0448\u0435\u0442 \u00abThe Art of Computer Programming: Volume 4B, Pre-fascicle 6A Satisfiability\u00bb, \u0433\u043e\u0432\u043e\u0440\u0438\u0442, \u0447\u0442\u043e \u043f\u043e \u043c\u043d\u043e\u0433\u0438\u043c \u0432\u043e\u043f\u0440\u043e\u0441\u0430\u043c \u043a\u043e\u043d\u0441\u0443\u043b\u044c\u0442\u0438\u0440\u0443\u0435\u0442\u0441\u044f \u0438\u043c\u0435\u043d\u043d\u043e \u0443 \u043d\u0435\u0433\u043e.<br \/>  <a href=\"https:\/\/www.cosic.esat.kuleuven.be\/ecrypt\/courses\/mykonos12\/slides\/day1\/slides-LS-SAT-1.pdf\"> Towards a new era of SAT Solvers<\/a><\/p>\n<p>  \u041c\u0430\u0442\u0435\u0440\u0438\u0430\u043b \u0441 \u0425\u0430\u0431\u0440\u044b:<br \/>  [1] <a href=\"http:\/\/habrahabr.ru\/post\/112305\/\">\u041f\u043e\u0447\u0435\u043c\u0443 \u044f \u043d\u0435 \u0432\u0435\u0440\u044e \u0432 \u043f\u0440\u043e\u0441\u0442\u044b\u0435 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u044b \u0434\u043b\u044f NP-\u043f\u043e\u043b\u043d\u044b\u0445 \u0437\u0430\u0434\u0430\u0447<\/a><br \/>  [2] <a href=\"http:\/\/habrahabr.ru\/post\/132127\">\u0415\u0449\u0435 \u043d\u0435\u043c\u043d\u043e\u0433\u043e \u043f\u0440\u043e P \u0438 NP<\/a><br \/>  [3] <a href=\"http:\/\/habrahabr.ru\/post\/112161\/\">\u041e\u0442\u043a\u0440\u044b\u0442\u043e\u0435 \u043f\u0438\u0441\u044c\u043c\u043e \u0443\u0447\u0435\u043d\u044b\u043c \u0438 \u044d\u0442\u0430\u043b\u043e\u043d\u043d\u0430\u044f \u0440\u0435\u0430\u043b\u0438\u0437\u0430\u0446\u0438\u044f \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u0430 \u0420\u043e\u043c\u0430\u043d\u043e\u0432\u0430 \u0434\u043b\u044f NP-\u043f\u043e\u043b\u043d\u043e\u0439 \u0437\u0430\u0434\u0430\u0447\u0438 3-\u0412\u042b\u041f<\/a><br \/>  [4] <a href=\"http:\/\/habrahabr.ru\/post\/101271\"> \u041e\u043f\u0443\u0431\u043b\u0438\u043a\u043e\u0432\u0430\u043d\u043e \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u043e P \u2260 NP?<\/a><br \/>  [5] <a href=\"http:\/\/habrahabr.ru\/post\/43224\/\">P=NP? \u0412\u0430\u0436\u043d\u0435\u0439\u0448\u0430\u044f \u043d\u0435\u0440\u0435\u0448\u0435\u043d\u043d\u0430\u044f \u0437\u0430\u0434\u0430\u0447\u0430 \u0442\u0435\u043e\u0440\u0435\u0442\u0438\u0447\u0435\u0441\u043a\u043e\u0439 \u0438\u043d\u0444\u043e\u0440\u043c\u0430\u0442\u0438\u043a\u0438.<\/a><br \/>  [6] <a href=\"http:\/\/habrahabr.ru\/post\/175113\/\">\u0422\u0435\u043e\u0440\u0435\u0442\u0438\u0447\u0435\u0441\u043a\u0430\u044f \u0438\u043d\u0444\u043e\u0440\u043c\u0430\u0442\u0438\u043a\u0430 \u0432 \u0410\u043a\u0430\u0434\u0435\u043c\u0438\u0447\u0435\u0441\u043a\u043e\u043c \u0423\u043d\u0438\u0432\u0435\u0440\u0441\u0438\u0442\u0435\u0442\u0435<\/a><br \/>  [7] <a href=\"http:\/\/habrahabr.ru\/post\/164557\/\">\u0422\u043e\u043f-10 \u0440\u0435\u0437\u0443\u043b\u044c\u0442\u0430\u0442\u043e\u0432 \u0432 \u043e\u0431\u043b\u0430\u0441\u0442\u0438 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u043e\u0432 \u0437\u0430 2012 \u0433\u043e\u0434<\/a><br \/>  [8] <a href=\"http:\/\/habrahabr.ru\/post\/139993\/&amp;post=1203984_258\/\">\u0414\u043e\u043a\u0430\u0437\u0430\u043d\u043e, \u0447\u0442\u043e \u0438\u0433\u0440\u0430 Super Mario \u044f\u0432\u043b\u044f\u0435\u0442\u0441\u044f NP-\u043f\u043e\u043b\u043d\u043e\u0439 \u0437\u0430\u0434\u0430\u0447\u0435\u0439<\/a><br \/>  [9] <a href=\"http:\/\/habrahabr.ru\/post\/196560\/\">\u0412\u0432\u0435\u0434\u0435\u043d\u0438\u0435 \u0432 \u0430\u043d\u0430\u043b\u0438\u0437 \u0441\u043b\u043e\u0436\u043d\u043e\u0441\u0442\u0438 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u043e\u0432 (\u0447\u0430\u0441\u0442\u044c 1)<\/a><br \/>  [10] <a href=\"http:\/\/habrahabr.ru\/post\/195482\/\">\u0412\u0432\u0435\u0434\u0435\u043d\u0438\u0435 \u0432 \u0430\u043d\u0430\u043b\u0438\u0437 \u0441\u043b\u043e\u0436\u043d\u043e\u0441\u0442\u0438 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u043e\u0432 (\u0447\u0430\u0441\u0442\u044c 2)<\/a> <br \/>  [11] <a href=\"http:\/\/habrahabr.ru\/post\/195996\/\">\u0412\u0432\u0435\u0434\u0435\u043d\u0438\u0435 \u0432 \u0430\u043d\u0430\u043b\u0438\u0437 \u0441\u043b\u043e\u0436\u043d\u043e\u0441\u0442\u0438 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u043e\u0432 (\u0447\u0430\u0441\u0442\u044c 3)<\/a> <br \/>  [12] <a href=\"http:\/\/habrahabr.ru\/post\/196226\/\">\u0412\u0432\u0435\u0434\u0435\u043d\u0438\u0435 \u0432 \u0430\u043d\u0430\u043b\u0438\u0437 \u0441\u043b\u043e\u0436\u043d\u043e\u0441\u0442\u0438 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u043e\u0432 (\u0447\u0430\u0441\u0442\u044c 4)<\/a><br \/>  [13] <a href=\"http:\/\/habrahabr.ru\/post\/188010\/\">\u0417\u043d\u0430\u0439 \u0441\u043b\u043e\u0436\u043d\u043e\u0441\u0442\u0438 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u043e\u0432 <\/a>    \t<\/p>\n<div class=\"clear\"><\/div>\n<\/p><\/div>\n<p> \u0441\u0441\u044b\u043b\u043a\u0430 \u043d\u0430 \u043e\u0440\u0438\u0433\u0438\u043d\u0430\u043b \u0441\u0442\u0430\u0442\u044c\u0438 <a href=\"http:\/\/habrahabr.ru\/post\/207112\/\"> http:\/\/habrahabr.ru\/post\/207112\/<\/a><\/p>\n","protected":false},"excerpt":{"rendered":"<div class=\"content html_format\">\n<blockquote><p>SAT \u0443\u0436\u0435 \u0442\u0435\u043c \u0445\u043e\u0440\u043e\u0448, \u0447\u0442\u043e \u043e\u043d \u0443\u043c \u0432 \u043f\u043e\u0440\u044f\u0434\u043e\u043a \u043f\u0440\u0438\u0432\u043e\u0434\u0438\u0442 <br \/>  \u041b\u043e\u043c\u043e\u043d\u043e\u0441\u043e\u0432 (<a href=\"http:\/\/i.imgur.com\/2nQ8VcA.jpg\">\u043e\u0440\u0438\u0433\u0438\u043d\u0430\u043b<\/a>)  <\/p><\/blockquote>\n<p>  <\/p>\n<h4>\u0412\u0432\u0435\u0434\u0435\u043d\u0438\u0435<\/h4>\n<p>  \u041d\u0430 \u0445\u0430\u0431\u0440\u0435 \u0443\u0436\u0435 \u043d\u0435\u043c\u0430\u043b\u043e \u0441\u0442\u0430\u0442\u0435\u0439, \u043f\u043e\u0441\u0432\u044f\u0449\u0435\u043d\u043d\u044b\u0445 \u043f\u0440\u043e\u0431\u043b\u0435\u043c\u0435 P vs. NP \u0438 \u0437\u0430\u0434\u0430\u0447\u0435 \u043e \u0432\u044b\u043f\u043e\u043b\u043d\u0438\u043c\u043e\u0441\u0442\u0438 \u043b\u043e\u0433\u0438\u0447\u0435\u0441\u043a\u0438\u0445 \u0444\u043e\u0440\u043c\u0443\u043b (SATisfiability problem). \u041e\u0434\u043d\u0430\u043a\u043e, \u0431\u043e\u043b\u044c\u0448\u0438\u043d\u0441\u0442\u0432\u043e \u0438\u0437 \u043d\u0438\u0445 \u043d\u0435 \u043e\u0442\u0432\u0435\u0447\u0430\u0435\u0442 \u043d\u0430 \u043d\u0435\u0441\u043a\u043e\u043b\u044c\u043a\u043e \u0441\u0430\u043c\u044b\u0445 \u0432\u0430\u0436\u043d\u044b\u0445 \u0432\u043e\u043f\u0440\u043e\u0441\u043e\u0432. \u041f\u043e\u0447\u0435\u043c\u0443 \u044d\u0442\u0430 \u043f\u0440\u043e\u0431\u043b\u0435\u043c\u0430 \u0434\u0435\u0439\u0441\u0442\u0432\u0438\u0442\u0435\u043b\u044c\u043d\u0430 \u0432\u0430\u0436\u043d\u0430 \u0434\u043b\u044f \u043d\u0430\u0441? \u0427\u0442\u043e \u0431\u0443\u0434\u0435\u0442, \u0435\u0441\u043b\u0438 \u0435\u0451 \u0440\u0435\u0448\u0430\u0442? \u0413\u0434\u0435 \u044d\u0442\u043e \u0432\u0441\u0435 \u0432\u043e\u043e\u0431\u0449\u0435 \u043f\u0440\u0438\u043c\u0435\u043d\u044f\u0435\u0442\u0441\u044f? \u0418 \u043f\u043e\u0447\u0435\u043c\u0443 \u043d\u0435\u043e\u0431\u0445\u043e\u0434\u0438\u043c\u043e \u0438\u043c\u0435\u0442\u044c \u0445\u043e\u0442\u044f \u0431\u044b \u043e\u0431\u0449\u0435\u0435 \u043f\u0440\u0435\u0434\u0441\u0442\u0430\u0432\u043b\u0435\u043d\u0438\u0435, \u043e \u0447\u0435\u043c \u0442\u0430\u043c \u0438\u0434\u0435\u0442 \u0440\u0435\u0447\u044c?<\/p>\n<p>  <img decoding=\"async\" src=\"http:\/\/habr.habrastorage.org\/post_images\/854\/10f\/e5e\/85410fe5e72138afd3136ec955a16af1.gif\" alt=\"image\"\/><\/p>\n<p>  \u0415\u0441\u043b\u0438 \u043c\u044b \u0434\u0435\u0442\u0430\u043b\u044c\u043d\u043e \u043f\u0440\u043e\u0430\u043d\u0430\u043b\u0438\u0437\u0438\u0440\u0443\u0435\u043c \u043d\u0430\u0438\u0431\u043e\u043b\u0435\u0435 \u0437\u0430\u043c\u0435\u0442\u043d\u044b\u0435 \u0440\u0430\u0431\u043e\u0442\u044b \u043d\u0430 \u0445\u0430\u0431\u0440\u0435 \u043f\u043e \u0434\u0430\u043d\u043d\u043e\u0439 \u0442\u0435\u043c\u0435 [<a href=\"http:\/\/habrahabr.ru\/post\/112305\/\">1<\/a>, <a href=\"http:\/\/habrahabr.ru\/post\/132127\/\">2<\/a>, <a href=\"http:\/\/habrahabr.ru\/post\/112161\/\">3<\/a>, <a href=\"http:\/\/habrahabr.ru\/post\/101271\/\">4<\/a>, <a href=\"http:\/\/habrahabr.ru\/post\/43224\/\">5<\/a>, <a href=\"http:\/\/habrahabr.ru\/post\/175113\/\">6<\/a>, <a href=\"http:\/\/habrahabr.ru\/post\/164557\/\">7<\/a>], \u0442\u043e \u0437\u0430\u043c\u0435\u0442\u0438\u043c, \u0447\u0442\u043e \u0441 \u043e\u0434\u043d\u043e\u0439 \u0441\u0442\u043e\u0440\u043e\u043d\u044b, \u043b\u044e\u0434\u0438 \u043e\u0431\u043b\u0430\u0434\u0430\u044e\u0449\u0438\u0435 \u0437\u043d\u0430\u043d\u0438\u044f\u043c\u0438 \u0432 \u043e\u0431\u043b\u0430\u0441\u0442\u0438 \u0432\u044b\u0447\u0438\u0441\u043b\u0438\u0442\u0435\u043b\u044c\u043d\u043e\u0439 \u0441\u043b\u043e\u0436\u043d\u043e\u0441\u0442\u0438 \u043d\u0435 c\u043c\u043e\u0433\u0443\u0442 \u043f\u043e\u0447\u0435\u0440\u043f\u043d\u0443\u0442\u044c \u043d\u0438\u0447\u0435\u0433\u043e \u043f\u0440\u0438\u043d\u0446\u0438\u043f\u0438\u0430\u043b\u044c\u043d\u043e \u043d\u043e\u0432\u043e\u0433\u043e \u0432 \u0434\u0430\u043d\u043d\u044b\u0445 \u0441\u0442\u0430\u0442\u044c\u044f\u0445. \u0421 \u0434\u0440\u0443\u0433\u043e\u0439 \u0441\u0442\u043e\u0440\u043e\u043d\u044b, \u0434\u0430\u043d\u043d\u044b\u0435 \u0441\u0442\u0430\u0442\u044c\u0438 \u043f\u043e-\u043f\u0440\u0435\u0436\u043d\u0435\u043c\u0443 \u043d\u0435 \u044f\u0432\u043b\u044f\u044e\u0442\u0441\u044f \u043e\u0431\u0449\u0435\u0434\u043e\u0441\u0442\u0443\u043f\u043d\u044b\u043c\u0438. \u0418\u043b\u043b\u044e\u0441\u0442\u0440\u0430\u0446\u0438\u044f \u0438\u0437 \u0437\u0430\u0433\u043e\u043b\u043e\u0432\u043a\u0430 \u043d\u0430\u0433\u043b\u044f\u0434\u043d\u043e \u0434\u0435\u043c\u043e\u043d\u0441\u0442\u0440\u0438\u0440\u0443\u0435\u0442 \u043f\u0440\u043e\u0431\u043b\u0435\u043c\u0443: \u0442\u0435\u043c, \u043a\u043e\u043c\u0443 \u0431\u044b\u043b\u043e \u043d\u0435 \u043f\u043e\u043d\u044f\u0442\u043d\u043e, \u0438\u0437 \u043d\u0435\u0451 \u043d\u0438\u0447\u0435\u0433\u043e \u043d\u0435 \u044f\u0441\u043d\u043e, \u0430 \u0442\u0435, \u043a\u0442\u043e \u043e\u0431 \u044d\u0442\u043e\u043c \u0443\u0436\u0435 \u0441\u043b\u044b\u0448\u0430\u043b, \u0432 \u043d\u0435\u0439 \u043d\u0435 \u043d\u0443\u0436\u0434\u0430\u044e\u0442\u0441\u044f.<\/p>\n<p>  \u0414\u0430\u043d\u043d\u0430\u044f \u0441\u0442\u0430\u0442\u044c\u044f \u043f\u0440\u0435\u0441\u043b\u0435\u0434\u0443\u0435\u0442 \u0434\u0432\u0435 \u0446\u0435\u043b\u0438: \u043f\u0435\u0440\u0432\u043e\u0435 \u2014 \u0434\u0430\u0442\u044c \u043e\u0431\u0449\u0435\u0435 \u043f\u0440\u0435\u0434\u0441\u0442\u0430\u0432\u043b\u0435\u043d\u0438\u0435 \u043e \u043f\u0440\u043e\u0431\u043b\u0435\u043c\u0435 \u0438 \u043e\u0442\u0432\u0435\u0442\u0438\u0442\u044c \u043d\u0430 \u0432\u043e\u043f\u0440\u043e\u0441, \u043f\u043e\u0447\u0435\u043c\u0443 \u0436\u0435 \u043d\u0430\u043c \u0441\u0442\u043e\u0438\u0442\u044c \u0437\u043d\u0430\u0442\u044c \u043e\u0431 \u044d\u0442\u043e\u0439 \u0437\u0430\u0434\u0430\u0447\u0435 (\u043f\u0435\u0440\u0432\u0430\u044f \u0447\u0430\u0441\u0442\u044c), \u0432\u0442\u043e\u0440\u043e\u0435 \u2014 \u043f\u0440\u0435\u0434\u043e\u0441\u0442\u0430\u0432\u0438\u0442\u044c \u043c\u0430\u0442\u0435\u0440\u0438\u0430\u043b \u00ab\u043d\u0430 \u0432\u044b\u0440\u043e\u0441\u0442\u00bb, \u043a\u043e\u0442\u043e\u0440\u044b\u0439 \u0431\u0443\u0434\u0435\u0442 \u0438\u043d\u0442\u0435\u0440\u0435\u0441\u0435\u043d \u043b\u044e\u0434\u044f\u043c \u0438\u043d\u0442\u0435\u0440\u0435\u0441\u0443\u044e\u0449\u0438\u043c\u0441\u044f \u0442\u0435\u043c\u0430\u0442\u0438\u043a\u043e\u0439, \u0430 \u0442\u0430\u043a \u0436\u0435 \u043c\u043e\u0436\u0435\u0442 \u0431\u044b\u0442\u044c \u043f\u043e\u043b\u0435\u0437\u0435\u043d \u0434\u043b\u044f \u0438\u0437\u0443\u0447\u0435\u043d\u0438\u044f \u0442\u0435\u043c\u044b \u0432 \u0434\u0430\u043b\u044c\u043d\u0435\u0439\u0448\u0435\u043c (\u0432\u0442\u043e\u0440\u0430\u044f \u0447\u0430\u0441\u0442\u044c).<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"footnotes":""},"categories":[],"tags":[],"class_list":["post-207112","post","type-post","status-publish","format-standard","hentry"],"_links":{"self":[{"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=\/wp\/v2\/posts\/207112","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=%2Fwp%2Fv2%2Fcomments&post=207112"}],"version-history":[{"count":0,"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=\/wp\/v2\/posts\/207112\/revisions"}],"wp:attachment":[{"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=%2Fwp%2Fv2%2Fmedia&parent=207112"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=%2Fwp%2Fv2%2Fcategories&post=207112"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=%2Fwp%2Fv2%2Ftags&post=207112"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}