Stochastic Boolean Satisfiability

• Achlioptas, D.: Threshold phenomena in random graph colouring and satisfiability, Ph.D. Dissertation, University of Toronto, 1999.

• Bayardo, Jr., R. J. and Schrag, R. C.: Using CSP look-back techniques to solve real-world SAT instances, in Proceedings of the Fourteenth National Conference on Artificial Intelligence, AAAI Press/The MIT Press, 1997, pp. 203–208.

• Beame, P. and Pitassi, T.: Simplified and improved resolution lower bounds, in 37th Annual Symposium on Foundations of Computer Science, IEEE, 1996, pp. 274–282.

• Beame, P., Karp, R., Pitassi, T. and Saks,M.: On the complexity of unsatisfiability of random k-CNF formulas, in Proceedings of the Thirtieth Annual ACM Symposium on Theory of Computing, 1998, pp. 561–571.

• Ben-Sasson, E. andWigderson, A.: Short proofs are narrow: Resolution made simple, in STOC 1999, 1999, pp. 517–526.

• Birnbaum, E. and Lozinskii, E. L.: The good old Davis-Putnam procedure helps counting models, J. Artificial Intelligence Res. 10 (1999), 457–477.

  Google Scholar 

• Cadoli, M., Giovanardi, A. and Schaerf, M.: Experimental analysis of the computational cost of evaluating quantified Boolean formulae, in Fifth Conference of the Italian Association for Artificial Intelligence (AI*IA'97), number 1321, Springer-Verlag, 1997, pp. 207–218.

• Cadoli, M., Giovanardi, A. and Schaerf, M.: An algorithm to evaluate quantified Boolean formulae, in Proceedings of the Fifteenth National Conference on Artificial Intelligence (AAAI-98), AAAI Press/The MIT Press, 1998, pp. 262–267.

• Chvátal, V. and Reed, B.: Mick gets some (the odds are on his side), in 33nd Annual Symposium on Foundations of Computer Science, 1992, pp. 620–627.

• Clegg, M., Edmonds, J. and Impagliazzo, R.: Using the Gröbner basis algorithm to find proofs of unsatisfiability, in Proceedings of the Twenty-Eighth Annual ACM Symposium on Theory of Computing, 1996, pp. 174–183.

• Condon, A., Feigenbaum, J., Lund, C. and Shor, P.: Random debators and the hardness of approximating stochastic functions, SIAM J. Comput. 26(2) (1997), 369–400.

  Google Scholar 

• Condon, A.: The complexity of stochastic games, Inform. and Comput. 96(2) (1992), 203–224.

  Google Scholar 

• Crawford, J. M. and Auton, L. D.: Experimental results in the crossover point in random 3SAT, Artificial Intelligence 81(1–2) (1996), 31–57.

  Google Scholar 

• Davis, M., Logemann, G. and Loveland, D.: A machine program for theorem proving, Comm. ACM 5 (1962), 394–397.

  Google Scholar 

• Dechter, R.: Bucket elimination: A unifying framework for probabilistic inference, in Proceedings of the 12th Conference on Uncertainty in Artificial Intelligence (UAI-96), Morgan Kaufmann, 1996, pp. 211–219.

• Freeman, J. W.: Improvements to propositional satisfiability search algorithms, Ph.D. Dissertation, Department of Computer and Information Science, University of Pennsylvania, 1995.

• Friedgut, E.: Necessary and sufficient conditions for sharp thresholds of graph properties, and the k-SAT problem, Preprint, 1997.

• Frieze, A. and Suen, S.: Analysis of two simple heuristics on a random instance of k-SAT, J. Algorithms 20(2) (1996), 312–355.

  Google Scholar 

• Gallo, G. and Urbani, G.: Algorithms for testing the satisfiability of propositional formulae, J. Logic Programming 7 (1989), 45–61.

  Google Scholar 

• Gent, I. and Walsh, T.: Beyond NP: The QSAT phase transition, Technical Report APES–05–1998, 1998.

• Goerdt, A.: A threshold for unsatisfiability, J. Comput. System Sci. 53 (1996), 469–486.

  Google Scholar 

• Gu, J., Purdom, P. W., Franco, J. and Wah, B. J.: Algorithms for the satisfiability (SAT) problem: A survey, in Satisfiability (SAT) Problem, DIMACS, Amer. Math. Soc., 1997, pp. 19–151.

• Harche, F., Hooker, J. N. and Thompson, G.: A computational study of satisfiability algorithms for propositional logic, ORSA J. Comput. 6 (1994), 423–435.

  Google Scholar 

• Hooker, J. N. and Vinay, V.: Branching rules for satisfiability, Technical Report GSIAWorking Paper 1994–09, Carnegie Mellon University, 1994. Revised January 1995.

• Jeroslow, R. and Wang, J.: Solving propositional satisfiability problems, Ann. Math. Artificial Intelligence 1 (1990), 167–187.

  Google Scholar 

• Kamath, A., Motwani, R., Palem, K. and Spirakis, P.: Tail bounds for occupancy and the satisfiability threshold conjecture, Random Structures Algorithms 7(1) (1995), 59–80.

  Google Scholar 

• Kautz, H. and Selman, B.: Pushing the envelope: Planning, propositional logic, and stochastic search, in Proceedings of the Thirteenth National Conference on Artificial Intelligence, AAAI Press/The MIT Press, 1996, pp. 1194–1201.

• Kearns, M., Mansour, Y. and Ng, A. Y.: A sparse sampling algorithm for near-optimal planning in large Markov decision processes, in Proceedings of the Sixteenth International Joint Conference of Artificial Intelligence (IJCAI-99), 1999.

• Kirousis, L. M., Kranakis, E., Krizanc, D. and Stamatiou, Y. C.: Approximating the unsatisfiability threshold of random formulas, Random Structures Algorithms 12(3) (1998), 253–269.

  Google Scholar 

• Li, C. M. and Anbulagan: Heuristics based on unit propagation for satisfiability problems, in Proceedings of the Fifteenth International Joint Conference on Artificial Intelligence, 1997, pp. 366–371.

• Littman, M. L., Goldsmith, J. and Mundhenk, M.: The computational complexity of probabilistic plan existence and evaluation, J. Artificial Intelligence Res. 9 (1998), 1–36.

  Google Scholar 

• Littman,M. L.: Probabilistic propositional planning: Representations and complexity, in Proceedings of the Fourteenth National Conference on Artificial Intelligence, AAAI Press/The MIT Press, 1997, pp. 748–754.

• Lusena, C., Goldsmith, J. and Mundhenk, M.: Nonapproximability results for partially observable Markov decision processes, Journal of Artificial Intelligence Research 14 (2001), 83–113.

  Google Scholar 

• Majercik, S. M. and Littman, M. L.: MAXPLAN: A new approach to probabilistic planning, in R. Simmons, M. Veloso and S. Smith (eds), Proceedings of the Fourth International Conference on Artificial Intelligence Planning, AAAI Press, 1998, pp. 86–93.

• Majercik, S. M. and Littman, M. L.: Contingent planning under uncertainty via probabilistic satisfiability, in Proceedings of the Sixteenth National Conference on Artificial Intelligence, AAAI Press, 1999, pp. 549–556.

• Monien, B. and Speckenmeyer, E.: Solving satisfiability in less than 2ⁿ steps, Discrete Appl. Math. 10 (1985), 287–295.

  Google Scholar 

• Mundhenk, M., Goldsmith, J., Lusena, C. and Allender, E.: Complexity of finite-horizon Markov decision process problems, Journal of the ACM 47 (2000), 681–720.

  Google Scholar 

• Papadimitriou, C. H. and Tsitsiklis, J. N.: The complexity of Markov decision processes, Math. Oper. Res. 12(3) (1987), 441–450.

  Google Scholar 

• Papadimitriou, C. H.: Games against nature, J. Comput. Systems Sci. 31 (1985), 288–301.

  Google Scholar 

• Paturi, R., Pudlak, P., Saks, M. and Zane, F.: An improved exponential time algorithm for k-SAT, in FOCS, 1998, pp. 628–637.

• Paturi, R., Pudlak, P. and Zane, F.: Satisfiability coding lemma, in FOCS, 1997, pp. 566–574.

• Peot, M.: Personal communication, 1998.

• Roth, D.: On the hardness of approximate reasoning, Artificial Intelligence 82(1–2) (1996), 273–302.

  Google Scholar 

• Selman, B., Kautz, H. and Cohen, B.: Local search strategies for satisfiability testing, in D. S. Johnson and M. A. Trick (eds), Cliques, Coloring, and Satisfiability, DIMACS Series in Discrete Math. and Theoret. Comput. Sci. 26, Amer. Math. Soc., 1996, pp. 521–531.

• Selman, B., Mitchell, D. and Levesque, H.: Generating hard satisfiability problems, Artificial Intelligence 81 (1996), 17–29.

  Google Scholar 

• Shachter, R. D.: Evaluating influence diagrams, Oper. Res. 34(6) (1986), 871–882.

  Google Scholar 

• Umans, C.: Personal communication, 1999.

Download references