The purpose of a DIMACS Challenge is to encourage and coordinate research in the experimental analysis of algorithms. The First DIMACS Challenge encouraged experimental work in the area of network flow and matchings. This Second DIMACS Challenge, on which this volume is based, took place in conjunction with the DIMACS Special Year on Combinatorial Optimization. Addressed here are three difficult combinatorial optimization problems: finding cliques in a graph, colouring the vertices of a graph, and solving instances of the satisfiability problem. These problems were chosen both for their practical interest and because of their theoretical intractability.

The satisfiability (SAT) problem is central in mathematical logic, computing theory, and many industrial applications. There has been a strong relationship between the theory, the algorithms and the applications of the SAT problem. This book aims to bring together work by the best theorists, algorithmists, and practitioners working on the sat problem and on industrial applications, as well as to enhance the interaction between the three research groups. The book features the applications of theoretical/algorithmic results to practical problems and presents practical examples for theoretical/algorithmic study. Major topics covered in the book include practical and industial SAT problems and benchmarks, significant case studies and applications of the SAT problem and SAT algorithms, new algorithms and improved techniques for satisfiability testing, specific data structures and implementation details of the SAT algorithms, and the theoretical study of the SAT problem and SAT algorithms.

Propositional logic has been recognized throughout the centuries as one of the cornerstones of reasoning in philosophy and mathematics. Over time, its formalization into Boolean algebra was accompanied by the recognition that a wide range of combinatorial problems can be expressed as propositional satisfiability (SAT) problems. Because of this dual role, SAT developed into a mature, multi-faceted scientific discipline, and from the earliest days of computing a search was underway to discover how to solve SAT problems in an automated fashion. This book, the Handbook of Satisfiability, is the second, updated and revised edition of the book first published in 2009 under the same name. The handbook aims to capture the full breadth and depth of SAT and to bring together significant progress and advances in automated solving. Topics covered span practical and theoretical research on SAT and its applications and include search algorithms, heuristics, analysis of algorithms, hard instances, randomized formulae, problem encodings, industrial applications, solvers, simplifiers, tools, case studies and empirical results. SAT is interpreted in a broad sense, so as well as propositional satisfiability, there are chapters covering the domain of quantified Boolean formulae (QBF), constraints programming techniques (CSP) for word-level problems and their propositional encoding, and satisfiability modulo theories (SMT). An extensive bibliography completes each chapter. This second edition of the handbook will be of interest to researchers, graduate students, final-year undergraduates, and practitioners using or contributing to SAT, and will provide both an inspiration and a rich resource for their work. Edmund Clarke, 2007 ACM Turing Award Recipient: "SAT solving is a key technology for 21st century computer science." Donald Knuth, 1974 ACM Turing Award Recipient: "SAT is evidently a killer app, because it is key to the solution of so many other problems." Stephen Cook, 1982 ACM Turing Award Recipient: "The SAT problem is at the core of arguably the most fundamental question in computer science: What makes a problem hard?"

Handbook of Approximation Algorithms and Metaheuristics, Second Edition reflects the tremendous growth in the field, over the past two decades. Through contributions from leading experts, this handbook provides a comprehensive introduction to the underlying theory and methodologies, as well as the various applications of approximation algorithms and metaheuristics. Volume 1 of this two-volume set deals primarily with methodologies and traditional applications. It includes restriction, relaxation, local ratio, approximation schemes, randomization, tabu search, evolutionary computation, local search, neural networks, and other metaheuristics. It also explores multi-objective optimization, reoptimization, sensitivity analysis, and stability. Traditional applications covered include: bin packing, multi-dimensional packing, Steiner trees, traveling salesperson, scheduling, and related problems. Volume 2 focuses on the contemporary and emerging applications of methodologies to problems in combinatorial optimization, computational geometry and graphs problems, as well as in large-scale and emerging application areas. It includes approximation algorithms and heuristics for clustering, networks (sensor and wireless), communication, bioinformatics search, streams, virtual communities, and more. About the Editor Teofilo F. Gonzalez is a professor emeritus of computer science at the University of California, Santa Barbara. He completed his Ph.D. in 1975 from the University of Minnesota. He taught at the University of Oklahoma, the Pennsylvania State University, and the University of Texas at Dallas, before joining the UCSB computer science faculty in 1984. He spent sabbatical leaves at the Monterrey Institute of Technology and Higher Education and Utrecht University. He is known for his highly cited pioneering research in the hardness of approximation; for his sublinear and best possible approximation algorithm for k-tMM clustering; for introducing the open-shop scheduling problem as well as algorithms for its solution that have found applications in numerous research areas; as well as for his research on problems in the areas of job scheduling, graph algorithms, computational geometry, message communication, wire routing, etc.

