Pragmatics of SAT
- Organizers: Katalin Fazekas, Alexey Ignatiev
- Webpage: http://www.pragmaticsofssat.org/2024/
- Description:
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.
International Workshop on Quantified Boolean Formulas and Beyond (QBF Workshop)
- Organizers: Hubie Chen, Friedrich Slivovsky, Martina Seidl
- Webpage: https://qbf24.pages.sai.jku.at/qbf/
- Description:
Quantified Boolean formulas (QBF) are an extension of propositional logic which allows for explicit quantification over propositional variables. The decision problem of QBF is PSPACE-complete compared to NP-completeness of the decision problem of propositional logic (SAT).
Many problems from application domains such as model checking, formal verification or synthesis are PSPACE-complete, and hence could be encoded in QBF. Considerable progress has been made in QBF solving throughout the past years. However, in contrast to SAT, QBF is not widely applied to practical problems in industrial settings. For example, the extraction and validation of models of (un)satisfiability of QBFs and has turned out to be challenging.
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.
Workshop on Counting, Sampling, and Synthesis
- Organizers: Paulius Dilkas, Priyanka Golia
- Webpage: https://mccompetition.org
- Description:
The Workshop on Counting, Sampling, and Synthesis is an event for researchers in model counting and sampling. It covers advanced topics such as weighted and projected counters/samplers and various domains such as SAT, SMT, ASP, and CP. This year, the workshop has expanded its focus to include the role of model counters, samplers, and solvers in automated synthesis. The goal of the workshop is to facilitate the exchange of cutting-edge theoretical and practical insights, with a particular emphasis on innovative solver technologies and their real-world applications. Additionally, the workshop provides an opportunity for developers of model counters to showcase their work and share detailed competition results, to encourage discussions that bridge theory and practice.
Indian SAT+SMT School [9th Edition]
- Organizers: Supratik Chakraborty, Priyanka Golia, Ashutosh Gupta, Saurabh Joshi,
Kumar Madhukar, Kuldeep S. Meel
- Webpage: https://sat-smt.in/
- Description:
SAT and SMT solvers are the backbone of a wide range of academic and industrial R&D activities today. These include software and hardware verification, logistics, planning, operations research, non-linear discrete optimization, model counting, machine learning, etc. Recent developments in the field suggest that these solvers may soon be leveraged in an even wider range of applications that touch almost all aspects of computing. Unfortunately, in India, the technical study of these solvers is limited to a few individuals/groups. This has hampered the growth of research and development in this area, both in the Indian academia and in the Indian industry. We organize the Indian SAT+SMT school every year in view of this gap. Each edition of the school typically includes a quick introduction to this topic, followed by tutorials on SAT+SMT solvers by eminent scientists and developers from around the world, and latest research and applications centered around these solvers.