Нормальная конъюнктивная форма (CNF) в булевой логике: определение, преобразование формул, применение в автоматическом доказательстве теорем и схемотехнике.
Сравнивайте с английским: нажмите на абзац — оригинал откроется в окне. Кнопка EN под абзацем показывает его прямо в тексте.
Содержание
Введение
Стандартная форма булевой функции
Standard form of Boolean function
В булевой логике формула находится в конъюнктивной нормальной форме (CNF) или клаузальной нормальной форме, если она представляет собой конъюнкцию одной или нескольких клауз, где клауза является дизъюнкцией литералов; другими словами, это произведение сумм или логическое И (AND) от логических ИЛИ (OR). Как каноническая нормальная форма, она полезна в автоматическом доказательстве теорем и теории схем. В автоматическом доказательстве теорем понятие "клаузальная нормальная форма" часто используется в более узком смысле, обозначая конкретное представление формулы CNF в виде набора множеств литералов.
In Boolean logic, a formula is in conjunctive normal form (CNF) or clausal normal form if it is a conjunction of one or more clauses, where a clause is a disjunction of literals; otherwise put, it is a product of sums or an AND of ORs. As a canonical normal form, it is useful in automated theorem proving and circuit theory. In automated theorem proving, the notion "clausal normal form" is often used in a narrower sense, meaning a particular representation of a CNF formula as a set of sets of literals.
Перевод в CNF
В классической логике каждая формула высказывания может быть преобразована в эквивалентную формулу, находящуюся в КНФ. Это преобразование основано на правилах логических эквивалентностей: исключение двойного отрицания, законы Де Моргана и дистрибутивность.
In classical logic each propositional formula can be converted to an equivalent formula that is in CNF. This transformation is based on rules about logical equivalences: double negation elimination, De Morgan's laws, and the distributive law.
Комплексность вычислений
Важный набор задач в вычислительной сложности включает в себя поиск присвоений переменным булевой формулы, выраженной в конъюнктивной нормальной форме, таких что формула истинна. Проблема k-SAT – это задача поиска удовлетворяющего присвоения булевой формуле, выраженной в КНФ, в которой каждая дизъюнкция содержит не более k переменных. 3-SAT является NP-полной (как и любая другая k-SAT задача при k>2), в то время как для 2-SAT известно решение в полиномиальное время. Как следствие, задача преобразования формулы в ДНФ с сохранением выполнимости является NP-трудной; двойственно, преобразование в КНФ с сохранением истинности также является NP-трудной; следовательно, преобразование в ДНФ или КНФ, сохраняющее эквивалентность, также является NP-трудной. Типичные задачи в этом случае включают формулы в "3КНФ": конъюнктивная нормальная форма с не более чем тремя переменными в каждом конъюнкте. Примеры таких формул, встречающихся на практике, могут быть очень большими, например, с 100 000 переменных и 1 000 000 конъюнктов. Формулу в КНФ можно преобразовать в равноудовлетворительную формулу в "kКНФ" (для k≥3), заменяя каждый конъюнкт, содержащий более k переменных, двумя конъюнктами и вводя Z как новую переменную, и повторяя это столько раз, сколько необходимо.
An important set of problems in computational complexity involves finding assignments to the variables of a boolean formula expressed in conjunctive normal form, such that the formula is true. The k SAT problem is the problem of finding a satisfying assignment to a boolean formula expressed in CNF in which each disjunction contains at most k variables. 3 SAT is NP complete (like any other k SAT problem with k>2) while 2 SAT is known to have solutions in polynomial time. As a consequence, the task of converting a formula into a DNF, preserving satisfiability, is NP hard; dually, converting into CNF, preserving validity, is also NP hard; hence equivalence preserving conversion into DNF or CNF is again NP hard. Typical problems in this case involve formulas in "3CNF": conjunctive normal form with no more than three variables per conjunct. Examples of such formulas encountered in practice can be very large, for example with 100,000 variables and 1,000,000 conjuncts. A formula in CNF can be converted into an equisatisfiable formula in "kCNF" (for k≥3) by replacing each conjunct with more than k variables by two conjuncts and with Z a new variable, and repeating as often as necessary.