Advertisement

Algorithms for the Satisfiability (SAT) Problem

  • Jun Gu
  • Paul W. Purdom
  • John Franco
  • Benjamin W. Wah

Abstract

An instance of the satisfiability (SAT) problem is a Boolean formula that has three components [102, 191]:
  • A set of n variables: x 1, x 2, x n .

  • A set of literals. A literal is a variable (Q = x) or a negation of a variable \( \left( {Q = \bar x} \right)\).

  • A set of m distinct clauses: C 1, C 2, ..., C m. Each clause consists of only literals combined by just logical or (V) connectives.

Keywords

Local Search Constraint Satisfaction Problem Local Search Algorithm Conjunctive Normal Form Disjunctive Normal Form 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [1]
    L. Abel. On the order of connections for automatic wire routing.IEEE Trans. on Computers, pages 1227–1233, Nov. 1972.Google Scholar
  2. [2]
    B. Abramson and M. Yung. Divide and conquer under global constraints: A solution to the n-queens problem.Journal of Parallel and Distributed Computing, 6: 649–662, 1989.CrossRefGoogle Scholar
  3. [3]
    Leonard M. Adleman Molecular Computation of Solutions to Combinatorial ProblemsScience, 266: 1021–1024, 1994.CrossRefGoogle Scholar
  4. [4]
    T. Agerwala. Microprogram Optimization: A Survey.IEEE Trans. on Computers, C-25: 962–973, Oct. 1976.Google Scholar
  5. [5]
    A.V. Aho, J.E. Hoperoft, and J.D. Ullman.The Design and Analysis of Computer Algorithms. Addison-Wesley, Reading, 1974.zbMATHGoogle Scholar
  6. [6]
    A.V. Aho, J.E. Hoperoft, and J.D. Ullman.Data Structures and Algorithms. Addison-Wesley, Reading, 1985.Google Scholar
  7. [7]
    A.V. Aho, R. Sethi, and J.D. Ullman.Compilers. Addison-Wesley, Reading, 1986.Google Scholar
  8. [8]
    A.V. Aho, D.S. Johnson, R.M. Karp, S.R. Kosaraju, C.C. McGeoch, C.H. Papadimitriou, and P. Pevzner,Theory of computing: Goals and directions, March 15, 1996.Google Scholar
  9. [9]
    S.B. Akers. Binary decision diagramsIEEE Transactions on Computers, C-27(6): 509–516, Jun. 1978.Google Scholar
  10. [10]
    W. Ahrens. Mathematische Unterhaltungen und Spiele (in German).B.G. Teubner (Publishing Company), Leipzig, 1918–1921.Google Scholar
  11. [11]
    S.B. Akers. On the use of the linear assignment algorithm in module placement. InProc. of the 18th ACM/IEEE Design Automation Conference, pages 137–144, 1981.CrossRefGoogle Scholar
  12. [12]
    J. Aloimonos. Visual shape computation.Proceedings of the IEEE, 76: 899–916, Aug. 1988.CrossRefGoogle Scholar
  13. [13]
    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
  14. [14]
    J.A. Anderson and E. Rosenfeld, editors.Neurocomputing: Foundations of Research. MIT Press, Cambridge, 1988.Google Scholar
  15. [15]
    S. Arora, C. Lund, R. Motwani, M. Sudan, and M. Szegedy. Proof verification and hardness of approximation problems. InProceedings 33rd IEEE Symposium on the Foundations of Computer Science, pages 14–23, 1992.CrossRefGoogle Scholar
  16. [16]
    K. J. Arrow and L. Hurwitz. Gradient method for concave programming, I: Local results. In K. J. Arrow, L. Hurwica, and H. Uzawa, editors,Studies in Linear and Nonlinear Programming. Stanford University Press, Stanford, CA, 1958.Google Scholar
  17. [17]
    P. Ashar, A. Ghosh, and S. Devadas. Boolean satisfiability and equivalence checking using general Binary Decision DiagramsIntegration,the VLSI journal, 13: 1–16, 1992.CrossRefGoogle Scholar
  18. [18]
    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.MathSciNetzbMATHCrossRefGoogle Scholar
  19. [19]
    B. Aspvall. Recognizing disguised NR(1) instances of the satisfiability problem.Journal of Algorithms 1, pages 97–103, 1980.MathSciNetzbMATHCrossRefGoogle Scholar
  20. [20]
    A. Bagchi, B. Servatius, and W. Shi. Fault tolerance in massively parallel computers. Presented in the 3rd International Symposium on AI & Mathematics, Jan. 1994.Google Scholar
  21. [21]
    H. Baird. Anatomy of a versatile page reader.Proceedings of the IEEE, 80 (7): 1059–1065, Jul. 1992.CrossRefGoogle Scholar
  22. [22]
    D. H. Ballard and C. M. Brown.Computer Vision. Prentice-Hall, Englewood Cliffs, New Jersey, 1982.Google Scholar
  23. [23]
    P. Banerjee, M.H. Jones, and J.S. Sargent. Parallel simulated annealing algorithms for cell placement on hypercube multiprocessors.IEEE Trans. on Parallel and Distributed Systems, 1 (1): 91–106, Jan. 1990.CrossRefGoogle Scholar
  24. [24]
    A.E. Barbour. Solutions to the minimization problem of fault-tolerant logic circuits.IEEE Trans. on Computers, 41 (4): 429–443, Apr. 1992.MathSciNetCrossRefGoogle Scholar
  25. [25]
    P. Beame and T. Pitassi. Simplified and improved resolution lower bounds. InProceedings of the 38th Annual Symposium of the Foundations of Computer Science, to appear, 1997.Google Scholar
  26. [26]
    S. Ben-Davis, B. Chor, O. Goldreich, and M. Luby. On the theory of average case complexity.J. of Computer and Systems Sciences, 44: 193–219, 1992.CrossRefGoogle Scholar
  27. [27]
    A. Ben-Tal, G. Eiger, and V. Gershovitz. Global minimization by reducing the duality gap.Mathematical Programming, 63: 193–212, 1994.MathSciNetzbMATHCrossRefGoogle Scholar
  28. [28]
    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
  29. [29]
    A. Beringer, G. Aschemann, H.H. Hoos, M. Metzger, and A. Wei. GSAT versus simulated annealing. InProceedings of ECAI’94, pages 130–134, 1994.Google Scholar
  30. [30]
    K. Berman, J. Franco, and J. Schlipf. Unique satisfiability for Horn sets can be solved in nearly linear time.Proc. Seventh Advanced Research Institute in Discrete Applied Mathematics (ARIDAM), New Brunswick, New Jersey, May, 1992. InDiscrete Applied Mathematics 60:77–91, 1995.Google Scholar
  31. [31]
    B. Bernhardsson. Explicit solutions to the n-queens problems for all n. ACM SIGART Bulletin,2(2):7, Apr. 1991, ACM Press.Google Scholar
  32. [32]
    P.A. Berstein, V. Hadzilacos, and N. Goodman.Concurrency Control and Recovery in Database Systems. Addison-Wesley Publication, 1987.Google Scholar
  33. [33]
    Wolfgang Bibel. Automated theorem proving.Vieweg, 1982.Google Scholar
  34. [34]
    N. N. Biswas. State Minimization of Incompletely Specified Sequential Machines.IEEE Trans. on Computers,C-23: 80–84, Jan. 1974.Google Scholar
  35. [35]
    J. R. Bitner and E. M. Reingold. Backtrack programming techniques.Comm. of ACM, 18 (11): 651–656, Nov. 1975.zbMATHCrossRefGoogle Scholar
  36. [36]
    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.MathSciNetCrossRefGoogle Scholar
  37. [37]
    J.P. Blanks. Near-optimal placement using a quadratic objective function. InProc. of the 22th ACM/IEEE Design Automation Conference, pages 609–615, 1985.CrossRefGoogle Scholar
  38. [38]
    J. Blazewicz. Scheduling dependent tasks with different arrival times to meet deadlines. InProc. of the International Workshop on Modeling and Performance Evaluation of Computer Systems, pages 57–65, 1976.Google Scholar
  39. [39]
    M. Böhm and E. Speckenmeyer. A fast parallel SAT-solver efficient workload balancing. Presented in the 3rd International Symposium on AI & Mathematics, Jan. 1994. To appear in Annals of Mathematics and Artificial Intelligence.Google Scholar
  40. [40]
    S. H. Bokhari. Partitioning problems in parallel, pipelined, and distributed computing.IEEE Trans. on Computers, 37 (1): 48–57, Jan 1988.MathSciNetCrossRefGoogle Scholar
  41. [41]
    F. Bonomi. On job assignment for a parallel system of processor sharing queues.IEEE Trans. on Computers, 39 (7): 858–869, July 1990.CrossRefGoogle Scholar
  42. [42]
    E. Boros, P.L. Hammer, and A. Kogan. Computational experiments with an exact SAT solver. Presented in the 3rd International Symposium on AI & Mathematics, Jan. 1994.Google Scholar
  43. [43]
    E. Boros, Y. Crama, P. L. Hammer. Polynomial-time inference of all valid implications for Horn and related formulae.Annals of Mathematics and Artificial Intelligence 1, pages 21–32, 1990.zbMATHCrossRefGoogle Scholar
  44. [44]
    E. Boros, P. L. Hammer, and X. Sun. Recognition of q-Horn formulae in linear time.Discrete Applied Mathematics 55, pages 1–13, 1994.MathSciNetzbMATHCrossRefGoogle Scholar
  45. [45]
    E. Boros, Y. Crama, P. L. Hammer, and M. Saks. A complexity index for satisfiability problems.SIAM Journal on Computing 23, pages 4549, 1994.MathSciNetCrossRefGoogle Scholar
  46. [46]
    H.N. Brady. An approach to topological pin assignment.IEEE Trans. on CAD, Vol. 3, pp. 250–255, July 1984.Google Scholar
  47. [47]
    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
  48. [48]
    M.A. Breuer. Min-cut placement.J. of Design Automation and Fault Tolerant Computing, 1: 343–362, 1976.Google Scholar
  49. [49]
    F. Brewer and D. Gajski. Chippe: A system for constraint driven behavioral synthesis.IEEE Trans. on CAD, 9 (7): 681–695, July 1990.Google Scholar
  50. [50]
    A.Z. Broder, A.M. Frieze, and E. Upfal. On the satisfiability and maximum satisfiability of random 3-CNF formulas. InProceedings of the Fourth Annual ACM-SIAM Symposium on Discrete Algorithms, pages 322–330, 1993.Google Scholar
  51. [51]
    M.J. Brooks and B.K.P. Horn. Shape and source from shading. InProc. of IJCAI’85, pages 932–936, Aug. 1985.Google Scholar
  52. [52]
    C.A. Brown, L.A. Finklestein, and P.W. Purdom. Backtrack Searching in the Presence of Symmetry.6th International Conference on Algebraic Algorithms and Error Correcting Codes (AAECC), Lecture Notes in Computer Science, Vol. 357, pp. 99–110.Google Scholar
  53. [53]
    C.A. Brown, L.A. Finklestein, and P.W. Purdom. Backtrack Searching in the Presence of Symmetry. Nordic Journal of Computing, to appear.Google Scholar
  54. [54]
    C.A. Brown and P.W. Purdom. An average time analysis of backtracking.SIAM J. on Computing, 10 (3): 583–593, Aug. 1981.MathSciNetzbMATHCrossRefGoogle Scholar
  55. [55]
    C.A. Brown and P.W. Purdom. An empirical comparison of backtracking algorithms.IEEE Trans. on Pattern Analysis and Machine Intelligence, PAMI-4(3): 309–316, May 1982.Google Scholar
  56. [56]
    B. Bruderlin. Constructing three dimensional geometric objects defined by constraints. InProceedings of 1986 ACM SIGGRAPH Workshop in Interactive Graphics, 1986.Google Scholar
  57. [57]
    M. Bruynooghe. Solving combinatorial search problems by intelligent backtracking.Information Processing Letters, 12 (1): 36–39, 1981.CrossRefGoogle Scholar
  58. [58]
    M. Bruynooghe. Graph coloring and constraint satisfaction. Technical Report CW 44, Dept. of Computer Science, Katholieke Universiteit Leuven, Dec. 1985.Google Scholar
  59. [59]
    M. Bruynooghe and L.M. Pereira.Deduction Revision by Intelligent Backtracking, pages 194–215. Ellis Horwood Limited, 1984.Google Scholar
  60. [60]
    R.E. Bryant. Graph-based algorithms for Boolean function manipulation.IEEE Trans. on Computers, C-35(8): 677–691, Aug. 1986.Google Scholar
  61. [61]
    R.E. Bryant. Symbolic Boolean manipulation with ordered binary-decision diagrams.ACM Computing Surveys, 24 (3): 293–318, Sept. 1992.CrossRefGoogle Scholar
  62. [62]
    R.E. Bryant. Binary Decision Diagrams Applied to SAT and Related Problems. Presented at 1996 DIMACS Workshop on Satisfiability Problem: Theory and Applications. March 11, 1996.Google Scholar
  63. [63]
    H. Kleine Büning. On generalized Horn formulas andk resolution.Theoretical Computer Science 116, pages 405–413, 1993.MathSciNetzbMATHCrossRefGoogle Scholar
  64. [64]
    H. Kleine Biining and T. Lettmann. Aussagenlogik: Deduktion and Algorithmen. B.G. Teubner, Stuttgart, 1993. English version to appear in 1996.Google Scholar
  65. [65]
    K. Bugrara and P. Purdom. Clause order backtracking. Technical Report 311, 1990.Google Scholar
  66. [66]
    K.M. Bugrara and C.A. Brown. On the average case analysis of some satisfiability model problems.Information Sciences, 40: 21–37, 1986.MathSciNetCrossRefGoogle Scholar
  67. [67]
    K.M. Bugrara, Y.F. Pan, and P. Purdom. Exponential average time for the pure literal rule.SIAM J. on Computing, 18: 409–418, 1989.MathSciNetzbMATHCrossRefGoogle Scholar
  68. [68]
    A. Bundy, editor.Catalogue of Artificial Intelligence Tools. Springer-Verlag, Berlin, 1984.zbMATHGoogle Scholar
  69. [69]
    J.L. Burns and A.R. Newton. Efficient constraint generation for hierarchical compaction. InProc. Intl Conf. on Computer Design, pages 197–200. IEEE Computer Society, Oct. 1987.Google Scholar
  70. [70]
    M. Buro and H.K. Büning. Report on a SAT competition. Technical report, FB-17 — Mathematik/Informatik, Universitat Paderborn, Nov. 1992.Google Scholar
  71. [71]
    M. Buro and H.K. Büning. Report on a SAT competition.Bulletin of the European Association for Theoretical Computer Science, 49: 143151, Feb. 1993.Google Scholar
  72. [72]
    M. Burstein and R. Pelavin. Hierarchical channel router. InProc. of the 20th ACM/IEEE Design Automation Conference, pages 591–597, Jun. 1983.CrossRefGoogle Scholar
  73. [73]
    G. Butler. Computing in Permutation and Matrix Groups II: Backtrack Algorithm.Math. Comp. 39: 671–680, 1982.Google Scholar
  74. [74]
    G. Butler and C.W.H. Lain. A General Backtracking Algorithm for the Isomorphism Problem of Combinatorial Objects. J. Symbolic Computation 1: 363–381, 1985.zbMATHCrossRefGoogle Scholar
  75. [75]
    V. Cerny. Thermodynamical approach to the traveling salesman problem: An efficient simulation algorithm.Journal of Optimization Theory and Applications, 45: 41–51, 1985.MathSciNetzbMATHCrossRefGoogle Scholar
  76. [76]
    S. Chakradhar, V. Agrawal, and M. Bushnell. Neural net and Boolean satisfiability model of logic circuits.IEEE Design &Test of Computers, pages 54–57, Oct. 1990.Google Scholar
  77. [77]
    I. Chakravarty. A generalized line and junction labeling scheine with applications to scene analysis.IEEE Trans. on Pattern Analysis and Machine Intelligence, PAMI-1(2): 202–205, Apr. 1979.Google Scholar
  78. [78]
    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.CrossRefGoogle Scholar
  79. [79]
    A.K. Chandra and P.M. Merlin. Optimal implementation of conjunctive queries in relational databases. InProceedings of the 9th ACM Symposium on Theory of Computing, pages 77–90, 1977.Google Scholar
  80. [80]
    V. Chandru and J. N. Hooker. Extended Horn sets in propositional logic.J. ACM 38, pages 205–221, 1991.MathSciNetzbMATHCrossRefGoogle Scholar
  81. [81]
    Y. Chang and B. W. Wah. Lagrangian techniques for solving a class of zero-one integer linear programs. InProc. Computer Software and Applications Conf., 1995.Google Scholar
  82. [82]
    Y.-J. Chang and B. W. Wah. Lagrangian techniques for solving a class of zero-one integer linear programs In Proc. Computer Software and Applications Conference,pages 156–161, Dallas, TX, August 1995. IEEEGoogle Scholar
  83. [83]
    M.T. Chao and J. Franco. Probabilistic analysis of two heuristics for the 3-satisfiability problem.SIAM J. on Computing, 15: 1106–1118, 1986.MathSciNetzbMATHCrossRefGoogle Scholar
  84. [84]
    M. T. Chao and J. Franco. Probabilistic analysis of a generalization of the unit-clause literal selection heuristics for thek satisfiable problem.Information Sciences, 51: 289–314, 1990.MathSciNetzbMATHCrossRefGoogle Scholar
  85. [85]
    R. Chandrasekaran. Integer programming problems for which a simple rounding type of algorithm works. In W. Pulleyblank, ed.Progress in Combinatorial Optimization. Academic Press Canada, Toronto, Ontario, Canada, pages 101–106, 1984.Google Scholar
  86. [86]
    H.R. Charney and D.L. Plato. Efficient partitioning of components. InProc. of the 5th Annual Design Automation Workshop, pages 16–21, 1968.Google Scholar
  87. [87]
    V. Chvâtal and E. Szemerédi. Many hard examples for resolution.J. of ACM, 35: 759–770, 1988.zbMATHCrossRefGoogle Scholar
  88. [88]
    W.T. Chen and L.L. Liu. Parallel approach for theorem proving in propositional logic.Inform. Sci., 41 (1): 61–76, 1987.MathSciNetzbMATHGoogle Scholar
  89. [89]
    R. T. Chin and C. R. Dyer. Model-based recognition in robot vision.ACM Computing Surveys, 18 (1): 67–108, Mar. 1986.CrossRefGoogle Scholar
  90. [90]
    Tam-Anh Chu.Synthesis of Self-Timed VLSI Circuits from Graph-theoretic Specifications. PhD thesis, Dept. of Electrical Engineering and Computer Science, MIT, June 1987.Google Scholar
  91. [91]
    Y. Chu, editor.Special Section on Chinese/Kanji Text and Data Processing. IEEE Computer, volume 18, number 1. IEEE Computer Society Press, 1985.Google Scholar
  92. [92]
    V. Chvâtal and B. Reed. Mick gets some (the odds are on his side). InProceedings on the Foundations of Computer Science, 1992.Google Scholar
  93. [93]
    A. Cichocki and R. Unbehauen. Switched-capacitor artificial neural networks for nonlinear optimization with constraints. InProc. of 1990 IEEE Int’l Symposium on Circuits and Systems, pages 2809–2812, 1990.CrossRefGoogle Scholar
  94. [94]
    J. Cleary. Logical arithmetic.Future Computing Systems, 2 (2), 1987.Google Scholar
  95. [95]
    W. F. Clocksin and C. S. Mellish.Programming in Prolog (2nd Edition). Springer-Verlag, Berlin, 1984.CrossRefGoogle Scholar
  96. [96]
    M.B. Clowes. On seeing things.Artificial Intelligence, 2: 79–116, 1971.CrossRefGoogle Scholar
  97. [97]
    J. Cohen, editor.Special Section on Logic Programming. Comm. of the ACM, volume 35, number 3. 1992.Google Scholar
  98. [98]
    J.P. Cohoon and W.D. Paris. Genetic placement. InDigest of the Int’l Conf. on Computer-Aided Design, pages 422–425, 1986.Google Scholar
  99. [99]
    A. Colmerauer. Opening the Prolog III universe.BYTE Magazine, pages 177–182, Aug. 1987.Google Scholar
  100. [100]
    J.S. Conery.Parallel Execution of Logic Programs. Kluwer Academic Publishers, Boston, 1987.CrossRefGoogle Scholar
  101. [101]
    M. Conforti, G. Cornuéjols, A. Kapoor, K. Vuskovié, and M. R. Rao. Balanced Matrices. Mathematical Programming: State of the Art. J. R. Birge and K. G. Murty, eds. Braun-Brumfield, United States. Produced in association with the 15th Int’1 Symposium on Mathematical Programming, University of Michigan, 1994.Google Scholar
  102. [102]
    S.A. Cook. The complexity of theorem-proving procedures. InProceedings of the Third ACM Symposium on Theory of Computing, pages 151–158, 1971.Google Scholar
  103. [103]
    S.A. Cook. Find hard instances of the satisfiability problem. Presented at the 1996 DIMACS Workshop on Satisfiability Problem: Theory and Applications. March 11, 1996.Google Scholar
  104. [104]
    P. R. Cooper and M. J. Swain. Parallelism and domain dependence in constraint satisfaction. Technical Report TR 255, Dept. of Computer Science, Univ. of Rochester, Dec. 1988.Google Scholar
  105. [105]
    T.H. Cormen, C.E. Leiserson, and R.L. Rivest.Introduction to Algorithms. MIT Press, Cambridge, 1990.zbMATHGoogle Scholar
  106. [106]
    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.MathSciNetzbMATHCrossRefGoogle Scholar
  107. [107]
    Y. Crama, P. L. Hammer, B. Jaumard, and B. Simeone. Product form parametric representation of the solutions to a quadratic boolean equation.R.A.I.R.O. Recherche opérationnelle/Operations Research 21: 287–306, 1987.MathSciNetzbMATHGoogle Scholar
  108. [108]
    Y. Crama, P. Hansen, and B. Jaumard. The basic algorithm for pseudo-boolean programming revisited.Discrete Applied Mathematics 29: 171–185, 1990.MathSciNetzbMATHCrossRefGoogle Scholar
  109. [109]
    J.M. Crawford and L.D. Auton. Experimental results on the crossover point in satisfiability problem. InProc. of AAAI’93, pages 21–27, Aug. 1993.Google Scholar
  110. [110]
    J. Crawford and L. Auton. Experimental results on the crossover point in satisfiability problems. Presented in the 3rd International Symposium on AI & Mathematics, Jan. 1994.Google Scholar
  111. [111]
    J.M. Crawford. Solving satisfiability problems using a combination of systematic and local search. Submitted to the DIMACS Challenge II Workshop, 1994.Google Scholar
  112. [112]
    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.Google Scholar
  113. [113]
    W. Dai and E.S. Kuh. Hierarchical floorplanning for building block layout. InDigest of Int’l Conf. on Computer-Aided Design, pages 454–457, 1986.Google Scholar
  114. [114]
    M. Dalal, and D. W. Etherington. A hierarchy of tractable satisfiability problems.Information Processing letters 44, pages 173–180, 1992.MathSciNetzbMATHCrossRefGoogle Scholar
  115. [115]
    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.Google Scholar
  116. [116]
    L. S. Davis. Shape matching using relaxation techniques.IEEE Trans. on Pattern Analysis and Machine Intelligence, PAMI-1(1): 60–72, Jan. 1979.Google Scholar
  117. [117]
    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.Google Scholar
  118. [118]
    M. Davis, G. Logemann, and D. Loveland. A machine program for theorem proving.Communications of the ACM, 5: 394–397, 1962.MathSciNetzbMATHCrossRefGoogle Scholar
  119. [119]
    M. Davis and H. Putnam. A computing procedure for quantification theory.J. of ACM, 7: 201–215, 1960.MathSciNetzbMATHCrossRefGoogle Scholar
  120. [120]
    J. de Kleer. An assumption-based TMS.Artificial Intelligence, 28: 127162, 1986.Google Scholar
  121. [121]
    J. de Kleer. Problems with ATMS.Artificial Intelligence, 28: 197–224, 1986.CrossRefGoogle Scholar
  122. [122]
    J. de Kleer. A comparison of ATMS and CSP techniques. InProceedings of 11 th IJCAI, pages 290–296, 1989.Google Scholar
  123. [123]
    J. de Kleer. Exploiting locality in a TMS. InProceedings of AAAI’90, pages 264–271, 1990.Google Scholar
  124. [124]
    R. Dechter. Learning while searching in constraint satisfaction problems. InProceedings of AAAI’86, 1986.Google Scholar
  125. [125]
    R. Dechter. A constraint-network approach to truth maintenance. Technical Report R-870009, Computer Science Dept., UCLA, Los Angeles, 1987.Google Scholar
  126. [126]
    R. Dechter. Enhancement schemes for constraint processing: Back-jumping, learning and cutset decomposition.Artificial Intelligence, 41 (3), 1990.Google Scholar
  127. [127]
    R. Dechter. Directional resolution: The Davis-Putnam procedure revisited. Presented in the 3rd International Symposium on AI & Mathematics, Jan. 1994.Google Scholar
  128. [128]
    R. Dechter and A. Dechter. Belief maintenance in dynamic constraint networks. InProceedings of AAAI’88, 1988.Google Scholar
  129. [129]
    R. Dechter and J. Pearl. Network-based heuristics for constraint-satisfaction problems.Artificial Intelligence, 34: 1–38, 1988.MathSciNetCrossRefGoogle Scholar
  130. [130]
    J.S. Denker, editor.Neural Networks for Computing, volume 151 ofAIP (Snowbird,Utah) Conference Proceedings. American Institute of Physics, New York, 1986.Google Scholar
  131. [131]
    N. Dershowitz, J. Hsiang, N. Josephson, and D. Plaisted. Associative-commutative rewriting. InProceedings of IJCAI, pages 940–944, 1983.Google Scholar
  132. [132]
    D.N. Deutsch. A ‘dogleg’ channel router. InProc. of the 13th ACM/IEEE Design Automation Conference, pages 425–433, Jun. 1976.Google Scholar
  133. [133]
    D.N. Deutsch. Compacted channel routing. InDigest Int’l Conf. on Computer-Aided Design, pages 223–225, Nov. 1985.Google Scholar
  134. [134]
    J. P. A. Deutsch. A short cut for certain combinational problems. InBritish Joint Comput. Conference, 1966.Google Scholar
  135. [135]
    S. Devadas. Optimal layout via Boolean satisfiability. InProceedings of ICCAD’89, pages 294–297, Nov. 1989.Google Scholar
  136. [136]
    S. Devadas, K. Keutzer, and J. White. Estimation of power dissipation in CMOS combinational circuits using Boolean function manipulation.IEEE Transactions on CAD, 11 (3): 373–383, Mar. 1992.Google Scholar
  137. [137]
    S. Devadas, H.T. Ma, A.R. Newton, and A.S. Vincentelli. A synthesis and optimization procedure for fully and easily testable sequential machines.IEEE Trans. on CAD, 8 (10): 1100–1107, Oct. 1989.Google Scholar
  138. [138]
    S.K. Dhall and C.L. Liu. On a real-time scheduling problem.Operations Research, 26 (1): 127–140, Feb. 1978.MathSciNetzbMATHCrossRefGoogle Scholar
  139. [139]
    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
  140. [140]
    M. Dincbas, H. Simonis, and P.V. Hentenryck. Solving a cutting-stock problem in constraint logic programming. InProceedings of the 5th International Conference on Logic Programming, 1988.Google Scholar
  141. [141]
    J. Doenhardt and T. Lengauer. Algorithm aspects of one-dimensional layout.IEEE Trans. on CAD, CAD-6(5): 863–878, 1987.Google Scholar
  142. [142]
    W.E. Donath. Placement and average interconnection lengths of computer logic. IEEE Trans. on Circuits and Systems,CAS-26(4):272–277, Apr. 1979.Google Scholar
  143. [143]
    W.E. Donath. Wire length distribution for placements of computer logic.IBM J. of Research and Development, 25 (3): 152–155, May 1981.CrossRefGoogle Scholar
  144. [144]
    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
  145. [145]
    W. F. Dowling and J. H. Gallier. Linear-time algorithms for testing the satisfiability of propositional Horn formulae.Journal of Logic Programming 1, pages 267–284, 1984.MathSciNetzbMATHCrossRefGoogle Scholar
  146. [146]
    J. Doyle. A truth maintenance system.Artificial Intelligence, 12: 23 1272, 1979.MathSciNetGoogle Scholar
  147. [147]
    B. Du and J. Gu. Sequential circuit test generation by Boolean satisfiability. 1996, to appear.Google Scholar
  148. [148]
    D.Z. Du, J. Gu, and P.M. Pardalos, editors.The Satisfiability (SAT) Problem. DIMACS Volume Series on Discrete Mathematics and Theoretical Computer Science, American Mathematical Society, 1996.Google Scholar
  149. [149]
    O. Dubois. Counting the number of solutions for instances of satisfiability.Theoretical Computer Science, 81: 49–64, 1991.MathSciNetzbMATHCrossRefGoogle Scholar
  150. [150]
    O. Dubois and J. Carlier. Probabilistic approach to the satisfiability problem.Theoretical Computer Science, 81: 65–75, 1991.MathSciNetzbMATHCrossRefGoogle Scholar
  151. [151]
    O. Dubois and Y. Boufkhad. Analysis of the space of solutions for random instances of the satisfiability problem.Proceedings of the fourth International Symposium on Artificial Intelligence and Mathematics, Ft. Lauderdale, Florida, p. 175, 1996.Google Scholar
  152. [152]
    O. Dubois, P. Andre, Y. Boufkhad, and J. Carlier. SAT versus UN-SAT.DIMACS Series Volume: Clique,Graph Coloring,and Satisfiability Second DIMACS Implementation Challenge. Editors: D.S. Johnson and M.A. Trick, 26, American Mathematical Society, 1996.Google Scholar
  153. [153]
    C. Eastman. Preliminary report on a system for general space planning.Comm. of ACM, 15 (2): 76–87, Feb. 1972.MathSciNetCrossRefGoogle Scholar
  154. [154]
    T. Eiter, P. Kilpelainen, and H. Mannila. Some remarks on renaming and satisfiability hierarchies. Summary Presented in the 3rd International Symposium on AI & Mathematics, Jan. 1994.Google Scholar
  155. [155]
    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
  156. [156]
    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.Google Scholar
  157. [157]
    B.-J. Falkowski and L. Schmitz. A note on the queens’ problem.Information Processing Letters, Vol. 23: 39–46, July 1986.MathSciNetCrossRefGoogle Scholar
  158. [158]
    M.Y. Fang and W.T. Chen. Vectorization of a generalized procedure for theorem proving in propositional logic on vector computers.IEEE Trans. on Knowledge and Data Engineering, 4 (5): 475–486, Oct. 1992.CrossRefGoogle Scholar
  159. [159]
    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.Google Scholar
  160. [160]
    O. D. Faugeras, editor.Fundamentals in Computer Vision. Cambridge University Press, London, 1983.Google Scholar
  161. [161]
    J. A. Feldman and Y. Yakimovsky. Decision theory and artificial intelligence: I. a semantics-based region analyzer.Artificial Intelligence, 5: 349–371, 1974.zbMATHCrossRefGoogle Scholar
  162. [162]
    J. D. Findler.Associative Networks: Representation and Use of Knowledge by Computers. Academic Press, New York, 1979.zbMATHGoogle Scholar
  163. [163]
    C.A. Floudas and P.M. Pardalos.A Collection of Test Problems for Constrained Global Optimization Algorithms. Springer Verlag, New York, 1990.zbMATHCrossRefGoogle Scholar
  164. [164]
    C.A. Floudas and P.M. Pardalos, editors.Recent Advances in Global Optimization. Princeton University Press, New York, 1992.Google Scholar
  165. [165]
    M.S. Fox.Constraint-Directed Search: A Case Study of Job-Shop Scheduling. Pitman, London, 1987.zbMATHGoogle Scholar
  166. [166]
    J. Franco. On the probabilistic performance of algorithms for the satisfiability problem.Information Processing Letters, 23: 103–106, 1986.CrossRefGoogle Scholar
  167. [167]
    J. Franco. Elimination of infrequent variables improves average case performance of satisfiability algorithms.SIAM J. on Computing, 20: 1119–1127, 1991.MathSciNetzbMATHCrossRefGoogle Scholar
  168. [168]
    J. Franco and Y.C. Ho. Probabilistic performance of heuristic for the satisfiability problem. Discrete Applied Mathematics,22:35–51, 1988/89.Google Scholar
  169. [169]
    J. Franco and M. Paull. Probabilistic analysis of the Davis-Putnam procedure for solving the satisfiability problem.Discrete Applied Mathematics, 5: 77–87, 1983.MathSciNetzbMATHCrossRefGoogle Scholar
  170. [170]
    J. Franco. 1993. On the occurrence of null clauses in random instances of satisfiability.Discrete Applied Mathematics 41, pp. 203–209.MathSciNetzbMATHCrossRefGoogle Scholar
  171. [171]
    J. Franco and R. Swaminathan. Toward a good algorithm for determining unsatisfiability of propositional formulas. 1996.Google Scholar
  172. [172]
    J. Franco, and R. Swaminathan. 1996. Average case results for Satisfiability algorithms under the random-clause-width model. To appear in Annals of Mathematics and Artificial Intelligence.Google Scholar
  173. [173]
    J. Franco, J. Goldsmith, J. Schlipf, E. Speckenmeyer, R. P. Swaminathan. 1996. An algorithm for the class of pure implicational formulas. Proceedings of theWorkshop on Satisfiability, Siena, Italy.Google Scholar
  174. [174]
    J. Franco. Relative Size of Certain Polynomial Time Solvable Subclasses of Satisfiability. DIMACS Volume, Series on Discrete Mathematics and Theoretical Computer Science, American Mathematical Society, 1997.Google Scholar
  175. [175]
    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.Google Scholar
  176. [176]
    F. Frayman and S. Mittal.Cossack: A Constraints-based Expert System for Configuration Tasks. Computational Mechanics Publications, Nadel, 1987.Google Scholar
  177. [177]
    J.W. Freeman. Improvements to the davis-putnam procedure for satisfiability. Jan. 1994.Google Scholar
  178. [178]
    E. C. Freuder. A sufficient condition for backtrack-free search.J. ACM, 29 (1): 24–32, Jan. 1982.MathSciNetzbMATHCrossRefGoogle Scholar
  179. [179]
    E. C. Freuder. A sufficient condition for backtrack-bounded search.J. ACM, 32 (4): 755–761, Oct. 1985.MathSciNetzbMATHCrossRefGoogle Scholar
  180. [180]
    E.C. Freuder and M.J. Quinn. Taking advantage of stable sets of variables in constraint satisfaction problems. InProceedings of 9th IJCAI, pages 1076–1078, 1985.Google Scholar
  181. [181]
    A. M. Frieze, and S. Suen. 1993. Analysis of simple heuristics for random instances of 3-SAT.Google Scholar
  182. [182]
    X. Fu. The complexity of resolution proofs.Google Scholar
  183. [183]
    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
  184. [184]
    Z. Galil. On the complexity of regular resolution and the Davis-Putnam procedure.Theoretical Computer Science, pages 23–46, 1977.Google Scholar
  185. [185]
    G. Gallo, and M. G. Scutella. Polynomially solvable satisfiability problems.Information Processing Letters 29, pages 221–227, 1988.MathSciNetzbMATHCrossRefGoogle Scholar
  186. [186]
    G. Gallo and G. Urbani. Algorithms for testing the satisfiability of propositional formulae.J. of Logic Programming, 7: 45–61, 1989.MathSciNetzbMATHCrossRefGoogle Scholar
  187. [187]
    G. Gallo and D. Pretolani. Hierarchies of polynomially solvable SAT problems. Presented in the 3rd International Symposium on AI & Mathematics, Jan. 1994.Google Scholar
  188. [188]
    H. Garcia-Molina. Using semantic knowledge for transaction processing in a distributed database. ACM Trans. on Database Systems, 8 (2), Jun. 1983.Google Scholar
  189. [189]
    M.R. Garey and D.S. Johnson. Complexity results for multiprocessor scheduling under resource constraints.SIAM J. Comput., 4: 397–411, 1975.MathSciNetzbMATHCrossRefGoogle Scholar
  190. [190]
    M.R. Garey and D.S. Johnson. Two-processors scheduling with start-times and deadlines.SIAM J. on Computing, 6: 416–426, 1977.MathSciNetzbMATHCrossRefGoogle Scholar
  191. [191]
    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.zbMATHGoogle Scholar
  192. [192]
    J.Gaschnig A constraint satisfaction method for inference making. In Proceedings of 12th Annual Allerton Conf. Circuit System Theory,1974.Google Scholar
  193. [193]
    J. Gaschnig. A general backtrack algorithm that eliminates most redundant tests. InProceedings of 9th IJCAI, page 457, 1977.Google Scholar
  194. [194]
    J. Gaschnig.Performance Measurements and Analysis of Certain Search Algorithms. PhD thesis, Carnegie-Mellon University, Dept. of Computer Science, May 1979.Google Scholar
  195. [195]
    A.V. Gelder. A satisfiability tester for non-clausal propositional calculus.Information and Computation, 79 (1): 1–21, Oct. 1988.MathSciNetzbMATHCrossRefGoogle Scholar
  196. [196]
    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.Google Scholar
  197. [197]
    S. Geman and C.-R. Hwang.Diffusions of Global optimization. Brown University, 1984.Google Scholar
  198. [198]
    M.R. Genesereth and N. J. Nilsson.Logical Foundations of Artificial Intelligence. Morgan Kaufmann Publishers, Los Altos, California, 1987.Google Scholar
  199. [199]
    I.P. Gent and T. Walsh. The hardest random SAT problems. InProceedings of KI’94, 1994.Google Scholar
  200. [200]
    P.C. Gilmore. A proof method for quantification theory.IBM J. Res. Develop., 4: 28–35, 1960.MathSciNetzbMATHCrossRefGoogle Scholar
  201. [201]
    A. Ginzberg.Algebraic Theory of Automata. Academic Press, New York, 1968.Google Scholar
  202. [202]
    F. Glover. Tabu search Part I.ORSA Journal on Computing, 1 (3): 190–206, Summer 1989.zbMATHGoogle Scholar
  203. [203]
    A. Goerdt. 1992. A threshold for unsatisfiability.Proceedings of 17th annual Symposium on Mathematical Foundations of Computer Science, Prague, Czechoslovakia.Google Scholar
  204. [204]
    A. Goldberg. Average case complexity of the satisfiability problem. InProc. Fourth Workshop on Automated Deduction, pages 1–6, 1979.Google Scholar
  205. [205]
    A. Goldberg. On the complexity of the satisfiability problem. Technical Report Courant Computer Science No. 16, New York University, 1979.Google Scholar
  206. [206]
    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 (Some printer errors in this paper were corrected inInformation Processing Letters, 16: 213, 1983 ).MathSciNetzbMATHCrossRefGoogle Scholar
  207. [207]
    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.Google Scholar
  208. [208]
    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.Google Scholar
  209. [209]
    J. Gu, P.W. Purdom, J. Franco, and B.W. Wah. Algorithms for satisfiability (SAT) problem: A survey.DIMACS Volume Series on Discrete Mathematics and Theoretical Computer Science,Vol. 35: The Satisfiability (SAT) Problem, pages 19–151, American Mathematical Society, 1997.Google Scholar
  210. [210]
    J. Gu, P.W. Purdom, J. Franco, and B. Wah. Algorithms for the Satisfiability Problem. Cambridge University Press, 1999.Google Scholar
  211. [211]
    J. Gu. Parallel algorithms and architectures for very fast search. Ph.D thesis. Technical Report UUCS-TR-88–005, July 1988.Google Scholar
  212. [212]
    J. Gu. How to solve Very Large-Scale Satisfiability problems. Technical Report UUCS-TR-88–032, 1988, and Technical Report UCECETR-90–002, 1990.Google Scholar
  213. [213]
    J. Gu. An 0-relaxation for global optimization. Technical Report UCECE-TR-91–003, Apr. 1991.Google Scholar
  214. [214]
    J. Gu. Efficient local search for very large-scale satisfiability problem. SIGART Bulletin 3(1):8–12, Jan. 1992, ACM Press.Google Scholar
  215. [215]
    J. Gu.On Optimizing a Search Problem. In N. G. Bourbakis, editor,Artificial Intelligence Methods and Applications, Vol. 1, chapter 2, pages 63–105. World Scientific Publishers, New Jersey, Jan. 1992.Google Scholar
  216. [216]
    J. Gu. TheUniSAT problem models (appendix).IEEE Trans. on Pattern Analysis and Machine Intelligence, 14 (8): 865, Aug. 1992.Google Scholar
  217. [217]
    J. Gu. Local search for satisfiability (SAT) problem.IEEE Trans. on Systems,Man,and Cybernetics, 23(4):1108–1129, Jul. 1993, and 24 (4): 709, Apr. 1994.Google Scholar
  218. [218]
    J. Gu. Global optimization for satisfiability (SAT) problem.IEEE Trans. on Knowledge and Data Engineering, 6(3):361–381, Jun. 1994, and 7 (1): 192, Feb. 1995.Google Scholar
  219. [219]
    J. Gu. Optimization Algorithms for the Satisfiability (SAT) Problem. In Advances in Optimization and Approximation. pages 72–154. Kluwer Academic Publishers, 1994.Google Scholar
  220. [220]
    J. Gu. Parallel algorithms for satisfiability (SAT) problem.DIMACS Volume Series on Discrete Mathematics and Theoretical Computer Science, Vol. 22, pages 105–161, American Mathematical Society, 1995.Google Scholar
  221. [221]
    J. Gu and R. Puri. Asynchronous circuit synthesis by Boolean satisfiability.IEEE Transactions on CAD of Integrated Circuits and Systems, 14 (8): 961–973, Aug. 1995.Google Scholar
  222. [222]
    J. Gu. Satisfiability Problems in VLSI Engineering. Presented at Annual Conference of the Institute for Operations Research and Management Science,Oct. 1995, and DIMACS Workshop on Satisfiability Problem, Mar. 1996. To appear in Discrete Applied Mathematics. Google Scholar
  223. [223]
    J. Gu, Q.P. Gu, and D.-Z. Du. Convergence properties of optimization algorithms for the satisfiability (SAT) problem.IEEE Trans. on Computers, 45 (2): 209–219, Feb. 1996.zbMATHGoogle Scholar
  224. [224]
    J. Gu and Lizhoudu. An efficient implementation of the SAT1.5 algorithm. Technical Report, USTC, Sept. 1995.Google Scholar
  225. [225]
    J. Gu. The Multi-SAT algorithm. Siena SAT Workshop and Workshop on Semidefinite and Interior-Point Methods, May 1996. To appear in Discrete Applied Mathematics.Google Scholar
  226. [226]
    J. Gu and Q.P. Gu. Average time complexities of several local search algorithms for the satisfiability (SAT) problem. Technical Report UCECE-TR-91–004, 1991. In Lecture Notes in Computer Science, Vol. 834, pp. 146–154, 1994 and to appear in IEEE Trans. on Knowledge and Data Engineering.Google Scholar
  227. [227]
    J. Gu. Optimization by multispace search. Technical Report UCECETR-90–001, Jan. 1990.Google Scholar
  228. [228]
    J. Gu.Multispace Search: A New Optimization Approach (Summary). InLecture Notes in Computer Science,Vol.834, pages 252–260. 1994.Google Scholar
  229. [229]
    J. Gu. Multispace search for satisfiability and NP-hard problems.DI-MACS Volume Series on Discrete Mathematics and Theoretical Computer Science,Vol.35, pages 407–517, American Mathematical Society, 1997.Google Scholar
  230. [230]
    J. Gu. Randomized and Deterministic Local Search for SAT and Scheduling Problems.DIMACS Volume Series on Discrete Mathematics and Theoretical Computer Science,Vol.43, pages 61–108, American Mathematical Society, 1998.Google Scholar
  231. [231]
    Gu and X. Huang. Local search with search space smoothing: A case study of the traveling salesman problem (TSP). Technical Report UCECE-TR-91–006, Aug. 1991. InIEEE Trans. on Systems,Man,and Cybernetics, 24(5):728–735, May 1994.Google Scholar
  232. [232]
    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.Google Scholar
  233. [233]
    J. Gu and W. Wang. A novel discrete relaxation architecture.IEEE Trans. on Pattern Analysis and Machine Intelligence, 14 (8): 857–865, Aug. 1992.CrossRefGoogle Scholar
  234. [234]
    J. Gu. Constraint-Based Search.Cambridge University Press, New York, to appear.Google Scholar
  235. [235]
    J. Gu. Optimization by multispace search.Kluwer Academic Publishers, to appear.Google Scholar
  236. [236]
    Y. Gurevich. Average case completeness.J. of Computer and Systems Sciences, 42 (3): 346–398, 1991.MathSciNetzbMATHCrossRefGoogle Scholar
  237. [237]
    A. Guzman.Computer Recognition of Three-Dimensional Objects in a Visual Scene. PhD thesis, MIT, 1968.Google Scholar
  238. [238]
    [238]S. Ha and E.A. Lee. Compile-time scheduling and assignment of data-flow program graphs with data-dependent iteration.IEEE Trans. onGoogle Scholar
  239. [239]
    A. Haken. The intractability of resolution.Theoretical Computer Science, 39: 297–308, 1985.MathSciNetzbMATHCrossRefGoogle Scholar
  240. [240]
    G.T. Hamachi and J.K. Ousterhout. A switchbox router with obstacle avoidance. In Proc. of the 21st ACM/IEEE Design AutomationGoogle Scholar
  241. [242]
    P. L. Hammer and S. Rudeanu. Boolean Methods in Operations Research and Related Areas. Springer-Verlag, New York, 1968.zbMATHCrossRefGoogle Scholar
  242. [243]
    P. Hansen and B. Jaumard. Uniquely solvable quadratic Boolean equations.Discrete Applied Mathematics 12: 147–154, 1985.MathSciNetzbMATHCrossRefGoogle Scholar
  243. [244]
    P. Hansen, B. Jaumard, and V. Mathon. Constrained Nonlinear 0–1 Programming.ORSA Journal on Computing 5: 97–119, 1993.MathSciNetzbMATHCrossRefGoogle Scholar
  244. [245]
    P. Hansen, B. Jaumard, and G. Plateau. An extension of nested satisfiability. Les Cahiers du GERAD, G-93–27, 1993.Google Scholar
  245. [246]
    P. Hansen and B. Jaumard. Algorithms for the maximum satisfiability problem.Computing, 44: 279–303, 1990.MathSciNetzbMATHCrossRefGoogle Scholar
  246. [247]
    E. R. Hansen.Global optimization using interval analysis. M. Dekker, New York, 1992.zbMATHGoogle Scholar
  247. [248]
    R. M. Haralick and G. Elliot. Increasing tree search efficiency for constraint satisfaction problems.Artificial Intelligence, 14: 263–313, 1980.CrossRefGoogle Scholar
  248. [249]
    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.Google Scholar
  249. [250]
    F. Harary.Graph Theory. Addison-Wesley, Reading, 1969.Google Scholar
  250. [251]
    W. S. Havens. A theory of schema labeling.Computational Intelligence,1(3–4 ): 127–139, 1985.Google Scholar
  251. [252]
    T. Hedges, W. Dawson, and Y.E. Cho. Bitmap graph build algorithm for compaction. InDigest Int’l Conf. on Computer-Aided Design, pages 340–342, Sep. 1985.Google Scholar
  252. [253]
    T. C. Henderson and L. S. Davis. Hierarchical models and analysis of shape.Pattern Recognition, 14 (1–6): 197–204, 1981.MathSciNetCrossRefGoogle Scholar
  253. [254]
    T. C. Henderson and A. Samal. Multi-constraint shape analysis.Image and Vision Computing, 4 (2): 84–96, May 1986.CrossRefGoogle Scholar
  254. [255]
    P. V. Hentenryck.Constraint Satisfaction in Logic Programming. The MIT Press, Cambridge, 1989.Google Scholar
  255. [256]
    P. Heusch. The Complexity of the Falsifiability Problem for Pure Implicational Formulas.Proc. 20th Int’l Symposium on Mathematical Foundations of Computer Science (MFCS’95), J. Wiedermann, P. Hajek (Eds.), Prague, Czech Republic.Lecture Notes in Computer Science (LNCS 969), Springer-Verlag, Berlin, pages 221–226, 1995.Google Scholar
  256. [257]
    G.E. Hinton and J.A. Anderson, editors.Parallel Models of Associative Memory. Lawrence Erlbaum Associates, Publishers, Hillsdale, New Jersey, 1981.Google Scholar
  257. [258]
    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 Microstructure of Cognition. Vol. 1: Foundations, volume 1, chapter 7, pages 282–317. The MIT Press, Cambridge, 1986.Google Scholar
  258. [259]
    E. J. Hoffman, J. C. Loessi, and R. C. Moore. Constructions for the solution of the m queens problem.Mathematics Magazine, pages 6672, 1969.Google Scholar
  259. [260]
    J. H. Holland.Adaption in Natural and Adaptive Systems. University of Michigan Press, Ann Arbor, 1975.Google Scholar
  260. [261]
    S.J. Hong and S. Muroga. Absolute minimization of completely specified switching functions.IEEE Trans. on Computers, 40 (1): 53–65, Jan. 1991.MathSciNetCrossRefGoogle Scholar
  261. [262]
    P. Hood and Grover. Designing real time systems in Ada. Technical Report 1123–1, SofTech, Inc., Waltham, Jan. 1986.Google Scholar
  262. [263]
    J. Hooker and V. Vinay. An empirical study of branching rules for satisfiability. Presented in the 3rd International Symposium on AI & Mathematics, Jan. 1994.Google Scholar
  263. [264]
    J.N. Hooker. Generalized resolution and cutting planes.Annals of Operations Research, 12: 217–239, 1988.MathSciNetCrossRefGoogle Scholar
  264. [265]
    J.N. Hooker. A quantitative approach to logical inference.Decision Support Systems, 4: 45–69, 1988.CrossRefGoogle Scholar
  265. [266]
    J.N. Hooker. Resolution vs. cutting plane solution of inference problems: Some computational experience.Operations Research Letter, 7 (1): 1–7, 1988.MathSciNetzbMATHCrossRefGoogle Scholar
  266. [267]
    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
  267. [268]
    A.L. Hopkins and et. al. FTMP–a highly reliable fault-tolerant multiprocessor for aircraft. InProceedings of the IEEE, pages 1221–1239, Oct. 1978.Google Scholar
  268. [269]
    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
  269. [270]
    B.K.P. Horn. Understanding image intensity.Artificial Intelligence, 8: 301–231, 1977.CrossRefGoogle Scholar
  270. [271]
    B.K.P. Horn and M. J. Brooks, editors.Shape from Shading. The MIT Press, Cambridge, 1989.Google Scholar
  271. [272]
    B.K.P. Horn and M.J. Brooks. The variational approach to shape from shading. Computer Vision, Graphics E4 Image Processing,33(2):174208, 1986.Google Scholar
  272. [273]
    E. Horowitz and S. Sahni.Fundamentals of Computer Algorithms. Computer Science Press, Rockville, 1978.zbMATHGoogle Scholar
  273. [274]
    R. Horst and H. Thy.Global Optimization: Deterministic Approaches. Springer Verlag, Berlin, 1990.zbMATHGoogle Scholar
  274. [275]
    J. Hsiang. Refutational theorem proving using term-rewriting systems.Artificial Intelligence, pages 255–300, 1985.Google Scholar
  275. [276]
    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.MathSciNetzbMATHCrossRefGoogle Scholar
  276. [277]
    X. Huang, J. Gu, and Y. W. A constrained approach to multi font character recognition.IEEE Transactions on Pattern Analysis And Machine Intelligence, 15 (8): 838–843, Aug. 1993.CrossRefGoogle Scholar
  277. [279]
    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
  278. [280]
    K. Ikeuchi. Model-based interpretation of range imagery. In Proc. of Image Understanding Workshop,pages 321–339. DARPA, Feb. 1987.Google Scholar
  279. [281]
    K. Ikeuchi and B.K.P. Horn. Numerical shape from shading and occluding boundaries.Artificial Intelligence, 17 (1–3): 141–184, 1981.CrossRefGoogle Scholar
  280. [282]
    R. Impagliazzo, L. Levin, and M. Luby. Pseudo-random number generation from one way function. InProceedings of the Third ACM Symposium on Theory of Computing, pages 12–14, 1989.Google Scholar
  281. [283]
    B.Indurkhya, H. S. Stone, and L. Xi-Cheng. Optimal partitioning of randomly generated distributed programs. IEEE Trans. on Software EngineeringSE-12:483–495, Mar 1986.Google Scholar
  282. [284]
    L. Ingber.Adaptive Simulated Annealing (ASA). Lester Ingber Research, 1995.Google Scholar
  283. [285]
    T.Ishida. Parallel rule firing in production systems. IEEE Trans. on Knowledge and Data Engineering,3(1):11–17, Mar. 1991.Google Scholar
  284. [286]
    A. Itai and J. Makowsky. On the complexity of Herbrand’s theorem. Working paper243, Department of Computer Science, Israel Institute of Technology, 1982.Google Scholar
  285. [287]
    N. Itazaki and K. Kinoshita. Test pattern generation for circuits with tri-state modules by z-algorithm. IEEE Trans. on CAD, 8(12):13271334, Dec. 1989.Google Scholar
  286. [288]
    K.Iwama. CNF satisfiability test by counting and polynomial average time. SIAM J. on Computing, pages 385–391, 1989.Google Scholar
  287. [289]
    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
  288. [290]
    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.Google Scholar
  289. [291]
    R.E. Jeroslow and J. Wang. Solving propositional satisfiability problems.Annals of Mathematics and AI, 1: 167–187, 1990.zbMATHGoogle Scholar
  290. [292]
    R.G. Jeroslow. Computation-oriented reductions of predicate to propositional logic.Decision Support Systems, 4: 183–197, 1988.CrossRefGoogle Scholar
  291. [293]
    D.S. Johnson. Approximation Algorithms for Combinatorial Problems.J. of Computer andSystems Sciences, 9: 256–278, 1974.zbMATHCrossRefGoogle Scholar
  292. [294]
    D.S. Johnson. More approaches to the traveling salesman guide.Nature, 330: 525, 1987.CrossRefGoogle Scholar
  293. [295]
    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
  294. [296]
    D.S. Johnson. Private Communications, 1993–1996.Google Scholar
  295. [297]
    D.S. Johnson and M.A. Trick, editors.Clique,Graph Coloring,and Satisfiability: Second DIMA CS Implementation Challenge. DIMACS Series Vol. 26. American Mathematical Society, 1996.Google Scholar
  296. [298]
    J.L. Johnson. A neural network approach to the 3-satisfiability problem.J. of Parallel and Distributed Computing, 6: 435–449, 1989.CrossRefGoogle Scholar
  297. [299]
    M.D. Johnston. Scheduling with neural networks — the case of the Hubble Space Telescope. InNASA Memo, 1989.Google Scholar
  298. [300]
    R. R. Johnson. Critical issues in computer architecture design. Private Communication, 1987–1994.Google Scholar
  299. [301]
    R.W. Johnson and A.M. McLoughlin. Computer-Aided Discovery of a Fast Matrix-Multiplication Algorithm.NRL Memorandum Report 3994 May 1979.Google Scholar
  300. [302]
    W. Lewis Johnson. Letter from the editor.SIGART Bulletin, 2(2):1, April 1991, ACM Press.Google Scholar
  301. [303]
    W. Lewis Johnson. Letter from the editor.SIGART Bulletin, 2(5):1, Oct. 1991, ACM Press.Google Scholar
  302. [304]
    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.Google Scholar
  303. [305]
    P.C. Jackson Jr. Heuristic search algorithms for the satisfiability problem. Submitted to the third IEEE TAI Conference, Jul. 1991.Google Scholar
  304. [306]
    A. E. W. Jones and G. W. Forbes. An adaptive simulated annealing algorithm for global optimization over continuous variables.Journal of Optimization Theory and Applications, 6: 1–37, 1995.MathSciNetzbMATHGoogle Scholar
  305. [307]
    Y.C. Ju, B. Rao, and R.A. Saleh. Consistency checking and optimization of macro-models.IEEE Trans. on CAD, 10 (8): 957–967, Aug. 1991.Google Scholar
  306. [308]
    A.P. Kamath, N.K. Karmarkar, K.G. Ramakrishnan, and M.G.C. Re-sende. Computational experience with an interior point algorithm on the satisfiability problem.Annals of Operations Research, 25: 43–58, 1990.MathSciNetzbMATHCrossRefGoogle Scholar
  307. [309]
    A.P. Kamath, N.K. Karmarkar, K.G. Ramakrishnan, and M.G.C. Re-sende. A continuous approach to inductive inference.Mathematical Programming, 57: 215–238, 1992.MathSciNetzbMATHCrossRefGoogle Scholar
  308. [310]
    A.P. Kamath, N.K. Karmarkar, K.G. Ramakrishnan, and M.G.C. Re-sende. Computational experience with an interior point algorithm on the satisfiability problem.Mathematical Sciences Research Center,AT &T Bell Laboratories, Oct. 1989.Google Scholar
  309. [311]
    A. Kamath, R. Motwani, K. Palem, and P. Spirakis. Tail Bounds for occupancy and the satisfiability threshold conjecture.Random Structures and Algorithms 7, pp. 59–80, 1995.MathSciNetzbMATHCrossRefGoogle Scholar
  310. [312]
    N. Karmarkar. A new polynomial-time algorithm for linear programming.Combinatorica, (4): 373–395, 1984.Google Scholar
  311. [313]
    G. Kedem and H. Watanabe. Graph optimization techniques for IC layout and compaction.IEEE Trans. on CAD, CAD-3: 12–20, 1984.Google Scholar
  312. [314]
    J. Kella. State Minimization of Incompletely Specified Sequential Machines.IEEE Trans. on Computers, C-19: 342–348, April 1970.Google Scholar
  313. [315]
    S. Kirkpatrick, C.D. Gelat, and M.P. Vecchi. Optimization by simulated annealing.Science, 220: 671–680, 1983.MathSciNetzbMATHCrossRefGoogle Scholar
  314. [316]
    S. Kirkpatrick, G. Gyorgyi, N. Tishby, and L. Troyansky. The statistical mechanics of k-satisfaction. InProceedings of Neural Information Processing Systems, Nov. 1993.Google Scholar
  315. [317]
    L.M. Kirousis and C.H. Papadimitriou. The complexity of recognizing polyhedral scenes.J. of Computer and System Sciences, 37: 14–38, 1988.MathSciNetzbMATHCrossRefGoogle Scholar
  316. [318]
    L. M. Kirousis, E. Kranakis, and D. Krizanc. A better upper bound for the unsatisfiability threshold. InDIMACS series in Discrete Mathematics and Theoretical Computer Science, 60, 1996.Google Scholar
  317. [319]
    J. Kittler and J. Illingworth. Relaxation labeling algorithms A review.Image and Vision Computing, pages 206–216, 1985.Google Scholar
  318. [320]
    D. E. Knuth. Estimating the efficiency of backtracking programs.Mathematics of Computation, 29 (129): 121–136, Jan. 1975.MathSciNetzbMATHCrossRefGoogle Scholar
  319. [321]
    D. Knuth. Nested satisfiability.Acta Informatica 28: 1–6, 1990.MathSciNetzbMATHCrossRefGoogle Scholar
  320. [322]
    K.L. Kodandapani and E.J. McGrath. A wirelist compare program for verifying VLSI layouts.IEEE Design and Test of Computers, 3 (3): 4651, 1986.Google Scholar
  321. [323]
    R. Kowalski. A proof procedure using connection graphs.J. ACM, 22 (4): 572–595, Oct. 1975.zbMATHCrossRefGoogle Scholar
  322. [324]
    M.R. Kramer and J. van Leeuwen.The Complexity of Wire Routing and Finding Minimum Area Layouts for Arbitrary VLSI Circuits, volume2, chapter VLSI Theory, pages129–146. Jai Press Inc., Greenwich, CT, 1984.Google Scholar
  323. [325]
    C.M. Krishna, K.G. Shin, and I.S. Bhandari. Processor tradeoffs in distributed real-time systems. IEEE Trans. on Computers,C-36(9):10301040, Sept. 1987.Google Scholar
  324. [326]
    D. C-L. Ku. DRA1 chip implementation report. Project Report, Dept. of Computer Science, Univ. of Utah, Mar. 1986.Google Scholar
  325. [327]
    Oliver Kullmann A systematic approach to 3-SAT-decision, yielding 3SAT-decision in less than 1.5045n steps. Theoretical Computer Science, to appear.Google Scholar
  326. [328]
    V. Kumar. Algorithms for constraint satisfaction problems: A survey. Technical Report TR-91–28, Dept. of Computer Science, Univ. of Minnesota, 1991.Google Scholar
  327. [329]
    V. Kumar. Algorithms for constraint satisfaction problems: A survey.The AI Magazine, 13 (1): 32–44, 1992.Google Scholar
  328. [330]
    V. Kumar and Y.-J Lin. A data-dependency based intelligent backtracking scheme for Prolog.J. of Logic Programming, 5 (2), June 1988.Google Scholar
  329. [331]
    T. G. Kurtz. Solutions of ordinary differential equations as limits of pure jump Markov processes.Journal of Applied Probability, 7: 49–58, 1970.MathSciNetzbMATHCrossRefGoogle Scholar
  330. [332]
    J. D. Laderman. A noncommutative algorithm for multiplying 3 x 3 matrices using 23 multiplications. Bull. Amer. Math. Soc.,82(1):126128, 1976.Google Scholar
  331. [333]
    E.D. Lagnese and D.E. Thomas. Architectural partitioning for system level synthesis of integrated circuits. IEEE Trans. on CAD,10(7):847–860, July 1991.Google Scholar
  332. [334]
    G. Lakhani and R. Varadarajan. A wire-length minimization algorithm for circuit layout compaction. InProc. of ISCAS’87, pages 276–279, May 1987.Google Scholar
  333. [335]
    B.S. Landman and R.L. Russo. On a pin versus block relationship for partitions of logic graphs.IEEE Trans. on Computers, C-20:14691479, Dec. 1971.Google Scholar
  334. [336]
    T. Larrabee. Test pattern generation using Boolean satisfiability.IEEE Trans. on Computer-Aided Design, 11 (1): 4–15, Jan. 1992.CrossRefGoogle Scholar
  335. [337]
    C. Lassez. Constraint logic programming.BYTE Magazine, pages 171–176, Aug. 1987.Google Scholar
  336. [338]
    L. Lavagno, K. Keutzer, and A. Sangiovanni-Vincentelii. Algorithms for Synthesis of Hazard-free Asynchronous Circuits. InProc. of 28th DAC, pages 302–308, 1991.Google Scholar
  337. [339]
    L. Lavagno, C. Moon, R. Brayton, and A. Sangiovanni-Vincentelli. Solving the State Assignment Problem for Signal Transition Graphs. InProc. of 29th DAC, pages 568–572, 1992.Google Scholar
  338. [340]
    E.L. Lawler, J.K. Lenstra, A.H.G. Rinnooy Kan, and D.B. Shmoys, editors.The Traveling Salesman Problem. John Wiley & Sons, New York, 1985.zbMATHGoogle Scholar
  339. [341]
    E.L. Lawler and D.E. Wood. Brance-and-bound methods: a survey.Operations Research, 14 (4): 699–719, Jul.—Aug. 1966.MathSciNetzbMATHGoogle Scholar
  340. [342]
    C. Y. Lee. Representation of Switching Circuits by Binary Decision Programs.Bell Systems Technical Journal, 38: 985–999, July 1959.Google Scholar
  341. [343]
    C. Lee. An algorithm for path connections and its applications.IEEE Trans. on Electronic Computers, VEC-10: 346–365, Sept. 1961.Google Scholar
  342. [344]
    E.A. Lee. Consistency in dataflow graphs.IEEE Trans. on Parallel and Distributed Systems, 2 (2): 223–235, Apr. 1991.CrossRefGoogle Scholar
  343. [345]
    R.C.T. Lee. Private Communications, 1992–1993.Google Scholar
  344. [346]
    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
  345. [347]
    H. R. Lewis. Renaming a set of clauses as a Horn set.Journal of the Association for Computing Machinery 25, pages 134–135, 1978.MathSciNetzbMATHCrossRefGoogle Scholar
  346. [348]
    G. J. Li and B. W. Wah. How to Cope with Anomalies in Parallel Approximate Branch-and-Bound Algorithms. inProc. National Conf. on Artificial Intelligence, AAAI, pages 212–215, Aug. 1984.Google Scholar
  347. [349]
    G.-J. Li.Parallel Processing of Combinatorial Search Problems. PhD thesis, School of Electrical Engineering, Purdue University, West Lafayette, Dec. 1985.Google Scholar
  348. [350]
    G. J. Li and B. W. Wah. How good are parallel and ordered depth-first searches? In Proc. Int’l Conf. on Parallel Processing,pages 992–999, University Park, PA, August 1986. Pennsylvania State Univ. Press.Google Scholar
  349. [351]
    G. J. Li and B. W. Wah. Computational efficiency of combinatorial OR-tree searches.Trans. on Software Engineering, 16 (1): 13–31, January 1990.MathSciNetGoogle Scholar
  350. [352]
    G.-J. Li and B. W. Wah. Parallel iterative refining A*: An efficient search scheme for solving combinatorial optimization problems. In Proc. Int’l Conf. on Parallel Processing,pages 608–615, University Park, PA, August 1991. Pennsylvania State Univ. Press.Google Scholar
  351. [353]
    J. Li and M. Chen. Compiling communication-efficient programs for massively parallel machinesIEEE Trans. on Parallel and Distributed Systems, 2 (3): 361–376, July 1991.CrossRefGoogle Scholar
  352. [354]
    Y.-Z. Liao and C.K. Wong. An algorithm to compact a VLSI symbolic layout with mixed constraints.IEEE Trans. on CAD, CAD-2(2): 6269, 1983.Google Scholar
  353. [355]
    D. Lichtenstein. Planar formulae and their uses.SIAM Journal on Computing 11:329–343 , 1982.Google Scholar
  354. [356]
    K.J. Lieberherr and E. Specker. Complexity of partial satisfaction.J. of ACM , 28:411–421 , 1981.Google Scholar
  355. [357]
    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.Google Scholar
  356. [358]
    K. J. Lin and C. S. Lin. Automatic Synthesis of Asynchronous Circuits. In Proc. of 28th DAC , pages 296–301, 1991.Google Scholar
  357. [359]
    S. Lin. Computer solutions of the traveling salesman problem.Bell Sys. Tech. Journal, 44 (10): 2245–2269, Dec. 1965.zbMATHGoogle Scholar
  358. [360]
    W. M. Lin and V. K. P. Kumar. Parallel architectures for discrete relaxation algorithm. AAAI Workshop on Parallel Algorithms for AI, Detroit, 20 Aug. 1989.Google Scholar
  359. [361]
    Y.-J. Lin.A Parallel Implementation of Logic Programs. PhD thesis, The Univ. of Texas at Austin, Dept. of Computer Science, May 1988.Google Scholar
  360. [362]
    R. P. Lippmann. An introduction to computing with neural net.IEEE ASSP Magazine ,4(2):4–22, April 1987.Google Scholar
  361. [363]
    Richard J. Lipton DNA Solution of Hard Computational Problems Science, 268:542–544.Google Scholar
  362. [364]
    C. D. Locke.Best-Effort Decision Making for Real-Time Scheduling. PhD thesis, Carnegie-Mellon University, May 1985.Google Scholar
  363. [365]
    D.W. Loveland.Automated Theorem Proving: A Logical Basis. North-Holland,1978.Google Scholar
  364. [366]
    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.Google Scholar
  365. [367]
    D.G. Luenberger Linear and Nonlinear Programming. Addison-Wesley, Reading, 1984.Google Scholar
  366. [368]
    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
  367. [369]
    A. K.Mackworth. Consistency in networks of relations. Artificial Intelligence, 8: 99–119, 1977.Google Scholar
  368. [370]
    A. El Maftouhi, and W. F. de la Vega. On Random 3-SAT. Manuscript, Laboratoire de Recherche en Informatique, Universite de paris-Sud, France. 1994.Google Scholar
  369. [371]
    F. Major, M. Turcotte, D. Gautheret, G. Lapalme, E. Fillion, and R. Cedergren. The combination of symbolic and numerical computation for three-dimensional modeling of RNA.Sciences, 253: 1255–1260, 1991.CrossRefGoogle Scholar
  370. [372]
    S. Malik, A. Wang, R. Brayton, and A. Sangiovanni-Vincentelli. Logic Verification Using Binary Decision Diagrams in a Logic Synthesis Environment. InProc. of ACM/IEEE International Conference on CAD, 1988.Google Scholar
  371. [373]
    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.Google Scholar
  372. [374]
    J.A. Makowsky and A. Sharell. On average case complexity of SAT symmetric distribution.J. of Logic and Computation, 5 (1): 71–92, Feb. 1995.MathSciNetzbMATHCrossRefGoogle Scholar
  373. [375]
    D. Marple and A.E. Gamal. Area-delay optimization of programmable logic arrays. Technical report, Stanford University, Sept. 1986.Google Scholar
  374. [376]
    T.A. Marsland and M. Campbell. Parallel search of strongly ordered game trees.ACM Computing Surveys, 14 (4): 533–551, Dec. 1982.CrossRefGoogle Scholar
  375. [377]
    T.A. Marsland and J. Schaeffer.Computers,Chess,and Cognition. Springer-Verlag, New York, 1990.zbMATHCrossRefGoogle Scholar
  376. [378]
    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
  377. [379]
    B. Mazure, L. Sais, and E. Gregoire. Tabu search for SAT. InProceedings of CP’95 Workshop on Solving Really Hard Problems, pages 127–130, 1995.Google Scholar
  378. [380]
    D. McAllester. Truth maintenance. InProceedings of AAAI’90, pages 1109–1116, 1990.Google Scholar
  379. [381]
    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. On Computers, C-34(11): 973–980, Nov. 1985.Google Scholar
  380. [382]
    J.J. McGregor. Relational consistency algorithms and their application in finding subgraph and graph isomorphisms.Information Sciences, 19: 229–250, 1979.MathSciNetzbMATHCrossRefGoogle Scholar
  381. [383]
    C.R. McLean and C.R. Dyer. An analog relaxation processor. InProceedings of the 5th International Conference on Pattern Recognition, pages 58–60, 1980.Google Scholar
  382. [384]
    K. Mehlhorn.Data Structures and Algorithms: Graph Algorithms and NP-Completeness. Springer-Verlag, Berlin, 1984.zbMATHGoogle Scholar
  383. [385]
    H.-M. Méjean, H. Morel, and G. Reynaud. A variational method for analyzing unit clause search. SIAM J. on ComputingGoogle Scholar
  384. [386]
    Z. Michalewicz.Genetic Algorithms + Data Structure = Evolution Programs. Springer-Verlag, 1994.Google Scholar
  385. [387]
    M. Minoux, The unique Horn-satisfiability problem and quadratic Boolean equations,“Annals of Mathematics and Artificial Intelligence special issue on connections between combinatorics and logic, J. Franco, M. Dunn, W. Wheeler, (eds. ) 1992.Google Scholar
  386. [388]
    S. Minton, M.D. Johnston, A.B. Philips, and P. Laird. Solving large-scale constraint satisfaction and scheduling problems using a heuristic repair method. InProceedings of AAAI’90, pages 17–24, Aug. 1990.Google Scholar
  387. [389]
    S. Minton, M.D. Johnston, A.B. Philips, and P. Laird. A heuristic repair method for constraint satisfaction and scheduling problems.Artificial Intelligence, 58: 161–205, 1992.MathSciNetzbMATHCrossRefGoogle Scholar
  388. [390]
    D.P. Miranker.TREAT: A New and Efficient Match Algorithm for AI Production Systems. Pitman, London, 1990.zbMATHGoogle Scholar
  389. [391]
    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.CrossRefGoogle Scholar
  390. [392]
    D. Mitchell, B. Selman, and H. Levesque. Hard and easy distributions of SAT problems. InProceedings of AAAI’92, pages 459–465, Jul. 1992.Google Scholar
  391. [393]
    M. Mitzenmacher. Tight thresholds for the pure literal rule. SRC Technical note 1997–011, Digital Research Corporation, Systems Research Center, Palo Alto, California, 1997 (obtained from http://gatekeeper.dec.com/pub/DEC/SRC/technicalnotes/abstracts/src-tn-1997–011.html).
  392. [394]
    R. Mohr and T. C. Henderson. Arc and path consistency revisited.Artificial Intelligence, 28: 225–233, 1986.CrossRefGoogle Scholar
  393. [395]
    B. Monien and E. Speckenmeyer. Solving satisfiability in less than 2’ steps.Discrete Applied Mathematics, 10: 117–133, 1983.MathSciNetGoogle Scholar
  394. [396]
    B. Monien, E. Speckenmeyer, and O. Vornberger. Superlinear Speedup for Parallel Backtracking.Google Scholar
  395. [397]
    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.CrossRefGoogle Scholar
  396. [398]
    P. Morris. The breakout method for escaping from local minima. InProc. of the 11th National Conf. on Artificial Intelligence, pages 4045, Washington, DC, 1993.Google Scholar
  397. [399]
    B.A. Murtagh and M.A. Saunders. MINOS 5.0 user’s guide. Technical Report SOL 83–20, Dept. of Operations Research, Stanford University, Stanford, CA, 1983.Google Scholar
  398. [400]
    B.A. Nadel. Constraint satisfaction algorithms.Computational Intelligence, 5: 188–224, 1989.CrossRefGoogle Scholar
  399. [401]
    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
  400. [402]
    D. Navinchandra.Exploration and Innovation in Design. Springer Verlag, Sadeh, 1990.Google Scholar
  401. [403]
    D. Navinchandra and D.H. Marks. Layout planning as a consistent labeling optimization problem. InProceedings of 4th International Symposium on Robotics and AI in Construction, 1987.Google Scholar
  402. [404]
    A. Newell and H. A. Simon.Human Problem Solving. Prentice-Hall, Englewood Cliffs, New Jersey, 1972.Google Scholar
  403. [405]
    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.Google Scholar
  404. [406]
    A. Nijenhuis and H. S. Wilf.Combinatorial Algorithms. Academic Press, New York, 1975.zbMATHGoogle Scholar
  405. [407]
    N.J. Nilsson.Principles of Artificial Intelligence. Tioga Publishing Company, Palo Alto, California, 1980.Google Scholar
  406. [408]
    M. Nishizawa. Partitioning of logic units.Fujitsu Scientific and Technical Journal, 7 (2): 1–13, Jun. 1971.Google Scholar
  407. [409]
    D. Pager. On the efficient algorithm for graph isomorphism.J. of ACM, 17 (4): 708–714, Jan. 1970.MathSciNetzbMATHCrossRefGoogle Scholar
  408. [410]
    C.H. Papadimitriou and K. Steiglitz. On the complexity of local search for the traveling salesman problem.SIAM J. on Computing, 6 (1): 7683, 1977.MathSciNetGoogle Scholar
  409. [411]
    C.H. Papadimitriou and K. Steiglitz.Combinatorial Optimization: Algorithms and Complexity. Prentice Hall, Englewood Cliffs, 1982.zbMATHGoogle Scholar
  410. [412]
    C.H. Papadimitriou. On selecting a satisfying truth assignment. InProceedings of the 32nd Annual Symposium of the Foundations of Computer Science, pages 163–169, 1991.Google Scholar
  411. [413]
    E. Koutsoupias, and C. H. Papadimitriou. 1992. On the greedy algorithm for satisfiability.Information Processing Letters 43, pp. 53–55.MathSciNetzbMATHCrossRefGoogle Scholar
  412. [414]
    C.H. Papadimitriou, Private Communications, 1996.Google Scholar
  413. [415]
    P.M. Pardalos and J.B. Rosen.Constrained Global Optimization: Algorithms and Applications. Springer Verlag, New York, 1987.zbMATHCrossRefGoogle Scholar
  414. [416]
    P. M. Pardalos.Complexity in numerical optimization. World Scientific, Singapore and River Edge, N.J., 1993.zbMATHCrossRefGoogle Scholar
  415. [417]
    A.M. Patel, N.L. Soong, and R.K. Korn. Hierarchical VLSI routing an approximate routing procedure.IEEE Trans. on CAD, CAD-4(2): 121–126, Apr. 1985.Google Scholar
  416. [418]
    W. Patterson.Mathematical Cryptology. Rowman & Littlefield, New Jersey, 1987.Google Scholar
  417. [419]
    P.G. Paulin and J.P. Knight. Force-directed scheduling for the behavioral synthesis of ASIC’s.IEEE Trans. on CAD, 8 (6): 661–679, June 1989.Google Scholar
  418. [420]
    J. Pearl.Heuristics. Addison-Wesley, Reading, 1984.Google Scholar
  419. [421]
    D. Pehoushek. SAT problem instances and algorithms. Private Communications, Stanford University, 1992.Google Scholar
  420. [422]
    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-11(6): 545–554, Jun. 1989.Google Scholar
  421. [423]
    L.M. Pereira and A. Porto.Selective Backtracking, pages 107–114. Academic Press, 1982.Google Scholar
  422. [424]
    C.Petrie. Revised dependency-directed backtracking for default reasoning. In Proceedings of AAAI’87,pages 167–172, 1987.Google Scholar
  423. [425]
    J. Peysakh,A fast algorithm to convert Boolean expressions into CNF, IBM Computer Science RC12913, No.57971, T.J. Watson, New York, 1987.Google Scholar
  424. [426]
    T. Pitassi and A. Urquhart. The complexity of the hajós calculus.SIAM J. on Disc. Math., 8 (3): 464–483, 1995.MathSciNetzbMATHCrossRefGoogle Scholar
  425. [427]
    J. Plotkin, J. Rosenthal, and J. Franco. Correction to probabilistic analysis of the Davis-Putnam Procedure for solving the Satisfiability problem.Discrete Applied Mathematics, 17: 295–299, 1987.MathSciNetzbMATHCrossRefGoogle Scholar
  426. [428]
    D.P. La Potin and S.W. Director. Mason: a global floorplanning approach for VLSI design.IEEE Trans. on CAD, CAD-5(4): 477–489, Oct. 1986.Google Scholar
  427. [429]
    D. K. Pradhan, editor.Fault-Tolerant Computing: Theory and Practice. Prentice-Hall, Englewood Cliffs, 1986.Google Scholar
  428. [430]
    D. Prawitz. An improved proof procedure.Theoria, 26 (2): 102–139, 1960.MathSciNetzbMATHGoogle Scholar
  429. [431]
    D. Pretolani. A linear time algorithm for unique Horn satisfiability.Information Processing Letters 48: 61–66, 1993.MathSciNetzbMATHCrossRefGoogle Scholar
  430. [432]
    D. Pretolani. Efficiency and stability of hypergraph SAT algorithmsDIMACS Series Volume: Clique,Graph Coloring,and Satisfiability — Second DIMACS Implementation Challenge. Editors: D.S. Johnson and M.A. Trick, American Mathematical Society, 1996.Google Scholar
  431. [433]
    P. Purdom. Survey of average time SAT performance. Presented in the 3rd International Symposium on AI & Mathematics, Jan. 1994.Google Scholar
  432. [434]
    P.W. Purdom. Tree size by partial backtracking.SIAM J. on Computing, 7 (4): 481–491, Nov. 1978.MathSciNetzbMATHCrossRefGoogle Scholar
  433. [435]
    P.W. Purdom. Search rearrangement backtracking and polynomial average time.Artificial Intelligence, 21: 117–133, 1983.CrossRefGoogle Scholar
  434. [436]
    P.W. Purdom. Solving satisfiability with less searching.IEEE Trans. on Pattern Analysis and Machine Intelligence, 6: 510–513, 1984.zbMATHCrossRefGoogle Scholar
  435. [437).
    P.W. Purdom. A survey of average time analyses of satisfiability algorithmsJ. of Information Processing, 13 (4): 449–455, 1990.zbMATHGoogle Scholar
  436. [438]
    P.W. Purdom. Average time for the full pure literal rule.Information Sciences, 1994 78: 269–291.CrossRefGoogle Scholar
  437. [439]
    P.W. Purdom and C.A. Brown. An analysis of backtracking with search rearrangement.SIAM J. on Computing, 12 (4): 717–733, Nov. 1983.MathSciNetzbMATHCrossRefGoogle Scholar
  438. [440]
    P.W. Purdom and C.A. Brown. The pure literal rule and polynomial average time.SIAM J. on Computing, 14: 943–953, 1985.MathSciNetzbMATHCrossRefGoogle Scholar
  439. [441]
    P.W. Purdom and C.A. Brown. Polynomial-average-time satisfiability problems.Information Science, 41: 23–42, 1987.MathSciNetzbMATHCrossRefGoogle Scholar
  440. [442]
    P.W. Purdom, C.A. Brown, and E.L. Robertson. Backtracking with multi-level dynamic search rearrangement.Acta Informatica, 15: 99113, 1981.MathSciNetGoogle Scholar
  441. [443]
    P.W. Purdom and G.N. Haven. Backtracking and probing. Technical Report No. 387, Dept. of Computer Science, Indiana University, Aug. 1993.Google Scholar
  442. [444]
    P.W. Purdom and G.N. Haven. Probe Order Backtracking. Accepted inSIAM J. on Computing, to appear in 1997.Google Scholar
  443. [445]
    R. Puri and J. Gu. An efficient algorithm to search for minimal closed covers in sequential machines.IEEE Transactions on CAD of Integrated Circuits and Systems, 12 (6): 737–745, Jun. 1993.CrossRefGoogle Scholar
  444. [446]
    R. Puri and J. Gu. An efficient algorithm for computer microword length minimization.IEEE Transactions on CAD of Integrated Circuits and Systems, 12 (10): 1449–1457, Oct. 1993.CrossRefGoogle Scholar
  445. [447]
    R. Puri and J. Gu. Area efficient synthesis of asynchronous interface circuits. InProc. of IEEE International Conference on Computer Design, 1994.Google Scholar
  446. [448]
    R. Puri and J. Gu. A divide-and-conquer approach for asynchronous circuit design. InProceedings of the 7th IEEE International Symposium on High-Level Synthesis, pages 118–125, May 1994.CrossRefGoogle Scholar
  447. [449]
    R. Puri and J. Gu. A BDD SAT solver for satisfiability testing.Annals of Mathematics and Artificial Intelligence,Vol. 17, pp. 315–337, 1996.MathSciNetzbMATHGoogle Scholar
  448. [450]
    C. D. V. P. Rao and N. N. Biswas. On the Minimization of Word-width in the Control Memory of a Microprogrammed Digital Computer.IEEE Trans. on Computers,C-32(9): 863–868, Sept. 1983.Google Scholar
  449. [451]
    C. V. S. Rao and N. N. Biswas. Minimization of Incompletely Specified Sequential Machines.IEEE Trans. on Computers,C-24: 1089–1100, Nov. 1975.Google Scholar
  450. [452]
    R.C. Read and D.G. Corneil. The graph isomorphism disease.J. of Graph Theory, 1: 339–363, 1977.MathSciNetzbMATHCrossRefGoogle Scholar
  451. [453]
    G.M. Reed and A.W. Roscoe. A timed model for communicating sequential processes. InProc. of ICALP’86, pages 314–323. Springer LNCS 226, 1986.Google Scholar
  452. [454]
    J. Reed, A. Sangiovanni-Vincentelli, and M. Santomauro. A new symbolic channel router: YACR2. IEEE Trans. on CAD,CAD-4(3):208219, July 1985.Google Scholar
  453. [455]
    M. Reichling. A simplified solution of the n queens’ problem.Information Processing Letters,Vol. 25: 253–255, June 1987.MathSciNetzbMATHGoogle Scholar
  454. [456]
    M. Resende and T. Feo. A GRASP for MAX-SAT. Presented in the 3rd International Symposium on AI & Mathematics, Jan. 1994.Google Scholar
  455. [457]
    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
  456. [458]
    R.L. Rivest and C.M. Fiduccia. A ‘greedy’ channel router. InProc. of the 19th ACM/IEEE Design Automation Conference, pages 418–424, Jun. 1982.Google Scholar
  457. [459]
    J.A. Robinson. A machine—oriented logic based on the resolution principle.Journal of the ACM, pages 23–41, 1965.Google Scholar
  458. [460]
    A. Rosenfeld. Computer vision: Basic principles.Proceedings of the IEEE, 76 (8): 863–868, Aug. 1988.CrossRefGoogle Scholar
  459. [461]
    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.Google Scholar
  460. [462]
    W. Rosiers and M. Bruynooghe. Empirical study of some constraint satisfaction problems. InProceedings of AIMSA’86, North Holland, Sept. 1986.Google Scholar
  461. [463]
    A.E. Ruehli, P.K. Wolff, and G. Goertzel. Analytical power/timing optimization technique for digital system. InProc. of the 14th ACM/IEEE Design Automation Conference, pages 142–146, Jun. 1977.Google Scholar
  462. [464]
    S. Russell and P. Norvig.Artificial Intelligence: A Modern Approach. Prentice-Hall, Englewood Cliffs, 1995.zbMATHGoogle Scholar
  463. [465]
    R.L. Russo. On the tradeoff between logic performance and circuitto-pin ratio for LSI.IEEE Trans. on Computers, C-21: 147–153, 1972.Google Scholar
  464. [466]
    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.Google Scholar
  465. [467]
    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
  466. [468]
    A. Saldanha, T. Villa, R.K. Brayton, and A.L. SangiovanniVincentelli. A Framework for Satisfying Input and Output Encoding Constraints. InProceedings of ACM/IEEE Design Automation Conference, pages 170–175, 1991.Google Scholar
  467. [469]
    A. Samal.Parallel Split-Level Relaxation. PhD thesis, Dept. of Computer Science, Univ. of Utah, Aug. 1988.Google Scholar
  468. [470]
    A. Samal and T. C. Henderson. Performance of arc consistency algorithms on the Cray. Technical Report UUCS-TR-87–017, Dept. of Computer Science, Univ. of Utah, July 23 1987.Google Scholar
  469. [471]
    A. Samal and T.C. Henderson. Parallel consistent labeling algorithms.International Journal of Parallel Programming, 1988.Google Scholar
  470. [472]
    T.J. Schaefer. The complexity of satisfiability problems. InProceedings of the 10th ACM Symposium on Theory of Computing, pages 216–226, 1978.Google Scholar
  471. [473]
    W.L. Schiele. Improved compaction by minimized length of wires. InProc. of the 20th ACM/IEEE Design Automation Conference, pages 121–127, 1983.CrossRefGoogle Scholar
  472. [474]
    I. Schiermeyer. Solving 3-Satisfiability in less than 0(1.579’ó) steps.Lecture Notes in Computer Science 702, pages 379–394, 1993.MathSciNetCrossRefGoogle Scholar
  473. [475]
    I. Schiermeyer. Pure literal lookahead: an O(1.497’ó) 3-Satisfiability algorithm. InProc. of the Workshop on Satisfiability, Universitâ delgi Studi, Siena, Italy, pages 63–72, 1996.Google Scholar
  474. [476]
    J. S. Schlipf, F. Annexstein, J. Franco, and R. Swaminathan. On finding solutions for extended Horn formulas.Information Processing Letters 54, pages 133–137, 1995.MathSciNetzbMATHCrossRefGoogle Scholar
  475. [477]
    B.M. Schwartzschild. Statistical mechanics algorithm for Monte Carlo optimization.Physics Today, 35: 17–19, 1982.Google Scholar
  476. [478]
    P. Schwarz and A. Spector. Synchronizing shared abstract types. A CM Trans. on Computer Systems,Aug. 1984.Google Scholar
  477. [479]
    M. G. Scutella. A note on Dowling and Gallier’s top-down algorithm for propositional Horn satisfiability.Journal of Logic Programming 8, pages 265–273, 1990.MathSciNetzbMATHCrossRefGoogle Scholar
  478. [480]
    C. Sechen and A.L. Sangiovanni-Vincentelli. The TIMBERWOLF placement and routing package. InProc. of the 1984 Custom Integrated Circuit Conf., May 1984.Google Scholar
  479. [481]
    B. Selman. Private Communications, Aug. 1992.Google Scholar
  480. [482]
    B. Selman, H. Levesque, and D. Mitchell. A new method for solving hard satisfiability problems. InProceedings of AAAI’92, pages 440446, Jul. 1992.Google Scholar
  481. [483]
    B. Selman and H. Kautz. Domain-independent extensions to GSAT: Solving large structured satisfiability problems. InProc. of the 13th Int’l Joint Conf. on Artificial Intelligence, pages 290–295, 1993.Google Scholar
  482. [484]
    B. Selman, H.A. Kautz, and B. Cohen. Local search strategies for satisfiability testing.DIMACS Series Volume: Clique,Graph Coloring,and Satisfiability — Second DIMACS Implementation Challenge. American Mathematical Society, pp. 290–295, 1996.Google Scholar
  483. [485]
    B. Selman, H. Kautz, and B. Cohen. Noise strategies for improving local search. InProc. of the 12th National Conf. on Artificial Intelligence, pages 337–343, Seattle, July 1994.Google Scholar
  484. [486]
    B. Selman, Private Communication, 1995.Google Scholar
  485. [487]
    E. M. Sentovich, K. J. Singh, L. Lavagno, C. Moon, R. Murgai, A. Saldanha, H. Savoj, P. R. Stephan, R. K. Brayton, and A. SangiovanniVincentelli. SIS: A System for Sequential Circuit Synthesis. Technical Report UCB/ERL M92/41, Dept. of EECS, Univ. of California, Berkeley, May, 1992.Google Scholar
  486. [488]
    M.J. Shensa. A computational structure for the propositional calculus. InProceedings of IJCAI, pages 384–388, 1989.Google Scholar
  487. [489]
    R.C.-J. Shi, A. Vannelli, and J. Vlach. An improvement on Karmarkar’s algorithm for integer programming. COAL Bulletin of the Mathematical Programming Society, 21: 23–28, 1992.Google Scholar
  488. [490]
    H. Shin, A.L. Sangiovanni-Vincentelli, and C.H. Sequin. Two-dimensional compaction by ‘zero refining’. InProc. of the 23rd ACM/IEEE Design Automation Conference, pages 115–122, Jun. 1986.CrossRefGoogle Scholar
  489. [491]
    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.MathSciNetCrossRefGoogle Scholar
  490. [492]
    P. Siegel.Representation et Utilization de la Connaissances en Calcul Propositionel. PhD thesis, University Aix-Marseille I I, 1987.Google Scholar
  491. [493]
    J.C. Simon. Off-line cursive word recognition.Proceedings of the IEEE, 80 (7): 1150–1161, Jul. 1992.CrossRefGoogle Scholar
  492. [494]
    R. Sosie and J. Gu. Quick n-queen search on VAX and Bobcat machines. CS547 AI Course Project, Winter Quarter, Feb. 1988.Google Scholar
  493. [495]
    R. Sosie 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
  494. [496]
    R. Sosie and J. Gu. A polynomial time algorithm for the n-queens problem. SIGART Bulletin,1(3):7–11, Aug. 1990, ACM Press.Google Scholar
  495. [497]
    R. Sosie and J. Gu. Fast search algorithms for the n-queens problem. IEEE Trans. on Systems, Man, and Cybernetics, SMC-21(6):15721576, Nov./Dec. 1991.Google Scholar
  496. [498]
    R. Sosie and J. Gu. 3,000,000 queens in less than one minute. SIGART Bulletin,2(2):22–24, Apr. 1991, ACM Press.Google Scholar
  497. [499]
    R. Sosie and J. Gu. A parallel local search algorithm for satisfiability (SAT) problem.Submitted for publication, 1993.Google Scholar
  498. [500]
    R. Sosie and J. Gu. A parallel local search algorithm for the n-queen problem.Submitted for publication, 1993.Google Scholar
  499. [501]
    R. Sosie and J. Gu. Efficient local search with conflict minimization.IEEE Trans. on Knowledge and Data Engineering, 6 (5): 661–668, Oct. 1994.Google Scholar
  500. [502]
    R. Sosie, J. Gu, and R. Johnson. The Unison algorithm: Fast evaluation of Boolean expressions. Accepted for publication inCommunications of the ACM in 1992.ACM Transactions on Design Automation of Electronic Systems, (1)4: 456–477, Oct. 1996.Google Scholar
  501. [503]
    R. Sosie, J. Gu, and R. Johnson. A universal Boolean evaluator.IEEE Trans. on Computers, accepted for publication in 1992.Google Scholar
  502. [504]
    J. Soukup. Circuit layout. InProceedings of the IEEE, pages 12811304, Oct. 1981.Google Scholar
  503. [505]
    E. Speckenmeyer. Personal Communication. 1996.Google Scholar
  504. [506]
    R. Stallman and G.J. Sussman. Forward reasoning and dependency directed backtracking.Artificial Intelligence, 9 (2): 135–196, 1977.zbMATHCrossRefGoogle Scholar
  505. [507]
    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
  506. [508]
    J.A. Stankovic. Real-time computing systems: The next generation. Manuscript. Feb. 18, 1988.Google Scholar
  507. [509]
    L. Sterling and E. Shapiro.The Art of Prolog,Advanced Programming Techniques. The MIT Press, Cambridge, Massachusetts, 1986.Google Scholar
  508. [510]
    H.S. Stone and P. Sipala. The average complexity of depth-first search with backtracking and cutoff.IBM J. Res. Develop., 30 (3): 242–258, May 1986.zbMATHCrossRefGoogle Scholar
  509. [511]
    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.CrossRefGoogle Scholar
  510. [512]
    C.Y. Suen, M. Berthod, and S. Mori. Automatic recognition of hand printed characters — the state of the art.Proceedings of the IEEE, 68 (4): 469–487, Apr. 1980.CrossRefGoogle Scholar
  511. [513]
    S. Sutanthavibul, E. Shragowitz, and J.B. Rosen. An analytical approach to floorplan design and optimization.IEEE Trans. on CAD, 10 (6): 761–769, June 1991.Google Scholar
  512. [514]
    R. P. Swaminathan and D. K. Wagner. The arborescence—realization problem.Discrete Applied Mathematics 59, pages 267–283, 1995.MathSciNetzbMATHGoogle Scholar
  513. [515]
    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 Design Automation Conference , pages 544–550, 1982.Google Scholar
  514. [516]
    A. Thayse and M. Davio, Boolean differential calculus and its application to switching theory,IEEE Trans. on Computers 22 (1973), 409–420.MathSciNetzbMATHCrossRefGoogle Scholar
  515. [517]
    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
  516. [518]
    A. Törn and A. 2. ilinskas.Global Optimization. Springer-Verlag, 1989.Google Scholar
  517. [519]
    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.Google Scholar
  518. [520]
    K. Truemper. Alpha-balanced graphs and matrices and GF(3)representability of matroids.Journal of Combinatorial Theory B 32, pages 112–139, 1982.MathSciNetzbMATHCrossRefGoogle Scholar
  519. [521]
    K. Truemper. Monotone Decomposition of Matrices. Technical Report UTDCS-1–94, University of Texas at Dallas. 1994.Google Scholar
  520. [522]
    K. Truemper. Polynomial algorithms for problems over d-systems. Presented in the 3rd International Symposium on AI & Mathematics, Jan. 1994.Google Scholar
  521. [523]
    K. Truemper. In preparation, expected 1997. Effective Logic Computation.Google Scholar
  522. [524]
    G.S. Tseitin. On the Complexity of Derivations in Propositional Calculus. InStructures in Constructive Mathematics and Mathematical Logic, Part II, A.O. Slisenko, ed., pages 115–125. 1968.Google Scholar
  523. [525]
    K. J. Turner.Computer Perception of Curved Objects Using a Television Camera. PhD thesis, Univ. Edinburgh, 1974.Google Scholar
  524. [526]
    J.D. Tygar and R. Ellickson.Efficient netlist comparison using hierarchy and randomization. In Proc. of the 22nd ACM/IEEE Design Automation Conference, pages 702–708, 1985.Google Scholar
  525. [527]
    J. E. Tyler. Parallel computer architectures and problem solving strategies for the consistent labeling problem. Master’s thesis, Dept. of Elec. Engg., Virginia Polytech. Inst. State Univ., Blacksburg, Virginia, Oct. 1983.Google Scholar
  526. [528]
    J.D. Ullman.Principles of Database Systems. Computer Science Press, Rockville, 1982.zbMATHGoogle Scholar
  527. [529]
    J.R. Ullman. An algorithm for subgraph isomorphism.J. ACM, 23 (1): 31–42, Jan. 1976.zbMATHCrossRefGoogle Scholar
  528. [530]
    J.R. Ullman. A binary ri-gram technique for automatic correction of substitution, deletion, insertion and reversal errors in words.The Computer Journal, 20 (2): 141–147, Feb. 1977.CrossRefGoogle Scholar
  529. [531]
    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.CrossRefGoogle Scholar
  530. [532]
    A. Urquhart. Hard examples for resolution.J. of ACM, 34: 209–219, 1987.MathSciNetzbMATHCrossRefGoogle Scholar
  531. [533]
    A. Urquhart. The complexity of gentzen systems for propositional logic.Theoretical Computer Science, 66: 87–97, 1989.MathSciNetzbMATHCrossRefGoogle Scholar
  532. [534]
    A. Urquhart. The relative complexity of resolution and cut-free gentzen systems.Annals of Mathematics and Artificial Intelligence, 6: 157–168, 1992.MathSciNetzbMATHCrossRefGoogle Scholar
  533. [535]
    A. Urquhart. The complexity of propositional proofs.The Bulletin of Symbolic Logic, 1 (4): 425–467, 1995.MathSciNetzbMATHGoogle Scholar
  534. [536]
    M. Valtorta. Response to “Explicit Solutions to the N-Queens Problem for all N.” SIG ART Bulletin,2(4):4, Aug. 1991, ACM Press.Google Scholar
  535. [537]
    M. van der Woude and X. Timermans. Compaction of hierarchical cells with minimum and maximum compaction constraints. InProc. Int’l Symposium on Circuits and Systems, pages 1018–1021, 1983.Google Scholar
  536. [538]
    P. Vanbekbergen, G. Goossens, F. Catthoor, and H. De Man. Optimized Synthesis of Asynchronous Control Circuits from Graph-Theoretic Specifications.IEEE Trans. on CAD, 11 (11): 1426–1438, Nov. 1992.Google Scholar
  537. [539]
    P. Vanbekbergen, B. Lin, G. Goossens, and H. De Man. A Generalized State Assignment Theory for Transformations on Signal Transition Graphs. InProc. of ICCAD, pages 112–117, 1992.Google Scholar
  538. [540]
    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
  539. [541]
    B. W. Wah, G. J. Li, and C. F. Yu. Multiprocessing of combinatorial search problems.IEEE Computer, 18(6):93–108, June 1985. Also inTutorial: Computers for Artificial Intelligence Applications, ed. B. W. Wah, IEEE Computer Society, 1986, pp. 173–188.Google Scholar
  540. [542]
    B. Wah and G.J. Li.Computers for Artificial Intelligence Applications. IEEE Computer Society Press, Washington D. C., 1986.Google Scholar
  541. [543]
    B.W. Wah, editor.New Computers for Artificial Intelligence Processing. IEEE Computer, volume 20, number 1. IEEE Computer Society Press, 1987.Google Scholar
  542. [544]
    B.W. Wah, M.B. Lowrie, and G.-J. Li. Computers for symbolic processing.Proceedings of the IEEE, 77 (4): 509–540, Apr. 1989.CrossRefGoogle Scholar
  543. [545]
    B. W. Wah, G. J. Li, and C. F. Yu. Multiprocessing of combinatorial search problems. In L. Kanal, V. Kumar, and P. S. Gopalakrishnan, editors,Parallel Algorithms for Machine Intelligence and Pattern Recognition, pages 102–145. Springer-Verlag, New York, NY, 1990.Google Scholar
  544. [546]
    B. W. Wah and L.-C. Chu. Combinatorial search algorithms with meta-control: Modeling and implementations.Int’l J. of Artificial Intelligence Tools, 1 (3): 369–397, September 1992.CrossRefGoogle Scholar
  545. [547]
    B. W. Wah and Y. Shang. A comparison of a class of IDA* search algorithms.Int’l J. of Artificial Intelligence Tools, 3 (4): 493–523, October 1995.Google Scholar
  546. [548]
    B. W. Wah and Y. Shang. A discrete lagrangian-based global-search method for solving satisfiability problems. In Ding-Zhu Du, Jun Gu, and Panos Pardalos, editors,Proc. of the DIMACS Workshop on Satisfiability Problem: Theory and Applications. American Mathematical Society, March 1996.Google Scholar
  547. [549]
    B. W. Wah and C. F. Yu. Stochastic modeling of branch-and-bound algorithms with best-first search.Trans. on Software Engineering, SE-11(9): 922–934, September 1985.Google Scholar
  548. [550]
    B. Wah and Y.-J. Chang. Trace-Based Methods for Solving Nonlinear Global Optimization and Satisfiability Problems.J. of Global Optimization. Submitted in July 1995 and accepted to appear in 1996.Google Scholar
  549. [551]
    D. Waltz. Generating semantic descriptions from drawings of scenes with shadows. Technical Report AI271, MIT, Nov. 1972.Google Scholar
  550. [552]
    D. Waltz. Understanding Line Drawings of Scenes with Shadows. InP. H. Winston, The Psychology of Computer Vision,chapter 2, pages 19–92. McGraw-Hill Book Company, New York, 1975.Google Scholar
  551. [553]
    W. Wang, J. Gu, and T. C. Henderson. A pipelined architecture for parallel image relaxation operations.IEEE Trans. on Circuits and Systems, CAS-34(11): 1375–1384, Nov. 1987.Google Scholar
  552. [554]
    W. Wang, J. Gu, and K.F. Smith. A regular layout for concurrent discrete relaxation computation. InProceedings of 1987 IEEE International CAS Symposium, pages 927–933, May 1987.Google Scholar
  553. [555]
    W. Wang and C.K. Rushforth. An adaptive local search algorithm for channel assignment problem.IEEE Trans. on Vehicular Technology, Vol. 45, No. 3, pp. 459–466, Aug. 1996.CrossRefGoogle Scholar
  554. [556]
    W. Wang and C.K. Rushforth. Structured partitioning for channel assignment problem.IEEE Trans. on Vehicular Technology, 1996.Google Scholar
  555. [557]
    M. B. Wells.Elements of Combinatorial Computing. Pergamon Press, Oxford, 1971.zbMATHGoogle Scholar
  556. [558]
    H.P. Williams. Linear and integer programming applied to the propositional calculus.Systems Research and Information Sciences, 2: 81–100, 1987.Google Scholar
  557. [559]
    P.H. Winston.Artificial Intelligence. Addison-Wesley, Reading, 1984.zbMATHGoogle Scholar
  558. [560]
    E.E. Witte, R.D. Chamberlain, and M.A. Franklin. Parallel simulated annealing using speculative computation.IEEE Trans. on Parallel and Distributed Systems, 2 (4): 483–494, Oct. 1991.CrossRefGoogle Scholar
  559. [561]
    L. Wos, G. A. Robinson, and D. Carson. Efficiency and completeness of the set of support strategy.Journal of the ACM, 12: 536–541, 1965.MathSciNetzbMATHCrossRefGoogle Scholar
  560. [562]
    L.C. Wu and C.Y. Tang. Solving the satisfiability problem by using randomized approach.Information Processing Letters, 41: 187–190, 1992.MathSciNetzbMATHCrossRefGoogle Scholar
  561. [563]
    T. Y. Young and K. S. Fu, editors.Handbook of Pattern Recognition and Image Processing. Academic Press, Orlando, 1986.zbMATHGoogle Scholar
  562. [564]
    C. F. Yu.Efficient Combinatorial Search Algorithm. PhD thesis, School of Electrical Engineering, Purdue University, West Lafayette, IN, Dec. 1986.Google Scholar
  563. [565]
    C. F. Yu and B. W. Wah. Stochastic modeling of branch-and-bound algorithms with best-first search.IEEE Trans. on Software Engineering, 11 (9): 922–934, Sept 1985.zbMATHGoogle Scholar
  564. [566]
    C.F. Yu and B.W. Wah. Efficient branch-and-bound algorithms on a two-level memory system.IEEE Trans. on Software Engineering, 14 (9): 1342–1356, Sept 1988.MathSciNetCrossRefGoogle Scholar
  565. [567]
    R. Zabih and D. McAllester. A rearrangement search strategy for determining propositional satisfiability. InProceedings of AAAI’88, pages 155–160, 1988.Google Scholar
  566. [568]
    V.N. Zemlyachenko, N.M. Korneeko, and R.I. Tyshkevich. Graph isomorphism problem.J. of Soviet Mathematics, 29: 1426–1481, 1985.zbMATHCrossRefGoogle Scholar
  567. [569]
    S. Zhang and A. G. Constantinides. Lagrange programming neural networks.IEEE Transactions on Circuits and Systems-II: Analog and Digital Signal Processing, 39 (7): 441–452, 1992.zbMATHCrossRefGoogle Scholar
  568. [570]
    S. Zhou. A trace-driven simulation study of dynamic load balancing.IEEE Trans. on Software Engineering, SE-14(9): 1327–1341, Sept. 1988.Google Scholar
  569. [571]
    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.Google Scholar

Copyright information

© Springer Science+Business Media Dordrecht 1999

Authors and Affiliations

  • Jun Gu
    • 1
  • Paul W. Purdom
    • 2
  • John Franco
    • 3
  • Benjamin W. Wah
    • 4
  1. 1.Dept. of Electrical and Computer EngineeringUniversity of CalgaryCalgaryCanada
  2. 2.Dept. of Computer ScienceIndiana UniversityBloomingtonUSA
  3. 3.Dept. of Computer ScienceUniversity of CincinnatiCincinnatiUSA
  4. 4.Dept. of Electrical and Computer EngineeringUniv. of Illinois at Urbana-ChampaignUrbanaUSA

Personalised recommendations