Mission Statement

A new computational paradigm has emerged in computer science over the past few decades, which is exemplified by the use of SAT solvers to tackle problems in the complexity class NP. According to this paradigm, a significant research and engineering investment is made towards developing highly efficient solvers for a prototypical problem (e.g., SAT), that is representative of a broader class of problems (e.g., NP). The cost of this investment is then amortized as these solvers are applied to a broader class of problems via reductions (in contrast to developing dedicated algorithms for each encountered problem). SAT solvers, for example, are now routinely used to solve problems in many domains, including diagnosis, planning, software and hardware verification.

BeyondNP.org is a community website that aims to disseminate and promote research that advances this emerging computational paradigm, focusing on solvers that reach beyond NP. This includes:

  1. Model counters, also known as #SAT solvers, which are now established as the prototypical solvers for the complexity class #P.

  2. Knowledge compilers, which reach further to other problems in the polynomial and counting hierarchies.

  3. QBF solvers, which are now established as the prototypical solvers for the complexity class PSPACE.

  4. Solvers for function problems, including optimization and subset minimal problems, e.g. MaxSAT, MUS and MCS, for different levels of the function polynomial hierarchy.

These solvers are increasingly used to effectively tackle a broad class of problems. For example, model counters and knowledge compilers are now the basis of state-of-the-art approaches for probabilistic reasoning, which arise in probabilistic graphical models, probabilistic programming and probabilistic databases. Knowledge compilers have been influential in online configuration systems (both Toyota and Renault have deployed online configuration systems based on knowledge compilation). QBF solvers have been used in model checking, verification, debugging, and testing. Finally, function problem solvers have been used in model-based diagnosis, design debugging, CAD and bioinformatics. 

BeyondNP.org will serve as a news and information aggregator for research on developing solvers that reach beyond NP, including a catalog of open-source solvers, repositories of corresponding benchmarks, and news on related academic activities.