- Submission Deadline: October 23, 2015
- Notification: November 23, 2015
- Workshop Dates: February 12-13, 2016
- Fahiem Bacchus (University of Toronto), On MaxSAT
- Stefano Ermon (Stanford University), On Model Counting
- Mikolas Janota (MSR Cambridge), On QBFs
- George Katsirelos (INRA), On MUSes and MCSes (tentative)
- Guy Van den Broeck (UCLA), On First-Order Knowledge Compilation
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).
The goal of this workshop is to help unify and promote research areas that advance this emerging computational paradigm, focusing on solvers that reach beyond NP. This includes, but is not limited to:
- Model counters, also known as #SAT solvers, which are now established as the prototypical solvers for the complexity class #P.
- Knowledge compilers, which reach to other problems in the polynomial and counting hierarchies.
- QBF solvers, which are now established as the prototypical solvers for the complexity class PSPACE.
- Solvers for function problems, including optimization and subset minimal problems, e.g. MaxSAT, MUS and MCS, that reach different levels of the function polynomial hierarchy.
TOPICS OF INTEREST
Algorithms underlying Beyond NP solvers; descriptions of implementations and/or evaluations of these solvers; their applications (including encodings); the complexity classes they reach; and their connections to one another. More broadly, submissions are solicited from three types of community members: those who develop solvers, those who use them to solve concrete problems, and those who are interested in the computational complexity of solvers and related problems. Submissions that can help disseminate “best practices” among the relevant research areas are also encouraged (e.g., competitions, benchmarks, and the development of open-source solvers).
Submissions should be formatted using the AAAI conference style and not exceed 6 pages (shorter submissions are welcome). Submissions should be made through EasyChair and are expected to explicate relevance to one of the Beyond NP themes (see http://beyondnp.org/workshop16/).
- Adnan Darwiche (University of California, Los Angeles, USA)
- Joao Marques-Silva (INESC-ID, IST, University of Lisbon, Portugal)
- Pierre Marquis (CRIL-CNRS/Université d’Artois, France)
- Fahiem Bacchus (University of Toronto, Canada)
- Supratik Chakraborty (IIT Mumbai, India)
- Stefano Ermon (Stanford University, USA)
- Marijn Heule (University of Texas, Austin, USA)
- Mikolas Janota (MSR Cambridge, UK)
- Matti Jarvisalo (University of Helsinki, Finland)
- Rupak Majumdar (Max-Planck Institute, Germany)
- Nina Narodytska (Samsung Research America, USA)
- Jakob Nordstrom (KTH Royal Institute of Technology, Sweden)
- Bart Selman (Cornell University, USA)
- Laurent Simon (University of Bordeaux, France)
- Dan Suciu (University of Washington, USA)
- Stefan Szeider (Technical University of Vienna, Austria)
- Guy Van den Broeck (UCLA, USA)
- Toby Walsh (NICTA, Australia)