Введение
Когда конечный набор S отношений приводит к задачам, разрешимым за полиномиальное время, или NP-полным задачам. В теории вычислительной сложности, являющейся областью информатики, теорема дихотомии Шефера, доказанная Томасом Джеромом Шефером, устанавливает необходимые и достаточные условия, при которых конечный набор S отношений над булевой областью приводит к задачам, разрешимым за полиномиальное время, или NP-полным задачам, когда отношения из S используются для ограничения некоторых пропозициональных переменных. Она называется теоремой дихотомии, поскольку сложность задачи, определяемой S, либо находится в классе P, либо является NP-полной, в отличие от классов промежуточной сложности, существование которых известно (при условии, что P ≠ NP) благодаря теореме Ладнера. Частными случаями теоремы дихотомии Шефера являются NP-полнота SAT (задачи булевой выполнимости) и два её популярных варианта: 1-в-3 SAT и 3SAT, где не все переменные равны (часто обозначается NAE 3SAT). Фактически, для этих двух вариантов SAT теорема дихотомии Шефера показывает, что их монотонные версии (где отрицания переменных не допускаются) также являются NP-полными.
In computational complexity theory, a branch of computer science, Schaefer's dichotomy theorem, proved by Thomas Jerome Schaefer, states necessary and sufficient conditions under which a finite set S of relations over the Boolean domain yields polynomial time or NP complete problems when the relations of S are used to constrain some of the propositional variables. It is called a dichotomy theorem because the complexity of the problem defined by S is either in P or is NP complete, as opposed to one of the classes of intermediate complexity that is known to exist (assuming P ≠ NP) by Ladner's theorem. Special cases of Schaefer's dichotomy theorem include the NP completeness of SAT (the Boolean satisfiability problem) and its two popular variants 1 in 3 SAT and not all equal 3SAT (often denoted by NAE 3SAT). In fact, for these two variants of SAT, Schaefer's dichotomy theorem shows that their monotone versions (where negations of variables are not allowed) are also NP complete.
Обобщения
Анализ был впоследствии уточнен: CSP(Γ) разрешим в co NLOGTIME, является L-полной, NL-полной, ⊕L-полной, P-полной или NP-полной задачей, и для данного Γ можно в полиномиальное время определить, какой из этих случаев имеет место. Теорема дихотомии Шефера также была обобщена с использованием пропозициональной логики графов вместо булевой логики.
Связанная работа
Если задача состоит в подсчете количества решений, обозначаемого как #CSP(Γ), то существует аналогичный результат для двоичной области, полученный Крейнгу и Германном. В частности, конечный набор отношений S над булевой областью определяет задачу выполнимости, разрешимую за полиномиальное время, если каждое отношение в S эквивалентно конъюнкции аффинных формул. Пусть Γ – конечный язык ограничений над булевой областью. Если задача #CSP(Γ) разрешима за полиномиальное время, то Γ имеет операцию Мальцева в качестве полиморфизма. В противном случае задача #CSP(Γ) является #P-полной. Операция Мальцева m – это троичная операция, удовлетворяющая . Примером операции Мальцева является операция "меньшинство", представленная в современной алгебраической формулировке теоремы дихотомии Шефера, приведенной выше. Таким образом, если Γ имеет операцию "меньшинство" в качестве полиморфизма, то не только возможно решить CSP(Γ) за полиномиальное время, но и вычислить #CSP(Γ) за полиномиальное время. Существует в общей сложности 4 операции Мальцева на булевых переменных, определяемые значениями и . Пример менее симметричной операции приведен в . На других областях, таких как группы, примерами операций Мальцева являются и . Для более крупных областей, даже для области размера три, существование полиморфизма Мальцева для Γ является недостаточным условием для разрешимости #CSP(Γ). Однако отсутствие полиморфизма Мальцева для Γ подразумевает #P-трудность #CSP(Γ).
For larger domains, even for a domain of size three, the existence of a Mal'tsev polymorphism for Γ is an insufficient condition for the tractability of #CSP(Γ). However, the absence of a Mal'tsev polymorphism for Γ implies the #P hardness of #CSP(Γ).