Сравнивайте с английским: нажмите на абзац — оригинал откроется в окне. Кнопка EN под абзацем показывает его прямо в тексте.
Содержание
Введение
В формальной логике выполнимость Хорна, или HORNSAT, — это задача определения, является ли заданное множество роговых клауз выполнимым или нет. Выполнимость Хорна и роговые клаузы названы в честь Альфреда Хорна. Роговая клауза — это клауза, содержащая не более одного положительного литерала, называемого головой клаузы, и любое количество отрицательных литералов, образующих тело клаузы. Роговая формула — это пропозициональная формула, образованная конъюнкцией роговых клауз. Выполнимость Хорна фактически является одной из "наиболее сложных" или "наиболее выразительных" задач, для которых известно, что она вычислима за полиномиальное время, в том смысле, что это P-полная задача. Задача выполнимости Хорна также может быть сформулирована для многозначных пропозициональных логик. Алгоритмы обычно не линейны, но некоторые из них являются полиномиальными; см. Hähnle (2001 или 2003) для обзора.
In formal logic, Horn satisfiability, or HORNSAT, is the problem of deciding whether a given set of propositional Horn clauses is satisfiable or not. Horn satisfiability and Horn clauses are named after Alfred Horn. A Horn clause is a clause with at most one positive literal, called the head of the clause, and any number of negative literals, forming the body of the clause. A Horn formula is a propositional formula formed by conjunction of Horn clauses. Horn satisfiability is actually one of the "hardest" or "most expressive" problems which is known to be computable in polynomial time, in the sense that it is a P complete problem. The Horn satisfiability problem can also be asked for propositional many valued logics. The algorithms are not usually linear, but some are polynomial; see Hähnle (2001 or 2003) for a survey.
Обобщение
Обобщением класса формул Хорна является класс переименовываемых формул Хорна, представляющий собой множество формул, которые можно привести к форме Хорна, заменив некоторые переменные на их отрицания. Проверка существования такой замены может быть выполнена за линейное время, следовательно, задача определения выполнимости таких формул находится в классе P, поскольку её можно решить, сначала выполнив эту замену, а затем проверив выполнимость полученной формулы Хорна. Выполнимость формул Хорна и переименовываемая выполнимость формул Хорна представляют собой один из двух важных подклассов задачи выполнимости, разрешимых за полиномиальное время; другим таким подклассом является 2-выполнимость.
A generalization of the class of Horn formulae is that of renamable Horn formulae, which is the set of formulae that can be placed in Horn form by replacing some variables with their respective negation. Checking the existence of such a replacement can be done in linear time; therefore, the satisfiability of such formulae is in P as it can be solved by first performing this replacement and then checking the satisfiability of the resulting Horn formula. Horn satisfiability and renamable Horn satisfiability provide one of two important subclasses of satisfiability that are solvable in polynomial time; the other such subclass is 2 satisfiability.
Двухрогный SAT
Двойной вариант задачи Horn SAT — это Dual Horn SAT, в которой каждая дизъюнкция содержит не более одного отрицательного литерала. Отрицание всех переменных преобразует экземпляр Dual Horn SAT в экземпляр Horn SAT. Хорн доказал в 1951 году, что Dual Horn SAT решается за полиномиальное время (классифицируется как P).
A dual variant of Horn SAT is Dual Horn SAT, in which each clause has at most one negative literal. Negating all variables transforms an instance of Dual Horn SAT into Horn SAT. It was proven in 1951 by Horn that Dual Horn SAT is in P.