Abstract
Recently algorithms for solving propositional satisfiability problem, or SAT, have aroused great interest, and more attention has been paid to transformation problem solving. The commonly used transformation is representation transform, but since its intermediate computing procedure is a black box from the viewpoint of the original problem, this approach has many limitations. In this paper, a new approach called algorithm transform is proposed and applied to solving SAT by Wu’s method, a general algorithm for solving polynomial equations. By establishing the correspondence between the primitive operation in Wu’s method and clause resolution in SAT, it is shown that Wu’s method, when used for solving SAT, is primarily a restricted clause resolution procedure. While Wu’s method introduces entirely new concepts, e.g. characteristic set of clauses, to resolution procedure, the complexity result of resolution procedure suggests an exponential lower bound to Wu’s method for solving general polynomial equations. Moreover, this algorithm transform can help achieve a more efficient implementation of Wu’s method since it can avoid the complex manipulation of polynomials and can make the best use of domain specific knowledge.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
Davis M, Logemann G, Loveland D. A machine program for theorem proving.Communications of the ACM, 1962, 5: 394–397.
Robinson J A. A machine-oriented logic based on the resolution principle.Journal of the ACM, 1965, 12(1): 23–41.
Wu W. Basic principles of mechanical theorem proving in geometries.,Journal of Automated Reasoning, 1986, 2: 221–252.
Kapur D, Kakshman Y N. Elimination Theory: An Introduction. Chapter 2 in Symbolic and Numerical Computation for Artificial Intelligence, Academic Press, 1992.
He Simin. The Design and Analysis of Algorithms for Satisfiability Problem. Ph.D. dissertation, Department of Computer Science and Technology, Tsinghua University, 1997.
Kapur D, Narendran P. An equational approach to theorem proving in first-order predicate calculus. InProceedings of the Ninth International Joint Conference on Aetificial Intelligence (IJCAI-85), Los Angeles, California, 1985, pp.1146–1153.
Wos L. Automated Reasoning: 33 Basic Research Problems. Prentice Hall, 1988.
Slagle J. Automatic theorem proving with renamable and semantic resolution.Journal of the ACM, 1967, 14: 687–697.
Haken A. The intractability of resolution.Theoretical Computer Science, 1985, 39: 297–308.
Mitchell D, Selman B, Levesque H. Hard and easy distribution of SAT problems. InProceedings of the Tenth National Conference on Artificial Intelligence (AAAI-92), San Jose, CA, July 1992, pp.459–465.
Selman B, Levesque H, Mitchell D. A new method for solving hard satisfiability problems. InProceedings of AAAI-92, San Jose, CA, July 1992, pp. 440–446.
Author information
Authors and Affiliations
Additional information
This work is supported by National Natural Science Foundation of China.
HE Simin was born in 1968 and had been studying in the Department of Computer Science and Technology, Tsinghua University since 1986 and received Ph.D. degree in 1997. His research interests include algorithmics, especially experimental algorithmics, and their applications.
ZHANG Bo was born in 1935 and is a Professor in the Department of Computer Science and Technology, Tsinghua University. He is a member of the Chinese Academy of Sciences and a Foreign Fellow of Russian Academy of Sciences. His research interests are foundation of artificial intelligence, including the theory and application of problem solving, artificial neural networks.
Rights and permissions
About this article
Cite this article
He, S., Zhang, B. Solving SAT by algorithm transform of Wu’s method. J. Comput. Sci. & Technol. 14, 468–480 (1999). https://doi.org/10.1007/BF02948788
Issue Date:
DOI: https://doi.org/10.1007/BF02948788