The paper is devoted to the applications of Tseitin transformations in some prepositional logics areas connected with the systems of logical equations. It is shown that Tseitin transformations of the system of logical equations do not change the number of its solutions and a bijection is pointed between the solutions of the system and its transformation result. Some results related to the usage of Tseitin transformations in obtaining bounds for the complexity of the propositional proof systems are given. By using Tseitin transformations, the simplest proofs of the NP-completeness problem for the solvability of a 2-degree logical equations system and of the #P-completeness problem for counting the number of satisfying assignments for any Home CNF are constructed too. By using Tseitin transformations, it is also shown that the ROBDD for any Boolean function given in a Home CNF or in a CNF with 2-literal disjuncts may not be build for a polynomial time if P ≠ NP
Download file
Counter downloads: 166
- Title ABOUT TSEITIN TRANSFORMATION IN LOGICAL EQUATIONS
- Headline ABOUT TSEITIN TRANSFORMATION IN LOGICAL EQUATIONS
- Publesher
Tomsk State University - Issue Prikladnaya Diskretnaya Matematika - Applied Discrete Mathematics 4(6)
- Date:
- DOI
Keywords
NP-completeness , propositional proof systems , Tseitin transformations , logical equations , NP-полнота , системы пропозиционального вывода , преобразования Цейтина , логические уравнения Authors
References
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.
ABOUT TSEITIN TRANSFORMATION IN LOGICAL EQUATIONS | Prikladnaya Diskretnaya Matematika - Applied Discrete Mathematics. 2009. № 4(6).
Download full-text version
Download fileCounter downloads: 281