Workshops

Pragmatics of SAT

The aim of the Pragmatics of SAT (PoS) workshop series is to provide a venue for researchers working on designing and/or applying Boolean satisfiability (SAT) solvers and related solver technologies, including but not restricting to satisfiability modulo theories (SMT), Answer set programming (ASP), and constraint programming (CP) as well as their optimization counterparts, to meet, communicate, and discuss latest results. This workshop allows researchers to share both fundamental theoretical insights into practical solvers, as well as new implementation-level insights and ‘gory’ technical details about their systems that may at times be difficult to publish in the main conferences on the declarative solving paradigms.

Organizers:

Deadlines:

  • April 8, 2018 (abstract)
  • April 15, 2018 (paper)

> Webpage

Quantified Boolean Formulas and Beyond

The goal of the International Workshop on Quantified Boolean Formulas (QBF Workshop) is to bring together researchers working on theoretical and practical aspects of QBF solving. In addition to that, it addresses (potential) users of QBF in order to reflect on the state-of-the-art and to consolidate on immediate and long-term research challenges. In particular, the following topics shall be considered at the workshop: 1) Directions of Solver Development 2) Certificates 3) Applications, and 4) Community platform and repository.

Organizers:

> Webpage

Proof Complexity

Proof complexity focuses on the complexity of theorem proving procedures. The central question in proof complexity is: given a theorem F (e.g., a propositional tautology) and a proof system P (i.e., a formalism usually comprised of axioms and rules), what is the size of the smallest proof of F in the system P? Moreover, how difficult is it to construct a small proof? Many ingenious techniques have been developed to try to answer these questions; and they bare tight relations to intricate theoretical questions from computational complexity (such as the celebrated P vs. NP problem), first-order arithmetic theories (e.g. separating theories of bounded arithmetic) as well as to practical problems in SAT solving.

Organizers:

Deadlines:

  • April 15, 2018 (abstract)

> Webpage