| 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:
> 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:
Deadlines:
> 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:
> Webpage |
|
| Cross-Fertilization Between CSP and SAT
Constraint Satisfaction Problems (CSP) and Boolean Satisfiability Problems (SAT) have much in common. However, they also differ in many important aspects, leading to major differences in solution techniques. More importantly, the CSP and SAT communities, while to some extent interacting with each other, are mostly separate communities with separate conferences and meetings. This workshop is designed as a venue for bridging the gap and for cross-fertilization between the two communities, in terms of ideas, problems, techniques, and results. |
Organizers:
Deadlines:
> Webpage |