On these pages we will collect information on affiliated events, including colocated conferences, workshops, competitions and the doctoral program. This page will be regularly updated with more information.

Colocated Conferences

SAT 2025 will colocate with:

Summer School

The SAT/SMT/AR summer school aims to bring a select group of students up to speed quickly in this exciting research area. The school continues the successful line of Summer Schools that ran from 2011 to 2024. The 2025 summer school will take place August 6 - 8 in St. Andrews

Dates: August 6 - 8 (in St. Andrews)
Organizers: Joan Espasa Arxer, Ian Gent, and Ruth Hoffmann
Webpage: https://sat-smt-ar-school.gitlab.io/www/2025/

Doctoral Program

The Joint CP/SAT Doctoral Programme (DP) is open to all research students, including past participants, who are conducting research related to constraint programming and satisfiability. The goal is to provide an informal environment for networking, presenting and discussing ongoing work, and receiving feedback from both fellow research students and experts in the field. Participation requires a paper submission to the DP, reviewing other submissions to the DP and attendance in person.

Dates: August 10 - 11
Organizers: Katalin Fazekas, and Mun See Chang
Webpage: https://satcpdp25.github.io/

Workshops

23rd International Workshop on Satisfiability Modulo Theories (SMT)

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.

Dates: August 10 - 11
Program Chairs: Sophie Tourret, and Jochen Hoenicke
Webpage: https://smt-workshop.cs.uiowa.edu/2025/index.shtml

Explanations with Constraints and Satisfiability

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.

Dates: August 10
Organisers: Bart Bogaerts, Tias Guns, Matti Järvisalo, and Jussi Rintanen
Webpage: https://sites.google.com/view/excos2025

Machine Learning for Solvers and Provers

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.

Dates: August 10
Organisers: Vijay Ganesh and Stefan Szeider
Webpage: https://ml4sp.github.io/

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.

Dates: August 11
Organizers: Mikoláš Janota, and Aina Niemetz
Webpage: https://www.pragmaticsofssat.org/2025/

LLMs meet Constraint Solving

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.

Dates: August 11
Organisers: Tias Guns, Serdar Kadioglu, Stefan Szeider, and Dimos Tsouros
Webpage: https://sites.google.com/view/llm-solve

Constraint Modelling and Reformulation

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.

Dates: August 11
Organisers: Ian Gent and Andreina Francisco
Webpage: https://modref.github.io/ModRef2025.html

Model Counting, Sampling and Synthesis

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.

Dates: August 11
Organisers: Paulius Dilkas and Priyanka Golia
Webpage: https://mccompetition.org/2025/mcw_description

Quantified Boolean Formulas and Beyond

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.

Dates: August 11 (morning only)
Organisers: Hubie Chen, Leroy Chew, Friedrich Slivovsky, and Martina Seidl
Webpage: https://qbf.pages.sai.jku.at/qbf25/

Progress Towards the Holy Grail

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.

Dates: August 11 (afternoon only)
Organiser: Lars Kotthoff
Webpage: https://freuder.wordpress.com/progress-towards-the-holy-grail-workshops/pthg-25/

Competitions

The SAT Competition

SAT Competition 2025 is a competitive event for solvers of the Boolean Satisfiability (SAT) problem. To keep up the driving force in improving SAT solvers, we want to motivate implementers to present their work to a broader audience and to compare it with that of others. Researchers from both academia and industry are invited to submit their solvers and benchmarks.

Organizers: Cayden Codel, Katalin Fazekas, Marijn Heule, Markus Iser
Webpage: https://satcompetition.github.io/2025/

The Pseudo-Boolean Competition

The goal of the Pseudo-Boolean Competition is to assess the state of the art in the field of pseudo-Boolean solvers, in the same spirit as the previous competitions and evaluations. This edition will be quite similar to the reboot of the Pseudo-Boolean Competition series in 2024, but we will use the opportunity to make some minor revisions of the set-up.

Organizers: Olivier Roussel
Webpage: https://www.cril.univ-artois.fr/PB25/

The Model Counting Competition

The 6th Competition on Model Counting (MC 2025) is a competition to deepen the relationship between latest theoretical and practical development on the various model counting problems and their practical applications. It targets the problem of counting the number of models of a Boolean formula.

Organizers: Arijit Shaw, Markus Hecher, Johannes K. Fichte
Webpage: https://mccompetition.org/index.html

The MiniZinc Challenge

The MiniZinc Challenge is an annual competition of constraint programming solvers on a variety of benchmarks. It has been held every year since 2008. The 15th MiniZinc Challenge will be held as part of CP 2025.

Judges: Jimmy H.M. Lee, Barry O’Sullivan, Roland Yap
Webpage: https://www.minizinc.org/challenge/2025/

The XCSP Competition

The seventh international XCSP3 constraint solver competition is organized to improve our knowledge about components (e.g., filtering algorithms, heuristics, search strategies, encodings, reformulation techniques and learning procedures) that are behind the efficiency of solving systems (referred to as constraint solvers in this document) for combinatorial constrained problems.

Organizers: Gilles Audemard, Christophe Lecoutre and Emmanuel Lonca
Webpage: https://www.xcsp.org/competitions/