This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Convergence Properties of Optimization Algorithms for the SAT Problem
February 1996 (vol. 45 no. 2)
pp. 209-218
ASCII Text
x 
 
Jun Gu, Qian-Ping Gu, Ding-Zhu Du, "Convergence Properties of Optimization Algorithms for the SAT Problem," IEEE Transactions on Computers, vol. 45, no. 2, pp. 209-218, February, 1996.
 
 
BibTex
x
 
@article{ 10.1109/12.485373,
author = {Jun Gu and Qian-Ping Gu and Ding-Zhu Du},
title = {Convergence Properties of Optimization Algorithms for the SAT Problem},
journal ={IEEE Transactions on Computers},
volume = {45},
number = {2},
issn = {0018-9340},
year = {1996},
pages = {209-218},
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 - 0018-9340
SP209
EP218
EPD - 209-218
A1 - Jun Gu,
A1 - Qian-Ping Gu,
A1 - Ding-Zhu 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 (CNF) formula. A new formulation, the Universal SAT problem model, which transforms the SAT problem on Boolean space into an optimization problem on real space has been developed [27], [28], [30]. Many optimization techniques, such as the steepest descent method, Newton's method, and the coordinate descent method, can be used to solve the Universal SAT problem. In this paper, we prove that, when the initial solution is sufficiently close to the optimal solution, the steepest descent method has a linear convergence ratio β < 1, Newton's method has a convergence ratio of order two, and the convergence ratio of the steepest descent method is approximately (1 −β/m) for the Universal SAT problem with m variables. An algorithm based on the coordinate descent method for the Universal SAT problem is also presented in this paper. Experimental results show that this algorithm is more efficient than some previous ones in finding a solution for certain classes of the satisfiable CNF formulas.

[1] A.V. Aho,J.E. Hopcroft, and J.D. Ullman,The Design and Analysis of Computer Algorithms.Reading, Mass.: Addison-Wesley, 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. 1-16, 1992.
[3] B. Aspvall, M.F. Plass, and R.E. Tarjan, "A linear-time algorithm for testing the truth of certain quantified Boolean formulas," Information Processing Letters, vol. 8, no. 3, pp. 121-132, Mar. 1979.
[4] J.R. Bitner and E.M. Reingold, "Backtrack programming techniques," Comm. ACM, vol. 18, no. 11, pp. 651-656, 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. 633-645, 1986.
[6] M. Bohm and E. Speckenmeyer, "A fast parallel SAT-solver—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. 583-593, Aug. 1981.
[8] R.E. Bryant, "Graph-Based Algorithms for Boolean Function Manipulation," IEEE Trans. Computers, Vol. C-35, No. 8, Aug. 1986, pp. 667-690.
[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. 54-57, 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. 61-76, 1987.
[12] M.B. Clowes, "On seeing things," Artificial Intelligence, vol. 2, pp. 79-116, 1971.
[13] J.S. Conery, Parallel Execution of Logic Programs.Boston: Kluwer Academic, 1987.
[14] S. A. Cook,“The Complexity of Theorem-Proving 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. 394-397, 1962.
[16] M. Davis and H. Putnam, "A Computing Procedure for Quantification Theory," J. ACM, vol. 7, July 1960, pp. 201-215.
[17] N. Dershowitz, J. Hsiang, N. Josephson, and D. Plaisted, "Associative-commutative rewriting," Proc. IJCAI, pp. 940-944, 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 multi-commodity flow problems," SIAM J. Computing, vol. 5, no. 4, pp. 691-703, 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. 475-486, Oct. 1992.
[21] J. Franco, "Elimination of infrequent variables improves average case performance of satisfiability algorithms," SIAM J. Computing, vol. 20, pp. 1,119-1,127, 1991.
[22] Z. Galil, "On the complexity of regular resolution and the Davis-Putnam procedure," Theoretical Computer Science, pp. 23-46, 1977.
[23] M.R. Garey and D.S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness.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. 28-35, 1960.
[26] A. Goldberg, P.W. Purdom, and C.A. Brown, "Average time analysis of simplified Davis-Putnam procedures," Information Processing Letters, vol. 15, no. 2, pp. 72-75, Sept. 1982.
[27] J. Gu, "How to solve very large-scale satisfiability (VLSS) problems," Technical Report UCECE-TR-90-002, 1988.
[28] J. Gu, “Efficient Local Search for Very Large-Scale Satisfiability Problem,” SIGART Bulletin, vol. 3, no. 1, pp. 8-12, Jan. 1992.
[29] J. Gu, “Local Search for Satisfiability (SAT) Problem,” IEEE Trans. Systems, Man, and Cybernetics, vol. 23, no. 4, pp. 1108-1129, July 1993.
[30] J. Gu, "Global optimization for satisfiability (SAT) problem," IEEE Trans. Knowledge and Data Engineering, vol. 6, no. 3, pp. 361-381, 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. 72-154.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. 105-161. 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 UCECE-TR-91-004, 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. 857-865, 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. 816-831, 1987.
[38] P. Hansen and B. Jaumard, "Algorithms for the maximum satisfiability problem," Computing, vol. 44, pp. 279-303, 1990.
[39] J.N. Hooker, "Generalized resolution and cutting planes," Annals of Operations Research, vol. 12, pp. 217-239, 1988.
[40] J.N. Hooker, "A quantitative approach to logical inference," Decision Support Systems, vol. 4, pp. 45-69, 1988.
[41] J.N. Hooker, "Resolution vs. cutting plane solution of inference problems: Some computational experience," Operations Research Letter, vol. 7, no. 1, pp. 1-7, 1988.
[42] J.N. Hooker and C. Fedjki, "Branch-and-cut solution of inference problems in propositional logic," Technical Report 77-88-89, GSIA, Carnegie Mellon Univ., Aug. 1989.
[43] J. Hsiang, "Refutational theorem proving using term-rewriting systems," Artificial Intelligence, pp. 255-300, 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. 235-252, 1992.
[45] D.A. Huffman, "Impossible objects as nonsense sentences," B. Meltzer and D. Michie, eds., Machine Intelligence, pp. 295-323.Edinburgh: Edinburgh Univ. Press, 1971.
[46] K. Iwama, "CNF satisfiability test by counting and polynomial average time," SIAM J. Computing, pp. 385-391, 1989.
[47] R.E. Jeroslow and J. Wang, "Solving propositional satisfiability problems," Annals of Mathematics and AI, vol. 1, pp. 167-187, 1990.
[48] R.G. Jeroslow, "Computation-oriented reductions of predicate to propositional logic," Decision Support Systems, vol. 4, pp. 183-197, 1988.
[49] J.L. Johnson, "A neural network approach to the 3-satisfiability problem," J. Parallel and Distributed Computing, vol. 6, pp. 435-449, 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. 43-58, 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. 53-55, Aug.10, 1992.
[53] T. Larrabee, "Test Pattern Generation Using Boolean Satisfiability," IEEE Trans. Computer-Aided Design, pp. 6-22, 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: North-Holland, 1978.
[56] D.G. Luenberger, Linear and Nonlinear Programming.Reading, Mass.: Addison-Wesley, 1984.
[57] A.K. Mackworth, "Consistency in networks of relations," Artificial Intelligence, vol. 8, pp. 99-119, 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. 973-980, 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. 163-169, 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. 117-133, 1983.
[63] S.-C. Chau and A.L. Liestman, "A Proposal for a Fault-Tolerant Binary Hypercube Architecture," Proc. 19th Int'l Symp. Fault-Tolerant Computing, pp. 323-330, June 1989.
[64] P.W. Purdom and C.A. Brown, "The pure literal rule and polynomial average time," SIAM J. Computing, vol. 14, pp. 943-953, 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 MAX-SAT," Proc. Third Int'l Symp. Artificial Intelligence and Mathematics, Jan. 1994.
[67] J.A. Robinson,“A machine-oriented logic based on the resolution principle,” J. of the ACM, vol. 12, no. 1, pp. 23-41, 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. 216-226, 1978.
[70] B. Selman, H. Levesque, and D. Mitchell, "A new method for solving hard satisfiability problems," Proc. AAAI'92, pp. 440-446, July 1992.
[71] M.J. Shensa, "A computational structure for the propositional calculus," Proc. IJCAI, pp. 384-388, 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. Aix-Marseille II, 1987.
[74] R. Sosic and J. Gu, "How to search for million queens," Technical Report UUCS-TR-88-008, 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. 1572-1576, 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 n-Queens Problem,” IEEE Trans. Knowledge and Data Engineering, vol. 21, no. 5, pp. 661-668, 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 d-systems" 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. 115-125. 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 non-clausal propositional calculus," Information and Computation, vol. 79, no. 1, pp. 1-21, 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. 509-540, Apr. 1989.
[88] D. Waltz, “Generating Semantic Descriptions from Drawing of Scenes with Shadows,” Technical Report AI-TR-271, 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. 81-100, 1987.
[90] P.H. Winston, Artificial Intelligence. Reading, Mass.: Addison-Wesley, 1984.

Index Terms:
Conjunctive normal form (CNF), satisfiability (SAT) problem, optimization algorithm, nonlinear programming, convergence ratio, time complexity.
Citation:
Jun Gu, Qian-Ping Gu, Ding-Zhu Du, "Convergence Properties of Optimization Algorithms for the SAT Problem," IEEE Transactions on Computers, vol. 45, no. 2, pp. 209-218, Feb. 1996, doi:10.1109/12.485373
Usage of this product signifies your acceptance of the Terms of Use.