
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
Jun Gu, QianPing Gu, DingZhu Du, "Convergence Properties of Optimization Algorithms for the SAT Problem," IEEE Transactions on Computers, vol. 45, no. 2, pp. 209218, February, 1996.  
BibTex  x  
@article{ 10.1109/12.485373, author = {Jun Gu and QianPing Gu and DingZhu Du}, title = {Convergence Properties of Optimization Algorithms for the SAT Problem}, journal ={IEEE Transactions on Computers}, volume = {45}, number = {2}, issn = {00189340}, year = {1996}, pages = {209218}, doi = {http://doi.ieeecomputersociety.org/10.1109/12.485373}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Computers TI  Convergence Properties of Optimization Algorithms for the SAT Problem IS  2 SN  00189340 SP209 EP218 EPD  209218 A1  Jun Gu, A1  QianPing Gu, A1  DingZhu Du, PY  1996 KW  Conjunctive normal form (CNF) KW  satisfiability (SAT) problem KW  optimization algorithm KW  nonlinear programming KW  convergence ratio KW  time complexity. VL  45 JA  IEEE Transactions on Computers ER   
Abstract—The satisfiability (SAT) problem is a basic problem in computing theory. Presently, an active area of research on SAT problem is to design efficient algorithms to find a solution for a satisfiable conjunctive normal form (
[1] A.V. Aho,J.E. Hopcroft, and J.D. Ullman,The Design and Analysis of Computer Algorithms.Reading, Mass.: AddisonWesley, 1974.
[2] P. Ashar, A. Ghosh, and S. Devadas., "Boolean satisfiability and equivalence checking using general binary decision diagrams," Integration, the VLSI J., vol. 13, pp. 116, 1992.
[3] B. Aspvall, M.F. Plass, and R.E. Tarjan, "A lineartime algorithm for testing the truth of certain quantified Boolean formulas," Information Processing Letters, vol. 8, no. 3, pp. 121132, Mar. 1979.
[4] J.R. Bitner and E.M. Reingold, "Backtrack programming techniques," Comm. ACM, vol. 18, no. 11, pp. 651656, Nov. 1975.
[5] C.E. Blair, R.G. Jeroslow, and J.K. Lowe, "Some results and experiments in programming techniques for propositional logic," Computers and Operations Research, vol. 55, pp. 633645, 1986.
[6] M. Bohm and E. Speckenmeyer, "A fast parallel SATsolver—efficient workload balancing," Proc. Third Int'l Symp. Artificial Inteligence and Mathematics, Jan. 1994.
[7] C.A. Brown and P.W. Purdom, "An average time analysis of backtracking," SIAM J. Computing, vol. 10, no. 3, pp. 583593, Aug. 1981.
[8] R.E. Bryant, "GraphBased Algorithms for Boolean Function Manipulation," IEEE Trans. Computers, Vol. C35, No. 8, Aug. 1986, pp. 667690.
[9] K. Bugrara and P. Purdom, "Clause order backtracking," Technical Report 311, 1990.
[10] S. Chakradhar, V. Agrawal, and M. Bushnell, "Neural net and Boolean satisfiability model of logic circuits," IEEE Design&Test of Computers, pp. 5457, Oct. 1990.
[11] W.T. Chen and L.L. Liu, "Parallel approach for theorem proving in propositional logic," Information Science, vol. 41, no. 1, pp. 6176, 1987.
[12] M.B. Clowes, "On seeing things," Artificial Intelligence, vol. 2, pp. 79116, 1971.
[13] J.S. Conery, Parallel Execution of Logic Programs.Boston: Kluwer Academic, 1987.
[14] S. A. Cook,“The Complexity of TheoremProving Procedures,”Proc. 3rd Ann. ACM Symposium on Theory of Computing,New York: Association for Computing Machinery, 1971, pp. 151–155.
[15] M. Davis, G. Logemann, and D. Loveland, "A machine program for theorem proving," Comm. ACM, vol. 5, pp. 394397, 1962.
[16] M. Davis and H. Putnam, "A Computing Procedure for Quantification Theory," J. ACM, vol. 7, July 1960, pp. 201215.
[17] N. Dershowitz, J. Hsiang, N. Josephson, and D. Plaisted, "Associativecommutative rewriting," Proc. IJCAI, pp. 940944, 1983.
[18] D.Z. Du., Convergence Theory of Feasible Direction Methods.New York: Science Press, 1991.
[19] S. Even, A. Itai, and A. Shamir, "On the complexity of timetable and multicommodity flow problems," SIAM J. Computing, vol. 5, no. 4, pp. 691703, 1976.
[20] M.Y. Fang and W.T. Chen, "Vectorization of a generalized procedure for theorem proving in propositional logic on vector computers," IEEE Trans. Knowledge and Data Engineering, vol. 4, no. 5, pp. 475486, Oct. 1992.
[21] J. Franco, "Elimination of infrequent variables improves average case performance of satisfiability algorithms," SIAM J. Computing, vol. 20, pp. 1,1191,127, 1991.
[22] Z. Galil, "On the complexity of regular resolution and the DavisPutnam procedure," Theoretical Computer Science, pp. 2346, 1977.
[23] M.R. Garey and D.S. Johnson, Computers and Intractability: A Guide to the Theory of NPCompleteness.New York: W.H. Freeman, 1979.
[24] M.R. Genesereth and N.J. Nilsson,Logical foundations of artificial intelligence, Morgan Kaufmann, Los Altos, CA, 1987.
[25] P.C. Gilmore, "A proof method for quantification theory," IBM J. Research and Development, vol. 4, pp. 2835, 1960.
[26] A. Goldberg, P.W. Purdom, and C.A. Brown, "Average time analysis of simplified DavisPutnam procedures," Information Processing Letters, vol. 15, no. 2, pp. 7275, Sept. 1982.
[27] J. Gu, "How to solve very largescale satisfiability (VLSS) problems," Technical Report UCECETR90002, 1988.
[28] J. Gu, “Efficient Local Search for Very LargeScale Satisfiability Problem,” SIGART Bulletin, vol. 3, no. 1, pp. 812, Jan. 1992.
[29] J. Gu, “Local Search for Satisfiability (SAT) Problem,” IEEE Trans. Systems, Man, and Cybernetics, vol. 23, no. 4, pp. 11081129, July 1993.
[30] J. Gu, "Global optimization for satisfiability (SAT) problem," IEEE Trans. Knowledge and Data Engineering, vol. 6, no. 3, pp. 361381, June 1994.
[31] J. Gu, "Optimization algorithms for the satisfiability (SAT) problem," Advances in Optimization and Approximation, D.Z. Du and J. Sun, eds., pp. 72154.Boston: Kluwer Academic, 1994.
[32] J. Gu, "Parallel processing for satisfiability (SAT) problem (invited paper)," DIMACS Volume Series Discrete Mathematics and Theoretical Computer Science, vol. 22, Parallel Processing on Discrete Optimization Problems, pp. 105161. American Mathematical Society Press, 1995.
[33] J. Gu and Q.P. Gu, "Average time complexities of several local search algorithms for the satisfiability problem," Technical Report UCECETR91004, 1991, to appear in IEEE Trans. Knowledge and Data Engineering.
[34] J. Gu, X. Huang, and B. Du, "A quantitative solution to constraint satisfaction," New Generation Computing, vol. 13, no. 1, Nov. 1994.
[35] J. Gu, P.W. Purdom, J. Franco, and B.W. Wah, "Algorithms for satisfiability (SAT) problem: A survey (invited paper)," to appear in DIMACS Volume Series on Discrete Mathematics and Theoretical Computer Science: The Satisfiability (SAT) Problem. American Mathematical Society Press, 1996.
[36] J. Gu and W. Wang, "A novel discrete relaxation architecture," IEEE Trans. Pattern Analysis and Machine Intelligence, vol. 14, no. 8, pp. 857865, Aug. 1992.
[37] J. Gu, W. Wang, and T.C. Henderson, "A Parallel Architecture for Discrete Relaxation Algorithm," IEEE Trans. Pattern Analysis and Machine Intelligence, vol. 9, no. 6, pp. 816831, 1987.
[38] P. Hansen and B. Jaumard, "Algorithms for the maximum satisfiability problem," Computing, vol. 44, pp. 279303, 1990.
[39] J.N. Hooker, "Generalized resolution and cutting planes," Annals of Operations Research, vol. 12, pp. 217239, 1988.
[40] J.N. Hooker, "A quantitative approach to logical inference," Decision Support Systems, vol. 4, pp. 4569, 1988.
[41] J.N. Hooker, "Resolution vs. cutting plane solution of inference problems: Some computational experience," Operations Research Letter, vol. 7, no. 1, pp. 17, 1988.
[42] J.N. Hooker and C. Fedjki, "Branchandcut solution of inference problems in propositional logic," Technical Report 778889, GSIA, Carnegie Mellon Univ., Aug. 1989.
[43] J. Hsiang, "Refutational theorem proving using termrewriting systems," Artificial Intelligence, pp. 255300, 1985.
[44] T.H. Hu, C.Y. Tang, and R.C.T. Lee, "An average case analysis of a resolution principle algorithm in mechanical theorem proving," Annals of Mathematics and Artificial Intelligence, vol. 6, pp. 235252, 1992.
[45] D.A. Huffman, "Impossible objects as nonsense sentences," B. Meltzer and D. Michie, eds., Machine Intelligence, pp. 295323.Edinburgh: Edinburgh Univ. Press, 1971.
[46] K. Iwama, "CNF satisfiability test by counting and polynomial average time," SIAM J. Computing, pp. 385391, 1989.
[47] R.E. Jeroslow and J. Wang, "Solving propositional satisfiability problems," Annals of Mathematics and AI, vol. 1, pp. 167187, 1990.
[48] R.G. Jeroslow, "Computationoriented reductions of predicate to propositional logic," Decision Support Systems, vol. 4, pp. 183197, 1988.
[49] J.L. Johnson, "A neural network approach to the 3satisfiability problem," J. Parallel and Distributed Computing, vol. 6, pp. 435449, 1989.
[50] A.P. Kamath, N.K. Karmarkar, K.G. Ramakrishnan, and M.G.C. Resende, "Computational experience with an interior point algorithm on the satisfiability problem," Annals of Operations Research, vol. 25, pp. 4358, 1990.
[51] A.P. Kamath, N.K. Karmarkar, K.G. Ramakrishnan, and M.G.C. Resende, "Computational experience with an interior point algorithm on the satisfiability problem," Working paper. Mathematical Sciences Research Center, AT&T Bell Laboratories, Oct. 1989.
[52] E. Koutsoupias and C.H. Papadimitriou, "On the greedy algorithm for satisfiability," Information Processing Letters, vol. 43, pp. 5355, Aug.10, 1992.
[53] T. Larrabee, "Test Pattern Generation Using Boolean Satisfiability," IEEE Trans. ComputerAided Design, pp. 622, Jan. 1992.
[54] Y.J. Lin, "A parallel implementation of logic programs," PhD thesis, Univ. of Texas at Austin, Dept. of Computer Science, May 1988.
[55] D.W. Loveland, Automated Theorem Proving: A Logical Basis.Amsterdam: NorthHolland, 1978.
[56] D.G. Luenberger, Linear and Nonlinear Programming.Reading, Mass.: AddisonWesley, 1984.
[57] A.K. Mackworth, "Consistency in networks of relations," Artificial Intelligence, vol. 8, pp. 99119, 1977.
[58] J.T. McCall, J.G. Tront, F.G. Gray, R.M. Haralick, and W.M. McCormack, "Parallel computer architectures and problem solving strategies for the consistent labeling problem," IEEE Trans. Computers, vol. 34, no. 11, pp. 973980, Nov. 1985.
[59] N.J. Nilsson, Principles of Artificial Intelligence. Morgan Kaufmann, 1980.
[60] C.H. Papadimitriou, "On selecting a satisfying truth assignment," Proc. 32nd Ann. Symp. Foundations of Computer Science, pp. 163169, 1991.
[61] C.H. Papadimitriu and K. Steiglitz, Combinatorial Optimization: Algorithms and Complexity. Prentice Hall, 1987.
[62] P.W. Purdom, "Search rearrangement backtracking and polynomial average time," Artificial Intelligence, vol. 21, pp. 117133, 1983.
[63] S.C. Chau and A.L. Liestman, "A Proposal for a FaultTolerant Binary Hypercube Architecture," Proc. 19th Int'l Symp. FaultTolerant Computing, pp. 323330, June 1989.
[64] P.W. Purdom and C.A. Brown, "The pure literal rule and polynomial average time," SIAM J. Computing, vol. 14, pp. 943953, 1985.
[65] P.W. Purdom and G.N. Haven, "Backtracking and probing," Technical Report No. 387, Dept. of Computer Science, Indiana Univ., Aug. 1993.
[66] M. Resende and T. Feo, "A GRASP for MAXSAT," Proc. Third Int'l Symp. Artificial Intelligence and Mathematics, Jan. 1994.
[67] J.A. Robinson,“A machineoriented logic based on the resolution principle,” J. of the ACM, vol. 12, no. 1, pp. 2341, Jan. 1965.
[68] A. Samal and T.C. Henderson, "Parallel consistent labeling algorithms," Int'l J. Parallel Programming, 1988.
[69] T.J. Schaefer, "The Complexity of Satisfiability Problems," Proc. 10th Ann. Symp. Theory of Computing, pp. 216226, 1978.
[70] B. Selman, H. Levesque, and D. Mitchell, "A new method for solving hard satisfiability problems," Proc. AAAI'92, pp. 440446, July 1992.
[71] M.J. Shensa, "A computational structure for the propositional calculus," Proc. IJCAI, pp. 384388, 1989.
[72] R.C.J. Shi, "An improvement on Karmarkar's algorithm for integer programming," June 1992.
[73] P. Siegel, "Representation et utilization de la connaissances en calcul propositionel," PhD thesis, Univ. AixMarseille II, 1987.
[74] R. Sosic and J. Gu, "How to search for million queens," Technical Report UUCSTR88008, Dept. of Computer Science, Univ. of Utah, Feb. 1988.
[75] R. Sosic and J. Gu, “Efficient Local Search with Conflict Minimation,” IEEE Trans. Systems, Man, and Cybernetics, vol. 21, no. 6, pp. 15721576, Nov./Dec. 1991.
[76] R. Sosic and J. Gu, "A parallel local search algorithm for satisfiability (SAT) problem," submitted for publication, 1993.
[77] R. Sosic and J. Gu, “Fast Search Algorithms for the nQueens Problem,” IEEE Trans. Knowledge and Data Engineering, vol. 21, no. 5, pp. 661668, Oct. 1994.
[78] R. Sosic, J. Gu, and R. Johnson, "The Unison algorithm: Fast evaluation of Boolean expressions," Comm. ACM, accepted for publication in 1992.
[79] R. Sosic, J. Gu, and R. Johnson, "A universal Boolean evaluator," IEEE Trans. Computers, accepted for publication in 1992.
[80] G. Strang, Linear Algebra and Its Applications.New York: Academic Press, 1976.
[81] K. Truemper, "Polynomial algorithms for problems over dsystems" Proc. Third Int'l Symp. Artificial Intelligence and Mathematics, Jan. 1994.
[82] G.S. Tseitin, "On the complexity of derivations in propositional calculus," Structures in Constructive Mathematics and Mathematical Logic, Part II, A.O. Slisenko, ed., pp. 115125. 1968.
[83] J.E. Tyler, "Parallel computer architectures and problem solving strategies for the consistent labeling problem," Master's thesis, Dept. of Electrical Eng., Virginia Polytechnic Inst. State Univ., Blacksburg, Va.., Oct. 1983.
[84] A. Van Gelder, "A satisfiability tester for nonclausal propositional calculus," Information and Computation, vol. 79, no. 1, pp. 121, Oct. 1988.
[85] B. Wah and G.J. Li, Computers for Artificial Intelligence Applications.Washington D.C.: IEEE CS Press, 1986.
[86] B.W. Wah, ed., "New computers for artificial intelligence processing," Computer, vol. 20, no. 1, Jan. 1987.
[87] B.W. Wah, M.B. Lowrie, and G.J. Li, "Computers for symbolic processing," Proc. IEEE, vol. 77, no. 4, pp. 509540, Apr. 1989.
[88] D. Waltz, “Generating Semantic Descriptions from Drawing of Scenes with Shadows,” Technical Report AITR271, Massachusetts Inst. Tech nology, 1972.
[89] H.P. Williams, "Linear and integer programming applied to the propositional calculus," Systems Research and Information Sciences, vol. 2, pp. 81100, 1987.
[90] P.H. Winston, Artificial Intelligence. Reading, Mass.: AddisonWesley, 1984.