Schedule (slides from invited talks available)
Accepted Papers

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)
10:30a-11:00a   Coffee break
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)
12:30p-02:00p   Lunch break
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)

Accepted Papers

  1. Bernhard Bliem, Günther Charwat, Markus Hecher and Stefan Woltran
    Subset Minimization in Dynamic Programming on Tree Decompositions
  2. Batya Kenig and Avigdor Gal
    Exploiting the Hidden Structure of Junction Trees for MPE
  3. Junkyu Lee, Radu Marinescu, Rina Dechter and Alexander Ihler
    From Exact to Anytime Solutions for Marginal Map
  4. Timothy Kopp, Parag Singla and Henry Kautz
    Toward Caching Symmetrical Subtheories for Weighted Model Counting
  5. 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
  6. Seyed Mehran Kazemi and David Poole
    Lazy Arithmetic Circuits
  7. 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.
  8. Vaishak Belle
    Satisfiability and Model Counting in Open Universes
  9. Jonas Vlasselaer, Angelika Kimmig, Anton Dries, Wannes Meert and Luc De Raedt
    Knowledge Compilation and Weighted Model Counting for Inference in Probabilistic Logic Programs
  10. Eric Gribkoff and Dan Suciu
    SlimShot: Probabilistic Inference for Web-Scale Knowledge Bases
  11. Dan Olteanu
    Factorized Databases: A Knowledge Compilation Perspective
  12. Valeriy Balabanov, Jie-Hong Roland Jiang, Alan Mishchenko and Christoph Scholl
    Clauses versus gates in CEGAR-based 2QBF solving
  13. Olaf Beyersdorff, Leroy Chew and Mikolas Janota
    Extension Variables in QBF Resolution
  14. Bart Bogaerts, Tomi Janhunen and Shahab Tasharrofi
    Solving QBF With Nested SAT Solvers
  15. Charles Jordan, William Klieber and Martina Seidl
    Non-CNF QBF Solving with QCIR

Invited Speakers

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

Organizing Committee

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)

Program Committee

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.

Important Dates

Submission Deadline: October 23, 2015
  November 6, 2015 (extended)
Notification: November 23, 2015
Workshop Date: February 12, 2016