Preface: The Beyond NP Workshop

A new computational paradigm has emerged in computer both Renault and Toyota have deployed online configuration science over the past few decades, which is exemplified by systems based on knowledge compilation). QBF solvers the use of SAT solvers to tackle problems in the complexity have been used in model checking, verification, debugging, class NP. Finally, function problem solvers have and engineering investment is made towards developing been used in model-based diagnosis, design debugging, highly efficient solvers for a prototypical problem CAD and bioinformatics. The cost of this investment is then on a variety of topics, including algorithms; descriptions amortized as these solvers are applied to a broader class of of implementations and/or evaluations of beyond NP problems via reductions (in contrast to developing dedicated solvers; their applications (including encodings); the complexity algorithms for each encountered problem). SAT solvers, classes they reach; and their connections to one for example, are now routinely used to solve problems in another.