This book contains a selection of papers presented at the conference on High Performance Software for Nonlinear Optimization (HPSN097) which was held in Ischia, Italy, in June 1997. The rapid progress of computer technologies, including new parallel architec tures, has stimulated a large amount of research devoted to building software environments and defining algorithms able to fully exploit this new computa tional power. In some sense, numerical analysis has to conform itself to the new tools. The impact of parallel computing in nonlinear optimization, which had a slow start at the beginning, seems now to increase at a fast rate, and it is reasonable to expect an even greater acceleration in the future. As with the first HPSNO conference, the goal of the HPSN097 conference was to supply a broad overview of the more recent developments and trends in nonlinear optimization, emphasizing the algorithmic and high performance software aspects. Bringing together new computational methodologies with theoretical ad vances and new computer technologies is an exciting challenge that involves all scientists willing to develop high performance numerical software. This book contains several important contributions from different and com plementary standpoints. Obviously, the articles in the book do not cover all the areas of the conference topic or all the most recent developments, because of the large number of new theoretical and computational ideas of the last few years.

Algorithmic graph theory has been expanding at an extremely rapid rate since the middle of the twentieth century, in parallel with the growth of computer science and the accompanying utilization of computers, where efficient algorithms have been a prime goal. This book presents material on developments on graph algorithms and related concepts that will be of value to both mathematicians and computer scientists, at a level suitable for graduate students, researchers and instructors. The fifteen expository chapters, written by acknowledged international experts on their subjects, focus on the application of algorithms to solve particular problems. All chapters were carefully edited to enhance readability and standardize the chapter structure as well as the terminology and notation. The editors provide basic background material in graph theory, and a chapter written by the book's Academic Consultant, Martin Charles Golumbic (University of Haifa, Israel), provides background material on algorithms as connected with graph theory.

The 8th International Conference on Theory and Applications of Satis?ability Testing(SAT2005)providedaninternationalforumforthemostrecentresearch on the satis?ablity problem (SAT). SAT is the classic problem of determining whether or not a propositional formula has a satisfying truth assignment. It was the ?rst problem shown by Cook to be NP-complete. Despite its seemingly specialized nature, satis?ability testing has proved to extremely useful in a wide range of di?erent disciplines, both from a practical as well as from a theoretical point of view. For example, work on SAT continues to provide insight into various fundamental problems in computation, and SAT solving technology has advanced to the point where it has become the most e?ective way of solving a number of practical problems. The SAT series of conferences are multidisciplinary conferences intended to bring together researchers from various disciplines who are interested in SAT. Topics of interest include, but are not limited to: proof systems and proof c- plexity; search algorithms and heuristics; analysis of algorithms; theories beyond the propositional; hard instances and random formulae; problem encodings; - dustrial applications; solvers and other tools. This volume contains the papers accepted for presentation at SAT 2005. The conference attracted a record number of 73 submissions. Of these, 26 papers were accepted for presentation in the technical programme. In addition, 16 - pers were accepted as shorter papers and were presented as posters during the technicalprogramme.Theacceptedpapersandposterpaperscoverthefullrange of topics listed in the call for papers.