В статье сообщается о применении преобразований Цейтина в различных областях пропозициональной логики, связанных с решением систем логических уравнений. Показывается, что преобразования Цейтина не изменяют числа решений системы логических уравнений, и строится биекция между множествами решений системы и результата её преобразований по Цейтину. Приводятся некоторые результаты по применению преобразований Цейтина к построению оценок сложности систем пропозиционального вывода. С использованием преобразований Цейтина строятся простейшие доказательства NP-полноты проблемы совместности системы логических уравнений степени 2 и #Р-полноты проблемы подсчёта числа выполняющих наборов для хорновской КНФ. С использованием преобразований Цейтина показывается также, что ROBDD-граф для булевой функции в хорновской КНФ или в КНФ с двухбуквенными дизъюнктами нельзя построить за полиномиальное время, если Р ≠ NP.
Скачать электронную версию публикации
Загружен, раз: 165
- Title О ПРЕОБРАЗОВАНИЯХ ЦЕЙТИНА В ЛОГИЧЕСКИХ УРАВНЕНИЯХ
- Headline О ПРЕОБРАЗОВАНИЯХ ЦЕЙТИНА В ЛОГИЧЕСКИХ УРАВНЕНИЯХ
- Publesher
Tomsk State University - Issue Прикладная дискретная математика 4(6)
- Date:
- DOI
Ключевые слова
NP-completeness , propositional proof systems , Tseitin transformations , logical equations , NP-полнота , системы пропозиционального вывода , преобразования Цейтина , логические уравнения Авторы
Ссылки
Valiant L. G. The complexity of enumeration and reliability problems // SIAM J. Сотр. 1979. V.8. P. 410-421.
Горшков С. П. О сложности задачи нахождения числа решений систем булевых уравнений // Дискретная математика. 1996. №8:1. С. 72-85.
Стокмейер Л. Классификация вычислительной сложности проблем // Кибернетический сборник. Новая серия. 1989. Вып. 26. С. 20-83.
Valiant L. G. The complexity of computing the permanent // Theor. Сотр. Sci. 1979. V. 8. P. 189-202.
Stockmeyer L. Classifying of computational complexity of problems // J. Symb. Logic. 1987. V. 52. No. 1. P. 1-43.
Семенов А. А., Заикин О. С., Беспалов Д. В. и др. Решение задач обращения дискретных функций на многопроцессорных вычислительных системах // Труды Четвертой Междунар. конф. РАСО'2008 (Москва, 26-29 октября 2008). М., 2008. С. 152-176.
Семенов А. А., Заикин О. С. Неполные алгоритмы в крупноблочном параллелизме комбинаторных задач // Вычислительные методы и программирование. 2008. Т. 9. С. 108-118.
Катленд Н. Вычислимость. Введение в теорию рекурсивных функций. М.: Мир, 1983.
<http://www.satlive.org>
Заикин О. С., Семенов А. А. Технология крупноблочного параллелизма в SAT-задачах // Проблемы управления. 2008. №1. С. 43-50.
Семенов А. А. Трансляция алгоритмов вычисления дискретных функций в выражения пропозициональной логики // Прикладные алгоритмы в дискретном анализе. Сер. Дискретный анализ и информатика. Вып. 2. Иркутск: Изд-во Ирк. ун-та, 2008. С. 70-98.
Черемисинова Л. Д., Новиков Д. Я. Проверка схемной реализации частичных булевых функций // Вестник Томского госуниверситета. Управление, вычислительная техника, информатика. 2008. №.4 (5). С. 102-111.
Агибалов Г. П. Дискретные автоматы на полурешетках. Томск: Изд-во Том. ун-та, 1993.
Горшков С. П. Применение теории NP-полных задач для оценки сложности решения систем булевых уравнений // Обозрение прикладной и промышленной математики. 1995. Т. 2. Вып.З. С. 325-398.
Тей А., Грибомон П., Луи Ж. и др. Логический подход к искусственному интеллекту. М.: Мир, 1991. 429 с.
Семенов А. А. Консервативные преобразования систем логических уравнений // Вестник Томского госуниверситета. Приложение. 2007. №23. С. 52-59.
Ben-Sasson E., Wigderson A. Short proofs are narrow - resolution made simple // Proc. of 31st Ann. ACM Symposium on Theory of Computing. 1999. P. 517-526.
Marqeus-Silva J. P., Sakallah K.A. GRASP: A search algorithm for propositional satisfiability // IEEE Trans. Сотр. 1999. V. 48. No. 5. P. 506-521.
Семенов А. А., Игнатьев А. С. Логические уравнения и двоичные диаграммы решений // Прикладные алгоритмы в дискретном анализе. Сер. Дискретный анализ и информатика. Вып. 2. Иркутск: Изд-во Ирк. ун-та, 2008. С. 99-126.
Meinel Ch., Theobald T. Algorithms and Data Structures in VLSI-Design: OBDD-Foundations and Applications. Berlin; Heidelberg; New York: Springer Verlag, 1998.
Lee С. Y. Representation of Switching Circuits by Binary-Decision Programs // Bell Syst. Techn. J. 1959. No. 38. P. 985-999.
Bryant R. E. Graph-Based Algorithms for Boolean Function Manipulation // IEEE Trans. Сотр. 1986. No. 35(8). P. 677-691.
Басс С. Р., Туран Д. Доказательство обобщенного принципа Дирихле методом резолюций // Кибернетический сборник. Новая серия. 1991. Вып. 28. С. 195-203.
Buss S. R., Turan G. Resolution proofs of generalized pigeonhole principles // Theoret. Сотр. Sci. 1988. No. 62. P. 311-317.
Хакен А. Труднорешаемость резолюций // Кибернетический сборник. Новая серия. 1991. Вып. 28. С. 179-194.
Haken A. The intractability of resolution // Theor. Сотр. Sci. 1985. No. 39. P. 297-308.
Робинсон Дж. А. Машинно-ориентированная логика, основанная на принципе резолюций // Кибернетический сборник. Новая серия. 1970. Вып. 7. С. 194-218.
Ченъ Ч., Ли Р. Математическая логика и автоматическое доказательство теорем. М.: Наука, 1983. 360 с.
Robinson J. A. A machine-oriented logic based on the resolution principle // J. ACM. 1965. V. 12. No. 1. P. 23-41.
Razborov A. A. Proof Complexity of Pigeonhole Principles // LNCS. 2002.V. 2295. P. 100-116.
Cook S. A., Reckhow R. The relative efficiency of propositional proof systems // J. Symb. Logic. 1979. V.44. P. 239-251.
Кук С. А. Сложность процедур вывода теорем // Кибернетический сборник. Новая серия. 1975. Вып. 12. С. 5-15.
Гэри М., Джонсон Д. Вычислительные машины и труднорешаемые задачи. М.: Мир, 1982.
Cook S. A. The complexity of theorem-proving procedures // Proc. 3rd Ann. ACM Symp. on Theory of Computing. ACM, 1971. P. 151-159.
Яблонский С.В. Введение в дискретную математику. М.: Наука, 1986. 384 с.
Семенов А. А. О преобразованиях Цейтина в логических уравнениях // Прикладная дискретная математика. Приложение. 2009. №1. С. 12-13.
Семенов А. А., Заикин О. С., Беспалов Д. В., Ушаков А. А. SAT-подход в криптоанализе некоторых систем поточного шифрования // Вычислительные технологии. 2008. Т. 13. №6. С. 134-150.
Een N., Sorensson N. Translating Pseudo-Boolean Constraints into SAT // J. Satisf., Boolean Mod. Сотр. 2006. No. 2. P. 1-25.
Groote J. F., Zantema H. Resolution and binary decision diagrams cannot simulate each other polynomially // J. Discr. Appl. Math. 2003. No. 130:2. P. 157-171.
Plaisted D., Greenbaum S. A Structure-preserving Clause Form Translation // J. Symb. Comput. 1986. V.2. P. 293-304.
Tseitin G. On the complexity of derivation in propositional calculus // Automat. Reasoning. 1983. V.2. P. 466-483.
Waisberg M. Untersuchungen uber den Aussagen kalkul von Heyting // Wiadom. Matemat. 1938. No. 46. P. 45-101.
Данцин Е. Я. Алгоритмика задачи выполнимости // Вопросы кибернетики. Проблемы сокращения перебора. М.: АН СССР, 1987. С. 7-29.
Цейтин Г. С. О сложности вывода в исчислении высказываний // Записки научных семинаров ЛОМИ АН СССР. 1968. Т. 8. С. 234-259.
О ПРЕОБРАЗОВАНИЯХ ЦЕЙТИНА В ЛОГИЧЕСКИХ УРАВНЕНИЯХ | Прикладная дискретная математика. 2009. № 4(6).
Скачать полнотекстовую версию
Полнотекстовая версияЗагружен, раз: 279