This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Global Optimization for Satisfiability (SAT) Problem
June 1994 (vol. 6 no. 3)
pp. 361-381

The satisfiability (SAT) problem is a fundamental problem in mathematical logic, inference, automated reasoning, VLSI engineering, and computing theory. Following CNF and DNF local search methods, we introduce the Universal SAT problem model, UniSAT, which transforms the discrete SAT problem on Boolean space {0, 1}/sup m/ into an unconstrained global optimization problem on real space E/sup m/. A direct correspondence between the solution of the SAT problem and the global minimum point of the UniSAT objective function is established. Many existing global optimization algorithms can be used to solve the UniSAT problems. Combined with backtracking/resolution procedures, a global optimization algorithm is able to verify satisfiability as well as unsatisfiability. This approach achieves significant performance improvements for certain classes of conjunctive normal form (CNF) formulas. It offers a complementary approach to the existing SAT algorithms.

[1] A. V. Aho, J. E. Hopcroft, and J. D. Ullman,The Design and Analysis of Computer Algorithms. Menlo Park, CA: Addison-Wesley, 1974.
[2] P. Ashar, A. Ghosh, and S. Devadas, "Boolean satisfiability and equivalence checking using general binary decision diagrams,"Integration., 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,"Inform. Processing Lett., vol. 8, no. 3, pp. 121-132, Mar. 1979.
[4] J. R. Bitner and E. M. Reingold, "Backtrack programming techniques,"Commun. 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,"Comput. Operations Res., vol. 5, pp. 633-645, 1986.
[6] A. Z. Broder, A. M. Frieze, and E. Upfal, "On the satisfiability and maximum satisfiability of random 3-CNF formulas," inProc. 4th Ann. ACM-SIAM Symp. Discrete Algorithms, 1993, pp. 322-330.
[7] C. A. Brown and P. W. Purdom, "An average time analysis of backtracking,"SIAM J. Comput., vol. 10, no. 3, pp. 583-593, Aug. 1981.
[8] R. E. Bryant, "Graph-based algorithms for Boolean function manipulation,"IEEE Trans. Comput., vol. C-35, no. 8, pp. 677-691, Aug. 1986.
[9] K. Bugrara and P. Purdom, "Clause order backtracking," Tech. Rep. 311, 1990.
[10] S. Chakradhar, V. Agrawal, and M. Bushnell, "Neural net and boolean satisfiability model of logic circuits,"IEEE Design and Test Comput., pp. 54-57, Oct. 1990.
[11] M. B. Clowes, "On seeing things,"Artificial Intell., vol. 2, pp. 79-116, 1971.
[12] J. Cohen, Ed., "Special section on logic programming,"Commun. ACM, vol. 35, 1992.
[13] A. Colmerauer, "Opening the Prolog III universe,"BYTE, pp. 177-182, Aug. 1987.
[14] S. A. Cook, "The complexity of theorem-proving procedures," inProc. 3rd Annu. ACM Symp. Theory of Comput., 1971, pp. 151-158.
[15] T.H. Cormen, C.E. Leiserson, and R.L. Rivest,Introduction to Algorithms, McGraw-Hill, Cambridge, Mass., 1990.
[16] V. Cerny, "A thermodynamical approach to the travelling salesman problem: An efficient simulation algorithm," Tech. Rep., Inst. of Physics and Biophysics, Comenius Univ., Bratislava, 1982.
[17] M. Davis, G. Logemann, and D. Loveland, "A machine program for theorem proving,"Commun. ACM, vol. 5, pp. 394-397, 1962.
[18] M. Davis and H. Putnam, "A computing procedure for quantification theory,"J. Ass. Comput. Mach., vol. 7, no. 3, pp. 201-215, 1960.
[19] J. deKleer, "Exploiting locality in a TMS," inProc. AAAI'90, 1990, pp. 264-271.
[20] N. Dershowitz, J. Hsiang, N. Josephson, and D. Plaisted, "Associative-commutative rewriting," inProc. IJCAI, 1983, pp. 940-944.
[21] S. Devadas, "Optimal layout via Boolean satisfiability," inProc. ICCAD'89, 1989, pp. 294-297.
[22] S. Devadas, K. Keutzer, and J. White, "Estimation of power dissipation in cmos combinational circuits using boolean function manipulation,"IEEE Trans. CAD, vol. 11, pp. 373-383, Mar. 1992.
[23] O. Dubois, "Counting the number of solutions for instances of satisfiability,"Theoretical Comput. Sci., vol. 81, pp. 49-64, 1991.
[24] O. Dubois and J. Cuber, "Probabilistic approach to the satisfiability problem,"Theoretical Comput. Sci., vol. 81, pp. 65-75, 1991.
[25] S. Even, A. Itai, and A. Shamir, "On the complexity of timetable and multicommodity flow problems,"SIAM J. Computing, vol. 5, no. 4, pp. 691-703, 1976.
[26] J. Franco and M. Paull, "Probabilistic analysis of the davis-Putnam procedure for solving the satisfiability problem,"Discrete Applied Mathematics, vol. 5, pp. 77-87, 1983.
[27] Z. Galil, "On the complexity of regular resolution and the Davis-Putnam procedure,"Theoretical Comput. Sci., pp. 23-46, 1977.
[28] M. R. Garey and D. S. Johnson,Computers and Intractability: A Guide to Theory of NP-Completeness. San Francisco, CA: Freeman, 1979.
[29] A. V. Gelder, "A satisfiability tester for non-clausal propositional calculus,"Inform. Computation, vol. 79, pp. 1-21, Oct. 1988.
[30] M.R. Genesereth and N.J. Nilsson,Logical Foundations of Artificial Intelligence, Morgan Kaufmann, San Mateo, Calif., 1987.
[31] A. Goldberg, P. W. Purdom, and C. A. Brown, "Average time analysis of simplified davis-putnam procedures,"Inform. Processing Lett., vol. 15, no. 2, pp. 72-75, Sept. 1982.
[32] D. E. Goldberg,Genetic Algorithms in Search, Optimization, and Machine Learning. Reading, MA: Addison-Wesley, 1989.
[33] J. Gu, "Parallel algorithms and architectures for very fast search," Tech. Rep. UUCS-TR-88-005, 1988.
[34] J. Gu, "How to solve very large-scale satisfiability (VLSS) problems," Tech. Rep., 1988 (present in part in J. Gu, "Benchmarking (SAT) algorithms," Tech. Rep. UCECE-TR-90-002, 1990).
[35] J. Gu, "Local search with backtracking: A complete algorithm for SAT problem," 1989.
[36] J. Gu, "Optimization algorithms with backtracking search," 1990.
[37] J. Gu, "Efficient local search for very large-scale satisfiability problem,"SIGART Bull., vol. 3, pp. 8-12, Jan. 1992.
[38] J. Gu, "On optimizing a search problem." inAdvanced Series on Artificial Intell., vol. 1, NJ: World Scientific, 1992, pp. 63-105.
[39] J. Gu, "Design efficient local search algorithms,"Lecture Notes in Comput. Sci., vol. 604, Berlin: Springer-Verlag, 1992, pp. 651-654.
[40] J. Gu, "The UniSAT problem models (appendix),"IEEE Trans. Patt. Anal. Mach. Intell., vol. 14, p. 865, Aug. 1992.
[41] J. Gu, "Local search for satisfiability (SAT) problem,"IEEE Trans. Syst., Man, Cybernetics, vol. 23, pp. 1108-1129, Jul/Aug. 1993.
[42] J. Gu, "Optimization algorithms for the satisfiability (SAT) problem," in Ding-Zhu Du, Ed.,New Advances in Optimization and Approximation. Boston: Kluwer Academic, 1994, pp. 72-154.
[43] J. Gu, "Multispace search: A new optimization approach," Tech. Rep. UCECE-TR-90-001, Mar. 1990.
[44] J. Gu, "Local search for satisfiability (SAT) problem," submitted for publication 1989.
[45] J. Gu, "Global optimization for satisfiability (SAT) problem," submitted for publication, 1989.
[46] J. Gu, "Local search, global optimization and resolution: A legal marriage of three," submitted for publication 1990.
[47] J. Gu,Constraint-based search. New York: Cambridge Univ. Press, 1994.
[48] J. Gu and Q. P. Gu, "Average time complexities of several local search algorithms for the satisfiability problem," Tech. Rep. UCECE-TR-91- 004, submitted for publication, 1991.
[49] J. Gu and Q. P. Gu, "Average time complexity of SAT14.5 algorithm," submitted for publication 1992.
[50] J. Gu, Q. P. Gu and D.-Z. Du, "Convergence properties of some optimization algorithms for the satisfiability problem," submitted for publication, 1992.
[51] J. Gu and X. Huang, "Implementation and performance of the SAT14.7 algorithm," submitted for publication, Feb. 1991.
[52] J. Gu, W. Wang, and T. C. Henderson, "A parallel architecture for discreie relaxation algorithm," inIEEE Trans. Patt. Anal. Machine Intell., vol. PAMI-9, no. 6, pp. 816-831, Nov. 1987.
[53] J. Gu and W. Wang, "VLSI architectures for discrete relaxation algorithm," inDiscrete Relaxation Techniques. New York: Oxford Univ. Press, 1990, pp. 111-136.
[54] J. Gu and W. Wang, "A novel discrete relaxation architecture,"IEEE Trans. Pattern Anal. Mach. Intell., vol. 14, pp. 857-865, Aug. 1992.
[55] P. Hansen and B. Jaumard, "Algorithms for the maximum satisfiability problem,"Computing, vol. 44, pp. 279-303, 1990.
[56] J. N. Hooker, "Generalized resolution and cutting planes,"Annals of Operations Res., vol. 12, pp. 217-239, 1988.
[57] J. N. Hooker, "A quantitative approach to logical inference,"Decision Support Syst., vol 4, no 1, 1988.
[58] J. N. Hooker, "Resolution vs. cutting plane solution of inference problems: Some computational experience,"Operations Res. Lett., vol. 7, pp. 1-7, 1988.
[59] J. N. Hooker and C. Fedjki, "Branch-and-cut solution of inference problems in propositional logic," Tech. Rep. 77-88-89, GSIA, Carnegie Mellon Univ., Aug. 1989.
[60] J. Hsiang "Refutational theorem proving using term-rewriting systems,"Artificial Intell., pp. 255-300, 1985.
[61] 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 Intell., vol. 6, pp. 235-252, 1992.
[62] X. Huang and J. Gu, "A quantitative solution for constraint satisfaction," submitted for publication, Mar. 1991.
[63] D. A. Huffman, "Impossible objects as nonsense sentences," in B. Meltzer and D. Michie, Eds.,Mach. Intell.Edinburgh, Scotland: Edinburgh University Press, 1971, pp. 295-323.
[64] K. Iwama, "CNF satisfiability test by counting and polynomial average time,"SIAM J. Computing, pp. 385-391, 1989.
[65] R. E. Jeroslow and J. Wang, "Solving propositional satisfiability problems,"Annals Mathematics and AI, vol.1, pp. 167-187, 1990.
[66] R. G. Jeroslow, "Computation-oriented reductions of predicate to propositional logic,"Decision Support Syst., vol. 4, pp. 183-197, 1988.
[67] J. Johnson, "A Neural Network Approach to the 3-Satisfiability Problem,"J. Parallel and Distributed Computing, Vol. 6, 1989, pp. 435-439.
[68] 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.
[69] R. M. Karp, "The probabilistic analysis of some combinatorial search algorithms," inAlgorithms and Complexity: New Directions and Recent Results. New York: Academic, 1976, pp. 1-19.
[70] S. Kirkpatrick, C. D. Gelat, and M. P. Vecchi, "Optimization by simulated annealing,"Sci., vol. 220, pp. 671-680, 1983.
[71] T. Larrabee, "Test pattern generation using Boolean satisfiability,"IEEE Trans. CAD, vol. 11, pp. 4-15, Jan. 1992.
[72] R. C. T. Lee, private commun., 1992-1993.
[73] D. G. Liu, J. G. Fei, Y. J. Yu, and G. Y. Li,FORTRAN Programs, vol. 1. Beijing, People's Republic of China: Guo Fang Gong Ye Press, 1980.
[74] D. W. Loveland,Automated Theorem Proving: A Logical Basis. Amsterdam: North-Holland, 1978.
[75] D. G. Luenberger,Linear and Nonlinear Programming. Reading, MA: Addison-Wesley, 1984.
[76] A. K. Mackworth, "Consistency in networks of relations,"Artificial Intell., vol. 8, pp. 99-119, 1977.
[77] D. McAllester, "Truth maintenance," inProc. AAAI'90, 1990, pp. 1109-1116.
[78] R. Mohr and T. C. Henderson, "Arc and path consistency revisited,"Artificial Intell., vol. 28, pp. 225-233, 1986.
[79] N. Nilsson,Principles of Artificial Intelligence. Palo Alto, CA: Tioga, 1980.
[80] C. H. Papadimitriou, "On selecting a satisfying truth assignment," inProc. 32nd Ann. Symp. Foundations of Comput. Sci., 1991, pp. 163-169.
[81] C. H. Papadimitriou and K. Steiglitz,Combinatorial Optimization: Algorithms and Complexity. Englewood Cliffs, NJ: Prentice-Hall, 1982.
[82] D. Pehoushek, "SAT problem instances and algorithms," private commun., Stanford Univ., 1992-1993.
[83] P. W. Purdom, "Search rearrangement backtracking and polynomial average time,"Artificial Intell., vol. 21, pp. 117-133, 1983.
[84] P. W. Purdom, private commun., 1992-1994.
[85] P. W. Purdom and C. A. Brown, "The pure literal rule and polynomial average time,"SIAM J. Comput., vol. 14, pp. 943-953, 1985.
[86] R. Puri and J. Gu, "An efficient algorithm for microword length minimization,"IEEE Trans. CAD, vol. 12, pp. 1449-1457, Oct. 1993.
[87] R. Puri and J. Gu, "A modular partitioning approach for asynchronous circuit synthesis,"IEEE Trans. CAD, to appear.
[88] J. A. Robinson, "A machined-oriented logic based on the resolution principle,"J. Assoc. Comput. Mach., vol. 12, no. 1, pp. 23-41, Jan. 1965.
[89] Y. G. Saab and V. B. Rao, "Combinatorial optimization by stochastic evolution,"IEEE Trans. CAD, vol. 10, pp. 525-535, Apr. 1991.
[90] T. J. Schaefer, "The complexity of satisfiability problems," inTenth Anna. Symp. Theory of Comput., 1978, pp. 216-226, (with authors corrections 1988).
[91] B. M. Schwartzschild, "Statistical mechanics algorithm for monte carlo optimization,"Phys. Today, vol. 35, pp. 17-19, 1982.
[92] B. Selman, private commun., Aug. 1992.
[93] B. Selman, H. Levesque, and D. Mitchell, "A new method for solving hard satisfiability problems," inProc. AAAI'92, 1992, pp. 440-446.
[94] M. J. Shensa, "A computational structure for the propositional calculus," inProc. IJCAI, 1989, pp. 384-388.
[95] R. C.-J. Shi, "An improvement on Karmarkar's algorithm for integer programming," June 1992.
[96] P. Siegel, "Representation et utilization de la connaissances en calcul propositionel," Ph.D. dissertation, University Aix-Marseille II, France, 1987.
[97] R. Sosic and J. Gu, "Quickn-queen search on VAX and Bobcat machines," CS 547 AI Class Project, Winter Quarter, Feb. 1988.
[98] R. Sosic and J. Gu, "How to search for million queens," Tech. Rep. UUCS-TR-88-008, Dept. of Comput. Sci., Univ. of Utah, Feb. 1988.
[99] R. Sosic and J. Gu, "Fast search algorithms for then-queens problem,"IEEE Trans. Syst., Man, Cybernetics, vol. 21, pp. 1572-1576, Nov./Dec. 1991.
[100] R. Sosic and J. Gu, "Efficient local search with conflict minimization,"IEEE Trans. Knowl. Data Eng., vol. 6, 1994.
[101] R. Sosic, J. Gu, and R. Johnson, "The Unison algorithm: Fast evaluation of Boolean expressions,"Commun. ACM, accepted for publication 1992.
[102] R. Sosic, J. Gu, and R. Johnson, "A universal Boolean evaluator,"IEEE Trans. Comput., accepted for publication, 1992.
[103] G. S. Tseitin, "On the complexity of derivations in propositional calculus," in A. O. Slisenko, Ed.,Structures in Constructive Mathematics and Mathematical Logic, Part II, 1968, pp. 115-125.
[104] D. Waltz, "Generating semantic descriptions from drawings of scenes with shadows," MAC-AI-TR-271, Mass. Inst. Technol., Cambridge, 1972.
[105] H. P. Williams, "Linear and integer programming applied to the propositional calculus,"Syst. Res. Inform. Sci., vol. 2, pp. 81-100, 1987.
[106] P. M. Winston,Artificial Intelligence. Reading, MA: Addison-Wesley, 1984.

Index Terms:
search problems; optimisation; formal logic; inference mechanisms; global optimization algorithms; satisfiability problem; SAT problem; mathematical logic; inference; automated reasoning; VLSI engineering; computing theory; CNF; DNF local search methods; Universal SAT problem model; UniSAT; discrete SAT problem; Boolean space; unconstrained global optimization problem; real space; direct correspondence; global minimum point; backtracking/resolution procedures; conjunctive normal form
Citation:
J. Gu, "Global Optimization for Satisfiability (SAT) Problem," IEEE Transactions on Knowledge and Data Engineering, vol. 6, no. 3, pp. 361-381, June 1994, doi:10.1109/69.334864
Usage of this product signifies your acceptance of the Terms of Use.