{"id":208774,"date":"2014-01-14T15:19:03","date_gmt":"2014-01-14T11:19:03","guid":{"rendered":"http:\/\/savepearlharbor.com\/?p=208774"},"modified":"-0001-11-30T00:00:00","modified_gmt":"-0001-11-29T21:00:00","slug":"","status":"publish","type":"post","link":"https:\/\/savepearlharbor.com\/?p=208774","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 \u0432\u0442\u043e\u0440\u0430\u044f)<\/span>"},"content":{"rendered":"<div class=\"content html_format\">   \t\u0412 <a href=\"http:\/\/habrahabr.ru\/post\/207112\/\">\u043f\u0440\u0435\u0434\u044b\u0434\u0443\u0449\u0435\u0439 \u0447\u0430\u0441\u0442\u0438<\/a> \u0431\u044b\u043b\u0438 \u043e\u0441\u0432\u0435\u0449\u0435\u043d\u044b \u043e\u0431\u0449\u0435\u0434\u043e\u0441\u0442\u0443\u043f\u043d\u044b\u0435 \u0432\u043e\u043f\u0440\u043e\u0441\u044b, \u043a\u0430\u0441\u0430\u044e\u0449\u0438\u0435\u0441\u044f SAT \u0438 P-NP: \u0438\u0441\u0442\u043e\u0440\u0438\u044f \u043f\u0440\u043e\u0431\u043b\u0435\u043c\u044b, \u0438\u043d\u0442\u0443\u0438\u0442\u0438\u0432\u043d\u044b\u0435 \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u0435\u043d\u0438\u044f \u043a\u043b\u0430\u0441\u0441\u043e\u0432 \u0438 \u0437\u0430\u0434\u0430\u0447, \u0443\u043a\u0430\u0437\u0430\u043d\u044b \u043e\u0441\u043d\u043e\u0432\u043d\u044b\u0435 \u043f\u0440\u0438\u043b\u043e\u0436\u0435\u043d\u0438\u044f SAT \u0438 \u043e\u0441\u043d\u043e\u0432\u043d\u044b\u0435 \u043f\u043e\u0441\u043b\u0435\u0434\u0441\u0442\u0432\u0438\u044f, \u0432 \u0441\u043b\u0443\u0447\u0430\u0438 \u0440\u0435\u0448\u0435\u043d\u0438\u044f P ?= NP (\u0442\u0430\u043c \u0436\u0435 \u043c\u043e\u0436\u043d\u043e \u043d\u0430\u0439\u0442\u0438 \u0434\u043e\u0441\u0442\u0430\u0442\u043e\u0447\u043d\u043e\u0435 \u0447\u0438\u0441\u043b\u043e \u0441\u0441\u044b\u043b\u043e\u043a \u043d\u0430 \u0440\u0430\u0437\u043b\u0438\u0447\u043d\u044b\u0439 \u043c\u0430\u0442\u0435\u0440\u0438\u0430\u043b \u0434\u043b\u044f \u0441\u0430\u043c\u043e\u0441\u0442\u043e\u044f\u0442\u0435\u043b\u044c\u043d\u043e\u0433\u043e \u0438\u0437\u0443\u0447\u0435\u043d\u0438\u044f \u0442\u0435\u043c\u0430\u0442\u0438\u043a\u0438).<\/p>\n<p>  \u0412 \u0434\u0430\u043d\u043d\u043e\u0439 \u0441\u0442\u0430\u0442\u044c\u0435 \u043c\u044b \u0440\u0430\u0441\u0441\u043c\u043e\u0442\u0440\u0438\u043c \u0442\u0435\u0445\u043d\u0438\u0447\u0435\u0441\u043a\u0443\u044e \u0441\u0442\u043e\u0440\u043e\u043d\u0443 \u0432\u043e\u043f\u0440\u043e\u0441\u0430, \u0430 \u0442\u0430\u043a \u0436\u0435 \u0444\u043e\u0440\u043c\u0430\u043b\u0438\u0437\u0443\u0435\u043c \u0438 \u043f\u0440\u0435\u0434\u0441\u0442\u0430\u0432\u0438\u043c \u0432 \u0434\u0435\u0442\u0430\u043b\u044f\u0445 \u043c\u0430\u0442\u0435\u0440\u0438\u0430\u043b \u0438\u0437 \u043f\u0440\u0435\u0434\u044b\u0434\u0443\u0449\u0435\u0439 \u0441\u0442\u0430\u0442\u044c\u0438.<\/p>\n<p>  <img decoding=\"async\" src=\"http:\/\/habr.habrastorage.org\/post_images\/ec5\/2c5\/848\/ec52c5848cb78645a2b82a6f5e2a8aca.jpg\"\/><\/p>\n<p>  \u043a\u0430\u0440\u0442\u0438\u043d\u043a\u0430 \u0438\u0437 \u0441\u0442\u0430\u0442\u044c\u0438 <a href=\"http:\/\/cacm.acm.org\/magazines\/2009\/8\/34498-boolean-satisfiability-from-theoretical-hardness-to-practical-success\/pdf\">Boolean Satisfiability: From Theoretical Hardness to Practical Success<\/a> (Communications of ACM) <\/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 (<a href=\"http:\/\/habrahabr.ru\/post\/207112\">\u043f\u0435\u0440\u0432\u0430\u044f \u0447\u0430\u0441\u0442\u044c<\/a>)<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 (\u0434\u0430\u043d\u043d\u0430\u044f \u0441\u0442\u0430\u0442\u044c\u044f)<br \/> \n<ol>\n<li>\u0427\u0442\u043e \u0431\u0443\u0434\u0435\u0442, \u0435\u0441\u043b\u0438\u2026 (\u0432 \u0434\u0435\u0442\u0430\u043b\u044f\u0445) <\/li>\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. \u041a\u043b\u0430\u0441\u0441 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>\u041e \u0441\u043e\u0432\u0440\u0435\u043c\u0435\u043d\u043d\u044b\u0445 SAT solver&#8217;\u0430\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 <a href=\"http:\/\/habrahabr.ru\/post\/112161\/\">\u0441\u0442\u0430\u0442\u044c\u044e \u0420\u043e\u043c\u0430\u043d\u043e\u0432\u0430<\/a> \u043e\u0436\u0438\u0434\u0430\u0435\u0442 reject<\/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<h4> \u0427\u0442\u043e \u0431\u0443\u0434\u0435\u0442, \u0435\u0441\u043b\u0438\u2026 <\/h4>\n<p>  \u0412 \u043f\u0440\u0435\u0434\u044b\u0434\u0443\u0449\u0435\u0439 \u0440\u0430\u0431\u043e\u0442\u0435, \u0431\u044b\u043b \u0440\u0430\u0441\u0441\u043c\u043e\u0442\u0440\u0435\u043d \u0442\u043e\u043b\u044c\u043a\u043e \u0441\u0430\u043c\u044b\u0439 \u043f\u0440\u043e\u0441\u0442\u043e\u0439 \u0441\u0446\u0435\u043d\u0430\u0440\u0438\u0439 \u0440\u0435\u0448\u0435\u043d\u0438\u044f, \u0447\u0442\u043e \u0432\u044b\u0437\u0432\u0430\u043b\u043e \u0440\u044f\u0434 \u0438\u043d\u0442\u0435\u0440\u0435\u0441\u043d\u044b\u0445 \u0437\u0430\u043c\u0435\u0447\u0430\u043d\u0438\u0439 (\u0430\u0432\u0442\u043e\u0440 \u0432\u044b\u0440\u0430\u0436\u0430\u0435\u0442 \u0431\u043b\u0430\u0433\u043e\u0434\u0430\u0440\u043d\u043e\u0441\u0442\u044c \u0437\u0430 \u0438\u043d\u0442\u0435\u0440\u0435\u0441\u043d\u044b\u0435 \u0438 \u043f\u043e\u043b\u0435\u0437\u043d\u044b\u0435 \u0441\u0441\u044b\u043b\u043a\u0438 \u043f\u043e \u0434\u0430\u043d\u043d\u043e\u043c\u0443 \u0432\u043e\u043f\u0440\u043e\u0441\u0443). \u0412 \u0434\u0430\u043d\u043d\u043e\u0439 \u0441\u0442\u0430\u0442\u044c\u0435 \u0440\u0430\u0441\u0441\u043c\u043e\u0442\u0440\u0438\u043c \u0432\u0441\u0435\u0432\u043e\u0437\u043c\u043e\u0436\u043d\u044b\u0435 \u043e\u043f\u0446\u0438\u0438 \u0438 \u0438\u0445 \u043f\u043e\u0441\u043b\u0435\u0434\u0441\u0442\u0432\u0438\u044f, \u043f\u0440\u0438\u043d\u0438\u043c\u0430\u044f \u0432\u043e \u0432\u043d\u0438\u043c\u0430\u043d\u0438\u044f \u043a\u043e\u043c\u043c\u0435\u043d\u0442\u0430\u0440\u0438\u0438 \u0438 \u0437\u0430\u043c\u0435\u0447\u0430\u043d\u0438\u044f \u043a \u043f\u0440\u0435\u0434\u044b\u0434\u0443\u0449\u0435\u0439 \u0440\u0430\u0431\u043e\u0442\u0435. <\/p>\n<p>  <a href=\"http:\/\/rjlipton.wordpress.com\/2009\/07\/03\/is-pnp-an-ill-posed-problem\/\">\u0417\u0434\u0435\u0441\u044c<\/a> \u0434\u043e\u0432\u043e\u043b\u044c\u043d\u043e \u0438\u043d\u0442\u0435\u0440\u0435\u0441\u043d\u043e \u0441 \u0445\u0443\u0434\u043e\u0436\u0435\u0441\u0442\u0432\u0435\u043d\u043d\u043e\u0439 \u0442\u043e\u0447\u043a\u0438 \u0437\u0440\u0435\u043d\u0438\u044f \u043e\u043f\u0438\u0441\u0430\u043d\u0430 \u0434\u0438\u0441\u043a\u0443\u0441\u0441\u0438\u044f \u0432\u043e\u043a\u0440\u0443\u0433 \u0440\u0430\u0437\u043b\u0438\u0447\u043d\u044b\u0445 \u0432\u0430\u0440\u0438\u0430\u043d\u0442\u043e\u0432 \u0440\u0435\u0448\u0435\u043d\u0438\u044f.<\/p>\n<h5>P = NP <\/h5>\n<p>  \u0412\u043e\u0437\u043c\u043e\u0436\u043d\u043e \u043d\u0435\u0441\u043a\u043e\u043b\u044c\u043a\u043e \u0432\u0430\u0440\u0438\u0430\u043d\u0442\u043e\u0432 \u0440\u0430\u0437\u0432\u0438\u0442\u0438\u044f \u0441\u0438\u0442\u0443\u0430\u0446\u0438\u0438  <\/p>\n<ul>\n<li> \u0420\u0435\u0448\u0435\u043d\u0438\u0435 \u043a\u043e\u043d\u0441\u0442\u0440\u0443\u043a\u0442\u0438\u0432\u043d\u043e\u0435<br \/> \n<ol>\n<li> \u041f\u043e\u043b\u0438\u043d\u043e\u043c \u0438\u043c\u0435\u0435\u0442 \u043d\u0435\u0432\u044b\u0441\u043e\u043a\u0443\u044e \u0441\u0442\u0435\u043f\u0435\u043d\u044c \u0438 \u0443\u043c\u0435\u0440\u0435\u043d\u043d\u044b\u0435 \u043a\u043e\u044d\u0444\u0444\u0438\u0446\u0438\u0435\u043d\u0442\u044b: \u0442\u043e\u0433\u0434\u0430 \u043f\u043e\u0434\u0440\u043e\u0431\u043d\u043e\u0441\u0442\u0438 <a href=\"http:\/\/habrahabr.ru\/post\/207112\/\">\u043e\u043f\u0438\u0441\u0430\u043d\u044b \u0432 \u0447\u0430\u0441\u0442\u0438 P = NP \u043f\u0440\u0435\u0434\u044b\u0434\u0443\u0449\u0435\u0439 \u0441\u0442\u0430\u0442\u044c\u0438<\/a>; \u0432\u043a\u0440\u0430\u0442\u0446\u0435: \u0440\u0443\u0445\u043d\u0435\u0442 \u0432\u0441\u044f \u043a\u0440\u0438\u043f\u0442\u043e\u0433\u0440\u0430\u0444\u0438\u044f<\/li>\n<li> \u041f\u043e\u043b\u0438\u043d\u043e\u043c \u0438\u043c\u0435\u0435\u0442 \u0432\u044b\u0441\u043e\u043a\u0443\u044e \u0441\u0442\u0435\u043f\u0435\u043d\u044c \u2014 \u0442\u043e\u0433\u0434\u0430 \u043d\u0438\u0447\u0435\u0433\u043e \u043d\u0435 \u0438\u0437\u043c\u0435\u043d\u0438\u0442\u0441\u044f \u0438 \u0441 \u043f\u0440\u0430\u043a\u0442\u0438\u0447\u0435\u0441\u043a\u043e\u0439 \u0442\u043e\u0447\u043a\u0438 \u0437\u0440\u0435\u043d\u0438\u044f P != NP<\/li>\n<\/ol>\n<p>   <\/li>\n<li> \u0420\u0435\u0448\u0435\u043d\u0438\u0435 \u043d\u0435\u043a\u043e\u043d\u0441\u0442\u0440\u0443\u043a\u0442\u0438\u0432\u043d\u043e\u0435<br \/> \n<ol>\n<li> \u0415\u0441\u043b\u0438 \u043c\u044b \u043d\u0435 \u0441\u043c\u043e\u0436\u0435\u043c \u043f\u043e\u043b\u0443\u0447\u0438\u0442\u044c \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c \u0438\u0437 \u0434\u0430\u043d\u043d\u043e\u0433\u043e \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u0430, \u0442\u043e \u0441 \u043f\u0440\u0430\u043a\u0442\u0438\u0447\u0435\u0441\u043a\u043e\u0439 \u0442\u043e\u0447\u043a\u0438 \u0437\u0440\u0435\u043d\u0438\u044f P != NP <\/li>\n<li> \u0415\u0441\u043b\u0438 \u043c\u043e\u0436\u0435\u043c, \u0442\u043e \u0432\u043e\u043f\u0440\u043e\u0441 P ?= NP, \u0442\u0440\u0430\u043d\u0441\u0444\u043e\u0440\u043c\u0438\u0440\u0443\u0435\u0442\u0441\u044f \u0432 \u0432\u043e\u043f\u0440\u043e\u0441 \u0432\u0440\u0435\u043c\u0435\u043d\u0438 \u0438 \u0441\u043e\u0437\u0434\u0430\u043d\u0438\u044f \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u0430 \u0438\u0437 \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u0430<\/li>\n<\/ol>\n<p>  <\/li>\n<\/ul>\n<h5>P != NP <\/h5>\n<p>  \u041a\u0430\u043a \u0438 \u0432 \u043f\u0440\u0435\u0434\u044b\u0434\u0443\u0449\u0435\u043c \u0441\u043b\u0443\u0447\u0430\u0435 \u0440\u0435\u0448\u0435\u043d\u0438\u0435 \u043c\u043e\u0436\u0435\u0442 \u0431\u044b\u0442\u044c \u043a\u043e\u043d\u0441\u0442\u0440\u0443\u043a\u0442\u0438\u0432\u043d\u044b\u043c \u0438 \u043d\u0435-\u043a\u043e\u043d\u0441\u0442\u0440\u0443\u043a\u0442\u0438\u0432\u043d\u044b\u043c. \u0420\u0430\u0441\u0441\u043c\u043e\u0442\u0440\u0438\u043c \u043a\u043e\u043d\u0441\u0442\u0440\u0443\u043a\u0442\u0438\u0432\u043d\u044b\u0439 \u0441\u043b\u0443\u0447\u0430\u0439 (\u043d\u0435\u043a\u043e\u043d\u0441\u0442\u0440\u0443\u043a\u0442\u0438\u0432\u043d\u044b\u0439 \u043f\u043e \u0441\u0442\u0440\u0443\u043a\u0442\u0443\u0440\u0435 \u0441\u0445\u043e\u0436 \u0441 \u043f\u0440\u0435\u0434\u044b\u0434\u0443\u0449\u0435\u043c \u0441\u043b\u0443\u0447\u0430\u0435\u043c)   <\/p>\n<ul>\n<li> \u0421\u043b\u043e\u0436\u043d\u043e\u0441\u0442\u044c \u0440\u0435\u0448\u0435\u043d\u0438\u044f \u0432\u0441\u0435\u0433\u0434\u0430 \u044d\u043a\u0441\u043f\u043e\u043d\u0435\u043d\u0446\u0438\u0430\u043b\u044c\u043d\u0430\u044f: \u043d\u0438\u043a\u0430\u043a\u0438\u0445 \u0438\u0437\u043c\u0435\u043d\u0435\u043d\u0438\u0439, \u0442\u0435\u043a\u0443\u0449\u0430\u044f \u043a\u0430\u0440\u0442\u0438\u043d\u0430 \u043c\u0438\u0440\u0430 \u043f\u043e\u043b\u043d\u043e\u0441\u0442\u044c\u044e \u0441\u043e\u0445\u0440\u0430\u043d\u0438\u0442\u0441\u044f, \u043d\u0438\u043a\u0430\u043a\u0438\u0445 \u0438\u0437\u043c\u0435\u043d\u0435\u043d\u0438\u0439 \u0432 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u0430\u0445 <\/li>\n<li> \u0421\u043b\u043e\u0436\u043d\u043e\u0441\u0442\u044c \u0440\u0435\u0448\u0435\u043d\u0438\u044f \u043d\u0435-\u0432\u0441\u0435\u0433\u0434\u0430 \u044d\u043a\u0441\u043f\u043e\u043d\u0435\u043d\u0446\u0438\u0430\u043b\u044c\u043d\u0430\u044f (\u0441\u043c. <a href=\"http:\/\/rjlipton.wordpress.com\/2009\/02\/12\/a-nightmare-about-sat\/\">\u044d\u0442\u043e\u0442 \u043f\u043e\u0441\u0442<\/a>), \u0430 \u0434\u043b\u044f \u0434\u043e\u0441\u0442\u0430\u0442\u043e\u0447\u043d\u043e\u0433\u043e \u043a\u043e\u043b\u0438\u0447\u0435\u0441\u0442\u0432\u0430 \u0441\u043b\u0443\u0447\u0430\u0435\u0432 \u043f\u043e\u043b\u0438\u043d\u043e\u043c\u0438\u0430\u043b\u044c\u043d\u0430\u044f. \u0412 \u0434\u0430\u043d\u043d\u043e\u043c \u0441\u043b\u0443\u0447\u0430\u0435, \u043f\u0440\u0430\u043a\u0442\u0438\u0447\u0435\u0441\u043a\u0438 \u043d\u0435\u0432\u043e\u0437\u043c\u043e\u0436\u043d\u043e \u043e\u0434\u043d\u043e\u0437\u043d\u0430\u0447\u043d\u043e \u043f\u0440\u0435\u0434\u0441\u043a\u0430\u0437\u0430\u0442\u044c, \u0447\u0442\u043e \u043f\u0440\u043e\u0438\u0437\u043e\u0439\u0434\u0435\u0442 \u0438 \u043c\u043e\u0436\u043d\u043e \u0442\u043e\u043b\u044c\u043a\u043e \u0441\u043f\u0435\u043a\u0443\u043b\u0438\u0440\u043e\u0432\u0430\u0442\u044c: \u0435\u0441\u043b\u0438 \u0437\u0430\u0434\u0430\u0447\u0430 \u0444\u0430\u043a\u0442\u043e\u0440\u0438\u0437\u0430\u0446\u0438\u0438 \u043f\u043e\u043f\u0430\u0434\u0430\u0435\u0442 \u0432 \u00ab\u043a\u043b\u0430\u0441\u0441 \u043b\u0435\u0433\u043a\u0438\u0445 \u0437\u0430\u0434\u0430\u0447\u00bb, \u0442\u043e \u0441 \u043f\u0440\u0430\u043a\u0442\u0438\u0447\u0435\u0441\u043a\u043e\u0439 \u0442\u043e\u0447\u043a\u0438 \u0437\u0440\u0435\u043d\u0438\u044f \u044d\u0442\u043e \u0431\u0443\u0434\u0435\u0442 \u044d\u043a\u0432\u0438\u0432\u0430\u043b\u0435\u043d\u0442\u043d\u043e P = NP \u0434\u043b\u044f \u0430\u0442\u0430\u043a\u0438 \u043d\u0430 RSA. <\/li>\n<li> \u0421\u043b\u043e\u0436\u043d\u043e\u0441\u0442\u044c \u0440\u0435\u0448\u0435\u043d\u0438\u044f \u0443\u043c\u0435\u0440\u0435\u043d\u043d\u0430\u044f \u0438\u043b\u0438 \u043d\u0438\u0437\u043a\u0430\u044f (e.g. n<sup>log(n)<\/sup>), \u0432 \u0434\u0430\u043d\u043d\u043e\u043c \u0441\u043b\u0443\u0447\u0430\u0435 \u0441 \u043f\u0440\u0430\u043a\u0442\u0438\u0447\u0435\u0441\u043a\u043e\u0439 \u0442\u043e\u0447\u043a\u0438 \u0437\u0440\u0435\u043d\u0438\u044f \u044d\u0442\u043e \u0431\u0443\u0434\u0435\u0442 \u044d\u043a\u0432\u0438\u0432\u0430\u043b\u0435\u043d\u0442\u043d\u043e P = NP<\/li>\n<\/ul>\n<h5>P vs. NP \u043d\u0435 \u0440\u0430\u0437\u0440\u0435\u0448\u0438\u043c\u0430 \u0432 \u0430\u043a\u0441\u0438\u043e\u043c\u0430\u0442\u0438\u043a\u0435 <a href=\"http:\/\/en.wikipedia.org\/wiki\/Zermelo%E2%80%93Fraenkel_set_theory\">ZFC<\/a> <\/h5>\n<p>  \u041f\u043e\u0434\u0440\u043e\u0431\u043d\u043e \u0438 \u0438\u043d\u0442\u0435\u0440\u0435\u0441\u043d\u043e \u043e\u0431 \u044d\u0442\u043e\u043c \u043d\u0430\u043f\u0438\u0441\u0430\u043d\u043e \u0432 \u0441\u0442\u0430\u0442\u044c\u0435 <a href=\"http:\/\/www.scottaaronson.com\/papers\/pnp.pdf\">Is P Versus NP Formally Independent? by Scott Aaronson<\/a> (\u0441\u0442\u0430\u0442\u044c\u044f \u0442\u0440\u0435\u0431\u0443\u0435\u0442 \u0434\u043e\u0441\u0442\u0430\u0442\u043e\u0447\u043d\u043e\u0439 \u043c\u0430\u0442\u0435\u043c\u0430\u0442\u0438\u0447\u0435\u0441\u043a\u043e\u0439 \u043a\u0443\u043b\u044c\u0442\u0443\u0440\u044b \u0434\u043b\u044f \u043f\u043e\u043d\u0438\u043c\u0430\u043d\u0438\u044f; \u043f\u0440\u0438\u043c\u0435\u0440\u043d\u043e\u0435 \u0432\u0440\u0435\u043c\u044f \u043f\u0440\u043e\u0447\u0442\u0435\u043d\u0438\u044f ~ 1\/2 \u0432\u0435\u0447\u0435\u0440\u0430). \u041f\u0440\u0438\u0432\u0435\u0434\u0435\u043c \u043a\u043e\u0440\u043e\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<p>  \u041e\u0441\u043d\u043e\u0432\u043d\u043e\u0439 \u043f\u043e\u0441\u044b\u043b \u0441\u0442\u0430\u0442\u044c\u0438 \u0432 \u0441\u043b\u0435\u0434\u0443\u044e\u0449\u0435\u043c, \u043c\u043e\u0436\u0435\u0442 \u0442\u0430\u043a \u043e\u043a\u0430\u0437\u0430\u0442\u044c\u0441\u044f, \u0447\u0442\u043e \u043e\u0431\u0435 \u0433\u0438\u043f\u043e\u0442\u0435\u0437\u044b P = NP \u0438 P != NP \u0441\u043e\u0433\u043b\u0430\u0441\u0443\u044e\u0442\u0441\u044f \u0441 \u0442\u0435\u043e\u0440\u0438\u0435\u0439 \u043c\u043d\u043e\u0436\u0435\u0441\u0442\u0432. \u042d\u0442\u043e \u043c\u043e\u0436\u0435\u0442 \u043f\u0440\u043e\u0438\u0437\u043e\u0439\u0442\u0438 \u0432 \u0442\u043e\u043c \u0441\u043b\u0443\u0447\u0430\u0435, \u0435\u0441\u043b\u0438 P vs. NP \u043d\u0435\u0437\u0430\u0432\u0438\u0441\u0438\u043c\u0430 \u043e\u0442 \u0430\u043a\u0441\u0438\u043e\u043c\u0430\u0442\u0438\u043a\u0438 \u0442\u0435\u043e\u0440\u0438\u0438 \u043c\u043d\u043e\u0436\u0435\u0441\u0442\u0432, \u043a\u0430\u043a \u043d\u0430\u043f\u0440\u0438\u043c\u0435\u0440 \u0430\u043a\u0441\u0438\u043e\u043c\u0430 \u0432\u044b\u0431\u043e\u0440\u0430 \u043d\u0435\u0437\u0430\u0432\u0438\u0441\u0438\u043c\u0430 \u043e\u0442 \u043e\u0441\u0442\u0430\u043b\u044c\u043d\u044b\u0445 \u0430\u043a\u0441\u0438\u043e\u043c \u0442\u0435\u043e\u0440\u0438\u0438 \u043c\u043d\u043e\u0436\u0435\u0441\u0442\u0432. \u0421 \u043f\u0440\u0430\u043a\u0442\u0438\u0447\u0435\u0441\u043a\u043e\u0439 \u0442\u043e\u0447\u043a\u0438 \u0437\u0440\u0435\u043d\u0438\u044f \u044d\u0442\u043e \u0431\u0443\u0434\u0435\u0442 \u043e\u0437\u043d\u0430\u0447\u0430\u0442\u044c, \u0447\u0442\u043e P != NP.<\/p>\n<h4>\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. \u041a\u043b\u0430\u0441\u0441 CoNP.<\/h4>\n<p>  \u0412 \u0442\u0435\u043e\u0440\u0438\u0438 \u0441\u043b\u043e\u0436\u043d\u043e\u0441\u0442\u0438 \u043f\u0440\u0438\u043d\u044f\u0442\u043e \u0444\u043e\u0440\u043c\u0443\u043b\u0438\u0440\u043e\u0432\u0430\u0442\u044c \u0437\u0430\u0434\u0430\u0447\u0438 \u0432 \u0432\u0438\u0434\u0435 \u00ab\u043f\u0440\u043e\u0431\u043b\u0435\u043c \u0440\u0430\u0437\u0440\u0435\u0448\u0438\u043c\u043e\u0441\u0442\u0438\u00bb \u0442.\u0435. \u0437\u0430\u0434\u0430\u0447\u0438, \u043e\u0442\u0432\u0435\u0442 \u043d\u0430 \u043a\u043e\u0442\u043e\u0440\u044b\u0435 \u043c\u043e\u0436\u0435\u0442 \u0431\u044b\u0442\u044c \u0442\u043e\u043b\u044c\u043a\u043e \u00ab\u0434\u0430\u00bb \u0438\u043b\u0438 \u00ab\u043d\u0435\u0442\u00bb. \u041a\u043b\u0430\u0441\u0441\u044b P \u0438 NP \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u043e \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u0435\u043d\u044b \u0432 \u0442\u0435\u0440\u043c\u0438\u043d\u0430\u0445 \u044f\u0437\u044b\u043a\u043e\u0432 \u0438 \u043c\u0430\u0448\u0438\u043d \u0422\u044c\u044e\u0440\u0438\u043d\u0433\u0430.<br \/>  <img decoding=\"async\" src=\"http:\/\/habr.habrastorage.org\/post_images\/6c4\/ed7\/360\/6c4ed7360a882229430c3721b69cab23.png\"\/><br \/>  \u0433\u0434\u0435 L<sub>M<\/sub> \u2014 \u044f\u0437\u044b\u043a \u043f\u0440\u0438\u043d\u0438\u043c\u0430\u0435\u043c\u044b\u0435 \u043c\u0430\u0448\u0438\u043d\u043e\u0439 M.<br \/>  \u041c\u044b \u0433\u043e\u0432\u043e\u0440\u0438\u043c, \u0447\u0442\u043e \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u0435\u043d\u043d\u0430\u044f \u0437\u0430\u0434\u0430\u0447\u0430 p \u043f\u0440\u0438\u043d\u0430\u0434\u043b\u0435\u0436\u0438\u0442 \u043a\u043b\u0430\u0441\u0441\u0443 P, \u0435\u0441\u043b\u0438 \u0441\u0443\u0449\u0435\u0441\u0442\u0432\u0443\u0435\u0442 \u0434\u0435\u0442\u0435\u0440\u043c\u0438\u043d\u0438\u0440\u043e\u0432\u0430\u043d\u043d\u0430\u044f \u043c\u0430\u0448\u0438\u043d\u0430 \u0422\u044c\u044e\u0440\u0438\u043d\u0433\u0430, \u043a\u043e\u0442\u043e\u0440\u0430\u044f \u043f\u0440\u0438\u043d\u0438\u043c\u0430\u0435\u043c \u044f\u0437\u044b\u043a L(p) \u0437\u0430 \u043f\u043e\u043b\u0438\u043d\u043e\u043c\u0438\u0430\u043b\u044c\u043d\u043e\u0435 \u0447\u0438\u0441\u043b\u043e \u0448\u0430\u0433\u043e\u0432.<\/p>\n<p>  \u0421 \u043a\u043b\u0430\u0441\u0441\u043e\u043c NP \u0432\u0441\u0451 \u043d\u0435\u043c\u043d\u043e\u0433\u043e \u0438\u043d\u0442\u0435\u0440\u0435\u0441\u043d\u0435\u0439, \u044d\u0442\u043e \u043a\u043b\u0430\u0441\u0441 \u0437\u0430\u0434\u0430\u0447, \u0433\u0434\u0435 \u043a\u043e\u0440\u0440\u0435\u043a\u0442\u043d\u043e\u0441\u0442\u044c \u0440\u0435\u0448\u0435\u043d\u0438\u044f \u043c\u043e\u0436\u0435\u0442 \u0431\u044b\u0442\u044c \u043f\u0440\u043e\u0432\u0435\u0440\u0435\u043d\u0430 \u0437\u0430 \u043f\u043e\u043b\u0438\u043d\u043e\u043c\u0438\u0430\u043b\u044c\u043d\u043e\u0435 \u0432\u0440\u0435\u043c\u044f. \u0424\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u043e \u043c\u044b \u0433\u043e\u0432\u043e\u0440\u0438\u043c, \u0447\u0442\u043e \u044f\u0437\u044b\u043a L \u043f\u0440\u0438\u043d\u0430\u0434\u043b\u0435\u0436\u0438\u0442 NP, \u0442\u043e\u0433\u0434\u0430 \u0438 \u0442\u043e\u043b\u044c\u043a\u043e \u0442\u043e\u0433\u0434\u0430 \u043a\u043e\u0433\u0434\u0430, \u0441\u0443\u0449\u0435\u0441\u0442\u0432\u0443\u0435\u0442 \u0434\u0435\u0442\u0435\u0440\u043c\u0438\u043d\u0438\u0440\u043e\u0432\u0430\u043d\u043d\u0430\u044f \u043c\u0430\u0448\u0438\u043d\u0430 \u0422\u044c\u044e\u0440\u0438\u043d\u0433\u0430 M, \u0442\u0430\u043a\u0430\u044f \u0447\u0442\u043e \u0434\u043b\u044f \u043b\u044e\u0431\u043e\u0439 \u0441\u0442\u0440\u043e\u043a\u0438 \u0445 \u0432\u0435\u0440\u043d\u043e:<br \/>  <img decoding=\"async\" src=\"http:\/\/habr.habrastorage.org\/post_images\/a8c\/596\/a55\/a8c596a55a2f6539260cf1731d590938.png\"\/> <br \/>  \u0433\u0434\u0435 |y| \u2014 \u043e\u0433\u0440\u0430\u043d\u0438\u0447\u0435\u043d \u043f\u043e\u043b\u0438\u043d\u043e\u043c\u043e\u043c \u0438 M \u0441\u043e\u0432\u0435\u0440\u0448\u0430\u0435\u0442 \u043f\u043e\u043b\u0438\u043d\u043e\u043c\u0438\u0430\u043b\u044c\u043d\u043e\u0435 \u0447\u0438\u0441\u043b\u043e \u0448\u0430\u0433\u043e\u0432. \u0414\u043b\u044f \u00aby\u00bb \u0441\u0443\u0449\u0435\u0441\u0442\u0432\u0443\u0435\u0442 \u0441\u043f\u0435\u0446\u0438\u0430\u043b\u044c\u043d\u044b\u0439 \u0442\u0435\u0440\u043c\u0438\u043d \u2014 \u0441\u0435\u0440\u0442\u0438\u0444\u0438\u043a\u0430\u0442. \u0424\u0430\u043a\u0442\u0438\u0447\u0435\u0441\u043a\u0438, \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u0435\u043d\u0438\u0435 \u0447\u0438\u0442\u0430\u0435\u0442\u0441\u044f \u0441\u043b\u0435\u0434\u0443\u044e\u0449\u0438\u043c \u043e\u0431\u0440\u0430\u0437\u043e\u043c \u2014 \u0437\u0430\u0434\u0430\u0447\u0430 \u043f\u0440\u0438\u043d\u0430\u0434\u043b\u0435\u0436\u0438\u0442 NP, \u0435\u0441\u043b\u0438 \u0441\u0443\u0449\u0435\u0441\u0442\u0432\u0443\u0435\u0442 \u043f\u043e\u043b\u0438\u043d\u043e\u043c\u0438\u0430\u043b\u044c\u043d\u043e\u0435 \u0440\u0435\u0448\u0435\u043d\u0438\u0435, \u043a\u043e\u0440\u0440\u0435\u043a\u0442\u043d\u043e\u0441\u0442\u044c \u043a\u043e\u0442\u043e\u0440\u043e\u0433\u043e \u043c\u043e\u0436\u0435\u0442 \u0431\u044b\u0442\u044c \u043f\u0440\u043e\u0432\u0435\u0440\u0435\u043d\u0430 \u0437\u0430 \u043f\u043e\u043b\u0438\u043d\u043e\u043c\u0438\u0430\u043b\u044c\u043d\u043e\u0435 \u0432\u0440\u0435\u043c\u044f. \u0417\u0430\u043c\u0435\u0442\u0438\u043c, \u0447\u0442\u043e \u0434\u0430\u043d\u043d\u043e\u0435 \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u0435\u043d\u0438\u0435 \u043d\u0435\u0441\u0438\u043c\u043c\u0435\u0442\u0440\u0438\u0447\u043d\u043e \u043e\u0442\u043d\u043e\u0441\u0438\u0442\u0435\u043b\u044c\u043d\u043e \u0432\u043e\u043f\u0440\u043e\u0441\u0430, \u043a\u043e\u0433\u0434\u0430 \u044f\u0437\u044b\u043a \u041d\u0415 \u043f\u0440\u0438\u043d\u0430\u0434\u043b\u0435\u0436\u0438\u0442 NP \u0442.\u0435. \u0432\u043e\u043f\u0440\u043e\u0441 \u041d\u0415 \u043f\u0440\u0438\u043d\u0430\u0434\u043b\u0435\u0436\u0438\u0442 \u043b\u0438 \u044f\u0437\u044b\u043a NP \u2014 \u044d\u0442\u043e \u043e\u0442\u0434\u0435\u043b\u044c\u043d\u044b\u0439 \u043a\u043b\u0430\u0441\u0441.<\/p>\n<p>  \u0427\u0442\u043e \u0436\u0435 \u0437\u0430 \u043a\u043b\u0430\u0441\u0441 Co-NP? Co-NP \u2014 complement NP, \u0438\u043d\u0442\u0443\u0438\u0442\u0438\u0432\u043d\u043e, \u044d\u0442\u043e \u043a\u043b\u0430\u0441\u0441, \u0437\u0430\u0434\u0430\u0447\u0438 \u0432 \u043a\u043e\u0442\u043e\u0440\u043e\u043c \u044f\u0432\u043b\u044f\u044e\u0442\u0441\u044f \u043e\u0442\u0440\u0438\u0446\u0430\u043d\u0438\u0435\u043c \u0437\u0430\u0434\u0430\u0447 \u0432 NP. \u0415\u0441\u043b\u0438 SAT, \u0441\u043f\u0440\u0430\u0448\u0438\u0432\u0430\u0435\u0442, \u0435\u0441\u043b\u0438 \u043b\u0438 \u0442\u0430\u043a\u043e\u0435 \u043f\u0440\u0438\u0441\u0432\u0430\u0438\u0432\u0430\u043d\u0438\u0435 \u0438\u0441\u0442\u0438\u043d\u0430\/\u043b\u043e\u0436\u044c \u043f\u0435\u0440\u0435\u043c\u0435\u043d\u043d\u044b\u043c, \u0447\u0442\u043e \u0444\u043e\u0440\u043c\u0443\u043b\u0430 \u0432\u0435\u0440\u043d\u0430, \u0442\u043e UNSAT \u0441\u043f\u0440\u0430\u0448\u0438\u0432\u0430\u0435\u0442, \u0432\u0435\u0440\u043d\u043e \u043b\u0438, \u0447\u0442\u043e \u0434\u043b\u044f \u0412\u0421\u0415\u0425 \u043f\u0440\u0438\u0441\u0432\u0430\u0438\u0432\u0430\u043d\u0438\u0439 \u0444\u043e\u0440\u043c\u0443\u043b\u0430 \u043d\u0435\u0432\u0435\u0440\u043d\u0430? \u0422.\u0435. \u0438\u043d\u0430\u0447\u0435 \u0433\u043e\u0432\u043e\u0440\u044f, \u0432\u0435\u0440\u043d\u043e \u043b\u0438, \u0447\u0442\u043e \u0441\u0435\u0440\u0442\u0438\u0444\u0438\u043a\u0430\u0442\u0430 \u043d\u0435 \u0441\u0443\u0449\u0435\u0441\u0442\u0432\u0443\u0435\u0442.<br \/>  <img decoding=\"async\" src=\"http:\/\/habr.habrastorage.org\/post_images\/ae9\/4ab\/1f8\/ae94ab1f80ff160e00da943198e0a350.png\"\/><br \/>  \u0438\u043b\u0438 \u043f\u043e-\u0434\u0440\u0443\u0433\u043e\u043c\u0443 \u044d\u0442\u043e \u043c\u043e\u0436\u043d\u043e \u0441\u0444\u043e\u0440\u043c\u0443\u043b\u0438\u0440\u043e\u0432\u0430\u0442\u044c \u0441\u043b\u0435\u0434\u0443\u044e\u0449\u0438\u043c \u043e\u0431\u0440\u0430\u0437\u043e\u043c:<br \/>  NP \u2014 \u044d\u0442\u043e \u043a\u043e\u043b\u043b\u0435\u043a\u0446\u0438\u044f \u044f\u0437\u044b\u043a\u043e\u0432 \u0441 \u043a\u0440\u0430\u0442\u043a\u0438\u043c\u0438 \u0441\u0435\u0440\u0442\u0438\u0444\u0438\u043a\u0430\u0442\u0430\u043c\u0438, \u043f\u043e\u0434\u0442\u0432\u0435\u0440\u0436\u0434\u0430\u044e\u0449\u0438\u043c\u0438 \u043f\u0440\u0438\u043d\u0430\u0434\u043b\u0435\u0436\u043d\u043e\u0441\u0442\u044c<br \/>  Co-NP \u2014 \u044d\u0442\u043e \u043a\u043e\u043b\u043b\u0435\u043a\u0446\u0438\u044f \u044f\u0437\u044b\u043a\u043e\u0432 \u0441 \u043a\u0440\u0430\u0442\u043a\u0438\u043c\u0438 \u0441\u0435\u0440\u0442\u0438\u0444\u0438\u043a\u0430\u0442\u0430\u043c\u0438, \u043e\u0442\u0432\u0435\u0440\u0433\u0430\u044e\u0449\u0438\u043c\u0438 \u043f\u0440\u0438\u043d\u0430\u0434\u043b\u0435\u0436\u043d\u043e\u0441\u0442\u044c (= \u043d\u0435 \u0441\u0443\u0449 \u0441\u0435\u0440\u0442\u0438\u0444\u0438\u043a\u0430\u0442\u0430 \u043f\u0440\u0438\u043d\u0430\u0434\u043b\u0435\u0436\u043d\u043e\u0441\u0442\u0438) <\/p>\n<p>  \u0415\u0441\u043b\u0438 NP != Co-NP, \u0442\u043e \u043c\u043d\u043e\u0436\u0435\u0441\u0442\u0432\u043e NP-\u043f\u043e\u043b\u043d\u044b\u0445 \u0438 Co-NP-\u043f\u043e\u043b\u043d\u044b\u0445 \u0437\u0430\u0434\u0430\u0447 \u043d\u0435 \u043f\u0435\u0440\u0435\u0441\u0435\u043a\u0430\u0435\u0442\u0441\u044f (\u0441\u043b\u0435\u0434\u0441\u0442\u0432\u0438\u0435 <a href=\"http:\/\/www.villesalo.com\/OtEoDoSNPHL.pdf\">Mahaney&#8217;s theorem<\/a>).<\/p>\n<p>  \u041f\u043e\u0434\u0440\u043e\u0431\u043d\u0435\u0435 \u043e \u044f\u0437\u044b\u043a\u0430\u0445, \u043c\u0430\u0448\u0438\u043d\u0430\u0445 \u0422\u044c\u044e\u0440\u0438\u043d\u0433\u0430 \u0438 \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u0435\u043d\u0438\u044f\u0445 \u043a\u043b\u0430\u0441\u0441\u043e\u0432 \u0441\u043b\u043e\u0436\u043d\u043e\u0441\u0442\u0438 \u043c\u043e\u0436\u043d\u043e \u043f\u0440\u043e\u0447\u0438\u0442\u0430\u0442\u044c \u0432 \u041c.\u0413\u044d\u0440\u0438, \u0414.\u0414\u0436\u043e\u043d\u0441\u043e\u043d: \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 (\u043d\u0430\u043f\u0440\u0438\u043c\u0435\u0440, <a href=\"http:\/\/cs.usu.edu.ru\/hardness\/data\/books\/NP-Complectness.pdf\">\u0437\u0434\u0435\u0441\u044c<\/a>)<\/p>\n<p>  \u0421\u043e\u0433\u043b\u0430\u0441\u043d\u043e \u0441\u043e\u0432\u0440\u0435\u043c\u0435\u043d\u043d\u044b\u043c \u043f\u0440\u0435\u0434\u0441\u0442\u0430\u0432\u043b\u0435\u043d\u0438\u044f\u043c \u043e\u0442\u043d\u043e\u0448\u0435\u043d\u0438\u0435 \u043c\u0435\u0436\u0434\u0443 NP, Co-NP \u0438 P \u0432\u044b\u0433\u043b\u044f\u0434\u0438\u0442 \u0441\u043b\u0435\u0434\u0443\u044e\u0449\u0438\u043c \u043e\u0431\u0440\u0430\u0437\u043e\u043c:<br \/>  <img decoding=\"async\" src=\"http:\/\/habr.habrastorage.org\/post_images\/c6d\/423\/45a\/c6d42345ae61526e6f8c12bd87d1099d.gif\"\/><br \/>  (\u043a\u0430\u0440\u0442\u0438\u043d\u043a\u0430 \u0432\u0437\u044f\u0442\u0430 <a href=\"http:\/\/staff.ustc.edu.cn\/~csli\/graduate\/algorithms\/book6\/chap36.htm\">\u043e\u0442\u0441\u044e\u0434\u0430<\/a>)<br \/>  \u0411\u043e\u043b\u044c\u0448\u0438\u043d\u0441\u0442\u0432\u043e \u0441\u043a\u043b\u043e\u043d\u044f\u044e\u0442\u0441\u044f \u043a \u0432\u0430\u0440\u0438\u0430\u043d\u0442\u0443 (d), \u043d\u043e \u043d\u0435\u043a\u043e\u0442\u043e\u0440\u044b\u0435 \u0441\u0447\u0438\u0442\u0430\u044e\u0442, \u0447\u0442\u043e \u0432\u0435\u0440\u043e\u044f\u0442\u043d\u044b \u0438 \u0434\u0440\u0443\u0433\u0438\u0435 \u043e\u043f\u0446\u0438\u0438 e.g. \u041a\u043d\u0443\u0442 \u0432 \u0447\u0435\u0440\u043d\u043e\u0432\u0438\u043a\u0435 <a href=\"http:\/\/www-cs-faculty.stanford.edu\/~knuth\/fasc6a.ps.gz\">The Art of Programming 4, 6A: Satisfibility<\/a> \u2014 \u0441\u0442\u0440\u0430\u043d\u0438\u0446\u0430 1, \u0441\u043d\u043e\u0441\u043a\u0430 (*): &quot;\u2026 \u0430\u0432\u0442\u043e\u0440 \u0434\u0430\u043d\u043d\u043e\u0439 \u043a\u043d\u0438\u0433\u0438, \u043e\u0434\u043d\u0430\u043a\u043e, \u043f\u043e\u0434\u043e\u0437\u0440\u0435\u0432\u0430\u0435\u0442, \u0447\u0442\u043e \u043f\u043e\u043b\u0438\u043d\u043e\u043c\u0438\u0430\u043b\u044c\u043d\u044b\u0435 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u044b [\u0434\u043b\u044f SAT \u2014 \u043f\u0440\u0438\u043c. \u0430\u0432\u0442\u043e\u0440\u0430] \u0434\u0435\u0439\u0441\u0442\u0432\u0438\u0442\u0435\u043b\u044c\u043d\u043e \u0441\u0443\u0449\u0435\u0441\u0442\u0432\u0443\u044e\u0442, \u0442\u043e\u043b\u044c\u043a\u043e \u043e\u043d\u0438 \u043d\u0430\u043c \u0435\u0449\u0435 \u043d\u0435 \u0438\u0437\u0432\u0435\u0441\u0442\u043d\u044b&#8230;&quot;.<\/p>\n<h4>2+p-SAT \u043f\u043e\u043b\u0438\u043d\u043e\u043c\u0438\u0430\u043b\u0435\u043d? <\/h4>\n<p>  \u0412 \u043f\u0440\u0435\u0434\u044b\u0434\u0443\u0449\u0435\u0439 \u0441\u0442\u0430\u0442\u044c\u0435, \u0431\u044b\u043b\u043e \u043f\u043e\u043a\u0430\u0437\u0430\u043d\u043e, \u0447\u0442\u043e 2-SAT \u043f\u043e\u043b\u0438\u043d\u043e\u043c\u0438\u0430\u043b\u0435\u043d, \u0442.\u0435. \u0435\u0441\u043b\u0438 \u043c\u044b \u043e\u0433\u0440\u0430\u043d\u0438\u0447\u0438\u043c \u043a\u0430\u0436\u0434\u043e\u0435 \u043f\u0440\u0435\u0434\u043b\u043e\u0436\u0435\u043d\u0438\u0435 (clause) \u0434\u0432\u0443\u043c\u044f \u043f\u0435\u0440\u0435\u043c\u0435\u043d\u043d\u044b\u043c\u0438, \u0442\u043e \u0437\u0430\u0434\u0430\u0447\u0430 \u043c\u043e\u0436\u0435\u0442 \u0431\u044b\u0442\u044c \u0440\u0435\u0448\u0435\u043d\u0430 \u044d\u0444\u0444\u0435\u043a\u0442\u0438\u0432\u043d\u043e. \u0420\u0430\u0441\u0441\u043c\u043e\u0442\u0440\u0438\u043c \u0435\u0441\u0442\u0435\u0441\u0442\u0432\u0435\u043d\u043d\u043e\u0435 \u043e\u0431\u043e\u0431\u0449\u0435\u043d\u0438\u0435 \u044d\u0442\u043e\u0439 \u0437\u0430\u0434\u0430\u0447\u0438, \u0447\u0442\u043e \u0435\u0441\u043b\u0438 \u0443 \u043d\u0430\u0441 \u0442\u043e\u043b\u044c\u043a\u043e \u0447\u0430\u0441\u0442\u044c \u043f\u0440\u0435\u0434\u043b\u043e\u0436\u0435\u043d\u0438\u0439 \u0441\u043e\u0434\u0435\u0440\u0436\u0438\u0442 3 \u043f\u0435\u0440\u0435\u043c\u0435\u043d\u043d\u044b\u0435? <\/p>\n<p>  \u041f\u0443\u0441\u0442\u044c p \u2014 \u044d\u0442\u043e \u043a\u043e\u043b\u0438\u0447\u0435\u0441\u0442\u0432\u043e \u043f\u0440\u0435\u0434\u043b\u043e\u0436\u0435\u043d\u0438\u0439 \u0441 3\u043c\u044f \u043f\u0435\u0440\u0435\u043c\u0435\u043d\u043d\u044b\u043c\u0438 \u043a \u043e\u0431\u0449\u0435\u043c\u0443 \u043a\u043e\u043b\u0438\u0447\u0435\u0441\u0442\u0432\u0443 \u043f\u0440\u0435\u0434\u043b\u043e\u0436\u0435\u043d\u0438\u0439. \u0422\u043e\u0433\u0434\u0430 \u0437\u0430\u0434\u0430\u0447\u0430 2+p SAT \u2014 \u044d\u0442\u043e \u0437\u0430\u0434\u0430\u0447\u0430 3-SAT, \u0432 \u043a\u043e\u0442\u043e\u0440\u043e\u0439 \u0437\u0430\u0440\u0430\u043d\u0435\u0435 \u0437\u0430\u0444\u0438\u043a\u0441\u0438\u0440\u043e\u0432\u0430\u043d\u043e \u043a\u043e\u043b\u0438\u0447\u0435\u0441\u0442\u0432\u043e \u043f\u0440\u0435\u0434\u043b\u043e\u0436\u0435\u043d\u0438\u0439 \u0441 3\u043c\u044f \u043f\u0435\u0440\u0435\u043c\u0435\u043d\u043d\u044b\u043c\u0438 \u0442.\u0435. p, \u0441\u043e\u043e\u0442\u0432\u0435\u0442\u0441\u0442\u0432\u0435\u043d\u043d\u043e (1 \u2014 p) \u043f\u0440\u0435\u0434\u043b\u043e\u0436\u0435\u043d\u0438\u0439 \u0438\u043c\u0435\u044e\u0442 1 \u0438\u043b\u0438 2 \u043f\u0435\u0440\u0435\u043c\u0435\u043d\u043d\u044b\u0435.<\/p>\n<p>  \u0421 \u0442\u0435\u043e\u0440\u0435\u0442\u0438\u0447\u0435\u0441\u043a\u043e\u0439 \u0442\u043e\u0447\u043a\u0438 \u0437\u0440\u0435\u043d\u0438\u044f, \u0434\u0430\u0436\u0435 \u0435\u0441\u043b\u0438 p \u2014 \u044d\u0442\u043e <a href=\"http:\/\/habrahabr.ru\/post\/77553\/#comment_2259030\">\u043a\u043e\u043d\u0446\u0435\u043d\u0442\u0440\u0430\u0446\u0438\u044f \u0431\u0430\u0440\u0431\u0430\u0440\u0438\u0439\u0441\u043a\u043e\u0439 \u0443\u0442\u043a\u0438 \u0432 \u043e\u0446\u0438\u043b\u043b\u043e\u043a\u043e\u043a\u0446\u0438\u043d\u0443\u043c\u0435<\/a> \u0442.\u0435. \u043b\u044e\u0431\u043e\u0435 \u043f\u043e\u043b\u043e\u0436\u0438\u0442\u0435\u043b\u044c\u043d\u043e\u0435 \u0447\u0438\u0441\u043b\u043e, \u0442\u043e \u0437\u0430\u0434\u0430\u0447\u0430 NP \u043f\u043e\u043b\u043d\u0430, \u043e\u0434\u043d\u0430\u043a\u043e \u043d\u0430 \u043f\u0440\u0430\u043a\u0442\u0438\u043a\u0435 \u044d\u0442\u043e \u0432\u044b\u0433\u043b\u044f\u0434\u0438\u0442 \u0441\u043e\u0432\u0435\u0440\u0448\u0435\u043d\u043d\u043e \u0438\u043d\u0430\u0447\u0435.<br \/>  \u041f\u0443\u0441\u0442\u044c \u043f\u043e \u043e\u0441\u0438 X \u2014 \u043e\u0431\u0449\u0435\u0435 \u043a\u043e\u043b\u0438\u0447\u0435\u0441\u0442\u0432\u043e \u043f\u0435\u0440\u0435\u043c\u0435\u043d\u043d\u044b\u0445 \u0432 \u0444\u043e\u0440\u043c\u0443\u043b\u0435, \u043f\u043e \u043e\u0441\u0438 Y \u2014 \u00ab\u0432\u044b\u0447\u0438\u0441\u043b\u0438\u0442\u0435\u043b\u044c\u043d\u0430\u044f \u0441\u0442\u043e\u0438\u043c\u043e\u0441\u0442\u044c\u00bb \u0440\u0435\u0448\u0435\u043d\u0438\u044f \u0434\u043b\u044f \u0434\u0430\u043d\u043d\u043e\u0439 \u0444\u043e\u0440\u043c\u0443\u043b\u044b (\u043e\u0431\u044b\u0447\u043d\u043e \u044d\u0442\u043e \u043a\u043e\u043b\u0438\u0447\u0435\u0441\u0442\u0432\u043e \u0432\u044b\u0437\u043e\u0432\u043e\u0432\\\u0440\u0435\u0448\u0435\u043d\u0438\u0439 state-of-the-art \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u0430 SAT-solver, \u0441\u043c. \u043a\u0440\u0430\u0442\u043a\u043e\u0435 \u043e\u043f\u0438\u0441\u0430\u043d\u0438\u0435 DPLL \u0438 CDCL \u0432 \u043f\u0440\u0435\u0434\u044b\u0434\u0443\u0449\u0435\u0439 \u0441\u0442\u0430\u0442\u044c\u0435).<br \/>  <img decoding=\"async\" src=\"http:\/\/habr.habrastorage.org\/post_images\/1eb\/e5d\/217\/1ebe5d217426fe88de7877812a93b41e.png\"\/><br \/>  (\u0433\u0440\u0430\u0444\u0438\u043a \u0432\u0437\u044f\u0442 \u0438\u0437 \u0440\u0430\u0431\u043e\u0442\u044b <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>).<\/p>\n<p>  \u0415\u0441\u043b\u0438 p &lt;= 0.4, \u0442\u043e \u0437\u0430\u0434\u0430\u0447\u0430 \u043f\u043e\u043b\u0438\u043d\u043e\u043c\u0438\u0430\u043b\u044c\u043d\u0430, \u0434\u0430\u0436\u0435 \u0431\u043e\u043b\u0435\u0435 \u0442\u043e\u0433\u043e, \u043b\u0438\u043d\u0435\u0439\u043d\u0430 \u043f\u043e \u0432\u0445\u043e\u0434\u043d\u044b\u043c \u0434\u0430\u043d\u043d\u044b\u043c. \u0415\u0441\u043b\u0438 p &gt; 0.4, \u0442\u043e \u043c\u044b \u043d\u0430\u0431\u043b\u044e\u0434\u0430\u0435\u043c \u043f\u043e\u0432\u0435\u0434\u0435\u043d\u0438\u0435 \u0441\u0445\u043e\u0436\u0435\u0435 \u0441 \u043a\u043b\u0430\u0441\u0441\u0438\u0447\u0435\u0441\u043a\u0438\u043c 3-SAT. \u0414\u043b\u044f \u0442\u043e\u0433\u043e, \u0447\u0442\u043e\u0431\u044b \u043e\u0431\u044a\u044f\u0441\u043d\u0438\u0442\u044c \u0434\u0430\u043d\u043d\u044b\u0439 \u044d\u0444\u0444\u0435\u043a\u0442 \u0440\u0430\u0441\u0441\u043c\u043e\u0442\u0440\u0438\u043c \u043a\u043b\u0430\u0441\u0441\u0438\u0447\u0435\u0441\u043a\u0438\u0439 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c DPLL (\u0432\u0437\u044f\u0442\u043e \u0438\u0437 <a href=\"http:\/\/www.mpi-inf.mpg.de\/vtsa12\/slides\/biere\/Biere-VTSA12-talk.pdf\">\u0441\u043b\u0430\u0439\u0434\u043e\u0432<\/a> Armin Biere):<br \/>  <img decoding=\"async\" src=\"http:\/\/habr.habrastorage.org\/post_images\/b81\/9cd\/ac5\/b819cdac5953f819932c19764d451766.png\"\/><\/p>\n<p>  \u0420\u0430\u0441\u0441\u043c\u043e\u0442\u0440\u0438\u043c \u043f\u0440\u043e\u0441\u0442\u043e\u0439 \u043f\u0440\u0438\u043c\u0435\u0440<br \/>  <img decoding=\"async\" src=\"http:\/\/habr.habrastorage.org\/post_images\/d22\/779\/849\/d22779849604281eb583c4a66ebc1ff4.png\"\/><br \/>  \u041f\u0443\u0441\u0442\u044c \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c, \u0432\u044b\u0431\u0440\u0430\u043b x<sub>2<\/sub> = 1<br \/>  <img decoding=\"async\" src=\"http:\/\/habr.habrastorage.org\/post_images\/a04\/aa3\/60d\/a04aa360d3c5e934c8342d208d504d0b.png\"\/><br \/>  \u0422\u043e\u0433\u0434\u0430 \u0444\u043e\u0440\u043c\u0443\u043b\u0430 \u0443\u043f\u0440\u043e\u0449\u0430\u0435\u0442\u0441\u044f \u0438 \u0443 \u043d\u0430\u0441 \u0435\u0441\u0442\u044c \u0434\u0432\u0430 \u043f\u0440\u0435\u0434\u043b\u043e\u0436\u0435\u043d\u0438\u044f \u0441 \u0435\u0434\u0438\u043d\u0441\u0442\u0432\u0435\u043d\u043d\u043e\u0439 \u043f\u0435\u0440\u0435\u043c\u0435\u043d\u043d\u043e\u0439 \u2014 \u0437\u043d\u0430\u0447\u0438\u0442, boolean constraint propagation \u0432\u044b\u0431\u0438\u0440\u0430\u0435\u0442 \u043e\u0434\u0438\u043d \u0438\u0437 \u043d\u0438\u0445, \u043d\u0430\u043f\u0440\u0438\u043c\u0435\u0440 x<sub>3<\/sub> \u0438 \u043f\u0440\u0438\u0441\u0432\u0430\u0438\u0432\u0430\u0435\u0442 \u0435\u0434\u0438\u043d\u0441\u0442\u0432\u0435\u043d\u043d\u043e\u0435 \u0434\u043e\u0441\u0442\u0443\u043f\u043d\u043e\u0435 \u0435\u043c\u0443 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0435<br \/>  <img decoding=\"async\" src=\"http:\/\/habr.habrastorage.org\/post_images\/1ee\/c36\/0ee\/1eec360ee8671ceb094863d35376346c.png\"\/><br \/>  \u043f\u043e\u0441\u043b\u0435 \u043f\u0440\u0438\u0441\u0432\u0430\u0438\u0432\u0430\u043d\u0438\u044f x<sub>3<\/sub>=1, BCP \u0441\u043d\u043e\u0432\u0430 \u043d\u0430\u0445\u043e\u0434\u0438\u0442 \u043f\u0440\u0435\u0434\u043b\u043e\u0436\u0435\u043d\u0438\u0435 \u0441 \u0435\u0434\u0438\u043d\u0441\u0442\u0432\u0435\u043d\u043d\u043e\u0439 \u043f\u0435\u0440\u0435\u043c\u0435\u043d\u043d\u043e\u0439 x<sub>1<\/sub>, \u0438 \u043f\u0440\u0438\u0441\u0432\u0430\u0438\u0432\u0430\u0435\u0442 x<sub>1<\/sub>=1<br \/>  <img decoding=\"async\" src=\"http:\/\/habr.habrastorage.org\/post_images\/853\/6a2\/dff\/8536a2dffddd5b9db8de1f35276403fb.png\"\/><br \/>  \u0422\u0430\u043a\u0438\u043c \u043e\u0431\u0440\u0430\u0437\u043e\u043c, \u043f\u043e\u0441\u043b\u0435 \u0435\u0434\u0438\u043d\u0441\u0442\u0432\u0435\u043d\u043d\u043e\u0433\u043e \u0440\u0435\u0448\u0435\u043d\u0438\u044f SAT solver, boolean constraint propagation \u043f\u043e\u0437\u0432\u043e\u043b\u044f\u0435\u0442 \u043d\u0430\u0439\u0442\u0438 \u0440\u0435\u0448\u0435\u043d\u0438\u0435 \u0432\u0441\u0435\u0439 \u0444\u043e\u0440\u043c\u0443\u043b\u044b. \u041f\u0440\u043e\u0438\u0441\u0445\u043e\u0434\u0438\u0442 \u044d\u0442\u043e \u043f\u0440\u0435\u0436\u0434\u0435 \u0432\u0441\u0435\u0433\u043e \u043f\u043e\u0442\u043e\u043c\u0443, \u0447\u0442\u043e \u0440\u0435\u0448\u0435\u043d\u0438\u0435 \u043d\u0430 \u043f\u0435\u0440\u0435\u043c\u0435\u043d\u043d\u0443\u044e \u0432 \u043f\u0440\u0435\u0434\u043b\u043e\u0436\u0435\u043d\u0438\u0438 \u0441 \u0434\u0432\u0443\u043c\u044f \u043f\u0435\u0440\u0435\u043c\u0435\u043d\u043d\u044b\u043c\u0438, \u0444\u0430\u043a\u0442\u0438\u0447\u0435\u0441\u043a\u0438 \u043e\u0434\u043d\u043e\u0437\u043d\u0430\u0447\u043d\u043e \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u044f\u0435\u0442 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0435 \u0435\u0449\u0435 \u043e\u0434\u043d\u043e\u0439 \u043f\u0435\u0440\u0435\u043c\u0435\u043d\u043d\u043e\u0439, \u0447\u0442\u043e \u0432\u044b\u0437\u044b\u0432\u0430\u0435\u0442 \u0446\u0435\u043b\u044b\u0439 \u043a\u0430\u0441\u043a\u0430\u0434 \u043f\u0440\u0438\u0441\u0432\u0430\u0438\u0432\u0430\u043d\u0438\u0439 \u0438 BCP \u044d\u0444\u0444\u0435\u043a\u0442\u0438\u0432\u043d\u043e \u0443\u043c\u0435\u043d\u044c\u0448\u0430\u0435\u0442 \u0444\u043e\u0440\u043c\u0443\u043b\u0443. \u0415\u0441\u043b\u0438 \u043f\u043e\u0434\u043e\u0431\u043d\u044b\u0439 \u043a\u0430\u0441\u043a\u0430\u0434 \u043f\u043e\u043a\u0440\u044b\u0432\u0430\u0435\u0442 \u0434\u043e\u0441\u0442\u0430\u0442\u043e\u0447\u043d\u043e\u0435 \u043a\u043e\u043b\u0438\u0447\u0435\u0441\u0442\u0432\u043e \u043f\u0435\u0440\u0435\u043c\u0435\u043d\u043d\u044b\u0445 \u0432 \u0444\u043e\u0440\u043c\u0443\u043b\u0435, \u0442\u043e \u0440\u0435\u0448\u0435\u043d\u0438\u0435 \u044f\u0432\u043b\u044f\u0435\u0442\u0441\u044f \u043b\u0438\u043d\u0435\u0439\u043d\u044b\u043c.<\/p>\n<h4>\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 <\/h4>\n<p>  \u0415\u0449\u0435 \u043e\u0434\u043d\u0430 \u0438\u043d\u0442\u0435\u0440\u0435\u0441\u043d\u0430\u044f \u0437\u0430\u0432\u0438\u0441\u0438\u043c\u043e\u0441\u0442\u044c \u044d\u0442\u043e \u0442\u0430\u043a \u043d\u0430\u0437\u044b\u0432\u0430\u0435\u043c\u0430\u044f clause-variable-ratio: \u0441\u043e\u043e\u0442\u043d\u043e\u0448\u0435\u043d\u0438\u0435 \u0447\u0438\u0441\u043b\u0430 \u043f\u0440\u0435\u0434\u043b\u043e\u0436\u0435\u043d\u0438\u0439 \u043a \u0447\u0438\u0441\u043b\u0443 \u043f\u0435\u0440\u0435\u043c\u0435\u043d\u043d\u044b\u0445. \u0418\u043d\u0442\u0443\u0438\u0442\u0438\u0432\u043d\u043e, \u0447\u0435\u043c \u0431\u043e\u043b\u044c\u0448\u0435 \u043f\u0440\u0435\u0434\u043b\u043e\u0436\u0435\u043d\u0438\u0439, \u0442\u0435\u043c \u0431\u043e\u043b\u044c\u0448\u0435 \u043e\u0433\u0440\u0430\u043d\u0438\u0447\u0435\u043d\u0438\u0439, \u0442\u0435\u043c \u0432\u0435\u0440\u043e\u044f\u0442\u043d\u0435\u0435, \u0447\u0442\u043e \u0444\u043e\u0440\u043c\u0443\u043b\u044b \u043d\u0435\u0432\u044b\u043f\u043e\u043b\u043d\u0438\u043c\u0430 \u2014 \u0441\u043b\u0438\u0448\u043a\u043e\u043c \u043c\u043d\u043e\u0433\u043e \u043e\u0433\u0440\u0430\u043d\u0438\u0447\u0435\u043d\u0438\u0439. \u041f\u0440\u043e \u0442\u0430\u043a\u0443\u044e \u043f\u0440\u043e\u0431\u043b\u0435\u043c\u0443 \u0433\u043e\u0432\u043e\u0440\u044f\u0442, \u0447\u0442\u043e \u043e\u043d\u0430 overconstrainted. \u0415\u0441\u043b\u0438 \u0436\u0435 \u043f\u0440\u0435\u0434\u043b\u043e\u0436\u0435\u043d\u0438\u0439 \u043c\u0430\u043b\u043e, \u0430 \u043f\u0435\u0440\u0435\u043c\u0435\u043d\u043d\u044b\u0445 \u043c\u043d\u043e\u0433\u043e, \u0442\u043e \u0437\u043d\u0430\u0447\u0438\u0442, \u0447\u0442\u043e \u0441\u0442\u0435\u043f\u0435\u043d\u0435\u0439 \u0441\u0432\u043e\u0431\u043e\u0434\u044b \u043c\u043d\u043e\u0433\u043e, \u0430 \u043e\u0433\u0440\u0430\u043d\u0438\u0447\u0435\u043d\u0438\u0439 \u043c\u0430\u043b\u043e. \u042d\u0442\u043e \u043f\u043e\u0437\u0432\u043e\u043b\u044f\u0435\u0442 \u043b\u0435\u0433\u043a\u043e \u043d\u0430\u0439\u0442\u0438 \u0440\u0435\u0448\u0435\u043d\u0438\u0435, \u0438 \u0432\u0435\u0440\u043e\u044f\u0442\u043d\u043e, \u0447\u0442\u043e \u0444\u043e\u0440\u043c\u0443\u043b\u0430 \u0432\u044b\u043f\u043e\u043b\u043d\u0438\u043c\u0430. \u041f\u0440\u043e \u043d\u0435\u0451 \u0433\u043e\u0432\u043e\u0440\u044f\u0442, \u0447\u0442\u043e \u043e\u043d\u0430 underconstrained.<\/p>\n<p>  \u0422\u0430\u043a \u043a\u0430\u043a \u043c\u044b \u0443\u0436\u0435 \u0440\u0430\u0441\u0441\u043c\u043e\u0442\u0440\u0435\u043b\u0438 2+p SAT, \u0442\u043e \u0431\u044b\u043b\u043e \u0431\u044b \u0442\u0430\u043a\u0436\u0435 \u0438\u043d\u0442\u0435\u0440\u0435\u0441\u043d\u043e \u0443\u0447\u0435\u0441\u0442\u044c \u043f\u0430\u0440\u0430\u043c\u0435\u0442\u0440 p \u0432 \u0434\u0430\u043d\u043d\u043e\u0439 \u0437\u0430\u0432\u0438\u0441\u0438\u043c\u043e\u0441\u0442\u0438, \u043a\u0430\u043a \u0441\u0442\u0435\u043f\u0435\u043d\u044c \u00ab\u043b\u0438\u043d\u0435\u0439\u043d\u043e\u0441\u0442\u0438\u00bb \u043f\u0440\u043e\u0431\u043b\u0435\u043c\u044b, \u0447\u0435\u043c \u0431\u043e\u043b\u044c\u0448\u0435 p, \u0442\u0435\u043c \u043c\u0435\u043d\u0435\u0435 \u044d\u0444\u0444\u0435\u043a\u0442\u0438\u0432\u0435\u043d boolean constraint propagation \u0438 \u0442\u0435\u043c \u0441\u043b\u043e\u0436\u043d\u0435\u0435 \u043d\u0430\u0439\u0442\u0438 \u0440\u0435\u0448\u0435\u043d\u0438\u0435.<\/p>\n<p>  <b>SAT\/UNSAT \u043f\u0435\u0440\u0435\u0445\u043e\u0434 \u0434\u043b\u044f 2+p SAT<\/b><br \/>  <img decoding=\"async\" src=\"http:\/\/habr.habrastorage.org\/post_images\/155\/fa4\/e27\/155fa4e27640c8fd4388ea03eab81883.png\"\/><br \/>  \u0413\u0440\u0430\u0444\u0438\u043a \u0438\u0437 \u0441\u0442\u0430\u0442\u044c\u0438 Nature: <a href=\"http:\/\/www.cs.cornell.edu\/selman\/papers\/pdf\/99.nature.phase.pdf\u200e\"> Determining computational complexity from characteristic `phase transitions&#8217; <\/a>by Remi Monasson, Riccardo Zecchina, Scott Kirkpatrick, Bart Selman and Lidror Troyanskyk<\/p>\n<p>  \u041d\u0430 \u0441\u0430\u043c\u043e\u043c \u0434\u0435\u043b\u0435, \u044d\u0442\u043e\u0442 \u0433\u0440\u0430\u0444\u0438\u043a \u0434\u0430\u0451\u0442 \u043d\u0430\u043c \u043d\u0435\u0447\u0442\u043e \u0431\u043e\u043b\u044c\u0448\u0435\u0435, \u0447\u0435\u043c \u043c\u044b \u0434\u0443\u043c\u0430\u0435\u043c: \u043e\u043d \u043f\u043e\u0437\u0432\u043e\u043b\u044f\u0435\u0442 \u0433\u0435\u043d\u0435\u0440\u0438\u0440\u043e\u0432\u0430\u0442\u044c \u00ab\u0441\u043b\u043e\u0436\u043d\u044b\u0435\u00bb \u0441\u043b\u0443\u0447\u0430\u0439\u043d\u044b\u0435 \u0444\u043e\u0440\u043c\u0443\u043b\u044b. \u0415\u0441\u043b\u0438 \u0444\u043e\u0440\u043c\u0443\u043b\u0430 \u043d\u0430\u0445\u043e\u0434\u0438\u0442\u0441\u044f \u0433\u0434\u0435-\u0442\u043e \u0432 \u0446\u0435\u043d\u0442\u0440\u0435 \u043c\u0435\u0436\u0434\u0443 SAT \u0438 UNSAT, \u044d\u0442\u043e \u0437\u043d\u0430\u0447\u0438\u0442, \u0447\u0442\u043e \u0434\u043b\u044f \u043d\u0435\u0451 \u0441\u043b\u043e\u0436\u043d\u043e \u043d\u0430\u0439\u0442\u0438 \u043c\u043e\u0434\u0435\u043b\u044c \u0438 \u0441\u043b\u043e\u0436\u043d\u043e \u0441\u0433\u0435\u043d\u0435\u0440\u0438\u0440\u043e\u0432\u0430\u0442\u044c \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u043e \u043d\u0435\u0432\u044b\u043f\u043e\u043b\u043d\u0438\u043c\u043e\u0441\u0442\u0438.<br \/>  \u0417\u0430\u0432\u0438\u0441\u0438\u043c\u043e\u0441\u0442\u044c \u0447\u0438\u0441\u043b\u0430 \u0432\u044b\u0437\u043e\u0432\u043e\u0432 DPLL \u043e\u0442 \u043f\u043e\u0437\u0438\u0446\u0438\u0438 SAT\/UNSAT \u043f\u0435\u0440\u0435\u0445\u043e\u0434\u0430 \u0438\u043c\u0435\u0435\u0442 \u0441\u043b\u0435\u0434\u0443\u044e\u0449\u0438\u0439 \u0432\u0438\u0434 <br \/>  <img decoding=\"async\" src=\"http:\/\/habr.habrastorage.org\/post_images\/878\/9ec\/460\/8789ec460500f47b46b5db8aff3cca18.png\"\/><br \/>  \u0413\u0440\u0430\u0444\u0438\u043a \u0438\u0437 \u0441\u0442\u0430\u0442\u044c\u0438 <a href=\"https:\/\/www.cs.toronto.edu\/~sacook\/homepage\/SAT.ps\">Finding Hard Instances of the Satis ability Problem: A Survey<\/a> by S. Cook, D. Mitchell<\/p>\n<h4>\u041e \u0441\u043e\u0432\u0440\u0435\u043c\u0435\u043d\u043d\u044b\u0445 SAT solver&#8217;\u0430\u0445<\/h4>\n<p>  \u0414\u0430\u0436\u0435 \u043d\u0430 \u043e\u043f\u0438\u0441\u0430\u043d\u0438\u0435 \u043e\u0441\u043d\u043e\u0432\u043d\u044b\u0445 \u043f\u0440\u0438\u043d\u0446\u0438\u043f\u043e\u0432, \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u043e\u0432 \u0438 \u044d\u0432\u0440\u0438\u0441\u0442\u0438\u043a \u0443\u0439\u0434\u0435\u0442 \u043d\u0435 \u043e\u0434\u043d\u0430 \u0441\u043e\u0442\u043d\u044f \u0441\u0442\u0440\u0430\u043d\u0438\u0446, \u043f\u043e\u044d\u0442\u043e\u043c\u0443 \u043e\u0433\u0440\u0430\u043d\u0438\u0447\u0438\u043c\u0441\u044f \u043e\u0434\u043d\u0438\u043c \u0438\u0437 \u043e\u043f\u0438\u0441\u0430\u043d\u0438\u0435\u043c \u043e\u0434\u043d\u043e\u0433\u043e \u0438\u0437 \u0441\u0430\u043c\u044b\u0445 \u043f\u043e\u043f\u0443\u043b\u044f\u0440\u043d\u044b\u0445 \u0438 \u043a\u043b\u044e\u0447\u0435\u0432\u044b\u0445 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u043e\u0432 SAT: CDCL \u2014 Conflict Driven Clause Learning. \u041a\u0430\u043a \u0441\u043b\u0435\u0434\u0443\u0435\u0442 \u0438\u0437 \u043d\u0430\u0437\u0432\u0430\u043d\u0438\u044f \u043e\u0434\u043d\u0430 \u0438\u0437 \u0433\u043b\u0430\u0432\u043d\u044b\u0445 \u043e\u0441\u043e\u0431\u0435\u043d\u043d\u043e\u0441\u0442\u0435\u0439 \u044d\u0442\u043e\u0433\u043e \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u0430 \u2014 \u044d\u0442\u043e \u0441\u043f\u043e\u0441\u043e\u0431\u043d\u043e\u0441\u0442\u044c \u0437\u0430\u043f\u043e\u043c\u0438\u043d\u0430\u0442\u044c \u0440\u0435\u0448\u0435\u043d\u0438\u044f, \u043a\u043e\u0442\u043e\u0440\u044b\u0435 \u043d\u0435 \u0432\u0435\u0434\u0443\u0442 \u043a \u0440\u0435\u0448\u0435\u043d\u0438\u044e, \u0430 \u0438\u043c\u0435\u043d\u043d\u043e \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c \u0437\u0430\u043f\u043e\u043c\u0438\u043d\u0430\u0435\u0442 \u0438\u0445 \u0432 \u0432\u0438\u0434\u0435 \u043f\u0440\u0435\u0434\u043b\u043e\u0436\u0435\u043d\u0438\u0439. \u0415\u0441\u043b\u0438 \u043c\u044b \u043f\u0440\u0438\u043d\u044f\u043b\u0438 \u0440\u0435\u0448\u0435\u043d\u0438\u044f x<sub>1<\/sub> = 1, x<sub>2<\/sub> = 2, x<sub>3<\/sub> = 1 \u0438 \u044d\u0442\u043e \u0432\u0435\u0434\u0435\u0442 \u043a \u043a\u043e\u043d\u0444\u043b\u0438\u043a\u0442\u0443, \u0442\u043e CDCL \u0437\u0430\u043f\u043e\u043c\u043d\u0438\u0442 \u043e\u0442\u0440\u0438\u0446\u0430\u043d\u0438\u0435 \u043a\u043e\u043d\u0444\u043b\u0438\u043a\u0442\u043d\u043e\u0439 \u043a\u043e\u043c\u0431\u0438\u043d\u0430\u0446\u0438\u0438.<br \/>  <img decoding=\"async\" src=\"http:\/\/habr.habrastorage.org\/post_images\/eee\/03f\/bc9\/eee03fbc993d1a56c02e3d77b268e73c.png\"\/><br \/>  \u043f\u043e \u043f\u0440\u0430\u0432\u0438\u043b\u0443 \u0414\u0435 \u041c\u043e\u0440\u0433\u0430\u043d\u0430 \u043f\u0440\u0438\u0432\u043e\u0434\u0438\u043c \u043a CNF \u0432\u0438\u0434\u0443<br \/>  <img decoding=\"async\" src=\"http:\/\/habr.habrastorage.org\/post_images\/7d9\/b3d\/bf5\/7d9b3dbf5949496b98f5bce1d24066b2.png\"\/><br \/>  \u0438 \u0434\u043e\u0431\u0430\u0432\u043b\u044f\u0435\u043c \u0435\u0433\u043e \u043a \u0444\u043e\u0440\u043c\u0443\u043b\u0435 <br \/>  <img decoding=\"async\" src=\"http:\/\/habr.habrastorage.org\/post_images\/d94\/1be\/3af\/d941be3af47ac7c92fdd5b29b693e357.png\"\/><\/p>\n<p>  \u0422\u0430\u043a\u0438\u043c \u043e\u0431\u0440\u0430\u0437\u043e\u043c \u0434\u0432\u0435 \u043a\u043b\u044e\u0447\u0435\u0432\u044b\u0435 \u0441\u043e\u0441\u0442\u0430\u0432\u043b\u044f\u044e\u0449\u0438\u0435 CDCL: \u0433\u0440\u0430\u0444 \u0438\u043c\u043f\u043b\u0438\u043a\u0430\u0446\u0438\u0439 \u0432\u043c\u0435\u0441\u0442\u0435 \u0441\u043e \u0441\u0442\u0435\u043a\u043e\u043c \u043f\u0440\u0438\u043d\u044f\u0442\u044b\u0445 \u0440\u0435\u0448\u0435\u043d\u0438\u0439 \u0438 \u0440\u0430\u0431\u043e\u0442\u0430 \u0441 \u043a\u043e\u043d\u0444\u043b\u0438\u043a\u0442\u043d\u044b\u043c\u0438 \u043a\u043e\u043c\u0431\u0438\u043d\u0430\u0446\u0438\u044f\u043c\u0438. \u041a\u0430\u043a \u043f\u0440\u0430\u0432\u0438\u043b\u043e, \u043f\u043e\u0441\u043b\u0435 \u043f\u0440\u0438\u043d\u044f\u0442\u0438\u044f \u0440\u0435\u0448\u0435\u043d\u0438\u044f, \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c \u043f\u0440\u043e\u0432\u043e\u0434\u0438\u0442 \u0432\u0441\u0435 \u0432\u043e\u0437\u043c\u043e\u0436\u043d\u044b\u0435 \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 \u0438 \u043f\u0440\u0438\u0445\u043e\u0434\u0438\u0442 \u043a \u043a\u043e\u043d\u0444\u043b\u0438\u043a\u0442\u0443. \u0413\u0440\u0430\u0444 \u0438\u043c\u043f\u043b\u0438\u043a\u0430\u0446\u0438\u0439 \u0438 \u0441\u0442\u0435\u043a \u0440\u0435\u0448\u0435\u043d\u0438\u0439, \u043f\u043e\u043a\u0430\u0437\u044b\u0432\u0430\u044e\u0442, \u043a\u0430\u043a\u0430\u044f \u043a\u043e\u043c\u0431\u0438\u043d\u0430\u0446\u0438\u044f \u0438 \u0440\u0435\u0448\u0435\u043d\u0438\u0435 \u043d\u0430 \u043a\u0430\u043a\u043e\u043c \u044d\u0442\u0430\u043f\u0435 \u043f\u0440\u0438\u0432\u0435\u043b\u043e \u043a \u043a\u043e\u043d\u0444\u043b\u0438\u043a\u0442\u0443, \u043d\u0430 \u043e\u0441\u043d\u043e\u0432\u0435 \u044d\u0442\u043e\u0433\u043e \u043f\u0440\u043e\u0438\u0441\u0445\u043e\u0434\u0438\u0442 \u0433\u0435\u043d\u0435\u0440\u0430\u0446\u0438\u044f \u043a\u043e\u043d\u0444\u043b\u0438\u043a\u0442\u043d\u043e\u0433\u043e \u043f\u0440\u0435\u0434\u043b\u043e\u0436\u0435\u043d\u0438\u044f \u2014 \u043e\u0442\u0441\u044e\u0434\u0430 \u0438 \u043d\u0430\u0437\u0432\u0430\u043d\u0438\u0435 Conflict Driven Clause Learning, \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c \u044d\u0444\u0444\u0435\u043a\u0442\u0438\u0432\u043d\u043e \u043d\u0430\u0445\u043e\u0434\u0438\u0442 \u043a\u043e\u043d\u0444\u043b\u0438\u043a\u0442\u043d\u044b\u0435 \u043a\u043e\u043c\u0431\u0438\u043d\u0430\u0446\u0438\u0438, \u0432\u044b\u0443\u0447\u0438\u0432\u0430\u0435\u0442 \u0438\u0445 \u0438 \u043f\u0440\u0438\u043d\u0438\u043c\u0430\u0435\u0442 \u0440\u0435\u0448\u0435\u043d\u0438\u044f, \u0443\u0447\u0438\u0442\u044b\u0432\u0430\u044f \u043a\u043e\u043d\u0444\u043b\u0438\u043a\u0442\u043d\u044b\u0435 \u043a\u043e\u043c\u0431\u0438\u043d\u0430\u0446\u0438\u0438.<\/p>\n<p>  \u041f\u043e\u0434\u0440\u043e\u0431\u043d\u0435\u0435 \u0440\u0430\u0441\u0441\u043c\u043e\u0442\u0440\u0438\u043c \u043f\u0440\u0438\u043c\u0435\u0440 \u0440\u0430\u0431\u043e\u0442\u044b CDCL \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u0430:  <\/p>\n<div class=\"slideshow\"><iframe loading=\"lazy\" src=\"http:\/\/www.slideshare.net\/slideshow\/embed_code\/14412470\" width=\"425\" height=\"355\" frameborder=\"0\" marginwidth=\"0\" marginheight=\"0\" scrolling=\"no\"><\/iframe><\/div>\n<p>    from <strong><a href=\"http:\/\/www.slideshare.net\/sakai\">Masahiro Sakai<\/a> <\/strong><\/p>\n<p>  \u041f\u043e\u0434\u0440\u043e\u0431\u043d\u0435\u0435 \u043e CDCL \u043d\u0430\u043f\u0438\u0441\u0430\u043d\u043e \u0432 \u0441\u043b\u0435\u0434\u0443\u044e\u0449\u0438\u0445 \u0440\u0430\u0431\u043e\u0442\u0430\u0445:<br \/>  Handbook of Satis\ufb01ability: <a href=\"https:\/\/www.enseignement.polytechnique.fr\/informatique\/INF321\/TD-12_13\/TD910\/files\/SATHandbook-CDCL.pdf\">Chapter 4. Con\ufb02ict-Driven Clause Learning SAT Solvers by Joao Marques-Silva, Ines Lynce and Sharad Malik<\/a><br \/>  SAT\/SMT Summer School 2013 \u0441\u043b\u0430\u0439\u0434\u044b \u0430\u0432\u0442\u043e\u0440\u0430 CDCL: <a href=\"http:\/\/satsmt2013.ics.aalto.fi\/slides\/Marques-Silva.pdf\">CDCL SAT Solvers &#038; SAT-Based Problem Solving<\/a><br \/>  \u0414\u0435\u0442\u0430\u043b\u044c\u043d\u043e\u0435 \u0438 \u0434\u043e\u0441\u0442\u0430\u0442\u043e\u0447\u043d\u043e\u0435 \u0442\u0435\u0445\u043d\u0438\u0447\u0435\u0441\u043a\u043e\u0435 \u043e\u043f\u0438\u0441\u0430\u043d\u0438\u0435 \u0440\u0430\u0431\u043e\u0442\u044b \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u0430 \u0438 \u0432\u043d\u0443\u0442\u0440\u0435\u043d\u043d\u0438\u0445 \u0441\u0442\u0440\u0443\u043a\u0442\u0443\u0440: <a href=\"http:\/\/www.cs.utexas.edu\/~hunt\/class\/2013-spring\/cs395t\/slides\/austin_CDCL.pdf\">Practical SAT Solving: Con\ufb02ict-driven SAT solvers<\/a><\/p>\n<h4>\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? <\/h4>\n<p>  \u0412\u043e-\u043f\u0435\u0440\u0432\u044b\u0445, \u043d\u0443\u0436\u043d\u043e \u043e\u0442\u0432\u0435\u0442\u0438\u0442\u044c \u043d\u0430 \u0440\u044f\u0434 \u0432\u043e\u043f\u0440\u043e\u0441\u043e\u0432 \u043d\u0430 \u0441\u043e\u043e\u0442\u0432\u0435\u0442\u0441\u0442\u0432\u0438\u0435 \u0440\u0435\u0448\u0435\u043d\u0438\u044f \u0437\u0434\u0440\u0430\u0432\u043e\u043c\u0443 \u0441\u043c\u044b\u0441\u043b\u0443  <\/p>\n<ol>\n<li> \u041c\u043e\u0436\u0435\u0442 \u043b\u0438 \u0440\u0430\u0431\u043e\u0442\u0430 \u043e\u0431\u044a\u044f\u0441\u043d\u0438\u0442\u044c \u043f\u043e\u0447\u0435\u043c\u0443 \u0434\u0440\u0443\u0433\u0438\u0435 \u043f\u043e\u043f\u044b\u0442\u043a\u0438 \u0440\u0435\u0448\u0438\u0442\u044c \u0437\u0430\u0434\u0430\u0447\u0443 \u043f\u0440\u043e\u0432\u0430\u043b\u0438\u043b\u0438\u0441\u044c, \u0430 \u043d\u0430\u0448\u0430 \u0440\u0430\u0431\u043e\u0442\u0430 \u043d\u0435\u0442<\/li>\n<li> \u041a\u0430\u043a \u0434\u0430\u043d\u043d\u0430\u044f \u0440\u0430\u0431\u043e\u0442\u0430 \u043e\u0431\u0445\u043e\u0434\u0438\u0442 \u0442\u0435\u043e\u0440\u0435\u043c\u044b \u043e \u043d\u0435\u0432\u044b\u0440\u0430\u0437\u0438\u043c\u043e\u0441\u0442\u0438 \u0442.\u0435. \u044f\u0432\u043d\u043e \u043f\u043e\u043a\u0430\u0437\u0430\u0442\u044c, \u0447\u0442\u043e \u0434\u0430\u043d\u043d\u044b\u0435 \u0442\u0435\u043e\u0440\u0435\u043c\u044b (e.g. Baker-Gill-Solovay theorem) \u043a \u0434\u0430\u043d\u043d\u043e\u0439 \u0440\u0430\u0431\u043e\u0442\u0435 \u043d\u0435 \u043f\u0440\u0438\u043c\u0435\u043d\u0438\u043c\u044b <\/li>\n<li> \u0415\u0441\u043b\u0438 P = NP \u0438 \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u043e \u043a\u043e\u043d\u0441\u0442\u0440\u0443\u043a\u0442\u0438\u0432\u043d\u043e, \u0442\u043e \u043e\u0431\u044f\u0437\u0430\u0442\u0435\u043b\u0435\u043d \u043f\u0440\u043e\u0442\u043e\u0442\u0438\u043f, \u0438\u043d\u0430\u0447\u0435 \u043d\u0438\u043a\u0442\u043e \u043d\u0435 \u043f\u043e\u0432\u0435\u0440\u0438\u0442 \u0432 \u0440\u0435\u0448\u0435\u043d\u0438\u0435<\/li>\n<li> \u0420\u0430\u0431\u043e\u0442\u0430 \u0441\u0430\u043c\u043e\u0434\u043e\u0441\u0442\u0430\u0442\u043e\u0447\u043d\u0430 \u0438 \u0434\u043e\u0441\u0442\u0443\u043f\u043d\u0430 \u044d\u043a\u0441\u043f\u0435\u0440\u0442\u0443 \u0434\u043b\u044f \u043f\u043e\u043d\u0438\u043c\u0430\u043d\u0438\u044f \u0442.\u0435. \u043e\u043d\u0430 \u0441\u043e\u0434\u0435\u0440\u0436\u0438\u0442 \u0432\u0441\u0435 \u043d\u0435\u043e\u0431\u0445\u043e\u0434\u0438\u043c\u044b\u0435 \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u0435\u043d\u0438\u044f, \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u0430 \u0432 \u0440\u0430\u0437\u0432\u0435\u0440\u043d\u0443\u0442\u043e\u043c \u0432\u0438\u0434\u0435 (\u0437\u0430\u0434\u0430\u0447\u0430 \u0442\u044b\u0441\u044f\u0447\u0435\u043b\u0435\u0442\u0438\u044f, \u043d\u0430\u043f\u0438\u0441\u0430\u043d\u043d\u0430\u044f \u043d\u0430 3\u0445 \u0441\u0442\u0440\u0430\u043d\u0438\u0446\u0430\u0445 \u0438\u0435\u0440\u043e\u0433\u043b\u0438\u0444\u0430\u043c\u0438 \u0438 \u043d\u0435\u0434\u043e\u0441\u0442\u0443\u043f\u043d\u044b\u043c \u044f\u0437\u044b\u043a\u043e\u043c, \u0432\u044b\u0437\u044b\u0432\u0430\u0435\u0442 \u043f\u043e\u0434\u043e\u0437\u0440\u0435\u043d\u0438\u0435 \u0438 \u0436\u0435\u043b\u0430\u043d\u0438\u0435 \u0443 \u043f\u0440\u043e\u0432\u0435\u0440\u044f\u044e\u0449\u0435\u0433\u043e \u043e\u0442\u0440\u0430\u0432\u0438\u0442\u044c \u0435\u0451 \u0432 \u043a\u043e\u0440\u0437\u0438\u043d\u0443 )<\/li>\n<li> \u0410\u0432\u0442\u043e\u0440\u044b \u043e\u0431\u043b\u0430\u0434\u0430\u044e\u0442 \u0445\u043e\u0440\u043e\u0448\u0438\u043c \u043f\u043e\u043d\u0438\u043c\u0430\u043d\u0438\u0435\u043c \u0442\u0435\u043e\u0440\u0438\u0438 \u0441\u043b\u043e\u0436\u043d\u043e\u0441\u0442\u0438 i.e. \u0437\u043d\u0430\u043a\u043e\u043c\u044b \u0441\u043e \u0432\u0441\u0435\u043c\u0438 \u043e\u0441\u043d\u043e\u0432\u043d\u044b\u043c\u0438 \u0442\u0440\u0443\u0434\u0430\u043c\u0438 \u0438 \u0440\u0430\u0431\u043e\u0442\u0430\u043c\u0438 \u0438 \u0437\u043d\u0430\u044e\u0442, \u0447\u0442\u043e \u043f\u0440\u043e\u0438\u0441\u0445\u043e\u0434\u0438\u043b\u043e \u0432 \u0434\u0430\u043d\u043d\u043e\u0439 \u043d\u0430\u0443\u0447\u043d\u043e\u0439 \u043e\u0431\u043b\u0430\u0441\u0442\u0438 \u0432 \u043f\u043e\u0441\u043b\u0435\u0434\u043d\u0438\u0435 \u0433\u043e\u0434\u044b<\/li>\n<\/ol>\n<p>  \u0414\u043e\u043f\u0443\u0441\u0442\u0438\u043c, \u0447\u0442\u043e \u0432\u0441\u0435 \u044d\u0442\u0438 \u0443\u0441\u043b\u043e\u0432\u0438\u044f \u0432\u044b\u043f\u043e\u043b\u043d\u0435\u043d\u044b, \u0442\u043e\u0433\u0434\u0430 \u0432\u0442\u043e\u0440\u043e\u0435, \u0447\u0442\u043e \u0431\u0443\u0434\u0435\u0442 \u0441\u0447\u0438\u0442\u0430\u0442\u044c\u0441\u044f \u043f\u0440\u0438\u0437\u043d\u0430\u043d\u043d\u044b\u043c \u0440\u0435\u0448\u0435\u043d\u0438\u0435\u043c? \u041f\u0443\u0431\u043b\u0438\u043a\u0430\u0446\u0438\u044f \u0432 \u0436\u0443\u0440\u043d\u0430\u043b\u0435 <a href=\"http:\/\/hornews.ru\/news\/last_news\/chelyabinskiy_matematik_reshil_odnu_iz_zadach_tyisyacheletiya.html\">\u00ab\u0410\u0432\u0442\u043e\u043c\u0430\u0442\u0438\u043a\u0430 \u0438 \u043c\u0435\u0445\u0430\u043d\u0438\u043a\u0430\u00bb<\/a>? \u0415\u0441\u0442\u044c \u043d\u0435\u0441\u043a\u043e\u043b\u044c\u043a\u043e \u043a\u043e\u043d\u0444\u0435\u0440\u0435\u043d\u0446\u0438\u0439, \u043f\u043e\u0434\u0445\u043e\u0434\u044f\u0449\u0438\u0445 \u0434\u043b\u044f \u0437\u0430\u0434\u0430\u0447\u0438 P vs NP:<br \/>  <a href=\"http:\/\/www.sigact.org\/stoc.html\">STOC, the Annual ACM Symposium on Theory of Computing <\/a><br \/>  <a href=\"http:\/\/talg.acm.org\/\">TAGL, ACM Transactions on Algorithms<\/a><br \/>  <a href=\"http:\/\/ieee-focs.org\/\">FOCS, The IEEE Annual Symposium on Foundations of Computer Science <\/a><\/p>\n<p>  \u0415\u0441\u043b\u0438 \u043e\u043d\u0438 (\u043b\u044e\u0431\u0430\u044f \u0438\u0437 \u044d\u0442\u0438\u0445 \u043a\u043e\u043d\u0444\u0435\u0440\u0435\u043d\u0446\u0438\u0439), \u043f\u0440\u0438\u0437\u043d\u0430\u044e\u0442 \u0432\u0430\u0448\u0435 \u0440\u0435\u0448\u0435\u043d\u0438\u0435, \u043c\u043e\u0436\u0435\u0442\u0435 \u0441\u043c\u0435\u043b\u043e \u0440\u0430\u0441\u0441\u0447\u0438\u0442\u044b\u0432\u0430\u0442\u044c \u043d\u0430 \u0441\u0432\u043e\u0439 \u043c\u0438\u043b\u043b\u0438\u043e\u043d \u2014 \u0434\u043e \u044d\u0442\u043e\u0433\u043e \u043c\u043e\u043c\u0435\u043d\u0442\u0430 \u0440\u0435\u0448\u0435\u043d\u0438\u0435 \u0441\u0447\u0438\u0442\u0430\u0435\u0442\u0441\u044f \u043e\u0434\u043d\u0438\u043c \u0438\u0437 \u043c\u043d\u043e\u0433\u0438\u0445 \u043d\u0435\u043f\u0440\u0430\u0432\u0438\u043b\u044c\u043d\u044b\u0445 \u0440\u0435\u0448\u0435\u043d\u0438\u0439 P vs. NP.<\/p>\n<p>  \u0418\u043d\u0442\u0435\u0440\u0435\u0441\u043d\u044b\u0439 roadmap (\u0442\u043e\u0447\u043d\u0435\u0435 \u0434\u0430\u0436\u0435 \u0438\u043d\u0442\u0435\u0440\u0430\u043a\u0442\u0438\u0432\u043d\u044b\u0439 \u0441\u043f\u0438\u0441\u043e\u043a \u0432\u043e\u043f\u0440\u043e\u0441\u043e\u0432) \u043f\u043e \u0432\u043e\u043f\u0440\u043e\u0441\u0443 \u043f\u0440\u043e\u0432\u0435\u0440\u043a\u0438 P vs. NP \u0440\u0435\u0448\u0435\u043d\u0438\u0439 \u043f\u0440\u0435\u0434\u0441\u0442\u0430\u0432\u043b\u0435\u043d <a href=\"http:\/\/gowers.tiddlyspace.com\/#%5B%5BA%20sitemap%20for%20the%20P%20versus%20NP%20notebook%5D%5D%20%5B%5BIs%20there%20a%20useful%20definition%20of%20simplicity%3F%5D%5D%20%5B%5BDoes%20P%3DNP%3F%5D%5D%20%5B%5BDo%20NP%20functions%20have%20polynomial%20circuit%20complexity%3F%5D%5D\">\u0437\u0434\u0435\u0441\u044c<\/a>.<\/p>\n<h4>\u041f\u043e\u0447\u0435\u043c\u0443 <a href=\"http:\/\/arxiv.org\/pdf\/1309.6078v1.pdf\">\u0441\u0442\u0430\u0442\u044c\u044e \u0420\u043e\u043c\u0430\u043d\u043e\u0432\u0430<\/a> \u043e\u0436\u0438\u0434\u0430\u0435\u0442 reject <\/h4>\n<p>  \u0415\u0441\u043b\u0438 \u0434\u0430\u0432\u0430\u0442\u044c \u043a\u0440\u0430\u0442\u043a\u0438\u0439 \u043e\u0442\u0432\u0435\u0442, \u0442\u043e \u043f\u043e\u0442\u043e\u043c\u0443, \u0447\u0442\u043e \u0441\u0442\u0430\u0442\u044c\u044f \u043d\u0435 \u043e\u0442\u0432\u0435\u0447\u0430\u0435\u0442 \u043d\u0438 \u043d\u0430 \u043e\u0434\u0438\u043d \u0438\u0437 \u0432\u043e\u043f\u0440\u043e\u0441\u043e\u0432 \u0438\u0437 \u0441\u043f\u0438\u0441\u043a\u0430 \u00ab\u0437\u0434\u0440\u0430\u0432\u043e\u0433\u043e \u0441\u043c\u044b\u0441\u043b\u0430\u00bb:  <\/p>\n<ol>\n<li>\u0412 \u0441\u0442\u0430\u0442\u044c\u0435 \u0432\u043e\u043e\u0431\u0449\u0435 \u043e\u0442\u0441\u0443\u0442\u0441\u0442\u0432\u0443\u0435\u0442 \u00abrelated work\u00bb, \u0441\u043e\u0437\u0434\u0430\u0435\u0442\u0441\u044f \u0432\u043f\u0435\u0447\u0430\u0442\u043b\u0435\u043d\u0438\u0435, \u0447\u0442\u043e 40 \u043b\u0435\u0442 \u0432 \u0442\u0435\u043e\u0440\u0438\u0438 \u0441\u043b\u043e\u0436\u043d\u043e\u0441\u0442\u0438 \u0432\u043e\u043e\u0431\u0449\u0435 \u043d\u0435 \u0431\u044b\u043b\u043e \u043f\u0440\u043e\u0433\u0440\u0435\u0441\u0441\u0430 (\u0430\u0432\u0442\u043e\u0440 \u0442\u043e\u043b\u044c\u043a\u043e \u043d\u0430 \u0441\u0435\u0431\u044f \u0441\u043e\u0441\u043b\u0430\u043b\u0441\u044f \u0442\u0440\u0438 \u0440\u0430\u0437\u0430): \u0434\u043b\u044f \u043f\u0440\u0438\u043c\u0435\u0440\u0430, \u043c\u043e\u0436\u043d\u043e \u0432\u0437\u0433\u043b\u044f\u043d\u0443\u0442\u044c \u043d\u0430 <a href=\"http:\/\/davidsjohnson.net\/columns\/col25.pdf\">The NP-Completeness Column: The Many Limits on Approximation by David S. Johnson<\/a>, \u0441\u0436\u0430\u0442\u043e \u043a\u0440\u0430\u0442\u043a\u043e \u043f\u043e \u0434\u0435\u043b\u0443 \u0440\u0430\u0441\u0441\u043a\u0430\u0437\u044b\u0432\u0430\u0435\u0442 \u043f\u0440\u043e \u0432\u0441\u0435 \u0441\u0432\u044f\u0437\u0430\u043d\u043d\u044b\u0435 \u0440\u0430\u0431\u043e\u0442\u044b, \u043d\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u0430\u044f \u043a\u0430\u0447\u0435\u0441\u0442\u0432\u0435\u043d\u043d\u0430\u044f \u0440\u0430\u0431\u043e\u0442\u0430 \u0432 TAGL<\/li>\n<li> \u0414\u0430\u043d\u043d\u0430\u044f \u0440\u0430\u0431\u043e\u0442\u0430 \u0434\u043e\u043f\u0443\u0441\u043a\u0430\u0435\u0442 \u0430\u043b\u0433\u0435\u0431\u0440\u0430\u0438\u0447\u0435\u0441\u043a\u043e\u0435 \u043f\u0440\u0435\u0434\u0441\u0442\u0430\u0432\u043b\u0435\u043d\u0438\u0435 (\u0442\u0430\u0431\u043b\u0438\u0447\u043a\u0438 \u0438\u0437 \u043f\u0435\u0440\u0435\u043c\u0435\u043d\u043d\u044b\u0445, \u0433\u0440\u0430\u0444 \u043d\u0430 \u044d\u0442\u0438\u0445 \u0442\u0430\u0431\u043b\u0438\u0447\u043a\u0430\u0445 \u0438 \u0447\u0443\u0442\u044c-\u043b\u0438 \u043d\u0435 conjunctive query \u0434\u043b\u044f \u043f\u0440\u043e\u0432\u0435\u0440\u043a\u0438 \u0441\u0432\u043e\u0439\u0441\u0442\u0432) \u2014 \u043d\u0430\u043f\u0440\u044f\u043c\u0443\u044e \u043f\u0440\u0438\u043c\u0435\u043d\u0438\u043c\u0430 \u0442\u0435\u043e\u0440\u0435\u043c\u0430 <a href=\"http:\/\/www.scottaaronson.com\/papers\/alg.pdf\">Aaronson-Wigderson<\/a> (\u043e\u0431\u043e\u0431\u0449\u0430\u044e\u0449\u0430\u044f \u0442\u0435\u043e\u0440\u0435\u043c\u0443 Baker-Gill-Solovay) \u043e \u043d\u0435\u0440\u0430\u0437\u0440\u0435\u0448\u0438\u043c\u043e\u0441\u0442\u0438 P vs. NP \u0441 \u043f\u043e\u043c\u043e\u0449\u044c\u044e \u0430\u043b\u0433\u0435\u0431\u0440\u0430\u0438\u0447\u0435\u0441\u043a\u0438\u0445 \u043c\u0435\u0442\u043e\u0434\u043e\u0432. \u041a\u0441\u0442\u0430\u0442\u0438, \u0435\u0441\u043b\u0438 \u0443 \u043f\u0440\u043e\u0432\u0435\u0440\u044f\u044e\u0449\u0438\u0445 \u0435\u0441\u0442\u044c \u0441\u043e\u043c\u043d\u0435\u043d\u0438\u0435, \u0447\u0442\u043e \u0432\u044b \u0438\u0433\u043d\u043e\u0440\u0438\u0440\u0443\u0435\u0442\u0435 \u0442\u0430\u043a\u0438\u0435 \u0440\u0435\u0437\u0443\u043b\u044c\u0442\u0430\u0442\u044b \u043d\u0430\u043c\u0435\u0440\u0435\u043d\u043d\u043e, \u044d\u0442\u043e \u0431\u0443\u0434\u0435\u0442 \u0438\u043d\u0442\u0435\u0440\u043f\u0440\u0435\u0442\u0438\u0440\u043e\u0432\u0430\u043d\u043e \u043f\u0440\u043e\u0442\u0438\u0432 \u043e\u0442\u043f\u0440\u0430\u0432\u043b\u0435\u043d\u043d\u043e\u0439 \u0440\u0430\u0431\u043e\u0442\u044b<\/li>\n<li> \u0413\u0434\u0435 \u043f\u0440\u043e\u0442\u043e\u0442\u0438\u043f \u043d\u0435 \u0443\u0431\u0435\u0433\u0430\u044e\u0449\u0438\u0439 \u043a \u044d\u043a\u0441\u043f\u043e\u043d\u0435\u043d\u0442\u0435 \u0432 \u0430\u0441\u0438\u043c\u043f\u0442\u043e\u0442\u0438\u043a\u0435?<\/li>\n<li> \u0413\u0434\u0435 \u043f\u0441\u0435\u0432\u0434\u043e\u043a\u043e\u0434 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u0430? \u0413\u0434\u0435 \u043f\u043e\u043b\u043d\u043e\u0446\u0435\u043d\u043d\u044b\u0439 \u0440\u0430\u0431\u043e\u0447\u0438\u0439 \u043f\u0440\u0438\u043c\u0435\u0440: \u0432\u0445\u043e\u0434\u043d\u044b\u0435 \u0434\u0430\u043d\u043d\u044b\u0435 \u2014 \u0438\u0437\u0432\u0435\u0441\u0442\u043d\u044b\u0439 \u0441\u043b\u043e\u0436\u043d\u044b\u0439 \u043f\u0440\u0438\u043c\u0435\u0440, \u043f\u043e\u044d\u0442\u0430\u043f\u043d\u043e \u043f\u043e\u043a\u0430\u0437\u0430\u043d\u0430 \u0440\u0430\u0431\u043e\u0442\u0430 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u0430 \u0438 \u0432\u044b\u0445\u043e\u0434\u043d\u044b\u0435 \u0434\u0430\u043d\u043d\u044b\u0435? \u0413\u0434\u0435 \u0444\u043e\u0440\u043c\u0430\u043b\u0438\u0437\u0430\u0446\u0438\u044f? \u0432 \u0441\u0442\u0430\u0442\u044c\u0435 \u043d\u0430 17 \u0441\u0442\u0440\u0430\u043d\u0438\u0446 \u0434\u0432\u0435 \u0444\u043e\u0440\u043c\u0443\u043b\u044b \u0432\u0438\u0434\u0430 (a =&gt; b) \u0438 \u043d\u0435\u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u044b\u0435 \u0444\u0440\u0430\u0437\u044b \u0432 \u0434\u0443\u0445\u0435: \u00abgrouping the lines of F with identical numbers of three non-empty columns;\u00bb<\/li>\n<li> \u041e\u0442\u0441\u0443\u0442\u0441\u0442\u0432\u0443\u044e\u0442 \u043a\u043b\u044e\u0447\u0435\u0432\u044b\u0435 \u0441\u0441\u044b\u043b\u043a\u0438 \u0432 \u0440\u0430\u0431\u043e\u0442\u0435, \u043d\u0430\u043f\u0440\u0438\u043c\u0435\u0440, \u043d\u0430 \u0440\u0430\u0431\u043e\u0442\u044b \u041b\u0435\u0432\u0438\u043d\u0430-\u041a\u0443\u043a\u0430. <\/li>\n<\/ol>\n<p>  \u0414\u0430\u043b\u0435\u0435, \u0434\u043e\u043f\u0443\u0441\u0442\u0438\u043c, \u0447\u0442\u043e \u0440\u0430\u0431\u043e\u0442\u0430 \u0431\u0443\u0434\u0435\u0442 \u0438\u0441\u043f\u0440\u0430\u0432\u043b\u0435\u043d\u0430, \u0442\u043e\u0433\u0434\u0430 \u043f\u043e-\u043f\u0440\u0435\u0436\u043d\u0435\u043c\u0443 \u043d\u0435 \u0438\u043c\u0435\u0435\u0442 \u0441\u043c\u044b\u0441\u043b\u0430 \u043f\u0438\u0441\u0430\u0442\u044c \u043e\u0442\u043a\u0440\u044b\u0442\u044b\u0435 \u043f\u0438\u0441\u044c\u043c\u0430 \u043d\u0438\u043a\u043e\u043c\u0443 \u2014 \u0441\u043e\u0432\u0440\u0435\u043c\u0435\u043d\u043d\u0430\u044f \u043d\u0430\u0443\u043a\u0430 \u0442\u0430\u043a \u043d\u0435 \u0440\u0430\u0431\u043e\u0442\u0430\u0435\u0442, \u044d\u0442\u043e \u0432\u0430\u0448\u0430 \u0437\u0430\u0434\u0430\u0447\u0430 \u0443\u0431\u0435\u0434\u0438\u0442\u044c \u043e\u0431\u0449\u0435\u0441\u0442\u0432\u0435\u043d\u043d\u043e\u0441\u0442\u044c \u0432 \u043f\u0440\u0430\u0432\u0438\u043b\u044c\u043d\u043e\u0441\u0442\u0438 \u0440\u0435\u0448\u0435\u043d\u0438\u044f. \u0421\u0434\u0435\u043b\u0430\u0442\u044c \u044d\u0442\u043e \u043c\u043e\u0436\u043d\u043e \u0442\u043e\u043b\u044c\u043a\u043e \u0447\u0435\u0440\u0435\u0437 \u043f\u0440\u0438\u0437\u043c\u0443 \u044d\u043a\u0441\u043f\u0435\u0440\u0442\u043d\u043e\u0433\u043e \u043c\u043d\u0435\u043d\u0438\u044f, \u0441\u043c. \u043a\u043e\u043d\u0444\u0435\u0440\u0435\u043d\u0446\u0438\u0438 \u043e\u043f\u0438\u0441\u0430\u043d\u043d\u044b\u0435 \u0432\u044b\u0448\u0435.<\/p>\n<h4> \u0427\u0442\u043e \u043f\u043e\u0447\u0438\u0442\u0430\u0442\u044c? <\/h4>\n<p>  \u041e\u0431\u044b\u0447\u043d\u043e \u0445\u043e\u0440\u043e\u0448\u043e \u0438 \u0434\u043e\u0441\u0442\u0443\u043f\u043d\u043e \u0432\u0441\u0451 \u043e\u0431\u044a\u044f\u0441\u043d\u044f\u044e\u0442 \u0432 SAT\/SMT \u043b\u0435\u0442\u043d\u0438\u0445 \u0448\u043a\u043e\u043b\u0430\u0445:<br \/>  <a href=\"http:\/\/satsmt2013.ics.aalto.fi\/program.shtml\">\u043c\u0430\u0442\u0435\u0440\u0438\u0430\u043b\u044b \u0448\u043a\u043e\u043b\u044b 2013 <\/a><br \/>  <a href=\"https:\/\/es-static.fbk.eu\/events\/satsmtschool12\/\">\u043c\u0430\u0442\u0435\u0440\u0438\u0430\u043b\u044b \u0448\u043a\u043e\u043b\u044b 2012<\/a><\/p>\n<p>  \u0421\u043a\u043e\u0440\u043e \u0431\u0443\u0434\u0435\u0442 \u0441\u0432\u0435\u0436\u0438\u0439 \u041a\u043d\u0443\u0442 \u043f\u0440\u043e SAT \u2014 \u0434\u043e\u0441\u0442\u0443\u043f\u0435\u043d \u0447\u0435\u0440\u043d\u043e\u0432\u0438\u043a: <a href=\"http:\/\/www-cs-faculty.stanford.edu\/~knuth\/fasc6a.ps.gz\">The Art of Programming 4, 6A: Satisfibility<\/a><\/p>\n<p>  \u0411\u043e\u043b\u044c\u0448\u043e\u0435 \u043a\u043e\u043b\u0438\u0447\u0435\u0441\u0442\u0432\u043e \u0441\u0441\u044b\u043b\u043e\u043a \u043f\u0440\u0438\u0441\u0443\u0442\u0441\u0442\u0432\u0443\u0435\u0442 \u0432 \u043f\u0440\u0435\u0434\u044b\u0434\u0443\u0449\u0435\u043c \u043f\u043e\u0441\u0442\u0435 <a href=\"http:\/\/habrahabr.ru\/post\/207112\/\">\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)<\/a><br \/>  \u041a\u043b\u044e\u0447\u0435\u0432\u044b\u0435 \u043f\u0440\u0438\u0432\u0435\u0434\u0435\u043c \u0437\u0434\u0435\u0441\u044c:<br \/>  \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>  \u043e\u0431 \u0438\u0441\u0442\u043e\u0440\u0438\u0438 NP:<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>  \u041e\u0434\u0438\u043d \u0438\u0437 \u043d\u0430\u0438\u0431\u043e\u043b\u0435\u0435 \u0438\u0437\u0432\u0435\u0441\u0442\u043d\u044b\u0445 \u0438 \u0443\u0432\u0430\u0436\u0430\u0435\u043c\u044b\u0445 \u0442\u0440\u0443\u0434\u043e\u0432 \u043f\u043e \u0442\u0435\u043e\u0440\u0438\u0438 \u0441\u043b\u043e\u0436\u043d\u043e\u0441\u0442\u0438:<br \/>  <a href=\"http:\/\/rutracker.org\/forum\/viewtopic.php?t=3509871\">\u0413\u044d\u0440\u0438 \u041c., \u0414\u0436\u043e\u043d\u0441\u043e\u043d \u0414. \u2014 \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 [1982]<\/a><\/p>\n<h4>\u0417\u0430\u0434\u0430\u0447\u043a\u0430 \u043d\u0430 \u043f\u043e\u0434\u0443\u043c\u0430\u0442\u044c<\/h4>\n<p>  \u041d\u0435\u0441\u0442\u044b\u043a\u043e\u0432\u043a\u0430 SAT, \u0440\u0435\u043b\u044f\u0446\u0438\u043e\u043d\u043d\u043e\u0439 \u0430\u043b\u0433\u0435\u0431\u0440\u044b \u0438 \u043f\u0440\u043e\u0431\u043b\u0435\u043c\u044b \u043e\u0441\u0442\u0430\u043d\u043e\u0432\u0430.<br \/>  \u0414\u0430\u043d\u043e \u0442\u0440\u0438 \u0443\u0442\u0432\u0435\u0440\u0436\u0434\u0435\u043d\u0438\u044f:<br \/>  1. \u041b\u043e\u0433\u0438\u043a\u0430 \u043f\u0435\u0440\u0432\u043e\u0433\u043e \u043f\u043e\u0440\u044f\u0434\u043a\u0430 \u0438 \u0440\u0435\u043b\u044f\u0446\u0438\u043e\u043d\u043d\u0430\u044f \u0430\u043b\u0433\u0435\u0431\u0440\u0430 \u0438\u043c\u0435\u044e\u0442 \u043e\u0434\u0438\u043d\u0430\u043a\u043e\u0432\u0443\u044e \u00ab\u0432\u044b\u0447\u0438\u0441\u043b\u0438\u0442\u0435\u043b\u044c\u043d\u0443\u044e \u0441\u043b\u043e\u0436\u043d\u043e\u0441\u0442\u044c\u00bb \u0442.\u00a0\u0435. \u0435\u0441\u043b\u0438 \u0437\u0430\u0434\u0430\u0447\u0430 \u0438\u043c\u0435\u0435\u0442 \u0441\u043b\u043e\u0436\u043d\u043e\u0441\u0442\u044c \u0425 \u0432 \u043e\u0434\u043d\u043e\u043c \u0444\u043e\u0440\u043c\u0430\u043b\u0438\u0437\u043c\u0435, \u0442\u043e \u0441\u0443\u0449\u0435\u0441\u0442\u0432\u0443\u0435\u0442 \u0435\u0451 \u0432\u044b\u0440\u0430\u0436\u0435\u043d\u0438\u0435 \u0432 \u0434\u0440\u0443\u0433\u043e\u043c \u0444\u043e\u0440\u043c\u0430\u043b\u0438\u0437\u043c\u0435 \u0441 \u0442\u0430\u043a\u043e\u0439 \u0436\u0435 \u0441\u043b\u043e\u0436\u043d\u043e\u0441\u0442\u044c\u044e (<a href=\"http:\/\/en.wikipedia.org\/wiki\/Codd&#39;s_theorem\">\u0441\u0441\u044b\u043b\u043a\u0430<\/a>).<br \/>  2. \u0420\u0435\u043b\u044f\u0446\u0438\u043e\u043d\u043d\u0430\u044f \u0430\u043b\u0433\u0435\u0431\u0440\u0430 \u043d\u0435 \u0441\u043f\u043e\u0441\u043e\u0431\u043d\u0430 \u0432\u044b\u0440\u0430\u0437\u0438\u0442\u044c \u0442\u0440\u0430\u043d\u0437\u0438\u0442\u0438\u0432\u043d\u0443\u044e \u0437\u0430\u043c\u044b\u043a\u0430\u043d\u0438\u0435 \u2013 \u0437\u0430\u0434\u0430\u0447\u0430 \u0432 \u043a\u043b\u0430\u0441\u0441\u0435 P (<a href=\"http:\/\/en.wikipedia.org\/wiki\/Relational_algebra#Transitive_closure\">relational algebra: transitive closure<\/a> ) <br \/>  3. SAT \u0434\u043b\u044f \u043b\u043e\u0433\u0438\u043a\u0438 \u043f\u0435\u0440\u0432\u043e\u0433\u043e \u043f\u043e\u0440\u044f\u0434\u043a\u0430 \u044d\u043a\u0432\u0438\u0432\u0430\u043b\u0435\u043d\u0442\u0435\u043d \u043f\u0440\u043e\u0431\u043b\u0435\u043c\u0435 \u043e\u0441\u0442\u0430\u043d\u043e\u0432\u0430 \u0438 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u0438\u0447\u0435\u0441\u043a\u0438 \u043d\u0435\u0440\u0430\u0437\u0440\u0435\u0448\u0438\u043c (<a href=\"http:\/\/en.wikipedia.org\/wiki\/Halting_problem#Relationship_with_G.C3.B6del.27s_incompleteness_theorems\">\u0441\u0441\u044b\u043b\u043a\u0430<\/a>).<br \/>  \u0412\u043e\u043f\u0440\u043e\u0441: \u041a\u0430\u043a \u0442\u0430\u043a\u043e\u0435 \u043c\u043e\u0436\u0435\u0442 \u0431\u044b\u0442\u044c?    \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\/208774\/\"> http:\/\/habrahabr.ru\/post\/208774\/<\/a><\/p>\n","protected":false},"excerpt":{"rendered":"<div class=\"content html_format\">   \t\u0412 <a href=\"http:\/\/habrahabr.ru\/post\/207112\/\">\u043f\u0440\u0435\u0434\u044b\u0434\u0443\u0449\u0435\u0439 \u0447\u0430\u0441\u0442\u0438<\/a> \u0431\u044b\u043b\u0438 \u043e\u0441\u0432\u0435\u0449\u0435\u043d\u044b \u043e\u0431\u0449\u0435\u0434\u043e\u0441\u0442\u0443\u043f\u043d\u044b\u0435 \u0432\u043e\u043f\u0440\u043e\u0441\u044b, \u043a\u0430\u0441\u0430\u044e\u0449\u0438\u0435\u0441\u044f SAT \u0438 P-NP: \u0438\u0441\u0442\u043e\u0440\u0438\u044f \u043f\u0440\u043e\u0431\u043b\u0435\u043c\u044b, \u0438\u043d\u0442\u0443\u0438\u0442\u0438\u0432\u043d\u044b\u0435 \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u0435\u043d\u0438\u044f \u043a\u043b\u0430\u0441\u0441\u043e\u0432 \u0438 \u0437\u0430\u0434\u0430\u0447, \u0443\u043a\u0430\u0437\u0430\u043d\u044b \u043e\u0441\u043d\u043e\u0432\u043d\u044b\u0435 \u043f\u0440\u0438\u043b\u043e\u0436\u0435\u043d\u0438\u044f SAT \u0438 \u043e\u0441\u043d\u043e\u0432\u043d\u044b\u0435 \u043f\u043e\u0441\u043b\u0435\u0434\u0441\u0442\u0432\u0438\u044f, \u0432 \u0441\u043b\u0443\u0447\u0430\u0438 \u0440\u0435\u0448\u0435\u043d\u0438\u044f P ?= NP (\u0442\u0430\u043c \u0436\u0435 \u043c\u043e\u0436\u043d\u043e \u043d\u0430\u0439\u0442\u0438 \u0434\u043e\u0441\u0442\u0430\u0442\u043e\u0447\u043d\u043e\u0435 \u0447\u0438\u0441\u043b\u043e \u0441\u0441\u044b\u043b\u043e\u043a \u043d\u0430 \u0440\u0430\u0437\u043b\u0438\u0447\u043d\u044b\u0439 \u043c\u0430\u0442\u0435\u0440\u0438\u0430\u043b \u0434\u043b\u044f \u0441\u0430\u043c\u043e\u0441\u0442\u043e\u044f\u0442\u0435\u043b\u044c\u043d\u043e\u0433\u043e \u0438\u0437\u0443\u0447\u0435\u043d\u0438\u044f \u0442\u0435\u043c\u0430\u0442\u0438\u043a\u0438).<\/p>\n<p>  \u0412 \u0434\u0430\u043d\u043d\u043e\u0439 \u0441\u0442\u0430\u0442\u044c\u0435 \u043c\u044b \u0440\u0430\u0441\u0441\u043c\u043e\u0442\u0440\u0438\u043c \u0442\u0435\u0445\u043d\u0438\u0447\u0435\u0441\u043a\u0443\u044e \u0441\u0442\u043e\u0440\u043e\u043d\u0443 \u0432\u043e\u043f\u0440\u043e\u0441\u0430, \u0430 \u0442\u0430\u043a \u0436\u0435 \u0444\u043e\u0440\u043c\u0430\u043b\u0438\u0437\u0443\u0435\u043c \u0438 \u043f\u0440\u0435\u0434\u0441\u0442\u0430\u0432\u0438\u043c \u0432 \u0434\u0435\u0442\u0430\u043b\u044f\u0445 \u043c\u0430\u0442\u0435\u0440\u0438\u0430\u043b \u0438\u0437 \u043f\u0440\u0435\u0434\u044b\u0434\u0443\u0449\u0435\u0439 \u0441\u0442\u0430\u0442\u044c\u0438.<\/p>\n<p>  <img decoding=\"async\" src=\"http:\/\/habr.habrastorage.org\/post_images\/ec5\/2c5\/848\/ec52c5848cb78645a2b82a6f5e2a8aca.jpg\"\/><\/p>\n<p>  \u043a\u0430\u0440\u0442\u0438\u043d\u043a\u0430 \u0438\u0437 \u0441\u0442\u0430\u0442\u044c\u0438 <a href=\"http:\/\/cacm.acm.org\/magazines\/2009\/8\/34498-boolean-satisfiability-from-theoretical-hardness-to-practical-success\/pdf\">Boolean Satisfiability: From Theoretical Hardness to Practical Success<\/a> (Communications of ACM) <\/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-208774","post","type-post","status-publish","format-standard","hentry"],"_links":{"self":[{"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=\/wp\/v2\/posts\/208774","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=208774"}],"version-history":[{"count":0,"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=\/wp\/v2\/posts\/208774\/revisions"}],"wp:attachment":[{"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=%2Fwp%2Fv2%2Fmedia&parent=208774"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=%2Fwp%2Fv2%2Fcategories&post=208774"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=%2Fwp%2Fv2%2Ftags&post=208774"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}