About Tseitin transformation in logical equations

A. A. Semenov

Prikladnaâ diskretnaâ matematika, no. 4 (2009), pp. 28-50.

Résumé

The paper is devoted to the applications of Tseitin transformations in some propositional 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 Horne CNF are constructed too. By using Tseitin transformations, it is also shown that the ROBDD for any Boolean function given in a Horne CNF or in a CNF with 2-literal disjuncts may not be build for a polynomial time if $P\neq NP$.

Détail

Keywords: logical equations, Tseitin transformations, propositional proof systems, NP-completeness.

Bibliographie

[1] Tseitin G. S., “O slozhnosti vyvoda v ischislenii vyskazyvanii”, Zapiski nauchnykh seminarov LOMI AN SSSR, 8, 1968, 234–259 | MR | Zbl

[2] Dantsin E. Ya., “Algoritmika zadachi vypolnimosti”, Voprosy kibernetiki. Problemy sokrascheniya perebora, AN SSSR, M., 1987, 7–29 | MR

[3] Waisberg M., “Untersuchungen uber den Aussagen kalkul von Heyting”, Wiadom. Matemat., 46 (1938), 45–101

[4] Tseitin G., “On the complexity of derivation in propositional calculus”, Automat. Reasoning, 2 (1983), 466–483

[5] Plaisted D., Greenbaum S., “A Structure-preserving Clause Form Translation”, J. Symb. Comput., 2 (1986), 293–304 | DOI | MR | Zbl

[6] Groote J. F., Zantema H., “Resolution and binary decision diagrams cannot simulate each other polynomially”, J. Discr. Appl. Math., 130:2 (2003), 157–171 | DOI | MR | Zbl

[7] Een N., Sorensson N., “Translating Pseudo-Boolean Constraints into SAT”, J. Satisf. Boolean Mod. Comp., 2 (2006), 1–25

[8] Semenov A. A., Zaikin O. S., Bespalov D. V., Ushakov A. A., “SAT-podkhod v kriptoanalize nekotorykh sistem potochnogo shifrovaniya”, Vychislitelnye tekhnologii, 13:6 (2008), 134–150

[9] Semenov A. A., “O preobrazovaniyakh Tseitina v logicheskikh uravneniyakh”, Prikladnaya diskretnaya matematika, Prilozhenie No 1 (2009), 12–13

[10] Yablonskii S. V., Vvedenie v diskretnuyu matematiku, Nauka, M., 1986, 384 pp. | MR

[11] Cook S. A., “The complexity of theorem-proving procedures”, Proc. 3rd Ann. ACM Symp. on Theory of Computing, ACM, 1971, 151–159; Kuk S. A., “Slozhnost protsedur vyvoda teorem”, Kiberneticheskii sbornik. Novaya seriya, 12, 1975, 5–15

[12] Geri M., Dzhonson D., Vychislitelnye mashiny i trudnoreshaemye zadachi, Mir, M., 1982 | MR

[13] Razborov A. A., “Proof Complexity of Pigeonhole Principles”, LNCS, 2295, 2002, 100–116 | MR | Zbl

[14] Cook S. A., Reckhow R., “The relative efficiency of propositional proof systems”, J. Symb. Logic, 44 (1979), 239–251 | DOI | MR

[15] Robinson J. A., “A machine-oriented logic based on the resolution principle”, J. ACM, 12:1 (1965), 23–41 ; Robinson Dzh. A., “Mashinno-orientirovannaya logika, osnovannaya na printsipe rezolyutsii”, Kiberneticheskii sbornik. Novaya seriya, 7, 1970, 194–218 | DOI | MR | Zbl | Zbl

[16] Chen Ch., Li R., Matematicheskaya logika i avtomaticheskoe dokazatelstvo teorem, Nauka, M., 1983, 360 pp. | MR | Zbl

[17] Haken A., “The intractability of resolution”, Theor. Comp. Sci., 39 (1985), 297–308 ; Khaken A., “Trudnoreshaemost rezolyutsii”, Kiberneticheskii sbornik. Novaya seriya, 28, 1991, 179–194 | DOI | MR | Zbl | Zbl

[18] Buss S. R., Turan G., “Resolution proofs of generalized pigeonhole principles”, Theoret. Comp. Sci., 62 (1988), 311–317 ; Bass S. R., Turan D., “Dokazatelstvo obobschennogo printsipa Dirikhle metodom rezolyutsii”, Kiberneticheskii sbornik. Novaya seriya, 28, 1991, 195–203 | DOI | MR | Zbl | Zbl

