Бинарный граф решений: различия между версиями

[[Булева формула]] определяется рекурсивным образом: [[булева переменная]] <math>x_i</math> является булевой формулой; если φ и ψ являются булевыми формулами, то ими являются также (<math>\lnot</math>φ), (φ <math>\land</math> ψ), (φ <math>\lor</math> ψ), (φ <math>\rightarrow</math> ψ) и (φ <math>\leftrightarrow</math> ψ). Операторы <math>\lnot</math>, <math>\land</math>, <math>\lor</math>, <math>\rightarrow</math>, <math>\leftrightarrow</math> называются логическими операциями; ради удобства записи скобки часто опускаются. Булевы формулы могут использоваться для представления произвольных булевых функций; однако проблемы выполнимости и эквивалентности формул также являются NP-полными. Булевы формулы являются менее краткими и сжатыми, чем булевы схемы: к примеру, функция четности имеет схемы линейного размера, тогда как представления в виде формул являются сверхполиномиальными. Точнее говоря, XOR<math>_n</math>: {0, 1}<math>^n</math> <math>\mapsto</math> {0, 1} определена следующим образом: она принимает значение 1 в точности на тех элементах {0, 1}<math>^n</math>, которые содержат нечетное число единиц. Определим размер формулы, равный количеству встречающихся в ней логических операций. Тогда для любой последовательности формул <math>\theta _1 \, </math>, <math>\theta _2 \, </math>, ... , такой, что <math>\theta _k \, </math> представляет XOR<math>_k</math>, размер <math>\theta _k \, </math> равен <math>\Omega(k^c) \, </math> для всех  <math>c \in Z^+ \, </math> [14 , главы 11 и 12].

Дизъюнкция представляет собой булеву формулу, содержащую только логические операции  и , причем  применяется только к переменным; к примеру, x1   x3  x5 является дизъюнкцией. Булева формула находится в дизъюнктивной нормальной форме (ДНФ), если она имеет вид D0  D1  …  Dk-1, где каждый член Di является дизъюнкцией. ДНФ-формулы могут представлять произвольные булевы функции, например, путем определения каждого входа, на котором формула принимает значение 1, как дизъюнкции. ДНФ-формулы применяются в проектировании логических схем, поскольку могут быть непосредственно переведены в ПЛМ [4]. Однако если проблема выполнимости ДНФ-формул решается тривиально, то проблема эквивалентности является NP-полной. Кроме того, если φ и ψ являются ДНФ-формулами, то φ и φ  ψ таковыми не являются, а перевод их в ДНФ, представляющие ту же функцию, может привести к экспоненциальному росту размера формулы.