О преобразованиях Цейтина в логических уравнениях

В статье сообщается о применении преобразований Цейтина в различных областях пропозициональной логики, связанных с решением систем логических уравнений. Показывается, что преобразования Цейтина не изменяют числа решений системы логических уравнений, и строится биекция между множествами решений системы и результата её преобразований по Цейтину. Приводятся некоторые результаты по применению преобразований Цейтина к построению оценок сложности систем пропозиционального вывода. С использованием преобразований Цейтина строятся простейшие доказательства NP-полноты проблемы совместности системы логических уравнений степени 2 и $\#P$-полноты проблемы подсчёта числа выполняющих наборов для хорновской КНФ. С использованием преобразований Цейтина показывается также, что ROBDD-граф для булевой функции в хорновской КНФ или в КНФ с двухбуквенными дизъюнктами нельзя построить за полиномиальное время, если $P\neq NP$.