Skip to main content
SpringerLink
Log in
Book cover

Advances in Optimization and Approximation pp 72–154Cite as

Optimization Algorithms for the Satisfiability (SAT) Problem

  • Chapter

Part of the book series: Nonconvex Optimization and Its Applications ((NOIA,volume 1))

Abstract

The satisfiability problem (SAT) is a fundamental problem in mathematical logic and computing theory. Methods to solve the satisfiability problem play an important role in the development of computing theory and systems. Traditional methods treat the SAT problem as a discrete, constrained decision problem. In this chapter, we show how to translate the SAT problem into an unconstrained optimization problem and use efficient local search and global optimization methods to solve the transformed optimization problem. This approach gives significant performance improvements for certain classes of conjunctive normal form (CNF) formulas. It offers a complementary approach to the existing SAT algorithms.1

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   129.00
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   169.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD   169.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. L. Abel. On the order of connections for automatic wire routing. IEEE Trans, on Computers, pages 1227–1233, Nov. 1972.

    Google Scholar 

  2. T. Agerwala. Microprogram Optimization: A Survey. IEEE Trans, on Computers, C-25: 962–973, Oct. 1976.

    Article  MathSciNet  Google Scholar 

  3. A.V. Aho, J.E. Hopcroft, and J.D. Ullman. The Design and Analysis of Computer Algorithms. Addison-Wesley, Reading, 1974.

    MATH  Google Scholar 

  4. A.V. Aho, R. Sethi, and J.D. Ullman. Compilers. Addison-Wesley, Reading, 1986.

    Google Scholar 

  5. S.B. Akers. On the use of the linear assignment algorithm in module placement. In Proc. of the 18th ACM/IEEE DAC, pages 137–144, 1981.

    Google Scholar 

  6. J. Aloimonos. Visual shape computation. Proceedings of the IEEE, 76: 899–916, Aug. 1988.

    Article  Google Scholar 

  7. J. A. Anderson and G. E. Hinton. Models of Information Processing in the Brain. In G. E. Hinton and J. A. Anderson, editors, Parallel Models of Associative Memory, chapter 1, pages 9–48. Lawrence Erlbaum Associates, Publishers, Hillsdale, New Jersey, 1981.

    Google Scholar 

  8. J.A. Anderson and E. Rosenfeld, editors. Neuro computing: Foundations of Research. MIT Press, Cambridge, 1988.

    Google Scholar 

  9. S. Arora, C. Lund, R. Motwani, M. Sudan, and M. Szegedy. Proof verification and hardness of approximation problems. In Proceedings 33rd IEEE Symposium on the Foundations of Computer Science, pages 14–23, 1992.

    Chapter  Google Scholar 

  10. P. Ashar, A. Ghosh, and S. Devadas. Boolean satisfiability and equivalence checking using general Binary Decision Diagrams. Integration, the VLSI journal, 13: 1–16, 1992.

    Article  Google Scholar 

  11. 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, 8 (3): 121–132, Mar. 1979.

    Article  MathSciNet  MATH  Google Scholar 

  12. H. Baird. Anatomy of a versatile page reader. Proceedings of the IEEE, 80(7).-1059–1065, Jul. 1992.

    Article  Google Scholar 

  13. D. H. Ballard and C. M. Brown. Computer Vision. Prentice-Hall, Englewood Cliffs, New Jersey, 1982.

    Google Scholar 

  14. A.E. Barbour. Solutions to the minimization problem of fault-tolerant logic circuits. IEEE Trans, on Computers, 41 (4): 429–443, Apr. 1992.

    Article  MathSciNet  Google Scholar 

  15. R. G. Bennetts. An Improved Method for Prime C-Class Derivation in the State Reduction of Sequential Networks. IEEE Trans, on Computers, C-20: 229–231, Feb. 1971.

    Google Scholar 

  16. P.A. Berstein, V. Hadzilacos, and N. Goodman. Concurrency Control and Recovery in Database Systems. Addison-Wesley Publication Co., 1987.

    Google Scholar 

  17. N. N. Biswas. State Minimization of Incompletely Specified Sequential Machines. IEEE Trans, on Computers, C-23: 80–84, Jan. 1974.

    Article  Google Scholar 

  18. J. R. Bitner and E. M. Reingold. Backtrack programming techniques. Comm. of ACM, 18 (11): 651–656, Nov. 1975.

    Article  MATH  Google Scholar 

  19. C.E. Blair, R.G. Jeroslow, and J.K. Lowe. Some results and experiments in programming techniques for propositional logic. Computers and Operations Research, 5: 633–645, 1986.

    Article  MathSciNet  Google Scholar 

  20. J.P. Blanks. Near-optimal placement using a quadratic objective function. In Proc. of the 22th ACM/IEEE DAC, pages 609–615, 1985.

    Chapter  Google Scholar 

  21. J. Blazewicz. Scheduling dependent tasks with different arrival times to meet deadlines. In Proc. of the International Workshop on Modelling and Performance Evaluation of Computer Systems, pages 57–65, 1976.

    Google Scholar 

  22. S. H. Bokhari. Partitioning problems in parallel, pipelined, and distributed computing. IEEE Trans, on Computers, 37 (1): 48–57, Jan 1988.

    Article  MathSciNet  Google Scholar 

  23. F. Bonomi. On job assignment for a parallel system of processor sharing queues. IEEE Trans, on Computers, 39 (7): 858–869, July 1990.

    Article  Google Scholar 

  24. H.N. Brady. An approach to topological pin assignment. IEEE Trans, on Computer-Aided Design, CAD-3: 250–255, July 1984.

    Article  Google Scholar 

  25. M. Brady, J.M. Hollerbach, T.L. Johnson, T. Lozano-Perez, and M.T. Mason, editors. Robot Motion: Planning and Control. The MIT Press, Cambridge, 1982.

    Google Scholar 

  26. M.A. Breuer. Min-cut placement. J. of Design Automation and Fault Tolerant Computing, 1: 343–362, 1976.

    Google Scholar 

  27. F. Brewer and D. Gajski. Chippe: A system for constraint driven behavioral synthesis. IEEE Trans, on Computer-Aided Design, 9 (7): 681–695, July 1990.

    Article  Google Scholar 

  28. A.Z. Broder, A.M. Frieze, and E. Upfal. On the satisfiability and maximum satisfiability of random 3-CNF formulas. In Proceedings of the Fourth Annual ACM-SIAM Symposium on Discrete Algorithms, pages 322–330, 1993.

    Google Scholar 

  29. M.J. Brooks and B.K.P. Horn. Shape and source from shading. In Proc. of IJCAI’85, pages 932–936, Aug. 1985.

    Google Scholar 

  30. C.A. Brown and P.W. Purdom. An average time analysis of backtracking. SIAM J. Comput 10 (3): 583–593, Aug. 1981.

    Article  MathSciNet  MATH  Google Scholar 

  31. B. Bruderlin. Constructing three dimensional geometric objects defined by constraints. In Proceedings of 1986 ACM SIGGRAPH Workshop in Interactive Graphics, 1986.

    Google Scholar 

  32. M. Bruynooghe. Graph coloring and constraint satisfaction. Technical Report CW 44, Dept. of Computer Science, Katholieke Universiteit Leuven, Dec. 1985.

    Google Scholar 

  33. R.E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Trans, on Computers, C-35(8): 677–691, Aug. 1986.

    Article  Google Scholar 

  34. K. Bugrara and P. Purdom. Clause order backtracking. Technical Report 311, 1990.

    Google Scholar 

  35. A. Bundy, editor. Catalogue of Artificial Intelligence Tools. Springer-Verlag, Berlin, 1984.

    MATH  Google Scholar 

  36. J.L. Burns and A.R. Newton. Efficient constraint generation for hierarchical compaction. In Proc. Intl. Conf. on Computer Design, pages 197–200. IEEE Computer Society, Oct. 1987.

    Google Scholar 

  37. M. Burstein and R. Pelavin. Hierarchical channel router. In Proc. of the 20th ACM/IEEE DAC, pages 591–597, Jun. 1983.

    Google Scholar 

  38. S. Chakradhar, V. Agrawal, and M. Bushnell. Neural net and boolean satisfiability model of logic circuits. IEEE Design and Test of Computers, pages 54–57, Oct. 1990.

    Google Scholar 

  39. I. Chakravarty. A generalized line and junction labelling scheme with applications to scene analysis. IEEE Trans, on Pattern Analysis and Machine Intelligence, PAMI-1(2): 202–205, Apr. 1979.

    Article  MathSciNet  Google Scholar 

  40. P.K. Chan, M.D.F. Schlag, C.D. Thomborson, and V.G. Oklobdzija. Delay optimization of carry-skip adders and block carry-lookahead adders using multidimensional dynamic programming. IEEE Trans, on Computers, 41 (8): 920–930, Aug. 1992.

    Article  Google Scholar 

  41. A.K. Chandra and P.M. Merlin. Optimal implementation of conjunctive queries in relational databases. In Proceedings of the 9th ACM Symposium on Theory of Computing, pages 77–90, 1977.

    Google Scholar 

  42. M.T. Chao and J. Franco. Probabilistic analysis of two heuristics for the 3-satisfiability problem. SIAM J. on Computing, 15: 1106–1118, 1986.

    Article  MathSciNet  MATH  Google Scholar 

  43. M.T. Chao and J. Franco. Probabilistic analysis of a generalization of the unit-clause literal selection heuristics for the k satisfiable problem. Information Science, 51: 289–314, 1990.

    Article  MathSciNet  MATH  Google Scholar 

  44. H.R. Charney and D.L. Plato. Efficient partitioning of components. In Proc. of the 5th Annual Design Automation Workshop, pages 16–21, 1968.

    Google Scholar 

  45. R. T. Chin and C. R. Dyer. Model-based recognition in robot vision. ACM Computing Surveys, 18 (1): 67–108, Mar. 1986.

    Article  Google Scholar 

  46. Y. Chu, editor. Special Section on Chinese/Kanji Text and Data Processing. IEEE Computer, volume 18, No. 1. Jan. 1985.

    Google Scholar 

  47. V. Chvatal and B. Reed. Mick gets some (the odds are on his side). In Proceedings on the Foundations of Computer Science, 1992.

    Google Scholar 

  48. J. Cleary. Logical arithmetic. Future Computing Systems, 2 (2), 1987.

    Google Scholar 

  49. M.B. Clowes. On seeing things. Artificial Intelligence, 2: 79–116, 1971.

    Article  Google Scholar 

  50. J. Cohen, editor. Special Section on Logic Programming. Comm. of the ACM, volume 35. 1992.

    Google Scholar 

  51. J.P. Cohoon and W.D. Paris. Genetic placement. In Digest of the Intl. Conf. on Computer-Aided Design, pages 422–425, 1986.

    Google Scholar 

  52. A. Colmerauer. Opening the Prolog III universe. BYTE Magazine, pages 177–182, Aug. 1987.

    Google Scholar 

  53. S.A. Cook. The complexity of theorem-proving procedures. In Proceedings of the Third ACM Symposium on Theory of Computing, pages 151–158, 1971.

    Google Scholar 

  54. T.H. Cormen, C.E. Leiserson, and R.L. Rivest. Introduction to Algorithms. MIT Press, Cambridge, 1990.

    MATH  Google Scholar 

  55. D.G. Corneil and D.G. Kirkpatrick. A theoretical analysis of various heuristics for the graph isomorphism problem. SIAM J. on Computing, 9 (2): 281–297, 1980.

    Article  MathSciNet  MATH  Google Scholar 

  56. V. Cěrny. A thermodynamical approach to the travelling salesman problem: An efficient simulation algorithm. Technical report, Institute of Physics and Biophysics, Comenius University, Bratislava, 1982.

    Google Scholar 

  57. Z. Cvetanovic. The effects of problem partitioning, allocation, and granularity on the performance of multiple-processor systems. IEEE Trans, on Computers, C-36(4): 421–432, Apr 1987.

    Article  Google Scholar 

  58. W. Dai and E.S. Kuh. Hierarchical floorplanning for building block layout. In Digest of Intl. Con, on Computer-Aided Design, pages 454–457, 1986.

    Google Scholar 

  59. S. R. Das, D. K. Banerji, and A. Chattopadhyay. On Control Memory Minimization in Microprogrammed Digital Computers. IEEE Trans, on Computers, C-22: 845–848, Sept. 1973.

    Article  MathSciNet  Google Scholar 

  60. L. S. Davis. Shape matching using relaxation techniques. IEEE Trans, on Pattern Analysis and Machine Intelligence, PAMI-l(1): 60–72, Jan. 1979.

    Google Scholar 

  61. L. S. Davis and T. C. Henderson. Hierarchical constraint processes for shape analysis. IEEE Trans, on Pattern Analysis and Machine Intelligence, PAMI-3(3): 265–277, May 1981.

    Article  Google Scholar 

  62. M. Davis, G. Logemann, and D. Loveland. A machine program for theorem proving. Communications of the ACM, 5: 394–397, 1962.

    Article  MathSciNet  MATH  Google Scholar 

  63. M. Davis and H. Putnam. A computing procedure for quantification theory. J. of ACM, pages 201–215, 1960.

    Google Scholar 

  64. J. de Kleer. Exploiting locality in a TMS. In Proceedings of AAAI’90, pages 264–271, 1990.

    Google Scholar 

  65. R. Dechter. A constraint-network approach to truth maintenance. Technical Report R-870009, Computer Science Dept., UCLA, Los Angeles, 1987.

    Google Scholar 

  66. R. Dechter and A. Dechter. Belief maintenance in dynamic constraint networks. In Proceedings of AAAI’88, 1988.

    Google Scholar 

  67. J.S. Denker, editor. Neural Networks for Computing, volume 151 of AIP (Snowbird, Utah) Conference Proceedings. American Institute of Physics, New York, 1986.

    Google Scholar 

  68. N. Dershowitz, J. Hsiang, N. Josephson, and D. Plaisted. Associative-commutative rewriting. In Proceedings of IJCAI, pages 940–944, 1983.

    Google Scholar 

  69. D.N. Deutsch. A ‘dogleg’ channel router. In Proc. of the 13th ACM/IEEE DAC, pages 425’433, Jun. 1976.

    Google Scholar 

  70. D.N. Deutsch. Compacted channel routing. In Digest Intl. Conf. on Computer-Aided Design, pages 223–225, Nov. 1985.

    Google Scholar 

  71. J. P. A. Deutsch. A short cut for certain combinational problems. In British Joint Comput. Conference, 1966.

    Google Scholar 

  72. S. Devadas. Optimal layout via boolean satisfiability. In Proceedings of ICCAD’89, pages 294–297, Nov. 1989.

    Google Scholar 

  73. S. Devadas, K. Keutzer, and J. White. Estimation of power dissipation in cmos combinational circuits using boolean function manipulation. IEEE Transactions on CAD, ll(3): 373–383, Mar. 1992.

    Google Scholar 

  74. S. Devadas, H.T. Ma, A.R. Newton, and A.L. Sangiovanni-Vincentelli. A synthesis and optimization procedure for fully and easily testable sequential machines. IEEE Trans, on Computer-Aided Design, 8 (10): 1100–1107, Oct. 1989.

    Article  Google Scholar 

  75. S.K. Dhalland C.L. Liu. On a real-time scheduling problem. Operations Research, 26(1): 127–140, Feb. 1978.

    Article  MathSciNet  Google Scholar 

  76. V. Dhar and A. Crocker. A problem-solver/TMS architecture for general constraint satisfaction problems. Technical report, Dept. of Information Systems, New York University, 1989.

    Google Scholar 

  77. M. Dincbas, H. Simonis, and P.V. Hentenryck. Solving a cutting-stock problem in constraint logic programming. In Proceedings of the 5th International Conference on Logic Programming, 1988.

    Google Scholar 

  78. J. Doenhardt and T. Lengauer. Algorithm aspects of one-dimensional layout. IEEE Trans, on Computer-Aided Design, CAD-6(5): 863–878, 1987.

    Article  Google Scholar 

  79. W.E. Donath. Placement and average interconnection lengths of computer logic. IEEE Trans. on Circuits and Systems, CAS-26(4): 272–277, Apr. 1979.

    Article  Google Scholar 

  80. W.E. Donath. Wire length distribution for placements of computer logic. IBM J. of Research and Development, 25 (3): 152–155, May 1981.

    Article  Google Scholar 

  81. W.E. Donath and A.J. Hoffman. Algorithms for partitioning of graphs and computer logic based on eigenvectors of connection matrices. IBM Technical Disclosure Bulletin 15, pages 938–944, 1972.

    Google Scholar 

  82. O. Dubois. Counting the number of solutions for instances of satisfiability. Theoretical Computer Science, 81: 49–64, 1991.

    Article  MathSciNet  MATH  Google Scholar 

  83. O. Dubois and J. Carlier. Probabilistic approach to the satisfiability problem. Theoretical Computer Science, 81: 65–75, 1991.

    Article  MathSciNet  MATH  Google Scholar 

  84. C. Eastman. Preliminary report on a system for general space planning. Comm. of ACM, 15 (2): 76 — 87, Feb. 1972.

    Article  MathSciNet  Google Scholar 

  85. K.P. Eswaran, J.N. Gray, R.A. Lorie, and I.L. Traiger. The notion of consistency and predicate look in a database system. Comm. of ACM, 19 (11), Nov. 1976.

    Google Scholar 

  86. S. Even, A. Itai, and A. Shamir. On the complexity of timetable and multi-commodity flow problems. SIAM J. on Computing, 5 (4): 691–703, 1976.

    Article  MathSciNet  MATH  Google Scholar 

  87. O. Faugeras and K. Price. Semantic description of aerial images using stochastic labeling. IEEE Trans, on Pattern Analysis and Machine Intelligence, PAMI-3(6): 633–642, Nov. 1981.

    Article  Google Scholar 

  88. O. D. Faugeras, editor. Fundamentals in Computer Vision. Cambridge University Press, London, 1983.

    Google Scholar 

  89. J. A. Feldman and Y. Yakimovsky. Decision theory and artificial intelligence: I. a semantics-based region analyser. Artificial Intelligence, 5: 349–371, 1974.

    Article  MATH  Google Scholar 

  90. J. D. Findler. Associative Networks: Representation and Use of Knowledge by Computers. Academic Press, New York, 1979.

    MATH  Google Scholar 

  91. M.S. Fox. Constraint-Directed Search: A Case Study of Job-Shop Scheduling. Pitman, London, 1987.

    MATH  Google Scholar 

  92. J. Franco Probabilistic analysis of the pure literal heuristic for the satisfiability problem. Annals of Operations Research, 1: 273–289, 1984.

    Article  Google Scholar 

  93. J. Franco. On the probabilistic performance of algorithms for the satisfiability problem. Information Processing Letters, 23: 103–106, 1986.

    Article  Google Scholar 

  94. J. Franco and Y.C. Ho. Probabilistic performance of heuristic for the satisfiability problem. Discrete Applied Mathematics, 22:35–51, 1988/89.

    Article  MathSciNet  MATH  Google Scholar 

  95. J. Franco and M. Paull. Probabilistic analysis of the davis-putnam procedure for solving the satisfiability problem. Discrete Applied Mathematics, 5: 77–87, 1983.

    Article  MathSciNet  MATH  Google Scholar 

  96. R.T. Frankot and R. Chellappa. A method for enforcing integrability in shape from shading algorithms. IEEE Trans, on Pattern Analysis and Machine Intelligence, PAMI-10(4): 439–451, Jul. 1988.

    Article  MATH  Google Scholar 

  97. F. Frayman and S. Mittal. Cossack: A Constraints-based Expert System for Configuration Tasks. Computational Mechanics Publications, Nadel, 1987.

    Google Scholar 

  98. T. W. Fuqua. Constraint kernels: Constraints and dependencies in a geometric modeling system. Master’s thesis, Dept. of Computer Science, Univ. of Utah, Aug. 1987.

    Google Scholar 

  99. Z. Galil. On the complexity of regular resolution and the Davis-Putnam procedure. Theoretical Computer Science, pages 23–46, 1977.

    Google Scholar 

  100. H. Garcia-Molina. Using semantic knowledge for transaction processing in a distributed database. ACM Trans, on Database Systems, 8 (2), Jun. 1983.

    Google Scholar 

  101. M.R. Garey and D.S. Johnson. Complexity results for multiprocessor scheduling under resource constraints. SIAM J. Comput., 4: 397–411, 1975.

    Article  MathSciNet  MATH  Google Scholar 

  102. M.R. Garey and D.S. Johnson. Two-processors scheduling with start-times and deadlines. SIAM J. on Computing, 6: 416–426, 1977.

    Article  MathSciNet  MATH  Google Scholar 

  103. M.R. Garey and D.S. Johnson. Computers and Intractability: A Guide to the Theory of NP-Completeness. W.H. Freeman and Company, San Francisco, 1979.

    MATH  Google Scholar 

  104. J. Gaschnig. A constraint satisfaction method for inference making. In Proceedings of 12th Annual Allerton Conf. Circuit System Theory, 1974.

    Google Scholar 

  105. J. Gaschnig. Performance Measurements and Analysis of Certain Search Algorithms. PhD thesis, Carnegie-Mellon University, Dept. of Computer Science, May 1979.

    Google Scholar 

  106. A.V. Gelder. A satisfiability tester for non-clausal propositional calculus. Information and Computation, 79 (1): 1–21, Oct. 1988.

    Article  MathSciNet  MATH  Google Scholar 

  107. S. Geman and D. Geman. Stochastic relaxation, gibbs distributions, and the bayesian restoration of images. IEEE Trans, on Pattern Analysis and Machine Intelligence, PAMI-6(6): 721–741, Nov. 1984.

    Article  MATH  Google Scholar 

  108. M.R. Genesereth and N. J. Nilsson. Logical Foundations of Artificial Intelligence. Morgan Kaufmann Publishers, Los Altos, California, 1987.

    MATH  Google Scholar 

  109. P.C. Gilmore. A proof method for quantification theory. IBM J. Res. Develop., 4: 28–35, 1960.

    Article  MathSciNet  MATH  Google Scholar 

  110. A. Ginzberg. Algebraic Theory of Automata. Academic Press, New York, 1968.

    Google Scholar 

  111. A. Goldberg. Average case complexity of the satisfiability problem. In Proc. Fourth Workshop on Automated Deduction, pages 1–6, 1979.

    Google Scholar 

  112. A. Goldberg. On the complexity of the satisfiability problem. Technical Report Courant Computer Science No. 16, New York University, 1979.

    Google Scholar 

  113. A. Goldberg, P.W. Purdom, and C.A. Brown. Average time analysis of simplified davis-putnam procedures. Information Processing Letters, 15(2): 72–75, 6 Sept. 1982.

    Article  MathSciNet  MATH  Google Scholar 

  114. D.E. Goldberg. Genetic Algorithms in Search, Optimization, and Machine Learning. Addison-Wesley, Reading, 1989.

    MATH  Google Scholar 

  115. A. Grasselli and F. Luccio. A Method for Minimizing the Number of Internal States in Incompletely Specified Sequential Networks. IEEE Trans, on Computers, EC-14: 350–359, June 1965.

    Article  MATH  Google Scholar 

  116. A. Grasselli and U. Montanari. On the Minimization of READ-ONLY Memories in Microprogrammed Digital Computers. IEEE Trans, on Computers, C-19: 1111–1114, Nov. 1970.

    Article  Google Scholar 

  117. J. Gu, W. Wang, and T. C. Henderson. A parallel architecture for discrete relaxation algorithm. IEEE Trans, on Pattern Analysis and Machine Intelligence, PAMI-9(6): 816–831, Nov. 1987.

    Article  Google Scholar 

  118. J. Gu. Parallel algorithms and architectures for very fast search. Technical Report UUCS-TR-88-005, Jul. 1988.

    Google Scholar 

  119. J. Gu. How to solve Very Large-Scale Satisfiability (VLSS) problems. Technical Report. 1988 (Present in part in, J. Gu, Benchmarking SAT Algorithms, Technical Report UCECE-TR-90-002, 1990 ).

    Google Scholar 

  120. J. Gu. Local search with backtracking: A complete algorithm for SAT problem. 1989.

    Google Scholar 

  121. J. Gu. Local search for satisfiability (SAT) problem. Submitted for publication, 1989.

    Google Scholar 

  122. J. Gu. Global optimization for satisfiability (SAT) problem. Submitted for publication, 1989.

    Google Scholar 

  123. J. Gu and W. Wang. VLSI Architectures for Discrete Relaxation Algorithm. In Discrete Relaxation Techniques, chapter 9, pages 111–136. Oxford University Press, New York, 1990.

    Google Scholar 

  124. J. Gu. Optimization algorithms with backtracking search. 1990.

    Google Scholar 

  125. J. Gu. Local search, global optimization, and resolution: A legal marriage of three. Submitted for publication, 1990.

    Google Scholar 

  126. J. Gu. Efficient local search for very large-scale satisfiability problem. SIGART Bulletin,3(1):8–12, Jan. 1992, ACM Press.

    Article  Google Scholar 

  127. J. Gu. On Optimizing a Search Problem. In Advanced Series on Artificial Intelligence, Vol. 1, chapter 2, pages 63–105. World Scientific, New Jersey, Jan. 1992.

    Google Scholar 

  128. J. Gu. Design Efficient Local Search Algorithms. In F. Belli and F.J. Radermacher, editors, Lecture Notes in Computer Science, Vol. 604-’ IEA/AIE, pages 651–654. Springer-Verlag, Berlin, Jun. 1992.

    Google Scholar 

  129. J. Gu. The UniSAT problem models (appendix). IEEE Trans, on Pattern Analysis and Machine Intelligence, 14 (8): 865, Aug. 1992.

    Google Scholar 

  130. J. Gu. Local search for satisfiability (SAT) problem. IEEE Trans, on Systems, Man, and Cybernetics, 23 (4): 1108–1129, Jul./Aug. 1993.

    Article  Google Scholar 

  131. J. Gu. Global optimization for satisfiability (SAT) problem. IEEE Trans, on Knowledge and Data Engineering, 6(2), Apr. 1994, in press.

    Google Scholar 

  132. J. Gu and W. Wang. A novel discrete relaxation architecture. IEEE Trans, on Pattern Analysis and Machine Intelligence, 14 (8): 857–865, Aug. 1992.

    Article  Google Scholar 

  133. J. Gu. Multispace Search: A New Optimization Approach. In New Advances in Optimization and Approximation. Ding-Zhu Du (ed). Kluwer Academic Publishers, Boston, MA, Jan. 1994.

    Google Scholar 

  134. J. Gu. Constraint-Based Search. Cambridge University Press, New York, 1994.

    Google Scholar 

  135. J. Gu and Q.P. Gu. Average time complexities of several local search algorithms for the satisfiability problem. Technical Report UCECE-TR-91-004, submittedfor publication. 1991.

    Google Scholar 

  136. J. Gu and Q.P. Gu. Average time complexity of SAT14.5 algorithm. Submitted for publication, 1992.

    Google Scholar 

  137. J. Gu, Q.P. Gu, and D.-Z. Du. Convergence properties of some optimization algorithms for the satisfiability problem. Submitted for publication, 1992.

    Google Scholar 

  138. J. Gu and X. Huang. Implementation and performance of the SAT14.7 algorithm. Submitted for publication. Feb. 1991.

    Google Scholar 

  139. J. Gu and X. Huang. Efficient local search with search space smoothing. IEEE Trans, on Systems, Man, and Cybernetics, 24(4), Apr. 1994, in press

    Google Scholar 

  140. A. Guzman. Computer Recognition of Three-Dimensional Objects in a Visual Scene. PhD thesis, MIT, 1968.

    Google Scholar 

  141. S. Ha and E.A. Lee. Compile-time scheduling and assignment of data-flow program graphs with data-dependent iteration. IEEE Trans, on Computers, 40 (11): 1225–1238, Nov. 1991.

    Article  Google Scholar 

  142. G.T. Hamachi and J.K. Ousterhout. A switchbox router with obstacle avoidance. In Proc. of the 21th ACM/IEEE DAC, pages 173–179, Jun. 1984.

    Google Scholar 

  143. M. Hanan, P.K. Wolff, and B.J. Agule. Some experimental results on placement techniques. J. of Design Automation and Fault-Tolerant Computing, 2: 145–168, May 1978.

    Google Scholar 

  144. P. Hansen and B. Jaumard. Algorithms for the maximum satisfiability problem. Computing, 44: 279–303, 1990.

    Article  MathSciNet  MATH  Google Scholar 

  145. R. M. Haralick and L. G. Shapiro. The consistent labeling problem: Part 1. IEEE Trans, on Pattern Analysis and Machine Intelligence, PAMI-1(2): 173–184, Apr. 1979.

    Article  MATH  Google Scholar 

  146. F. Harary. Graph Theory. Addison-Wesley, Reading, 1969.

    Google Scholar 

  147. W. S. Havens. A theory of schema labelling. Computational Intelligence, 1 (3 and 4): 127–139, 1985.

    Article  Google Scholar 

  148. T. Hedges, W. Dawson, and Y.E. Cho. Bitmap graph build algorithm for compaction. In Digest Intl. Conf. on Computer-Aided Design, pages 340–342, Sep. 1985.

    Google Scholar 

  149. T. C. Henderson and L. S. Davis. Hierarchical models and analysis of shape. Pattern Recognition, 14 (1–6): 197–204, 1981.

    Article  MathSciNet  Google Scholar 

  150. T. C. Henderson and A. Samal. Multiconstraint shape analysis. Image and Vision Computing, 4 (2): 84–96, May 1986.

    Article  Google Scholar 

  151. G.E. Hinton and T.J. Sejnowski. Learning and Relearning in Boltzmann Machine. In D. E. Rumelhart and J. L. McClelland, editors, Parallel Distributed Processing: Explorations in the Micro structure of Cognition. Vol. 1: Foundations, volume 1, chapter 7, pages 282—317. The MIT Press, Cambridge, 1986.

    Google Scholar 

  152. S.J. Hong and S. Muroga. Absolute minimization of completely specified switching functions. IEEE Trans, on Computers, 40 (1): 53–65, Jan. 1991.

    Article  MathSciNet  Google Scholar 

  153. P. Hood and Grover. Designing real time systems in Ada. Technical Report 1123-1, SofTech, Inc., Waltham, Jan. 1986.

    Google Scholar 

  154. J.N. Hooker. Generalized resolution and cutting planes. Annals of Operations Research, 12: 217–239, 1988.

    Article  MathSciNet  Google Scholar 

  155. J.N. Hooker. A quantitative approach to logical inference. Decision Support Systems, 4:45–69, 1988.

    Article  Google Scholar 

  156. J.N. Hooker. Resolution vs. cutting plane solution of inference problems: Some computational experience. Operations Research Letter, 7(1):1–7, 1988.

    Article  MathSciNet  MATH  Google Scholar 

  157. J.N. Hooker and C. Fedjki. Branch-and-cut solution of inference problems in propositional logic. Technical Report 77-88-89, GSIA, Carnegie Mellon University, Aug. 1989.

    Google Scholar 

  158. A.L. Hopldns and et. al. FTMP — a highly reliable fault-tolerant multiprocessor for aircraft. In Proceedings of the IEEE, pages 1221–1239, Oct. 1978.

    Google Scholar 

  159. B.K.P. Horn. Obtaining Shape from Shading Information, in The Psychology of Computer Vision, P.H. Winston, editor, pages 115–155. McGraw-Hill, New York, 1975.

    Google Scholar 

  160. B.K.P. Horn. Understanding image intensity. Artificial Intelligence, 8: 301–231, 1977.

    Article  Google Scholar 

  161. B.K.P. Horn and M. J. Brooks, editors. Shape from Shading. The MIT Press, Cambridge, 1989.

    Google Scholar 

  162. B.K.P. Horn and M.J. Brooks. The variational approach to shape from shading. Computer Vision, Graphics and Image Processing, 33 (2): 174–208, 1986.

    Article  Google Scholar 

  163. J. Hsiang. Refutational theorem proving using term-rewriting systems. Artificial Intelligence, pages 255–300, 1985.

    Google Scholar 

  164. 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, 6: 235–252, 1992.

    Article  MathSciNet  MATH  Google Scholar 

  165. X. Huang and J. Gu. A quantitative solution for constraint satisfaction. Submitted for publication. Mar. 1991.

    Google Scholar 

  166. X. Huang, J. Gu, and Y. Wu. A constrained approach to multifont character recognition. IEEE Transactions on Pattern Analysis And Machine Intelligence, 15 (8): 838–843, Aug. 1993.

    Article  Google Scholar 

  167. D.A. Huffman. Impossible Objects as Nonsense Sentences. In B. Meltzer and D. Michie, Eds., Machine Intelligence, pages 295–323. Edinburgh University Press, Edinburgh, Scotland,1971.

    Google Scholar 

  168. R. A. Hummel and S. W. Zucker. On the foundations of relaxation labeling processes. IEEE Trans, on Pattern Analysis and Machine Intelligence, PAMI-5(3): 267–287, May 1983.

    Article  MATH  Google Scholar 

  169. K. Ikeuchi. Model-based interpretation of range imagery. In Proc. of the DRAPA Image Understanding Workshop, pages 321–339. DRAPA, DoD, USA, DARPA, DoD, Feb. 23–25 1987.

    Google Scholar 

  170. K. Ikeuchi and B.K.P. Horn. Numerical shape from shading and occluding boundaries. Artificial Intelligence, 17 (1–3): 141–184, 1981.

    Article  Google Scholar 

  171. B. Indurkhya, H. S. Stone, and L. Xi-Cheng. Optimal partitioning of randomly generated distributed programs. IEEE Trans, on Software Engineering, SE-12: 483–495, Mar 1986.

    Google Scholar 

  172. T. Ishida. Parallel rule firing in production systems. IEEE Trans, on Knowledge and Data Engineering, 3 (1): 11–17, Mar. 1991.

    Article  Google Scholar 

  173. N. Itazaki and K. Kinoshita. Test pattern generation for circuits with tri-state modules by z-algorithm. IEEE Trans, on Computer-Aided Design, 8 (12): 1327–1334, Dec. 1989.

    Article  Google Scholar 

  174. K. Iwama. CNF satisfiability test by counting and polynomial average time. SIAM J. on Computing, pages 385–391, 1989.

    Google Scholar 

  175. F. Jahanian and A.K. Mok. Safety analysis of timing properties in real-time systems. IEEE Trans, on Software Engineering, SE-12(9): 890–904, Sept. 1986.

    Google Scholar 

  176. T. Jayasri and D. Basu. An Approach to Organizing Microinstructions Which Minimizes the Width of Control Store Words. IEEE Trans, on Computers, C-25: 514–521, May 1976.

    Article  MathSciNet  Google Scholar 

  177. R.E. Jeroslow and J. Wang. Solving propositional satisfiability problems. Annals of Mathematics and AI, 1: 167–187, 1990.

    MATH  Google Scholar 

  178. R.G. Jeroslow. Computation-oriented reductions of predicate to propositional logic. Decision Support Systems, 4: 183–197, 1988.

    Article  Google Scholar 

  179. D.S. Johnson. More approaches to the traveling salesman guide. Nature, 330: 525, 1987.

    Article  Google Scholar 

  180. D.S. Johnson. Local Optimization and the Traveling Salesman Problem. In M.S. Paterson, editor, Lecture Notes in Computer Science, Vol. 443: Automata, Languages and Programming,pages 446–461. Springer-Verlag, Berlin, 1990.

    Google Scholar 

  181. J.L. Johnson. A neural network approach to the 3-satisfiability problem. J. of Parallel and Distributed Computing, 6: 435–449, 1989.

    Article  Google Scholar 

  182. W. Lewis Johnson. Letter from the editor. SIGART Bulletin, 2(2):1, April 1991, ACM Press.

    Google Scholar 

  183. J. R. Josephson, B. Chandrasekaran, J. W. Smith Jr., and M. C. Tanner. A mechanism for forming composite explanatory hypotheses. IEEE Trans, on Systems, Man, and Cybernetics,SMC-17(3):445–454, May/June 1987.

    Article  Google Scholar 

  184. P.C. Jackson Jr. Heuristic search algorithms for the satisfiability problem. Submitted to the third IEEE TAI Conference, Jul. 1991.

    Google Scholar 

  185. Y.C. Ju, B. Rao, and R.A. Saleh. Consistency checking and optimization of macromodels. IEEE Trans, on Computer-Aided Design, 10 (8): 957–967, Aug. 1991.

    Article  Google Scholar 

  186. 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.

    Google Scholar 

  187. R.M. Karp. The Probabilistic Analysis of Some Combinatorial Search Algorithms. In Algorithms and Complexity: New Directions and Recent Results, pages 1–19. Academic Press, New York, 1976.

    Google Scholar 

  188. G. Kedem and H. Watanabe. Graph optimization techniques for IC layout and compaction. IEEE Trans, on Computer-Aided Design, CAD-3: 12–20, 1984.

    Article  Google Scholar 

  189. J. Kella. State Minimization of Incompletely Specified Sequential Machines. IEEE Trans, on Computers, C-19: 342–348, April 1970.

    MathSciNet  MATH  Google Scholar 

  190. S. Kirkpatrick, C.D. Gelat, and M.P. Vecchi. Optimization by simulated annealing. Science, 220: 671–680, 1983.

    Article  MathSciNet  Google Scholar 

  191. K.L. Kodandapani and E.J. McGrath. A wirelist compare program for verifying VLSI layouts. IEEE Design and Test of Computers, 3 (3): 46–51, 1986.

    Article  Google Scholar 

  192. E. Koutsoupias and C.H. Papadimitriou. On the greedy algorithm for satisfiability. Information Processing Letters, 43: 53–55, 10 August 1992.

    Article  MathSciNet  MATH  Google Scholar 

  193. R. Kowalski. A proof procedure using connection graphs. J. ACM, 22 (4): 572–595, Oct. 1975.

    Article  MATH  Google Scholar 

  194. M.R. Kramer and J. van Leeuwen. The Complexity of Wire Routing and Finding Minimum Area Layouts for Arbitrary VLSI Circuits, volume 2, chapter VLSI Theory, pages 129–146. Jai Press Inc., Greenwich, CT, 1984.

    Google Scholar 

  195. C.M. Krishna, K.G. Shin, and I.S. Bhandari. Processor tradeoffs in distributed real-time systems. IEEE Trans. on Computers, C-36(9): 1030–1040, Sept. 1987.

    Article  Google Scholar 

  196. V. Kumar. Algorithms for constraint satisfaction problems: A survey. Technical Report TR-91-28, Dept. of Computer Science, Univ. of Minnesota, 1991.

    Google Scholar 

  197. V. Kumar. Algorithms for constraint satisfaction problems: A survey. The AI Magazine, 13 (1): 32–44, 1992.

    Google Scholar 

  198. E.D. Lagnese and D.E. Thomas. Architectural partitioning for system level synthesis of integrated circuits. IEEE Trans, on Computer-Aided Design, 10 (7): 847–860, July 1991.

    Article  Google Scholar 

  199. G. Lakhani and R. Varadarajan. A wire-length minimization algorithm for circuit layout compaction. In Proc. of ISCAS’87, pages 276–279, May 1987.

    Google Scholar 

  200. B.S. Landman and R.L. Russo. On a pin versus block relationship for partitions of logic graphs. IEEE Trans, on Computers, C-20: 1469–1479, Dec. 1971.

    Article  Google Scholar 

  201. T. Larrabee. Test pattern generation using boolean satisfiability. IEEE Trans, on Computer-Aided Design, 11 (1): 4–15, Jan. 1992.

    Article  Google Scholar 

  202. C. Lassez. Constraint logic programming. BYTE Magazine, pages 171–176, Aug. 1987.

    Google Scholar 

  203. E.L. Lawler, J.K. Lenstra, A.H.G. Rinnooy Kan, and D.B. Shmoys, editors. The Traveling Salesman Problem. John Wiley and Sons, New York, 1985.

    MATH  Google Scholar 

  204. C. Lee. An algorithm for path connections and its applications. IEEE Trans, on Electronic Computers, VEC-10: 346–365, Sept. 1961.

    Article  Google Scholar 

  205. E.A. Lee. Consistency in dataflow graphs. IEEE Trans, on Parallel and Distributed Systems, 2 (2): 223–235, Apr. 1991.

    Article  Google Scholar 

  206. R.C.T. Lee. Private Communications, 1992–1993.

    Google Scholar 

  207. J.P. Lehoczky and L. Sha. Performance of real-time bus scheduling algorithms. ACM Performance Evaluation Review, 14(1), May 1986. Special Issue.

    Google Scholar 

  208. J. Li and M. Chen. Compiling communication-efficient programs for massively parallel machines. IEEE Trans, on Parallel and Distributed Systems, 2 (3): 361–376, July 1991.

    Article  Google Scholar 

  209. Y.-Z. Liao and C.K. Wong. An algorithm to compact a VLSI symbolic layout with mixed constraints. IEEE Trans, on Computer-Aided Design, CAD-2(2): 62–69, 1983.

    Article  Google Scholar 

  210. F.C.H. Lin and R.M. Keller. The gradient model load balancing method. IEEE Trans, on Software Engineering, SE-13(1): 32–38, Jan. 1987.

    Article  Google Scholar 

  211. S. Lin. Computer solutions of the traveling salesman problem. Bell Sys. Tech. Journal, 44 (10): 2245–2269, Dec. 1965.

    MATH  Google Scholar 

  212. R.P. Lippmann. An introduction to computing with neural net. IEEE ASSP Magazine, 4 (2): 4–22, April 1987.

    Article  Google Scholar 

  213. C.D. Locke. Best-Effort Decision Making for Real-Time Scheduling. PhD thesis, Carnegie-Mellon University, May 1985.

    Google Scholar 

  214. D.W. Loveland. Automated Theorem Proving: A Logical Basis. North-Holland, Amsterdam, 1978.

    MATH  Google Scholar 

  215. F. Luccio. Extending the Definition of Prime Compatibility Classes of States in Incompletely Specified Sequential Machine Reduction. IEEE Trans, on Computers, C-18: 537–540, Jun. 1969.

    Article  MATH  Google Scholar 

  216. D.G. Luenberger. Linear and Nonlinear Programming. Addison-Wesley, Reading, 1984.

    MATH  Google Scholar 

  217. N.A. Lynch. Multi-level atomicity — a new correctness criterion for database concurrency control. ACM Trans, on Database Systems, 8 (4), Dec. 1983.

    Google Scholar 

  218. A. K. Mackworth. Consistency in networks of relations. Artificial Intelligence, 8: 99–119, 1977.

    Article  MATH  Google Scholar 

  219. J. Malik and D. Maydan. Recovering three-dimensional shape from a single image of curved objects. IEEE Trans, on Pattern Analysis and Machine Intelligence, PAMI-11(6): 555–566, Jun. 1989.

    Article  Google Scholar 

  220. D. Marple and A.E. Gamal. Area-delay optimization of programmable logic arrays. Technical report, Stanford University, Sept. 1986.

    Google Scholar 

  221. T.A. Marsland and M. Campbell. Parallel search of strongly ordered game trees. Computing Surveys, 14 (4): 533–551, Dec. 1982.

    Article  Google Scholar 

  222. T.A. Marsland and J. Schaeffer. Computers, Chess, and Cognition. Springer-Verlag, New York, 1990.

    MATH  Google Scholar 

  223. D.W. Matula, W.G. Marble, and J.D. Isaacson. Graph coloring algorithms. In Graph Theory and Computing. R.C. Read, editor, pages 109–122. Academic Press, New York, 1972.

    Google Scholar 

  224. D. McAllester. Truth maintenance. In Proceedings of AAAI’90, pages 1109–1116, 1990.

    Google Scholar 

  225. J.J. McGregor. Relational consistency algorithms and their application in finding subgraph and graph isomorphisms. Information Sciences, 19: 229–250, 1979.

    Article  MathSciNet  MATH  Google Scholar 

  226. C.R. McLean and C.R. Dyer. An analog relaxation processor. In Proceedings of the 5th International Conference on Pattern Recognition, pages 58–60, 1980.

    Google Scholar 

  227. K. Mehlhorn. Data Structures and Algorithms: Graph Algorithms and NP-Completeness. Springer-Verlag, Berlin, 1984.

    MATH  Google Scholar 

  228. S. Minton, M.D. Johnston, A.B. Philips, and P. Laird. Solving large-scale constraint satisfaction and scheduling problems using a heuristic repair method. In Proceedings of AAAI’9O, pages 17–24, Aug. 1990.

    Google Scholar 

  229. D.P. Miranker. TREAT: A New and Efficient Match Algorithm for AI Production Systems. Pitman, London, 1990.

    MATH  Google Scholar 

  230. D.P. Miranker and B.J. Lofaso. The organization and performance of a treat-based production system compiler. IEEE Trans, on Knowledge and Data Engineering, 3 (1): 3–10, Mar. 1991.

    Article  Google Scholar 

  231. D. Mitchell, B. Selman, and H. Levesque. Hard and easy distributions of SAT problems. In Proceedings of AAAP’92, pages 459–465, Jul. 1992.

    Google Scholar 

  232. R. Mohr and T. C. Henderson. Arc and path consistency revisited. Artificial Intelligence, 28: 225–233, 1986.

    Article  Google Scholar 

  233. S. Mori, C.Y. Suen, and K. Yamamoto. Historical review of ocr research and development. Proceedings of the IEEE, 80 (7): 1029–1058, Jul. 1992.

    Article  Google Scholar 

  234. B.A. Nadel and J. Lin. Automobile transmission design as a constraint satisfaction problem: A collaborative research project with ford motor co. Technical report, Wayne State University, 1990.

    Google Scholar 

  235. D. Navinchandra. Exploration and Innovation in Design. Springer Verlag, Sadeh, 1990.

    Google Scholar 

  236. D. Navinchandra and D.H. Marks. Layout planning as a consistent labeling optimization problem. In Proceedings of 4th International Symposium on Robotics and AI in Construction, 1987.

    Google Scholar 

  237. A. Newell and H. A. Simon. Human Problem Solving. Prentice-Hall, Englewood Cliffs, New Jersey, 1972.

    Google Scholar 

  238. L.M. Ni, C. Xu, and T.B. Gendreau. A distributed drafting algorithm for load balancing. IEEE Trans, on Software Engineering, SE-11(10): 1153–1161, Oct. 1985.

    Article  Google Scholar 

  239. A. Nijenhuis and H. S. Wilf. Combinatorial Algorithms. Academic Press, New York, 1975.

    MATH  Google Scholar 

  240. N.J. Nilsson. Principles of Artificial Intelligence. Tioga Publishing Company, Palo Alto, California, 1980.

    MATH  Google Scholar 

  241. M. Nishizawa. Partitioning of logic units. Fujitsu Scientific and Technical Journal, 7 (2): 1–13, Jun. 1971.

    Google Scholar 

  242. D. Pager. On the efficient algorithm for graph isomorphism. J. ACM, 17 (4): 708–714, Jan. 1970.

    Article  MathSciNet  MATH  Google Scholar 

  243. C.H. Papadimitriou. On selecting a satisfying truth assignment. In Proceedings of the 32nd Annual Symposium of the Foundations of Computer Science, pages 163–169, 1991.

    Chapter  Google Scholar 

  244. C.H. Papadimitriou. Private Communications, Mar. 1992.

    Google Scholar 

  245. C.H. Papadimitriou and K. Steiglitz. On the complexity of local search for the traveling salesman problem. SIAM J. on Computing, 6 (1): 76–83, 1977.

    Article  MathSciNet  MATH  Google Scholar 

  246. C.H. Papadimitriou and K. Steiglitz. Combinatorial Optimization: Algorithms and Complexity. Prentice Hall, Englewood Cliffs, 1982.

    MATH  Google Scholar 

  247. A.M. Patel, N.L. Soong, and R.K. Korn. Hierarchical VLSI routing — an approximate routing procedure. IEEE Trans, on Computer-Aided Design, CAD-4(2): 121–126, Apr. 1985.

    Article  Google Scholar 

  248. W. Patterson. Mathematical Cryptology. Rowman and Littlefield, New Jersey, 1987.

    Google Scholar 

  249. P.G. Paulin and J.P. Knight. Force-directed scheduling for the behavioral synthesis of asic’s. IEEE Trans, on Computer-Aided Design, 8 (6): 661–679, June 1989.

    Article  Google Scholar 

  250. D. Pehoushek. SAT problem instances and algorithms. Private Communications, Stanford University, 1992.

    Google Scholar 

  251. M.A. Penna. A shape form shading analysis for a single perspective image of a polyhedron. IEEE Trans, on Pattern Analysis and Machine Intelligence, PAMI-ll(6):545–554, Jim. 1989.

    Article  Google Scholar 

  252. D.P. La Potin and S.W. Director. Mason: a global floorplanning approach for VLSI design. IEEE Trans, on Computer-Aided Design, CAD-5(4): 477–489, Oct. 1986.

    Google Scholar 

  253. D. K. Pradhan, editor. Fault-Tolerant Computing: Theory and Practice. Prentice-Hall,Englewood Cliffs, 1986.

    Google Scholar 

  254. D. Prawitz. An improved proof procedure. Theoria, 26 (2): 102–139, 1960.

    Article  MathSciNet  MATH  Google Scholar 

  255. P. Purdom. A survey of average time analyses of satisfiability algorithms. J. of Information Processing, 13 (4): 449–455, 1990.

    MATH  Google Scholar 

  256. P.W. Purdom. Tree size by partial backtracking. SIAM J. Compute 7 (4): 481–491, Nov. 1978.

    Article  MathSciNet  MATH  Google Scholar 

  257. P.W. Purdom. Search rearrangement backtracking and polynomial average time. Artificial Intelligence, 21: 117–133, 1983.

    Article  Google Scholar 

  258. P.W. Purdom. Private Communications, 1992–1993.

    Google Scholar 

  259. P.W. Purdom and C.A. Brown. An analysis of backtracking with search rearrangement. SIAM J. Compute 12 (4): 717 — 733, Nov. 1983.

    Article  MathSciNet  MATH  Google Scholar 

  260. P.W. Purdom and C.A. Brown. The pure literal rule and polynomial average time. SIAM J. Comput., 14: 943–953, 1985.

    Article  MathSciNet  MATH  Google Scholar 

  261. P.W. Purdom and C.A. Brown. Polynomial-average-time satisfiability problems. Information Science, 41: 23–42, 1987.

    Article  MathSciNet  MATH  Google Scholar 

  262. P.W. Purdom, C.A. Brown, and E.L. Robertson. Backtracking with multi-level dynamic search rearrangement. Acta Informatica, 15: 99–113, 1981.

    Article  MathSciNet  MATH  Google Scholar 

  263. R. Puri and J. Gu. An efficient algorithm to search for minimal closed covers in sequential machines. IEEE Transactions on CAD, 12 (6): 737–745, Jun. 1993.

    Google Scholar 

  264. R. Puri and J. Gu. An efficient algorithm for microword length minimization. IEEE Transactions on CAD, 12 (10): 1449 — 1457, Oct. 1993.

    Google Scholar 

  265. R. Puri and J. Gu. A modular partitioning approach for asynchronous circuit synthesis. IEEE Transactions on CAD, to appear.

    Google Scholar 

  266. C. D. V. P. Rao and N. N. Biswas. On the Minimization of Wordwidth in the Control Memory of a Microprogrammed Digital Computer. IEEE Trans, on Computers, C-32(9): 863–868, Sept. 1983.

    Article  Google Scholar 

  267. C. V. S. Rao and N. N. Biswas. Minimization of Incompletely Specified Sequential Machines. IEEE Trans, on Computers, C-24: 1089–1100, Nov. 1975.

    Article  MathSciNet  MATH  Google Scholar 

  268. R.C. Read and D.G. Corneil. The graph isomorphism disease. J. of Graph Theory, 1: 339–363, 1977.

    Article  MathSciNet  MATH  Google Scholar 

  269. G.M. Reed and A.W. Roscoe. A timed model for communicating sequential processes. In Proc. of ICALP’86, pages 314–323. Springer LNCS 226, 1986.

    Google Scholar 

  270. J. Reed, A. Sangiovanni-Vincentelli, and M. Santomauro. A new symbolic channel router: YACR2. IEEE Trans. on Computer-Aided Design, CAD-4(3): 208–219, July 1985.

    Article  Google Scholar 

  271. R.L. Rivest. Cryptography. In Handbook of Theoretical Computer Science. J. V. Leeuwen, editor, chapter 13, pages 719–756. The MIT Press, Cambridge, 1990.

    Google Scholar 

  272. R.L. Rivest and C.M. Fiduccia. A ‘greedy’ channel router. In Proc. of the 19th ACM/IEEE DAC, pages 418–424, Jun. 1982.

    Google Scholar 

  273. J.A. Robinson. A machine-oriented logic based on the resolution principle. Journal of the ACM, pages 23–41, 1965.

    Google Scholar 

  274. A. Rosenfeld. Computer vision: Basic principles. Proceedings of the IEEE, 76 (8): 863–868, Aug. 1988.

    Article  Google Scholar 

  275. A. Rosenfeld, R. A. Hummel, and S. W. Zucker. Scene labeling by relaxation operations. IEEE Trans, on Systems, Man, and Cybernetics, SMC-6(6): 420–433, June 1976.

    Article  MathSciNet  MATH  Google Scholar 

  276. A.E. Ruehli, P.K. Wolff, and G. Goertzel. Analytical power/timing optimization technique for digital system. In Proc. of the 14th ACM/IEEE DAC, pages 142–146, Jun. 1977.

    Google Scholar 

  277. R.L. Russo. On the tradeoff between logic performance and circuit-to-pin ratio for LSI. IEEE Trans, on Computers, C-21: 147–153, 1972.

    Article  Google Scholar 

  278. R.L. Russo, P.H. Oden, and P.K. Wolff. A heuristic procedure for the partitioning and mapping of computer logic graphs. IEEE Trans, on Computers, C-20: 1455–1462, Dec. 1971.

    Article  Google Scholar 

  279. Y.G. Saab and V. B. Rao. Combinatorial optimization by stochastic evolution. IEEE Transactions on CAD, CAD-10(4): 525–535, Apr. 1991.

    Google Scholar 

  280. A. Saldanha, T. Villa, R.K. Brayton, and A.L. Sangiovanni-Vincentelli. A Framework for Satisfying Input and Output Encoding Constraints. In Proceedings of ACM/IEEE Design Automation Conference, pages 170–175, 1991.

    Google Scholar 

  281. T.J. Schaefer. The complexity of satisfiability problems. In Proceedings of the 10th ACM Symposium on Theory of Computing, pages 216–226, 1978.

    Google Scholar 

  282. W.L. Schiele. Improved compaction by minimized length of wires. In Proc. of the 20th ACM/IEEE DAC, pages 121–127, 1983.

    Google Scholar 

  283. B.M. Schwartzschild. Statistical mechanics algorithm for monte carlo optimization. Physics Today, 35: 17–19, 1982.

    Google Scholar 

  284. P. Schwarz and A. Spector. Synchronizing shared abstract types. ACM Trans. on Computer Systems, Aug. 1984.

    Google Scholar 

  285. C. Sechen and A.L. Sangiovanni-Vinpentelli. The timberwolf placement and routing package. In Proc. of the 1984 Custom Integrated Circuit Conf., May 1984.

    Google Scholar 

  286. B. Selman. Private Communications, Aug. 1992.

    Google Scholar 

  287. B. Selman, H. Levesque, and D. Mitchell. A new method for solving hard satisfiability problems. In Proceedings of AAAI’92, pages 440–446, Jul. 1992.

    Google Scholar 

  288. M.J. Shensa. A computational structure for the propositional calculus. In Proceedings of IJCAI, pages 384–388, 1989.

    Google Scholar 

  289. R.C.-J. Shi. An improvement on Karmarkar’s algorithm for integer programming. Jun. 1992.

    Google Scholar 

  290. H. Shin, A.L. Sangiovanni-Vincentelli, and C.H. Sequin. Two-dimensional compaction by ‘zero refining’. In Proc. of the 23th ACM/IEEE DAC, pages 115–122, Jun. 1986.

    Google Scholar 

  291. K.G. Shin and M.-S. Chen. On the number of acceptable task assignments in distributed computing systems. IEEE Trans, on Computers, 39 (1): 99–110, Jan. 1990.

    Article  MathSciNet  Google Scholar 

  292. P. Siegel. Representation et Utilization de la Connaissances en Calcul Propositionel. PhD thesis, University Aix-Marseille II, 1987.

    Google Scholar 

  293. J.C. Simon. Off-line cursive word recognition. Proceedings of the IEEE, 80 (7): 1150–1161, Jul. 1992.

    Article  Google Scholar 

  294. R. Sosič and J. Gu. Quick n -queen search on VAX and Bobcat machines. CS 547 AI Class Project, Winter Quarter Feb. 1988.

    Google Scholar 

  295. R. Sosič and J. Gu. How to search for million queens. Technical Report UUCS-TR-88-008, Dept. of Computer Science, Univ. of Utah, Feb. 1988.

    Google Scholar 

  296. R. Sosič and J. Gu. A polynomial time algorithm for the n -queens problem. SIGART Bulletin, 1(3):7–11, Oct. 1990, ACM Press.

    Article  Google Scholar 

  297. R. Sosič eind J. Gu. Fast search algorithms for the n -queens problem. IEEE Trans, on Systems, Man, and Cybernetics, SMC-21(6):1572–1576, Nov./Dec. 1991.

    Article  MATH  Google Scholar 

  298. R. Sosič and J. Gu. 3,000,000 queens in less than one minute. SIGART Bulletin, 2(2):22–24, Apr. 1991, ACM Press.

    Google Scholar 

  299. R. Sosič and J. Gu. Efficient local search with conflict minimization. IEEE Trans, on Knowledge and Data Engineering, Vol. 6, 1994.

    Google Scholar 

  300. R. Sosič, J. Gu, and R. Johnson. The Unison algorithm: Fast evaluation of Boolean expressions. Communications of ACM, accepted for publication in 1992.

    Google Scholar 

  301. R. Sosič, J. Gu, and R. Johnson. A universal Boolean evaluator. to appear.

    Google Scholar 

  302. J. Soukup. Circuit layout. In Proceedings of the IEEE, pages 1281–1304, Oct. 1981.

    Google Scholar 

  303. J. Stankovic, K. Ramamritham, and S. Cheng. Evaluation of a bidding algorithm for hard real-time distributed systems. IEEE Trans. on Computers, C-34(12): 1130–1143, Dec. 1985.

    Google Scholar 

  304. J.A. Stankovic. Real-time computing systems: The next generation. Manuscript. Feb. 18, 1988.

    Google Scholar 

  305. H.S. Stone and J.M. Stone. Efficient search techniques — an empirical study of the n -queens problem. IBM J. Res. Develop., 31 (4): 464–474, July 1987.

    Google Scholar 

  306. G. Strang. Linear Algebra and Its Applications. Academic Press, New York, 1976.

    MATH  Google Scholar 

  307. C.Y. Suen, M. Berthod, and S. Mori. Automatic recognition of handprinted characters — the state of the art. Proceedings of the IEEE, 68 (4): 469–487, Apr. 1980.

    Article  Google Scholar 

  308. S. Sutanthavibul, E. Shragowitz, and J.B. Rosen. An analytical approach to floorplan design and optimization. IEEE Trans, on Computer-Aided Design, 10 (6): 761–769, June 1991.

    Article  Google Scholar 

  309. M. Takashima, T. Mitsuhashi, T.Chiba, and K. Yoshida. Programs for verifying circuit connectivity of MOS/VLSI artwork. In Proc. of the 19th ACM/IEEE DAC, pages 544–550, 1982.

    Google Scholar 

  310. H. Tokuda, J. Wendorf, and H. Wang. Implementation of a time driven scheduler for real-time operating systems. In Proc. of the Real-Time Systems Symposium, Dec. 1987.

    Google Scholar 

  311. P. P. Trabado, A. Lloris-Ruiz, and J. Ortega-Lopera. Solution of Switching Equations Based on a Tabular Algebra. IEEE Trans, on Computers, C-42: 591–596, May 1993.

    Article  Google Scholar 

  312. G.S. Tseitin. On the Complexity of Derivations in Propositional Calculus. In Structures in Constructive Mathematics and Mathematical Logic, Part II, A.O. Slisenko, ed., pages 115–125. 1968.

    Google Scholar 

  313. K. J. Turner. Computer Perception of Curved Objects Using a Television Camera. PhD thesis, Univ. Edinburgh, 1974.

    Google Scholar 

  314. J.D. Tygar and R. Ellickson. Efficient netlist comparison using hierarchy and randomization. In Proc. of the 22th ACM/IEEE DAC, pages 702–708, 1985.

    Chapter  Google Scholar 

  315. J.D. Ullman. Principles of Database Systems. Computer Science Press, Rockville, 1982.

    MATH  Google Scholar 

  316. J.R. Ullman. An algorithm for subgraph isomorphism. J. ACM, 23 (1): 31–42, Jan. 1976.

    Article  MATH  Google Scholar 

  317. J.R. Ullman. A binary n-gram technique for automatic correction of substitution, deletion, insertion and reversal errors in words. The Computer Journal, 20 (2): 141–147, Feb. 1977.

    Article  Google Scholar 

  318. S.D. Urban and L.M.L. Delcambre. Constraint analysis: A design process for specifying operations on objects. IEEE Trans, on Knowledge and Data Engineering, 2 (4): 391–400, Dec. 1990.

    Article  Google Scholar 

  319. M. van der Woude and X. Timermans. Compaction of hierarchical cells with minimum and maximum compaction constraints. In Proc. Intl. Symposium on Circuits and Systems, pages 1018–1021, 1983.

    Google Scholar 

  320. P. Vanbekbergen, B. Lin, G. Goossens, and H. De Man. A Generalized State Assignment Theory for Transformations on Signal Transition Graphs. In Proceedings of ICCAD’92, pages 112–117, 1992.

    Google Scholar 

  321. P. Vanbekbergen, B. Lin, G. Goossens, and H. De Man. A Generalized State Assignment Theory for Transformations on Signal Transition Graphs. J. of VLSI Signal processing, 1993. In Press.

    Google Scholar 

  322. D. Waltz. Generating semantic descriptions from drawings of scenes with shadows. Technical Report AI271, MIT, Nov. 1972.

    Google Scholar 

  323. D. Waltz. Understanding Line Drawings of Scenes with Shadows. In P. H. Winston, The Psychology of Computer Vision, chapter 2, pages 19–92. McGraw-Hill Book Company, New York, 1975.

    Google Scholar 

  324. H.P. Williams. Linear and integer programming applied to the propositional calculus. Systems Research and Information Sciences, 2: 81 — 100, 1987.

    Google Scholar 

  325. P.H. Winston. Artificial Intelligence. Addison-Wesley, Reading, 1984.

    MATH  Google Scholar 

  326. L.C. Wu and C.Y. Tang. Solving the satisfiability problem by using randomized approach. Information Processing Letters, 41: 187–190, 1992.

    Article  MathSciNet  MATH  Google Scholar 

  327. T. Y. Young and K. S. Fu, editors. Handbook of Pattern Recognition and Image Processing. Academic Press, Orlando, 1986.

    MATH  Google Scholar 

  328. R. Zabih and D. McAllester. A rearrangement search strategy for determining propositional satisfiability. In Proceedings of AAAI’88, pages 155–160, 1988.

    Google Scholar 

  329. V.N. Zemlyachenko, N.M. Korneeko, and R.I. Tyshkevich. Graph isomorphism problem. J. of Soviet Mathematics, 29: 1426–1481, 1985.

    Article  MATH  Google Scholar 

  330. S. Zhou. A trace-driven simulation study of dynamic load balancing. IEEE Trans, on Software Engineering, SE-14(9): 1327–1341, Sept. 1988.

    Article  Google Scholar 

  331. S. W. Zucker, R. A. Hummel, and A. Rosenfeld. An application of relaxation labeling to line and curve enhancement. IEEE Trans, on Computers, C-26: 394–403, 922–929, 1977.

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dept. of Electrical and Computer Engineering, University of Calgary, Calgary, Alberta, T2N 1N4, Canada

    Jun Gu

Authors
  1. Jun Gu
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. University of Minnesota, USA

    Ding-Zhu Du

  2. Institute of Applied Mathematics, Beijing, China

    Ding-Zhu Du

  3. National University of Singapore, Singapore

    Jie Sun

Rights and permissions

Reprints and permissions

Copyright information

© 1994 Kluwer Academic Publishers

About this chapter

Cite this chapter

Gu, J. (1994). Optimization Algorithms for the Satisfiability (SAT) Problem. In: Du, DZ., Sun, J. (eds) Advances in Optimization and Approximation. Nonconvex Optimization and Its Applications, vol 1. Springer, Boston, MA. https://doi.org/10.1007/978-1-4613-3629-7_6

Download citation

  • DOI: https://doi.org/10.1007/978-1-4613-3629-7_6

  • Publisher Name: Springer, Boston, MA

  • Print ISBN: 978-1-4613-3631-0

  • Online ISBN: 978-1-4613-3629-7

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation