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.

For further information, please visit the Pragmatics of SAT workshop website.

Workshop Date: July 4, 2023

Counting and Sampling

The International Workshop on Counting and Sampling aims to provide a venue for researchers working on model counting such as model counting (mc), weighted model counting/sum of products (wmc), projected model counting (pmc) as well as sampling models within the realm but not restricting to Boolean satisfiability (SAT), satisfiability modulo theories (SMT), Answer set programming (ASP), and constraint programming (CP). It encourages to meet, communicate, and discuss the latest theoretical and practical results, in particular results on novel solvers, related solver technologies, new theoretical advances, practical academic and industrial applications as well as the linking theory and practice. The workshop is also the place for developers of model counters to present their solvers and the presentation of detailed results on the model counting competition.

For further information, please visit the Counting and Sampling workshop website.

Workshop Date: July 4, 2023

Quantified Boolean Formulas and Beyond

The goal of the International Workshop on Quantified Boolean Formulas and Beyond (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. The workshop also welcomes work on reasoning with quantifiers in related problems, such as dependency QBF (DQBF), quantified constraint satisfaction problems (QCSP), and satisfiability modulo theories (SMT) with quantifiers.

For further information, please visit the QBF workshop website.

Workshop Date: July 4, 2023

OptiLog Tutorial

OptiLog is a Python framework for the rapid prototyping of SAT-based systems. OptiLog includes functionality for loading and creating formulas, dynamic loading of incremental SAT solvers with support for external libraries, modules for modelling problems into Non-CNF format with support for Pseudo Boolean constraints, for tuning, evaluating and parsing the results of applications. All these enhancements allow OptiLog to become a swiss knife for SAT-based applications in academic and industrial environments. During this talk, we will glimpse what we can do with OptiLog and see some use cases.

Tutorial Date: 16:00, July 4, 2023