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.
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.
These solvers are increasingly used to effectively tackle a broad class of problems (e.g., probabilistic graphical models, programming and databases; online configuration systems; verification, debugging, and testing).
Topics of interest to the workshop include algorithms; descriptions of implementations and/or evaluations of beyond NP 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).
The format of the workshop will include presentations, posters and potentially panels.
Friday, February 12
|09:00a-09:15a||Welcome and introduction|
|09:15a-09:45a||Invited talk by Fahiem Bacchus: On MaxSAT|
|09:45a-10:15a||Invited talk by George Katsirelos: On MUSes and MCSes|
|10:15a-10:30a||Poster spotlights (1,2,3)|
|11:00a-11:30a||Invited talk by Stefano Ermon: On Model Counting|
|11:30a-12:00p||Invited talk by Guy Van den Broeck: On First-Order Knowledge Compilation|
|12:00p-12:30p||Poster spotlights (4,5,6,7,8,9)|
|02:00p-02:30p||Invited talk by Malte Helmert: On Planners as Beyond NP Solvers|
|02:30p-03:00p||Invited talk by Mikolas Janota: On QBFs|
|03:00p-03:30p||Poster spotlights (10,11,12,13,14,15)|
|03:30p-03:45p||Concluding remarks and discussion|
|03:45p-05:30p||Poster session (with coffee)|
- Bernhard Bliem, Günther Charwat, Markus Hecher and Stefan Woltran
Subset Minimization in Dynamic Programming on Tree Decompositions
- Batya Kenig and Avigdor Gal
Exploiting the Hidden Structure of Junction Trees for MPE
- Junkyu Lee, Radu Marinescu, Rina Dechter and Alexander Ihler
From Exact to Anytime Solutions for Marginal Map
- Timothy Kopp, Parag Singla and Henry Kautz
Toward Caching Symmetrical Subtheories for Weighted Model Counting
- Kuldeep S. Meel, Moshe Vardi, Supratik Chakraborty, Daniel J. Fremont, Sanjit A. Seshia, Dror Fried, Alexander Ivrii and Sharad Malik
Constrained Sampling and Counting: Universal Hashing meets SAT Solving
- Seyed Mehran Kazemi and David Poole
Lazy Arithmetic Circuits
- Christian Muise, Sheila McIlraith, Chris Beck and Eric Hsu
DSHARP: Fast d-DNNF Compilation with sharpSAT (Amended Version)
See the addendum to the original paper.
- Vaishak Belle
Satisfiability and Model Counting in Open Universes
- Jonas Vlasselaer, Angelika Kimmig, Anton Dries, Wannes Meert and Luc De Raedt
Knowledge Compilation and Weighted Model Counting for Inference in Probabilistic Logic Programs
- Eric Gribkoff and Dan Suciu
SlimShot: Probabilistic Inference for Web-Scale Knowledge Bases
- Dan Olteanu
Factorized Databases: A Knowledge Compilation Perspective
- Valeriy Balabanov, Jie-Hong Roland Jiang, Alan Mishchenko and Christoph Scholl
Clauses versus gates in CEGAR-based 2QBF solving
- Olaf Beyersdorff, Leroy Chew and Mikolas Janota
Extension Variables in QBF Resolution
- Bart Bogaerts, Tomi Janhunen and Shahab Tasharrofi
Solving QBF With Nested SAT Solvers
- Charles Jordan, William Klieber and Martina Seidl
Non-CNF QBF Solving with QCIR
|Fahiem Bacchus (University of Toronto, Canada)||On MaxSAT|
|Stefano Ermon (Stanford University, USA)||On Model Counting|
|Malte Helmert (University of Basel, Switzerland)||On Planners as Beyond NP Solvers|
|Mikolas Janota (MSR Cambridge, UK)||On QBFs|
|George Katsirelos (INRA, France)||On MUSes and MCSes|
|Guy Van den Broeck (UCLA, USA)||On First-Order Knowledge Compilation|
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)
The Workshop on Beyond NP was held in conjunction with the Thirtieth AAAI Conference on Artificial Intelligence (AAAI-16), in Phoenix, Arizona, USA. The workshop was held on Friday, February 12, 2016, at the Phoenix Convention Center.
|November 6, 2015 (extended)|
|Notification:||November 23, 2015|
|Workshop Date:||February 12, 2016|