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

[[Булева формула]] определяется рекурсивным образом: [[булева переменная]] <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-полными. Булевы формулы являются менее краткими и сжатыми, чем булевы схемы: к примеру, функция четности имеет схемы линейного размера, тогда как представления в виде формул являются сверхполиномиальными. Точнее говоря, XORn: {0, 1}<math>^n</math> (стрелка вправо с коротким «упором» слева) {0; 1} определена следующим образом: она принимает значение 1 в точности на тех элементах {0, 1}<math>^n</math>, которые содержат нечетное число единиц. Определим размер формулы, равный количеству встречающихся в ней логических операций. Тогда для любой последовательности формул θ1, θ2, … , такой, что θk представляет XORk, размер θk равен Ω(kc) для всех c  Z+ [14 , главы 11 и 12].