Skip to main content
SpringerLink
Log in

Ten Challenges Redux: Recent Progress in Propositional Reasoning and Search

  • Conference paper
Principles and Practice of Constraint Programming – CP 2003 (CP 2003)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2833))

Abstract

In 1997 we presented ten challenges for research on satisfiability testing [1]. In this paper we review recent progress towards each of these challenges, including our own work on the power of clause learning and randomized restart policies.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Selman, B., Kautz, H.A., McAllester, D.A.: Ten challenges in propositional reasoning and search. In: Proceedings of the Fifteenth International JointConference on Artificial Intelligence (IJCAI 1997), pp. 50–54 (1997)

    Google Scholar 

  2. Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without BDDs. In: Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems, Amsterdam, The Netherlands, March 1999, pp. 193–207 (1999)

    Google Scholar 

  3. Velev, M.N., Bryant, R.E.: Effective use of boolean satisfiability procedures in the formal verification of superscalar and vliw microprocessors. In: Proc. 38th Design Automation Conference (DAC 2001), pp. 226–231 (2001)

    Google Scholar 

  4. Bjesse, P., Leonard, T., Mokkedem, A.: Finding bugs in an alpha microprocessor using satisfiability solvers. In: Proc. 13th Int. Conf. on Computer Aided Verification (2001)

    Google Scholar 

  5. Simon, L., Le Berre, D., Hirsch, E.: The sat2002 competition (2002), http://www.satlive.org/SATCompetition/onlinereport.pdf

  6. Le Berre, D., Simon, L.: The essentials of the sat 2003 competition, Under review (2003). Draft, available at http://www.lri.fr/simon/contest03/results/

  7. http://www.cs.washington.edu/homes/kautz/challenge/ .

  8. Johnson, D.S., Trick, M.A. (eds.): Cliques, Coloring and Satisfiability: second DIMACS Implementation Challenge. DIMACS Series in Disc. Math. and Theor. Computer Science, vol. 26. AMS, Providence (1996)

    MATH  Google Scholar 

  9. Davis, M., Logemann, G., Loveland, D.: A machine program for theorem proving. Communications of the ACM 5, 394–397 (1979)

    Article  MathSciNet  Google Scholar 

  10. Li, C.M., Gerard, S.: On the limit of branching rules for hard random unsatisfiable 3-sat. In: Proc. ECAI (2000)

    Google Scholar 

  11. Dubois, O., Dequen, G.: A backbone-search heuristic for efficient solving of hard 3-sat formulae. In: Proc. of the 17th International Joint Conference on Artificial Intelligence (IJCAI 2001) (2001)

    Google Scholar 

  12. Monasson, R., Zecchina, R., Kirkpatrick, S., Selman, B., Troyansky, L.: Determining computational complexity from characteristic phase transitions. Nature 400(8), 133–137 (1999)

    MathSciNet  Google Scholar 

  13. Martin, O., Monasson, R., Zecchina, R.: Statistical mechanics methods and phase transitions in optimization problems. Theor. Computer Science 265 (2001)

    Google Scholar 

  14. Phase transitions and algorithmic complexity ipam (July 2002), http://www.ipam.ucla.edu/programs/ptac2002/ptac2002-schedule.html

  15. Achlioptas, D., Beame, P., Molloy, M.: A sharp threshold in proof complexity. In: Proc., 33st Annual ACM Symp. on Theory of Computing, Crete, Greece, July 2001, pp. 337–346 (2001)

    Google Scholar 

  16. Bollobas, B., Borgs, C., Chayes, J.T., Han Kim, J., Wilson, D.B.: The scaling window of the 2sat transition. Rand. Struct. Alg. 18, 301 (2001)

    Google Scholar 

  17. Achlioptas, D., Lefteris, Kirousis, M., Kranakis, E., Krizanc, D.: Dimitris Achlioptas, Lefteris, M. Kirousis, Evangelos Kranakis, and Danny Krizanc. Rigorous results for (2+p)-sat. Theor. Comp. Sci. 265, 109–129 (2001)

    Article  MATH  Google Scholar 

  18. Dubois, O., Monasson, R., Selman, B., Zecchina, R.: Phase transitions in combinatorial problems. Theor. Computer Science, 265 (2001) (special issue)

    Google Scholar 

  19. Friedgut, E.: Sharp thresholds of graph properties, and the k-sat problem. Journal of the American Mathematical Society 12, 1017–1054 (1999)

    Article  MATH  MathSciNet  Google Scholar 

  20. Gomes, C., Selman, B.: Satisfied with physics. Science 297, 784–785 (2002) (perspective article)

    Article  Google Scholar 

  21. Hogg, T., Huberman, B., Williams, C.: Phase Transitions and Complexity. Artificial Intelligence 81, 1–2 (1996) (special Issue)

    Article  MathSciNet  Google Scholar 

  22. Mitchell, D.G., Selman, B., Levesque, H.J.: Hard and easy distributions for SAT problems. In: Proc. 10th Natl. Conf. on Artificial Intelligence, pp. 459–465 (1992)

    Google Scholar 

  23. Mézard, M., Parisi, G., Zecchina, R.: Analytic and algorithmic solution of random satisfiability problems. Science 297, 812 (2002)

    Article  Google Scholar 

  24. Selman, B., Kautz, H., Cohen, B.: Local search strategies for satisfiability testing. Dimacs Ser. in Discr. Math. and Theor. Comp. Science, vol. 26, pp. 521–532. AMS, Providence (1996)

    Google Scholar 

  25. Crawford, J.M., Kearns, M.J., Schapire, R.E.: The minimal disagreement parity problem as a hard satisfiability problem (1995) (unpublished manuscript)

    Google Scholar 

  26. Warners, J., van Maaren, H.: A two phase algorithm for solving a class of hard satisability problems. Operations Research Letters 23, 81–88 (1999)

    Article  Google Scholar 

  27. Li, C.M.: Integrating equivalency reasoning into davis-putnam procedure. In: Proceedings of the National Conference on Articial Intelligence, pp. 291–296 (2000)

    Google Scholar 

  28. Morris, P.: The breakout method for escaping from local minima. In: Proc. AAAI 1993, pp. 40–45 (1993)

    Google Scholar 

  29. Selman, B., Kautz, H.: An empirical study of greedy local search for satisfiability testing. In: Proc. AAAI 1993, pp. 46–51 (1993)

    Google Scholar 

  30. Wu, Z., Wah, B.W.: Trap escaping strategies in discrete lagrangian methods for solving hard satisfiability and maximum satisfiability problems. In: Proc. AAAI 1999, pp. 673–678 (1999)

    Google Scholar 

  31. Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. Information and Computation 98(2), 142–170 (1992)

    Article  MATH  MathSciNet  Google Scholar 

  32. McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Dordrecht (1993)

    MATH  Google Scholar 

  33. Davis, M., Putnam, H.: A computing procedure for quantification theory. Journal of the ACM 7 (1960)

    Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

  35. Cook, S.A., Reckhow, R.A.: The relative efficiency of propositional proof systems. Journal of Symbolic Logic 44(1), 36–50 (1977)

    MathSciNet  Google Scholar 

  36. Bonet, M.L., Esteban, J.L., Galesi, N., Johansen, J.: On the relative complexity of resolution refinements and cutting planes proof systems. SIAM J. Comput. 30(5), 1462–1484 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  37. Ben-Sasson, E., Impagliazzo, R., Wigderson, A.: Near-optimal separation of treelike and general resolution. Technical Report TR00-005, Elec. Colloq. Comput. Compl (2000), http://www.eccc.uni-trier.de/eccc/

  38. Haken, A.: The intractability of resolution. Theoretical Computer Science 39, 297–308 (1985)

    Article  MATH  MathSciNet  Google Scholar 

  39. Chvatal, V., Szemeredi, E.: Many hard examples for resolution. Journal of the ACM 35(4), 759–208 (1988)

    Google Scholar 

  40. Cook, S., Mitchell, D.: Finding hard instances of the satisfiability problem: a survey. DIMACS Series in Discr. Math. and Theoretical Comp. Sci. 35, 1–17 (1997)

    MathSciNet  Google Scholar 

  41. Roberto, J., Bayardo Jr., Schrag, R.C.: Using CST look-back techniques to solve real-world SAT instances. In: Proceedings, AAAI 1997: 14th Natl. Conf. on Art. Intel., pp. 203–208 (1997)

    Google Scholar 

  42. Zhang, H.: SATO: An efficient propositional prover. In: McCune, W. (ed.) CADE 1997. LNCS, vol. 1249, pp. 272–275. Springer, Heidelberg (1997)

    Google Scholar 

  43. Stallman, R., Sussman, G.: And forward reasoning and dependency-directed backtracking in a system for computer-aided circuit analysis. Artificial Intelligence 9(2) (1977)

    Google Scholar 

  44. de Kleer, J., Williams, B.C.: Diagnosing multiple faults. Artificial Intelligence 32(1), 97–130 (1987)

    Article  MATH  Google Scholar 

  45. Davis, R.: Diagnostic reasoning based on structure and behavior. Artificial Intelligence 24, 347–410 (1984)

    Article  Google Scholar 

  46. Marques-Silva, J.P., Sakallah, K.A.: GRASP – a new search algorithm for satisfiability. In: Proc. of the International Conference on Computer Aided Design, San Jose, CA, pp. 220–227. ACM/IEEE (1996)

    Google Scholar 

  47. Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Proc. of the 38th Design Automation Conference, Las Vegas, NV, June 2001, pp. 530–535. ACM/IEEE (2001)

    Google Scholar 

  48. Zhang, L., Madigan, C.F., Moskewicz, M.H., Malik, S.: Efficient conflict driven learning in a boolean satisfiability solver. In: Proc. of the International Conference on Computer Aided Design, San Jose, CA, pp. 279–285. ACM/IEEE (2001)

    Google Scholar 

  49. Goldberg, E., Novikov, Y.: Berkmin: A fast and robust sat solver. In: Proceedings of Design Automation and Test in Europe (DATE) 2002, pp. 142–149 (2002)

    Google Scholar 

  50. Marques-Silva, J.P.: An overview of backtrack search satisfiability algorithms. In: 5th International Symposium on Artificial Intelligence and Mathematics, Fort Lauderdale, Florida (January 1998)

    Google Scholar 

  51. Beame, P., Kautz, H., Sabharwal, A.: Understanding the power of clause learning. In: Proc. of the 18th International Joint Conference on Artificial Intelligence, Acapulco, Mexico (August 2003)

    Google Scholar 

  52. Gomes, C.P., Selman, B., Kautz, H.: Boosting Combinatorial Search Through Randomization. In: Proc. 15th Natl. Conf. on Artificial Intelligence (AAAI 1998), pp. 431–438 (1998)

    Google Scholar 

  53. Baptista, L., Silva, J.P.M.: Using randomization and learning to solve hard real-world instances of satisfiability. Prin. and Prac. of Const. Prog (2000)

    Google Scholar 

  54. Beame, P., Agarwal, A., Kautz, H.: Using problem structure for efficient clause learning. In: Proceedings of the Sixth International Conference on Theory and Applications of Satisfiability Testing (2003)

    Google Scholar 

  55. Bonet, M.L., Galesi, N.: A study of proof search algorithms for resolution and polynomial calculus. In: Proc., 40th Annual Symp. on Found. of Comput. Sci., pp. 422–432. IEEE, Los Alamitos (1999)

    Google Scholar 

  56. Ben-Sasson, E., Impagliazzo, R., Wigderson, A.: Near-optimal separation of treelike and general resolution. Technical Report TR00-005, Electronic Colloquium in Computation Complexity (2000), http://www.eccc.uni-trier.de/eccc/

  57. Beame, P., Impagliazzo, R., Pitassi, T., Segerlind, N.: Memoization and DPLL: Formula caching proof systems. In: Proc. 18th Annual IEEE Conf. on Comput. Complexity, Aarhus, Denmark (July 2003)

    Google Scholar 

  58. Krishnamurthy, B.: Short proofs for tricky formulas. Acta Informatica 22, 253–275 (1985)

    Article  MATH  MathSciNet  Google Scholar 

  59. Crawford, J., Ginsberg, M., Luks, E., Roy, A.: Symmetry-breaking predicates for search problems. In: Proc. Intl. Conf. Principles of Knowledge Representation and Reasoning, pp. 148–159 (1996)

    Google Scholar 

  60. Aloul, F.A., Markov, I.L., Sakallah, K.A.: Efficient symmetry breaking for boolean satisfiability. In: Proc. Intl. Joint Conf. on Artificial Intelligence (IJCAI 2003) (2003)

    Google Scholar 

  61. Urquhart, A.: The symmetry rule in propositional logic. Discrete Applied Mathematics 96, 177–193 (1999)

    Article  MathSciNet  Google Scholar 

  62. Beame, P., Impagliazzo, R., Pitassi, T., Segerlind, N.: Memoization and dpll: formula caching proof systems. In: IEEE Conference on Computational Complexity (2003)

    Google Scholar 

  63. Bacchus, F., Dalmao, S., Pitassi, T.: Dpll with caching: A new algorithm for #sat and bayesian inference, Technical Report TR03-003, Electronic Cooloquium in Computational Complexity (2003), http://www.ecc.uni-trier.de/eccc/

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

    Article  MATH  MathSciNet  Google Scholar 

  65. Kamath, A.P., Karmarker, N.K., Ramakrishnan, K.G., Resende, M.G.C.: Computational experience with an interior point algorithm on the satisfiability problem. In: Proc. Integer Programming and Combinatorial Optimization (1990)

    Google Scholar 

  66. Warners, J.P., de Klerk, E., van Maaren, H.: Relaxations of the satisfiability problem using semidefinite programming (1999)

    Google Scholar 

  67. Joachim Walser. Solving linear pseudo-boolean constraint problems with local search. In: Proc. 14th Natl. Conf. on Artificial Intelligence (AAAI 1997) (1998)

    Google Scholar 

  68. Aloul, F., Ramani, A., Markov, I., Sakallah, K.: Generic ilp versus specialized 0-1 ilp: an update. In: Intl. Conf. on Computer Aided Design (ICCAD) (2002)

    Google Scholar 

  69. Parkes, A.: Pb-lib: The pseudo-boolean library (2003)

    Google Scholar 

  70. Williams, R., Gomes, C., Selman, B.: Backdoors to typical case complexity. In: Proc. of the Eighteenth International Joint Conference on Artificial Intelligence (IJCAI 2003) (2003)

    Google Scholar 

  71. Wei, W., Selman, B.: Accelerating random walks. In: Van Hentenryck, P. (ed.) CP 2002. LNCS, vol. 2470, p. 216. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  72. Wah, B.W., Shang, Y.: A discrete langrangian-based global- search method for solving satisfiability problems. J. of Global Optim. 12 (1998)

    Google Scholar 

  73. Selman, B., Levesque, H., Mitchell, D.: Gsat: A new method for solving hard satisfiability problems. In: Proceedings of the 10th National Conference on Artificial Intelligence (AAAI 1992), San Jose, CA, pp. 440–446. AAAI Press, Menlo Park (1992)

    Google Scholar 

  74. Schuurmans, D., Southey, F.: Local search characteristics of incomplete SAT procedures. In: Proceedings of the 17th National Conference on Articial Intelligence (AAAI 2000), pp. 297–302 (2000)

    Google Scholar 

  75. Semerjian, G., Monasson, R.: A study of pure random walk on random satisfiability problems with physical methods. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 120–134. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  76. Hoos, H.: On the run-time behaviour of stochastic local search algorithms for SAT. In: Proceedings of AAAI 1999, pp. 661–666. AAAI Press, Menlo Park (1999)

    Google Scholar 

  77. Hoos, H.: Stochastic local search — methods, models, applications. PhD Thesis, TU Darmstadt (1998)

    Google Scholar 

  78. Boyan, J.A., Moore, A.W.: Learning evaluation functions for global optimization and Boolean satisfiability. In: Proceedings of the 15th National Conference on Articial Intelligence (AAAI 1998), pp. 3–10 (1998)

    Google Scholar 

  79. Frank, J., Cheeseman, P., Stutz, J.: When gravity fails: Local search topology. Journal of Artificial Intelligence Research 7, 249–281 (1997)

    MATH  MathSciNet  Google Scholar 

  80. Hirsch, E.A., Kojevnikov, A.: Unitwalk: A new sat solver that uses local search guided by unit clause elimination. In: PDMI preprint 9/2001, Steklov Institute of Mathematics at St.Petersburg (2001)

    Google Scholar 

  81. Paturi, R., Pudlak, P., Zane, F.: Satisfiability coding lemma. In: Proc. of the 38th Annual IEEE Symposium on Foundations of Computer Science, FOCS 1997, pp. 566–574 (1997)

    Google Scholar 

  82. Li, X.Y., Stallman, M., Brglez, F.: Qingting: A local search sat solver using an effective switching strategy and efficient unit propagation. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 53–68. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  83. Brafman, R.I.: A simplifier for propositional formulas with many binary clauses. In: Proc. IJCAI 2001, pp. 515–520 (2001)

    Google Scholar 

  84. Bacchus, F., Winter, J.: Effective preprocessing with hyper-resolution and equality reduction. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 341–355. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  85. Ostrowski, R., Grigoire, E., Mazure, B., Sais, L.: Recovering and exploiting structural knowledge from cnf formulas. In: Van Hentenryck, P. (ed.) CP 2002. LNCS, vol. 2470, pp. 185–199. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  86. Habet, D., Li, C.M., Devendeville, L., Vasquez, M.: A hybrid approach for sat. In: Van Hentenryck, P. (ed.) CP 2002. LNCS, vol. 2470, p. 172. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  87. Mazure, B., Sais, L., Gregoire, E.: Boosting complete techniques thanks to local search methods. In: Proc. Math and AI (1996)

    Google Scholar 

  88. Gomes, C.P., Selman, B., Crato, N., Kautz, H.: Heavy-tailed phenomena in satisfiability and constraint satisfaction problems. J. of Automated Reasoning 24(1–2), 67–100 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  89. Chen, H., Gomes, C., Selman, B.: Formal models of heavy-tailed behavior in combinatorial search. In: Walsh, T. (ed.) CP 2001. LNCS, vol. 2239, p. 408. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  90. Gent, I., Walsh, T.: Easy Problems are Sometimes Hard. Artificial Intelligence 70, 335–345 (1993)

    Article  MathSciNet  Google Scholar 

  91. Walsh, T.: Search in a Small World. In: Proceedings of the International Joint Conference on Artificial Intelligence, Stockholm, Sweden (1999)

    Google Scholar 

  92. Luby, M., Sinclair, A., Zuckerman, D.: Optimal speedup of las vegas algorithms. Information Process. Letters, 173–180 (1993)

    Google Scholar 

  93. Horvitz, E., Ruan, Y., Gomes, C., Kautz, H., Selman, B., Chickering, M.: A Bayesian approach to tackling hard computational problems. In: Proc. 17th Conc. on Uncertainty in Artificial Intelligence (UAI 2001) (2001)

    Google Scholar 

  94. Kautz, H., Horvitz, E., Ruan, Y., Selman, B., Gomes, C.: Dynamic randomized restarts: Optimal restart policies with observation. In: AAAI 2002 (2002)

    Google Scholar 

  95. Ruan, Y., Horvitz, E., Kautz, H.: Restart policies with dependence among runs: A dynamic programming approach. In: Van Hentenryck, P. (ed.) CP 2002. LNCS, vol. 2470, p. 573. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  96. Ruan, Y., Horvitz, E., Kautz, H.: Hardness-aware restart policies, under review (2003)

    Google Scholar 

  97. Walsh, T.: Reformulating propositional satisfiability as constraint satisfaction. In: Choueiry, B.Y., Walsh, T. (eds.) SARA 2000. LNCS (LNAI), vol. 1864, p. 233. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  98. Prestwich, S.: Local search on sat-encoded csps. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 105–119. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  99. van Beek, P., Dechter, R.: Constraint tightness and looseness versus local and global consistency. JACM 44(4), 549–566 (1997)

    Article  MATH  Google Scholar 

  100. Bessiere, C., Hebrard, E., Walsh, T.: Local consistencies in sat. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 299–314. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  101. Kautz, H.A., McAllester, D.A., Selman, B.: Encoding plans in propositional logic. In: Proc. of the 5th Intl. Conf. on Princ. of Knowl. Repr. and Reasoning, Boston, MA, November 1996, pp. 374–384 (1996)

    Google Scholar 

  102. Michael Ernst, Todd D. Millstein, and Daniel S. Weld. Automatic SATcompilation of planning problems. In: IJCAI, pp. 1169–1177 (1997)

    Google Scholar 

  103. Achlioptas, D., Gomes, C.P., Kautz, H.A., Selman, B.: Generating satisfiable problem instances. In: AAAI/IAAI, pp. 256–261 (2000)

    Google Scholar 

  104. Kautz, H., Selman, B.: Pushing the envelope: planning, propositional logic, and stochastic search. In: Proceedings of the 13th AAAI, pp. 1194–2001 (1996)

    Google Scholar 

  105. Matthew, L., Ginsberg, A.J.: Parkes, and Amitabha Roy. Supermodels and robustness. In: AAAI/IAAI, pp. 334–339 (1998)

    Google Scholar 

  106. Johnson, D.: Experimental analysis of algorithms: The good, the bad, and the ugly, Invited Lecture, AAAI 1996, Portland, OR (1996), See also http://www.research.att.com/~dsj/papers/exper.ps

  107. Gomes, C.P., Selman, B.: Problem Structure in the Presence of Perturbations. In: Proceedings of the 14 National Conference on Artificial Intelligence (AAAI 997), New Providence, RI, pp. 221–227. AAAI Press, Menlo Park (1997)

    Google Scholar 

  108. Massacci, F.: Using walk-SAT and rel-sat for cryptographic key search. In: Proc. IJCAI 1999, pp. 290–295 (1999)

    Google Scholar 

  109. Kautz, H.A., Selman, B.: Unifying SAT-based and graph-based planning. In: Proc. of the 16th International Joint Conference on Artificial Intelligence, pp. 318–325, Stockholm, Sweden (August 1999)

    Google Scholar 

  110. Clarke, E.M., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Formal Methods in System Design 19(1), 7–34 (2001)

    Article  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science & Engineering, University of Washington, Seattle, WA, 98195, USA

    Henry Kautz

  2. Department of Computer Science, Cornell University, Ithaca, NY, 14853, USA

    Bart Selman

Authors
  1. Henry Kautz
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Bart Selman
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Dipartimento di Matematica Pura ed Applicata, Università di Padova, Via Trieste 63, 35121, Padova, Italy

    Francesca Rossi

Rights and permissions

Reprints and permissions

Copyright information

© 2003 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Kautz, H., Selman, B. (2003). Ten Challenges Redux: Recent Progress in Propositional Reasoning and Search. In: Rossi, F. (eds) Principles and Practice of Constraint Programming – CP 2003. CP 2003. Lecture Notes in Computer Science, vol 2833. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45193-8_1

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-45193-8_1

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-20202-8

  • Online ISBN: 978-3-540-45193-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation