Determining the satisfiability of first-order formulas modulo background theories, known as the Satisfiability Modulo Theories (SMT) problem, has proved to be an enabling technology for verification, synthesis, test generation, compiler optimization, scheduling, and other areas. The success of SMT techniques depends on the development of both domain-specific decision procedures for each background theory (e.g., linear arithmetic, the theory of arrays, or the theory of bit-vectors) and combination methods that allow one to obtain more versatile SMT tools, usually leveraging Boolean satisfiability (SAT) solvers. These ingredients together make SMT techniques well-suited for use in larger automated reasoning and verification efforts. The aim of the workshop is to bring together researchers and users of SMT tools and techniques.
Organisers: Jochen Hoenicke and Sophie Tourret
The ExCoS workshop offers a platform for discussing recent advances and exploring future research directions in the intersection of constraint solving and explainability. This includes developing techniques for explaining solver outcomes (e.g. unsatisfiability, optimality), ways of making the constraint solving process more explainable, as well as ways of using constraint solvers to compute explanations in various application settings, such as in machine learning and planning.
Organisers: Bart Bogaerts, Tias Guns, Matti Jarvisalo, and Jussi Rintanen
Learning and reasoning have been the two foundational pillars of AI since its inception, yet it is only in the past decade that interactions between these fields have become increasingly prominent. In particular, machine learning (ML) has had a substantial impact on SAT/SMT and CP solvers, as well as automated theorem provers. Recent advances have demonstrated the power of ML to inform solver heuristics, guide proof search, and optimize algorithm portfolios. Despite growing interest in this direction, work on ML for solvers and provers is often scattered across multiple research communities — SAT, SMT, CP, theorem proving, formal methods, and machine learning - with few opportunities for focused interaction. This workshop aims to bring together researchers and practitioners working at the intersection of machine learning and formal reasoning systems. It provides a forum for the presentation of recent work, the exchange of ideas, and the fostering of collaboration between these communities.
Organisers: Vijay Ganesh and Stefan Szeier
Since the seminal work on Partial Max-CSP by Freuder in 1992, research on soft constraints has grown in several directions in the Constraint Programming and related fields, including Max-SAT, Max-SMT, Markov Random Fields, and Pseudo-Boolean optimization. A common research topic is discrete optimization with a nonlinear objective function and symbolic domains. The goal of this workshop is to present current work done in this domain, to encourage discussions between researchers from different fields, and to attract new researchers willing to contribute or just discover the domain.
Organisers: George Katsirelos and Carlos Ansotegui
Recent advancements in Large Language Models (LLMs) have opened exciting new possibilities for many domains, thanks to their powerful natural language processing capabilities. However, they struggle with consistency, logical reasoning, and guaranteeing correctness. In contrast, constraint solvers offer precise, explainable, and optimal solutions but require structured problem formulations and expert knowledge. Recent research has explored leveraging LLMs as modeling assistants to automate constraint formulation, while constraint solvers have been employed to enhance LLM control, verification, and structured reasoning. The LLM-Solve workshop brings together researchers at this emerging intersection, fostering discussions on hybrid approaches, neuro-symbolic methods, solver-guided reasoning, and LLM assisted modeling. This workshop aims to cultivate advances in LLM-powered constraint solving and constraint-driven LLMs.
Organisers: Tias Guns, Serdar Kadioglu, Stefan Szeier, and Dimos Tsouros
The importance of modelling and model reformulation is widely recognised in many domains, such as for CP, MIP, SAT, SMT and other kinds of general-purpose solvers. There has been significant research effort in recent years into modelling and model reformulation, such as automating techniques used by expert modellers, and developing tools and techniques to target multiple types of solvers from one model. The purpose of ModRef is to be a forum for all kinds of work in modelling, including new models or new modelling ideas for any amenable problem (whether a new application or a classic benchmark), reformulation techniques to improve the performance of models when solved by general-purpose solvers, and automated modelling techniques, tools, and languages. We solicit original papers that contribute to the understanding of modelling or model reformulation.
Organisers: Ian Gent and Andreina Francisco
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.
Organisers: Mikoláš Janota and Aina Niemetz
The International Workshop on Counting, Sampling, and Synthesis is an event for researchers in model counting, sampling, and automated synthesis. It covers advanced topics such as weighted and projected counters/samplers in various domains, including SAT, SMT, ASP, and CP. The workshop has expanded its focus to include the role of model counters, samplers, and solvers in the area of automated synthesis. The goal of the workshop to facilitate the exchange of cutting-edge theoretical and practical insights, focusing on innovative solver technologies and their real-world applications. Additionally, the workshop allows developers of model counters to showcase their work and share detailed competition results, encouraging discussions that bridge theory and practice.
Organisers: Paulius Dilkas and Priyanka Golia
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 and extensions like DQBF. 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.
Organisers: Hubie Chen, Leroy Chew, Friedrich Slivovsky, and Martina Seidl
Over twenty years ago the paper “In Pursuit of the Holy Grail” proposed that Constraint Programming was well-positioned to pursue the Holy Grail of Computer Science: the user simply states the problem and the computer solves it. This workshop, the eighth in a series, is intended to encourage and showcase progress in that pursuit, in particular regarding the automation of problem acquisition, model reformulation, solver construction, user explanation.
Organiser: Lars Kotthoff