[19] Lee C. Y., “Representation of Switching Circuits by Binary-Decision Programs”, Bell Syst. Techn. J., 38 (1959), 985–999 | MR

[20] Bryant R. E., “Graph-Based Algorithms for Boolean Function Manipulation”, IEEE Trans. Comp., 35:8 (1986), 677–691 | DOI | Zbl

[21] Meinel Ch., Theobald T., Algorithms and Data Structures in VLSI-Design: OBDD-Foundations and Applications, Springer Verlag, Berlin–Heidelberg–New York, 1998

[22] Semenov A. A., Ignatev A. S., “Logicheskie uravneniya i dvoichnye diagrammy reshenii”, Prikladnye algoritmy v diskretnom analize, Diskretnyi analiz i informatika, 2, Izd-vo Irk. un-ta, Irkutsk, 2008, 99–126

[23] Marqeus-Silva J. P., Sakallah K A., “GRASP: A search algorithm for propositional satisfiability”, IEEE Trans. Comp., 48:5 (1999), 506–521 | DOI | MR

[24] Ben-Sasson E., Wigderson A., “Short proofs are narrow – resolution made simple”, Proc. of 31st Ann. ACM Symposium on Theory of Computing, 1999, 517–526 | MR

[25] Semenov A. A., “Konservativnye preobrazovaniya sistem logicheskikh uravnenii”, Vestnik Tomskogo gosuniversiteta. Prilozhenie, 2007, no. 23, 52–59

[26] Tei A., Gribomon P., Lui Zh. i dr., Logicheskii podkhod k iskusstvennomu intellektu, Mir, M., 1991, 429 pp.

[27] Gorshkov S. P., “Primenenie teorii NP-polnykh zadach dlya otsenki slozhnosti resheniya sistem bulevykh uravnenii”, Obozrenie prikladnoi i promyshlennoi matematiki, 2:3 (1995), 325–398 | MR

[28] Agibalov G. P., Diskretnye avtomaty na polureshetkakh, Izd-vo Tom. un-ta, Tomsk, 1993 | Zbl

[29] Cheremisinova L. D., Novikov D. Ya., “Proverka skhemnoi realizatsii chastichnykh bulevykh funktsii”, Vestnik Tomskogo gosuniversiteta. Upravlenie, vychislitelnaya tekhnika, informatika, 2008, no. 4(5), 102–111

[30] Semenov A. A., “Translyatsiya algoritmov vychisleniya diskretnykh funktsii v vyrazheniya propozitsionalnoi logiki”, Prikladnye algoritmy v diskretnom analize, Diskretnyi analiz i informatika, 2, Izd-vo Irk. un-ta, Irkutsk, 2008, 70–98

[31] Katlend N., Vychislimost. Vvedenie v teoriyu rekursivnykh funktsii, Mir, M., 1983 | MR

[32] http://www.satlive.org

[33] Zaikin O. S., Semenov A. A., “Tekhnologiya krupnoblochnogo parallelizma v SAT-zadachakh”, Problemy upravleniya, 2008, no. 1, 43–50

[34] Semenov A. A., Zaikin O. S., “Nepolnye algoritmy v krupnoblochnom parallelizme kombinatornykh zadach”, Vychislitelnye metody i programmirovanie, 9 (2008), 108–118

[35] Semenov A. A., Zaikin O. S., Bespalov D. V. i dr., “Reshenie zadach obrascheniya diskretnykh funktsii na mnogoprotsessornykh vychislitelnykh sistemakh”, Trudy Chetvertoi Mezhdunar. konf., PACO'2008 (Moskva, 26–29 oktyabrya 2008), M., 2008, 152–176

[36] Valiant L. G., “The complexity of computing the permanent”, Theor. Comp. Sci., 8 (1979), 189–202 | DOI | MR

[37] Stockmeyer L., “Classifying of computational complexity of problems”, J. Symb. Logic, 52:1 (1987), 1–43 ; Stokmeier L., “Klassifikatsiya vychislitelnoi slozhnosti problem”, Kiberneticheskii sbornik. Novaya seriya, 26, 1989, 20–83 | DOI | MR | Zbl

[38] Valiant L. G., “The complexity of enumeration and reliability problems”, SIAM J. Comp., 8 (1979), 410–421 | DOI | MR | Zbl

[39] Gorshkov S. P., “O slozhnosti zadachi nakhozhdeniya chisla reshenii sistem bulevykh uravnenii”, Diskretnaya matematika, 8:1 (1996), 72–85 | MR | Zbl