Preface: Volume 9

Great strides have been made in recent years in the theory and practice of propositional satisfiability testing. On the theoretical side, a wide range of mathematical approaches - ranging from classical combinatorial analysis to arguments based on statistical physics - have increased our understanding of problem hardness. On the practical side, new systematic and non-systematic search algorithms have increased the size of problems that can be solved by several orders of magnitude. As a result there is an growing interest in using SAT as a practical tool for solving real-world problems, as well as using the insights gained from SAT research to create problem-specific solutions. CS 2001 Workshop on Theory and Applications of Satisfiability Testing brought together researchers from different communities - including theory, artificial intelligence, verification, mathematical theorem-proving, and operations research - in order to share ideas and increase synergy between theoretical and empirical work. rkshop was held in conjunction with the Sixteenth Annual IEEE Symposium on Logic in Computer Science. The workshop took place June 14-15, 2001, at Boston University. d speakers at the workshop were Alasdair Urquhart, Daniel Jackson, and Michael Littman. In addition 33 papers and posters were presented. itors thank the efforts of the program committee: ranco (University of Cincinnati) eame (University of Washington) tickel (SRI) alsh (York University) McAllester (AT&T Laboratories) Jackson (M.I.T.) w Ginsberg (University of Oregon) Gomes (Cornell University). o give special thanks to the LICS 2001 organizers, including Joseph Halpern (Program Chair), Harry Mairson (Conference Chair), and Leonid Libkin (Workshop Chair).