Schedule

Jump to day: Sunday / Monday / Tuesday / Wednesday / Thursday / Friday

Last-minute changes: SAT will be in JMS 641 on Friday.
Sunday 10th August – Morning  
All Sunday events are in the James McCune Smith Learning Hub (JMS). Registration and catering are on the ground floor. The large central escalators are the quickest way to the conference rooms. Please note that the Subway does not start running until 10am on Sundays, so for those attending the first session and travelling from the city centre, you may wish to take a bus (Google Maps knows all the local bus companies: use "Boyd Orr Building" as your destination).
09:15 – 10:30
SMT
SMT 1: Invited Talk
JMS 641
Welcome
09:15 – 09:30
Deciding Satisfiability of Quantified Bitvector Formulae with BDDs
Jan Strejček
09:30 – 10:30
10:30 – 11:00
All
Coffee Break
JMS Foyer
11:00 – 12:30
SMT
SMT 2: Quantifier Instantiation and Combination of Theories
JMS 641
Quantifier Instantiations: To Mimic or To Revolt?
Jan Jakubuv and Mikoláš Janota
11:00 – 11:20
From MBQI to Enumerative Instantiation and Back
Marek Dančo, Petra Hozzová and Mikoláš Janota
11:20 – 11:40
Being polite is not enough (and other limits of theory combination)
Guilherme Toledo
11:40 – 12:00
A Few Exercises on the Complexity of Congruence Closure with Cardinality Constraints
Ellen Dasnois and Pascal Fontaine
12:00 – 12:20
DP
CP / SAT Doctoral Programme 1
JMS 745
Opening
11:00 – 11:20
Improving Reduction Techniques in Pseudo-Boolean Conflict Analysis
Orestis Lomis, Jo Devriendt, Hendrik Bierlee and Tias Guns
11:20 – 11:27
Practically Feasible Proof Logging for Pseudo-Boolean Optimization
Wietze Koops, Daniel Le Berre, Magnus O. Myreen, Jakob Nordström, Andy Oertel, Yong Kiam Tan and Marc Vinyals
11:30 – 11:39
Certified Implicit Hitting Set Solving with Local Search for Pseudo-Boolean Optimization
Benjamin Bogø, Xiamin Chen, Wietze Koops, Pinyan Lu, Jakob Nordström, Marc Vinyals and Qingzhao Wu
11:39 – 11:57
Efficient Certified Reasoning for Binarized Neural Networks
Jiong Yang, Yong Kiam Tan, Mate Soos, Magnus O. Myreen and Kuldeep S. Meel
12:00 – 12:09
Proof logging the Generalized Totalizer Encoding
Carlos Cantero, Bart Bogaerts and Dieter Vandesande
12:09 – 12:27
ExCoS
ExCoS 1
JMS 743
Welcome
10:50 – 11:00
Proving and Explaining the Equivalence of Constraint Formulations
Pablo Manrique, Stefan Szeider
11:00 – 11:22
Explaining SAT Solving Using Causal Reasoning
Jiong Yang, Arijit Shaw, Teodora Baluta, Mate Soos, Kuldeep S. Meel
11:22 – 11:45
Using Certifying Constraint Solvers for Generating Step-Wise Explanations
Ignace Bleukx, Maarten Flippo, Emir Demirovic, Bart Bogaerts, Tias Guns
11:45 – 12:07
Counterfactual Explanations for Unsatisfiable Producer/Consumer Problems
Sharmi Dev Gupta, Helmut Simonis, Luis Quesada, Barry O'Sullivan
12:07 – 12:30
ML4SP
ML4SP Workshop
JMS 630
Machine Learning Guidance for an Automatic Theorem Prover
Martin Suda
11:00 – 11:45
Automated Streamliner Selection via Algorithm Configuration and Selection
Nguyen Dang
11:45 – 12:30
12:30 – 13:30
All
Lunch
JMS Foyer
  Sunday 10th August – Afternoon  
13:30 – 15:00
SMT
SMT 3: Theories
JMS 641
Evaluating Binary Polynomials using Subpolynomials
Jacob M. Howe, Martin Brain and Arnau Gàmez-Montolio
13:30 – 14:00
Satisfiability Modulo Exponential Integer Arithmetic
Florian Frohn and Jürgen Giesl
14:00 – 14:20
Constraint Propagation for Bit-Vectors in Alt-Ergo
Hichem Rami Ait-El-Hara, Guillaume Bury, Basile Clément and Pierre Villemot
14:20 – 14:40
Boosting MCSat Modulo Nonlinear Integer Arithmetic via Local Search
Enrico Lipparini, Thomas Hader, Ahmed Irfan and Stéphane Graham-Lengrand
14:40 – 15:00
DP
Invited Talk
JMS 745
How Not To Do It
Ian Gent
13:30 – 14:30
DP
CP / SAT Doctoral Programme 2
JMS 745
Certified Grounding of Extensions of First-Order Logic
Daimy Van Caudenberg, Carlos Cantero, Markus Anders and Bart Bogaerts
14:30 – 14:48
ExCoS
ExCoS 2
JMS 743
Creating Pen and Paper Puzzles with a Unique Solution
Christopher Jefferson
13:30 – 13:52
Understanding How Players Solve Puzzles
Thomas Lofaro, Ruth Hoffmann, Miriam Sturdee, Christopher Jefferson, Alice M Lynch
13:52 – 14:15
Preference Elicitation for Explanations in Logic Puzzles
Marco Foschini, Marianne Defresne, Emilio Gamba, Bart Bogaerts, Tias Guns
14:15 – 14:37
Explanations for Planning via CSP: Application to a Concrete Use Case
Nika Beriachvili, Rebecca Eifler, Arthur Bit-Monnot
14:37 – 15:00
ML4SP
ML4SP Workshop
JMS 630
Machine Learning for Quantifiers
Mikoláš Janota
13:30 – 14:15
Applying Machine Learning to Improve SAT Solvers: Some Highlights
Sean Holden
14:15 – 15:00
15:00 – 15:30
All
Coffee Break
JMS Foyer
15:30 – 17:10
SMT
SMT 4: Applications
JMS 641
Comparative Analysis of SMT Solvers for Differential Cryptanalysis of SHA-2
Marcel Barlik and Martin Brain
15:30 – 15:50
Space Explanations of Neural Network Classification
Tomáš Kolárik, Faezeh Labbaf, Martin Blicha, Michael Wand, Natasha Sharygina and Grigory Fedyukovich
15:30 – 16:10
Approximate SMT Counting Beyond Discrete Domains
Arijit Shaw and Kuldeep S. Meel
16:10 – 16:30
Syntax-Guided Synthesis with CounterExample Guided E-graphs: A Work-In-Progress Report
Guy Frankel, Rudi Schneider, Michel Steuwer and Elizabeth Polgreen
16:30 – 16:50
On Writing SMT-LIB Scripts: Metrics and a new Dataset
Soaibuzzaman and Jan Oliver Ringert
16:50 – 17:10
DP
CP / SAT Doctoral Programme 3
JMS 745
Analyzing Self-stabilization of Synchronous Unison via Propositional Satisfiability
Asma Khoualdia, Sami Cherif, Stéphane Devismes and Léo Robert
15:30 – 15:39
An Evaluation of Constraint-Based Approaches to Cumulative Scheduling with Delays
Antton Kasslin and Jeremias Berg
15:39 – 15:57
Optimizing 2D Cutting: A Bin Packing Approach to Minimize Scraps and Maximize their Reusability
Manuel Chastenay, Xavier Zwingmann, Claude-Guy Quimper and Jonathan Gaudreault
16:00 – 16:09
Improved Energetic Reasoning Checker for Cumulative Constraint with Profile
Rosaly Zoller Bodo Ngono, Yves Pascal Ndjopnang Wantiep and Roger Kameugne
16:09 – 16:27
Exact Methods for the Travelling Salesperson Problem with Self-Deleting Graphs
Daniel Pekar and J. Christopher Beck
16:30 – 16:39
Preemptive jobshop scheduling with maximum workload constraints
Tanguy Terrien and Cyrille Briand
16:39 – 16:57
ExCoS
ExCoS 3
JMS 743
A Framework for Data-driven Explainability in Mathematical Optimization
Michael Hartisch
15:30 – 15:52
Explanations for Hierarchical Neuro-Symbolic AI
Sushmita Paul, Jinqiang Yu, Jip J. Dekker, Maria Garcia de la Banda, Peter J. Stuckey, Alexey Ignatiev
15:52 – 16:15
Explaining Mismatches in Expected versus Perceived Behavior for Interacting Digital Systems
Mohammad Alkhiyami, Gianluca Martino, Goerschwin Fey
16:15 – 16:37
Explainable Rational Synthesis in Multi-Agent Systems
Alireza Farhadi, Mohammad Izadi, Jafar Habibi, Tobias Meggendorfer
16:37 – 17:00
ML4SP
ML4SP Workshop
JMS 630
ML-guided search for Mixed Integer Linear Programming
Bistra Dilkina
15:30 – 16:15
Panel
16:15 – 17:00
  Monday 11th August – Morning 1  
Monday events are in the James McCune Smith Learning Hub (JMS), the entry level of the Boyd Orr Building (BO), and the ground floor of the Wolfson Medical Building (WMB). The large central escalators are the quickest way to the conference rooms in the JMS. The Boyd Orr building is connected directly to the JMS on the ground floor and on levels 4 and 6. The WMB is directly opposite, across University Avenue. Registration and catering are on the ground floor of the JMS.
09:00 – 10:30
SMT
SMT 5: Invited talk
BO LT1
Invited Talk: SAT Reasoning in CDCL(T) Solvers
Katalin Fazekas
09:00 – 10:00
SMT
SMT 5: Optimization Modulo Theory
BO LT1
An Optimization Modulo Theories-based Approach to Cumulative Scheduling with Delays
Antton Kasslin
10:00 – 10:30
DP
CP / SAT Doctoral Programme 4
JMS 745
Machine Learning Model for Selecting Assignments of Variables for SAT Problems
Jonathan Oliva and Peter Nightingale
09:00 – 09:18
Dependency-Curated Large Neighbourhood Search
Frej Knutar Lewander, Pierre Flener and Justin Pearson
09:18 – 09:27
Do LLMs Understand Constraint Programming? Zero-Shot Constraint Programming Model Generation Using LLMs
Yuliang Song and Eldan Cohen
09:30 – 09:48
Transformer-based Feature Learning for Algorithm Selection in Combinatorial Optimisation
Alessio Pellegrino, Özgür Akgün, Zeynep Kiziltan, Ian Miguel and Nguyen Dang
09:48 – 09:57
Approximate SMT Counting Beyond Discrete Domains
Arijit Shaw and Kuldeep S. Meel
10:00 – 10:18
Learning to Bound for Maximum Common Subgraph Algorithms
Buddhi Wathsala Kothalawala, Henning Koehler and Qing Wang
10:18 – 10:27
ModRef
Invited Talk
JMS 743
Automated Reasoning in Discrete Geometry: Discovery, Verification, and Symmetry
Marijn Heule
09:00 – 10:00
ModRef
ModRef 1
JMS 743
Machine Learning Model for Selecting Assignments of Variables for SAT Problems
Jonathan Benjamin Oliva Salinas, Peter Nightingale
10:00 – 10:15
STRIPS-2-DyPDL: Translating Automated Planning Problems into Domain-Independent Dynamic Programming Problems
Dillon Ze Chen
10:15 – 10:30
PoS
Pragmatics of SAT 1
BO LT2
Opening
09:00 – 09:30
Remembering Allen Van Gelder
09:30 – 10:00
SAT-Web: A web based educational SAT visualisation tool
James Madgwick and Martin Mariusz Lester
10:00 – 10:30
LLM-Solve
Invited Talk
WMB Yudowitz
Neurosymbolic CP
Florian Regin
09:00 – 09:40
LLM-Solve
Assisting Constraint Modeling with LLMs
WMB Yudowitz
CP-Model-Zoo: A Natural Language Query System for Constraint Programming Models
Augustin Crespin, Ioannis Kostis, Hélène Verhaeghe, Pierre Schaus
09:40 – 10:05
Automated Constraint Model Modification with Large Language Models
Adam Kuca, Phong Le, Nguyen Dang
10:05 – 10:30
QBF
QBF 1
WMB Gannochy
Welcome
09:00 – 09:05
Quantified Integer Programming --- a tutorial
Michael Hartisch
09:05 – 09:50
Computationally Hard Problems Are Hard for QBF Proof Systems Too
Agnes Schleitzer and Olaf Beyersdorff
09:50 – 10:10
Model Counting for Dependency Quantified Boolean Formulas
Long-Hin Fung, Che Cheng, Jie-Hong Roland Jiang, Friedrich Slivovsky and Tony Tan
10:10 – 10:30
10:30 – 11:00
All
Coffee Break
JMS Foyer
  Monday 11th August – Morning 2  
11:00 – 12:30
SMT
SMT 6: Solvers + Benchmarks + SMT-LIB
BO LT1
Visualization of execution traces in Colibri 2 SMT solver
Christophe Junke and François Bobot
11:00 – 11:20
A Conjecture Regarding SMT Instability
Can Cebeci, Nikolaj Bjørner, George Candea and Clément Pit-Claudel
11:20 – 11:40
A Catalog of SMT-LIB Benchmarks
Hans-Jörg Schurr, Mathias Preiner, Aina Niemetz, Clark Barrett, Pascal Fontaine and Cesare Tinelli
11:40 – 12:00
A Proposal for an OMT Extension to SMT-LIB
Nestan Tsiskaridze, Andrew Reynolds, Cesare Tinelli and Clark Barrett
12:00 – 12:20
DP
Invited Talk
JMS 745
In the Reviewer’s Eye
Sophie Tourret
11:00 – 12:00
DP
CP / SAT Doctoral Programme 5
JMS 745
Circuit Learning for Boolean Satisfiability Problem
Zhengyuan Shi and Qiang Xu
12:00 – 12:18
ModRef
ModRef 2
JMS 743
Undefinedness in Planning with Arrays
Carla Davesa Sureda, Joan Espasa, Ian Miguel, Mateu Villaret
11:00 – 11:25
Asymptotically Smaller Encodings for Graph Problems and Scheduling
Bernardo Subercaseaux
11:25 – 11:50
Declarative pearl: I put a SAT solver in your SAT solver so you can find backdoors slowly
Martin Mariusz Lester. Short Presentation
11:50 – 12:05
Evaluating the Impact of Encoding on SAT Based Constraint Solving in Exchequer
Aadil Sattar, Martin Mariusz Lester
12:05 – 12:20
PoS
Pragmatics of SAT 2 (Optimization)
BO LT2
Certifying Pareto Optimality in Multi-Objective Maximum Satisfiability
Christoph Jabs, Jeremias Berg, Bart Bogaerts and Matti Järvisalo
11:00 – 11:30
Improving Watched Pseudo-Boolean Propagation with Significant Literals
Mia Müßig and Jan Johannsen
11:30 – 12:00
Ordered Objectives in MaxSAT
Jeremias Berg, Andre Schidler and Matti Järvisalo
12:00 – 12:30
LLM-Solve
LLMs and Solvers
WMB Yudowitz
LLMs as Translators, Not Thinkers: Structured Output Enables Stronger NP-Hard Problem Solving
Haoyu Wang, Dan Roth
11:00 – 11:30
HiGHS-MCP: Enabling Large Language Models to Solve Optimization Problems with HiGHS
Wilfred Springer
11:30 – 12:00
From Portfolio Solvers to Agentic Solvers
Roberto Amadini, Simone Gazza
12:00 – 12:30
QBF
QBF 2
WMB Gannochy
Breaking Symmetries in Quantified Graph Search: A Comparative Study
Mikoláš Janota, Markus Kirchweger, Tomáš Peitl and Stefan Szeider
11:00 – 11:20
Graph Choosability via SAT: Beyond the Nullstellensatz
Markus Kirchweger, Tomáš Peitl, David Seka and Stefan Szeider
11:20 – 11:40
PyQBF: A Python Framework for Solving Quantified Boolean Formulas
Mark Peyrer, Maximilian Heisinger and Martina Seidl
11:40 – 12:00
Discussion
12:00 – 12:30
MC
Model Counting 1
WMB Hugh Fraser
Opening Remarks
11:00 – 11:10
Approximate SMT Counting Beyond Discrete Domains
Arijit Shaw and Kuldeep S. Meel
11:10 – 11:40
Numerical Considerations in Weighted Model Counting
Randal Bryant
11:40 – 12:10
12:30 – 13:30
All
Lunch
JMS Foyer
  Monday 11th August – Afternoon 1  
13:30 – 15:00
SMT
SMT 7: SMT-COMP
BO LT1
Instability Track for SMT-COMP
Amar Shah, Yi Zhou, Marijn Heule and Bryan Parno
13:30 – 13:50
SMT-COMP presentation
Martin Jonáš, François Bobot, David Deharbe and Dominik Winterer
13:50 – 14:00
DP
CP / SAT Doctoral Programme 6
JMS 745
Problem Partitioning via Proof Prefixes
Zachary Battleman, Joseph Reeves and Marijn Heule
13:30 – 13:39
Workload Balancing in a Food Distribution Center Comparing Constraint Programming and Mixed-Integer Linear Programming
Josep Maria Salvia Hornos, Ivet Rafegas Fonoll, Cèsar Fernandez Camón and Carles Mateu
13:39 – 13:57
Streamlining Distributed SAT Solver Design
Niccolò Rigi-Luperti, Dominik Schreiber and Armin Biere
14:00 – 14:09
Beyond Core-Guided MaxSAT
Ion Mikel Liberal, Jordi Levy and Ilario Bonacina
14:09 – 14:27
Enumerating All Boolean Matches
Yogev Shalmon and Alexander Nadel
14:30 – 14:39
MaxSAT and pseudo-Boolean Solutions for the Multi-Skill Project Scheduling Problem
Wilber Bermeo, Mateu Villaret and Jordi Coll
14:39 – 14:57
ModRef
ModRef 3
JMS 743
Solver-Aided Expansion of Loops to Avoid Generate-and-Test
Niklas Dewally, Özgür Akgün
13:30 – 13:55
Integer Linear Programming Techniques for Enhancing Branch and Bound MaxSAT Solvers
Jialu Zhang, Chu-Min Li, Sami Cherif, Shuolin Li, Zhifei Zheng
13:55 – 14:20
Modeling the p-Dispersion Problem with Distance Constraints
Panteleimon Iosif, Nikolaos Ploskas, Kostas Stergiou, Dimos Tsouros
14:20 – 14:45
Mutual B refinements as a justification for constraints model reformulations
Jean-Louis Dufour
14:45 – 15:00
PoS
Pragmatics of SAT 3 (SAT)
BO LT2
Conflict-Driven SAT Solving using XOR-OR-AND Normal Forms
Julian Danner and Martin Kreuzer
13:30 – 14:00
Revisiting Clause Vivification
Florian Pollitt, Mathias Fleury, Armin Biere, Karem Sakallah, Marijn Heule, Jiawei Chen and Yonathan Fisseha
14:00 – 14:30
Incremental Inprocessing Rules beyond Resolution
Katalin Fazekas, Florian Pollitt, Mathias Fleury and Armin Biere
14:30 – 15:00
LLM-Solve & PTHG
Joint LLM-Solve / PTHG Invited Talk
WMB Yudowitz
Neural Meets Symbolic: Synergies Between Language Models and Constraint Reasoning
Stefan Szeider
13:30 – 14:10
LLM-Solve
Generating and Evaluating Constraint Models
WMB Yudowitz
Do LLMs Understand Constraint Programming? Zero-Shot Constraint Programming Model Generation Using LLMs
Yuliang Song, Eldan Cohen
14:10 – 14:35
LLM-as-a-Judge For Combinatorial Optimization Modelisations from Natural Language
Emma Frechette, Louis-Martin Rousseau, Tias Guns
14:35 – 15:00
PTHG
PTHG Workshop
WMB Gannochy
Progress towards the Holy Grail: Solving
Peter Stuckey
14:15 – 15:00
MC
Model Counting 2
WMB Hugh Fraser
Cara: An Isomorphism-Based #SAT Solver
Petr Illner
13:30 – 14:00
Surveying the Model Counting Competition 2025
Johannes K. Fichte, Markus Hecher and Arijit Shaw
14:00 – 14:30
Towards Real-Time Approximate Counting
Yash Pote, Kuldeep S. Meel and Jiong Yang
14:30 – 15:00
15:00 – 15:30
All
Coffee Break
JMS Foyer
  Monday 11th August – Afternoon 2  
15:30 – 17:30
SMT
SMT 8: SMT-LIB Discussion + Business Meeting
BO LT1
SMT-LIB discussion
Cesare Tinelli
15:30 – 16:15
Business Meeting
Sophie Tourret
16:15 – 17:00
DP
CP / SAT Doctoral Programme 7
JMS 745
Integer Linear Programming Preprocessing for Maximum Satisfiability
Jialu Zhang, Chu-Min Li, Sami Cherif, Shuolin Li and Zhifei Zheng
15:30 – 15:48
Fine-Grained Complexity Analysis of Dependency Quantified Boolean Formulas
Che Cheng, Long-Hin Fung, Jie-Hong Roland Jiang, Friedrich Slivovsky and Tony Tan
15:48 – 15:57
Symmetry Breaking in the Subgraph Isomorphism Problem
Joseph Loughney, Ruth Hoffmann and Mun See Chang
16:00 – 16:18
Reencoding Unique Literal Clauses
Aeacus Sheng, Joseph Reeves and Marijn Heule
16:18 – 16:27
Modelling Multi-dimensional Arrays in Unified Planning
Carla Davesa Sureda, Joan Espasa Arxer, Ian Miguel and Mateu Villaret
16:30 – 16:48
Learn to Unlearn
Florian Pollitt, Bernhard Gstrein, André Schidler, Mathias Fleury and Armin Biere
16:48 – 16:57
ModRef
ModRef 4
JMS 743
Modeling the Inglenook Shunting Puzzle
Helmut Simonis, Luis Quesada
15:30 – 15:55
A new Constraint Programming model for the Multiple Constant Multiplication
Cantaloube Théo, Xiao Peng, Christine Solnon, Anastasia Volkova
15:55 – 16:20
Where Now For Modelling in SAT, Constraints, Planning, and Everywhere Else?
16:20 – 17:30
PoS
Pragmatics of SAT 4 (Certification)
BO LT2
How to discover short, shorter, and the shortest proofs of unsatisfiability: a branch-and-bound approach for resolution proof length minimization
Konstantin Sidorov, Jacobus G. M. van der Linden, Gonçalo Correia, Mathijs de Weerdt and Emir Demirović
15:30 – 16:00
Certified Implicit Hitting Set Solving with Local Search for Pseudo-Boolean Optimization
Benjamin Bogø, Xiamin Chen, Wietze Koops, Pinyan Lu, Jakob Nordström, Marc Vinyals and Qingzhao Wu
16:00 – 16:30
Faster Certified Symmetry Breaking using Orders with Auxiliary Variables
Markus Anders, Bart Bogaerts, Benjamin Bogø, Arthur Gontier, Wietze Koops, Ciaran McCreesh, Magnus Myreen, Jakob Nordström, Andy Oertel, Adrian Rebola-Pardo and Yong Kiam Tan
16:30 – 17:00
LLM-Solve
Benchmarking LLMs
WMB Yudowitz
Benchmarking LLMs for CP model generation
Kostis Michailidis, Dimos Tsouros, Tias Guns
15:30 – 16:00
PTHG
PTHG Workshop
WMB Gannochy
ML-guided and Robust Constraint Acquisition
Hendrik Bierlee, Dimos Tsouros, Senne Berden, and Tias Guns
15:30 – 16:00
LLM-Solve & PTHG
Joint Panel with PTHG
WMB Yudowitz
Are LLMs the missing piece to get us to the Holy Grail?
16:00 – 17:30
19:30 – late
  Tuesday 12th August – Morning  
Tuesday events are in the James McCune Smith Learning Hub (JMS) and the entry level of the Boyd Orr Building (BO). The large central escalators are the quickest way to the conference rooms in the JMS. The Boyd Orr building is connected directly to the JMS on the ground floor and on levels 4 and 6. Registration and catering are on the ground floor of the JMS.
09:00 – 10:30
All
Opening
BO LT1
09:00 – 09:30
All
Invited Talk: Ruzica Piskac
BO LT1
Jakob Nordström
10:30 – 11:00
All
Coffee Break
JMS Foyer
11:00 – 12:30
CP A
Applications 1
BO LT1
Jimmy Lee
Andreas Schutt, Matteo Cardellini, Jip J. Dekker, Daniel Harabor, Marco Maratea, and Mauro Vallati
11:00 – 11:30
Yousra El Ghazi, Djamal Habet, and Cyril Terrioux
11:30 – 12:00
Duc Anh Le, Stéphanie Roussel, and Christophe Lecoutre
12:00 – 12:30
CP B
Solver Tuning / Selection / Parallelisation
JMS 745
Laurent Michel
Zhengyuan Shi, Wentao Jiang, Xindi Zhang, Jin Luo, Yun Liang, Zhufei Chu, and Qiang Xu
11:00 – 11:30
Peng Lin, Shaowei Cai, Mengchuan Zou, and Shengqi Chen
11:30 – 12:00
Alessio Pellegrino, Özgür Akgün, Nguyen Dang, Zeynep Kiziltan, and Ian Miguel
12:00 – 12:30
SoCS
Best Paper
JMS 743
SoCS
Multi-Agent Pathfinding 1
JMS 743
Jiří Švancara
Shao-Hung Chan, Thomy Phan, Jiaoyang Li and Sven Koenig
12:00 – 12:20
Daniel Koch and Stefan Funke
12:20 – 12:30
SAT
QBF
BO LT2
Clemens Hofstadler
Olaf Beyersdorff, Ilario Bonacina, Kaspar Kasche, Meena Mahajan, and Luc Spachmann
11:00 – 11:30
Leroy Chew and Tomáš Peitl
11:30 – 12:00
Che Cheng, Long-Hin Fung, Jie-Hong Roland Jiang, Friedrich Slivovsky, and Tony Tan
12:00 – 12:30
12:30 – 14:00
DP
CP / SAT Doctoral Programme Posters
JMS Foyer
All
Lunch
JMS Foyer
  Tuesday 12th August – Afternoon  
14:00 – 15:00
CP A
Model Counting to the Rescue
BO LT1
Michael Codish
Dekel Zak, Jingyi Mei, Jean-Marie Lagniez, and Alfons Laarman
14:00 – 14:30
Mohimenul Kabir, Van-Giang Trinh, Samuel Pastva, and Kuldeep S Meel
14:30 – 15:00
CP B
Applications 2
JMS 745
Hélène Verhaeghe
Younes Mechqrane and Ismail Elabbassi
14:00 – 14:30
Florentina Voboril, Vaidyanathan Peruvemba Ramaswamy, and Stefan Szeider
14:30 – 15:00
SoCS
Tutorial
JMS 743
Hana Rudová
Heuristic Search vs. Constraint Programming for Single Machine Scheduling
Christopher Beck
14:00 – 15:00
SAT
Tool and Short Papers
BO LT2
Daniel Le Berre
Suwei Yang, Yong Lai, and Kuldeep S. Meel
14:00 – 14:20
Christoph Jabs
14:20 – 14:40
15:00 – 15:30
All
Coffee Break
JMS Foyer
15:30 – 17:00
CP A
Verification / Certification / Testing
BO LT1
Peter Stuckey
Wietze Koops, Daniel Le Berre, Magnus O. Myreen, Jakob Nordström, Andy Oertel, Yong Kiam Tan, and Marc Vinyals
15:30 – 16:00
Ghiles Ziat and Martin Pépin
16:00 – 16:30
CP B
Tutorial
JMS 745
Modelling for Scheduling and Rostering Problems with Constraint Programming
Helmut Simonis
15:30 – 17:00
SoCS
Single Agent Motion Planning
JMS 743
Oren Salzman
Matan Sudry, Tom Jurgenson and Erez Karpas
15:30 – 15:50
Muhammad Suhail Saleem, Rishi Veerapaneni and Maxim Likhachev
15:50 – 16:10
SoCS
Satisfiability
JMS 743
Rishi Veerapaneni
Dominik Schreiber, Christoph Jabs and Jeremias Berg
16:10 – 16:30
Andre Schidler and Stefan Szeider
16:50 – 17:00
SAT
Sampling and Model Counting
BO LT2
Johannes Fichte
Ananth Kidambi, Guramrit Singh, Paulius Dilkas, and Kuldeep S. Meel
15:30 – 16:00
Yong Lai, Haolong Tong, Zhenghang Xu, and Minghao Yin
16:00 – 16:30
Dingding Dong and Nitya Mani
16:30 – 17:00
19:00 – 20:30
  Wednesday 13th August – Morning  
Wednesday events are in the James McCune Smith Learning Hub (JMS) and the entry level of the Boyd Orr Building (BO). The large central escalators are the quickest way to the conference rooms in the JMS. The Boyd Orr building is connected directly to the JMS on the ground floor and on levels 4 and 6. Catering is on the ground floor of the JMS.
09:00 – 10:00
10:00 – 10:30
All
Coffee Break
JMS Foyer
10:30 – 12:00
CP A
Best Papers
BO LT1
Maria Garcia de la Banda
Ignace Bleukx, Ryma Bouzazouma, Tias Guns, Nadine Laage, and Guillaume Poveda
10:30 – 11:00
J. Christopher Beck, Ryo Kuroiwa, Jimmy H.M. Lee, Peter J. Stuckey, and Allen Z. Zhong
11:00 – 11:30
Hannes Ihalainen, Jeremias Berg, Matti Järvisalo, and Bart Bogaerts
11:30 – 12:00
SoCS
Heuristic Search 1
JMS 743
Rick Valenzano
Garrett Fereday and Eric Hansen
10:30 – 10:50
Devin Wild Thomas and Wheeler Ruml
10:50 – 11:10
Ernst Althaus, Markus Blumenstock, Nick Rassau, Felix Martin Schuhknecht and Anton Quentin Zimdars
11:10 – 11:30
Lior Siag, Ariel Felner and Shahaf S. Shperberg
11:30 – 11:50
Takumi Shimoda and Alex Fukunaga
11:50 – 12:00
SAT
Lots of Solutions
BO LT2
Stefan Szeider
Alexander Nadel and Yogev Shalmon
10:30 – 11:00
L. Sunil Chandran, Rishikesh Gajjala, and Kuldeep S. Meel
11:00 – 11:30
Maja Aaslyng Dall, Raúl Pardo, Thomas Lumley, and Andrzej Wasowski
11:30 – 12:00
12:00 – 13:30
All
Lunch
JMS Foyer
  Wednesday 13th August – Afternoon  
13:30 – 15:00
CP A
Modelling Languages / Interfaces
BO LT1
Özgür Akgün
Jip J. Dekker, Jason Nguyen, Peter J. Stuckey, and Guido Tack
13:30 – 14:00
Ryo Kuroiwa and J. Christopher Beck
14:00 – 14:30
Jef Jacobs, Wolfgang De Meuter, and Jens Nicolay
14:30 – 15:00
CP B
Tutorial
JMS 745
Parallel Constraint Solving
Dominik Schreiber and Shaowei Cai
13:30 – 15:00
SoCS
DC Invited Talk
JMS 743
Lukáš Chrpa and Franceso Percassi
When Models Meet the Real World: Lessons from Applied AI Research
Mauro Vallati
13:30 – 14:30
SoCS
Best Student Paper
JMS 743
Maxim Likhachev
Mark Carlson, Daniel Harabor and Peter J. Stuckey
14:30 – 14:50
SoCS
Heuristic Search 2
JMS 743
Maxim Likhachev
Dawson Brown and Rick Valenzano
14:50 – 15:00
SAT
Pseudo-Boolean and Bit-Vectors
BO LT2
Marc Vinyals
Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez Carbonell, and Rui Zhao
13:30 – 14:00
Orestis Lomis, Jo Devriendt, Hendrik Bierlee, and Tias Guns
14:00 – 14:30
Zvika Berger, Yoni Zohar, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark Barrett, and Cesare Tinelli
14:30 – 15:00
15:00 – 15:30
All
Coffee Break
JMS Foyer
15:30 – 17:30
CP A
Constraints Awards
BO LT1
Zeynep Kiziltan
Constraints journal Classic Paper Award
15:30 – 16:00
Constraints journal Prominent Paper Award
16:00 – 16:30
CP A
ACP General Assembly
BO LT1
16:30 – 17:30
SoCS
Spotlights 1
JMS 743
Lukáš Chrpa and Franceso Percassi
15:30 – 16:15
SoCS
Posters 1
JMS Foyer
16:15 – 17:30
SAT
Synthesis and Solvers
BO LT2
Ilario Bonacina
Anna B. Jakobsen, Anders B. Clausen, Jaco van de Pol, and Irfansha Shaik
15:30 – 16:00
Irfansha Shaik and Jaco van de Pol
16:00 – 16:30
Dominik Schreiber, Niccolò Rigi-Luperti, and Armin Biere
16:30 – 17:00
Aeacus Sheng, Joseph Reeves, and Marijn Heule
17:00 – 17:30
  Thursday 14th August – Morning  
Thursday events are in the James McCune Smith Learning Hub (JMS) and the entry level of the Boyd Orr Building (BO). The large central escalators are the quickest way to the conference rooms in the JMS. The Boyd Orr building is connected directly to the JMS on the ground floor and on levels 4 and 6. Catering is on the ground floor of the JMS.
09:00 – 10:00
All
Invited Talk: Sylvie Thiébaux
BO LT1
Ariel Felner
Graph Learning for Planning
09:00 – 10:00
10:00 – 10:30
All
Coffee Break
JMS Foyer
10:30 – 12:00
CP A
Awards
BO LT1
Gilles Pesant
ACP Research Award
Laurent Michel
10:30 – 11:00
ACP ECR Award
Emir Demirović
11:00 – 11:30
ACP Doctoral Research Award
Ruiwei Wang
11:30 – 12:00
CP A
Announcements
BO LT1
Gilles Pesant
CP Summer School and 2026 Announcements
12:00 – 12:05
SoCS
Multi-Agent Pathfinding 2
JMS 743
Keisuke Okumura
Daniel Koyfman, Dor Atzmon, Shahaf Shperberg and Ariel Felner
10:30 – 10:50
Matej Husár, Jiří Švancara and Roman Barták
10:50 – 11:00
Jonathan Morag, Noy Gabay, Daniel Koyfman and Roni Stern
11:00 – 11:10
Runzhe Liang, Rishi Veerapaneni, Daniel Harabor, Jiaoyang Li and Maxim Likhachev
11:10 – 11:20
Shahar Bardugo, Daniel Koyfman and Dor Atzmon
11:20 – 11:40
Jiaqi Tan, Yudong Luo, Jiaoyang Li and Hang Ma
11:40 – 12:00
SAT
MaxSAT
BO LT2
Matti Järvisalo
Andre Schidler and Stefan Szeider
10:30 – 11:00
Ilario Bonacina, María-Luisa Bonet, Sam Buss and Massimo Lauria
11:00 – 11:30
12:00 – 13:00
All
Lunch
JMS Foyer
  Thursday 14th August – Afternoon  
13:00 – 15:10
CP A
Competitions
BO LT1
13:00 – 13:30
CP A
Applications 3
BO LT1
Helmut Simonis
Manuel Chastenay, Xavier Zwingmann, Claude-Guy Quimper, and Jonathan Gaudreault
14:05 – 14:35
Miguel Antoons, Augustin Delecluse, Samih Zein, and Pierre Schaus
14:35 – 15:05
CP B
Constraints / QIP / Core-Boosted LS
JMS 745
Louis-Martin Rousseau
Konstantin Sidorov, Imko Marijnissen, and Emir Demirović
14:05 – 14:35
Michael Hartisch and Leroy Chew
14:35 – 15:05
CP A
Extra Coffee
JMS Foyer
15:05 – 15:10
SoCS
More Lunch
JMS Foyer
13:00 – 13:30
SoCS
Tutorial
JMS 743
Roni Stern
Maximising Throughput in Lifelong Multi-Agent Pathfinding
Daniel Harabor
13:30 – 14:30
SoCS
Heuristic Search 3
JMS 743
Mauro Vallati
Weimin Huang, Natalie Isenberg, Ján Drgoňa, Draguna Vrabie and Bistra Dilkina
14:30 – 14:50
Shahaf Shperberg, Lior Siag, Nathan Sturtevant and Ariel Felner
14:50 – 15:00
SoCS
Extra Coffee
JMS Foyer
15:00 – 15:10
SAT
Short Talks 1
BO LT2
SAT
Awards
BO LT2
Jeremias Berg, Jakob Nordström and Olaf Beyersdorff
13:20 – 14:20
SAT
PBO and MC Competitions
BO LT2
Jeremias Berg, Jakob Nordström and Olaf Beyersdorff
14:20 – 15:10
15:10 – 15:30
All
Coffee Break
JMS Foyer
15:30 – 17:30
CP A
Applications 4
BO LT1
Guido Tack
Mikael Z. Lagerkvist and Magnus Rattfeldt
15:30 – 16:00
Michael Prümm, Peter Nightingale, and Felix Ulrich-Oltean
16:00 – 16:30
Valentin Antuori, Damien T. Wojtowicz, and Emmanuel Hebrard
16:30 – 17:00
CP B
Learning Solvers
JMS 745
Tias Guns
Emmanuel Hebrard
15:30 – 16:00
Robbin Baauw, Maarten Flippo, and Emir Demirović
16:00 – 16:30
Jip J. Dekker, Alexey Ignatiev, Peter J. Stuckey, and Allen Z. Zhong
16:30 – 17:00
SoCS
Spotlights 2
JMS 743
Lukáš Chrpa and Franceso Percassi
15:30 – 16:15
SoCS
Posters 2
JMS Foyer
16:15 – 17:30
SAT
SAT Competition
BO LT2
Jeremias Berg, Jakob Nordström and Olaf Beyersdorff
15:30 – 16:00
SAT
SAT General Assembly
BO LT2
Olaf Beyersdorff
16:00 – 17:30
19:00 – 23:30
  Friday 15th August
Friday events are in the James McCune Smith Learning Hub (JMS) and the entry level of the Boyd Orr Building (BO). The large central escalators are the quickest way to the conference rooms in the JMS. The Boyd Orr building is connected directly to the JMS on the ground floor and on levels 4 and 6. Catering is on the ground floor of the JMS.
09:00 – 10:00
CP A
Symmetries & Graphs
BO LT1
Ruth Hoffmann
Michael Codish and Mikolas Janota
09:00 – 09:30
CP B
Applications 5
JMS 745
Christine Solnon
Asma Khoualdia, Sami Cherif, Stéphane Devismes, and Léo Robert
09:00 – 09:30
Nguyen Dang, Ian P. Gent, Peter Nightingale, Felix Ulrich-Oltean, and Jack Waller
09:30 – 10:00
SoCS
Heuristic Search 4
JMS 743
Nathan Sturtevant
Shizhe Zhao, Yancheng Wu and Zhongqiang Ren
09:20 – 09:40
Vidal Alcázar, Michael Barley, Natasha de Kriek, Santiago Franco, Angel Garcia-Olaya, Tim Hartill, Patricia Riddle, Chris Triggs and Henry Zwart
09:40 – 10:00
SAT
Short Talks 2
JMS 641
Katalin Fazekas
Pravesh Koirala, Aditya Shrey, and Forrest Laine
09:00 – 09:20
Bernhard Gstrein, Florian Pollitt, André Schidler, Mathias Fleury, and Armin Biere
09:20 – 09:40
Ryoga Ohashi, Takehide Soh, Daniel Le Berre, Hidetomo Nabeshima, Mutsunori Banbara, Katsumi Inoue, and Naoyuki Tamura
09:40 – 10:00
10:00 – 10:30
CP A
ACP DEI: Current/Future Initiatives
BO LT1
10:00 – 10:30
SoCS
Coffee Break
JMS Foyer
10:00 – 10:30
SAT
Algebraic Approaches
JMS 641
Katalin Fazekas
Ilario Bonacina and Jordi Levy
10:00 – 10:30
10:30 – 12:30
CP A
Coffee Break
JMS Foyer
10:30 – 11:00
CP A
Talking About Graphs
BO LT1
Peter Nightingale
Daniel Pekar and J. Christopher Beck
11:00 – 11:30
Xiao Peng and Christine Solnon
11:30 – 12:00
Artem Kaznatcheev and Sofia Vazquez Alferez
12:00 – 12:30
CP B
Coffee Break
JMS Foyer
10:30 – 11:00
CP B
Search
JMS 745
Ian Gent
Frej Knutar Lewander, Pierre Flener, and Justin Pearson
11:00 – 11:30
Tim Luchterhand, Emmanuel Hebrard, and Sylvie Thiebaux
11:30 – 12:00
Buddhi W. Kothalawala, Henning Koehler, and Qing Wang
12:00 – 12:30
SoCS
Learning and Search
JMS 743
Shahaf Shperberg
Hasan Ferit Eniser, Songtuan Lin, Nicola Müller, Anastasia Isychev, Valentin Wüstholz, Isabel Valera, Jörg Hoffmann and Maria Christakis
11:10 – 11:20
SoCS
SoCS Community Meeting
JMS 743
11:20 – 12:30
SAT
Coffee Break
JMS Foyer
10:30 – 11:00
SAT
Proofs
JMS 641
Massimo Lauria
Randal Bryant, Yong Kiam Tan, and Marijn Heule
11:00 – 11:30
Jiong Yang, Yong Kiam Tan, Mate Soos, Magnus O. Myreen, and Kuldeep S. Meel
11:30 – 12:00
Zachary Battleman, Joseph Reeves, and Marijn Heule
12:00 – 12:30
12:30 – 12:50
All
Closing
BO LT1
12:50 – 14:00
All
Packed Lunch (Stay and Socialise, or Take Away)
JMS Foyer
SoCS Spotlights and Posters
  Wednesday Afternoon
SoCS
Spotlights 1
JMS 743
Lukáš Chrpa and Franceso Percassi
Exploring the Trade-off Between Flexible and Deployable Models for PDDL+ Urban Traffic Control (Extended Abstract)
Sandra Castellanos-Paez, Francesco Percassi, Mauro Vallati
Multi-Agent Path Finding for Schedule Constrained Automation (Extended Abstract)
Kareem Eissa, Rayal Prasad, Ankur Kapoor
Object Packing and Scheduling for Sequential 3D Printing: A Linear Arithmetic Model and a CEGAR-Inspired Optimal Solver (Extended Abstract)
Pavel Surynek, Vojtěch Bubník, Lukáš Matěna, Petr Kubiš
You May Split but You Might Work It Out Later: First Steps Toward Merging Nodes in MAPF (Extended Abstract)
Grigorios Mouratidis, Bernhard Nebel, Sven Koenig
Bidirectional Heuristic Search in Longest Path Problems (Extended Abstract)
Tzur Shubi, Solomon Eyal Shimony, Ariel Felner, and Shahaf Shperberg
Prioritised Planning with Guarantees
Jonathan Morag
New Directions in Bidirectional Search (Student Abstract)
Lior Siag
Binarized Nested Rollout Policy Adaptation for the Optimization of the Grain Boundary Problem
Maruna So and Stefan Edelkamp
Multi-Agent Path Finding: Policies Instead of Plans
Jakub Mestek
Independence Detection in SAT-based MAPF under Time Uncertainty
Mrinalini Subramanian and Roman Barták
A Formalism for Optimal Search with Dynamic Heuristics
Remo Christen
15:30 – 16:15
SoCS
Posters 1
JMS Foyer
Each Spotlights 1 talk will also have a poster.
 
Real-time Cost-algebraic Heuristic Search
Devin Wild Thomas and Wheeler Ruml
Bi-Objective Search for the Traveling Salesman Problem with Time Windows and Vacant Penalties
Shizhe Zhao, Yancheng Wu and Zhongqiang Ren
Lightweight and Effective Preference Construction in PIBT for Large-Scale Multi-Agent Pathfinding
Keisuke Okumura and Nagai Hiroki
From Agent Centric to Obstacle Centric Planning: A Makespan-Optimal Algorithm for the Multi-Agent Warehouse Rearrangement Problem
Yaakov Sherma, Eyal Weiss and Oren Salzman
Guiding the Search for the Euclidean Shortest Path Problem
Daniel Koch and Stefan Funke
A Conflict-Driven Approach for Reaching Goals Specified with Negation as Failure
Forest Agostinelli
Decoupling Generation and Evaluation for Parallel Greedy Best-First Search
Takumi Shimoda and Alex Fukunaga
Using Action-Policy Testing in RL to Reduce the Number of Bugs
Hasan Ferit Eniser, Songtuan Lin, Nicola Müller, Anastasia Isychev, Valentin Wüstholz, Isabel Valera, Jörg Hoffmann and Maria Christakis
Hierarchical DeepPruner: A Novel Framework for Search Space Reduction
Ankur Nath and Alan Kuhnle
Efficient Primal Heuristics for Mixed Binary Quadratic Programs Using Suboptimal Rounding Guidance
Weimin Huang, Natalie Isenberg, Ján Drgoňa, Draguna Vrabie and Bistra Dilkina
Sub-microsecond grid path planning, at what cost?
Mark Carlson, Daniel Harabor and Peter J. Stuckey
16:15 – 17:30
  Thursday Afternoon
SoCS
Spotlights 2
JMS 743
LSRP*: Scalable and Anytime Planning for Multi-Agent Path Finding with Asynchronous Actions (Extended Abstract)
Shuai Zhou, Shizhe Zhao, Zhongqiang Ren
Suboptimal Search with Dynamic Distribution of Suboptimality (Extended Abstract)
Mohammadreza Hami, Nathan Sturtevant
Surrogate-Assisted Monte-Carlo Tree Search in Facility Location and Beyond (Extended Abstract)
Saeid Amiri, Danial Dervovic, Parisa Zehtabi, Michael Cashmore
Hierarchical Seating Allocation (Extended Abstract)
Anton Ipsen, Michael Cashmore, Parisa Zehtabi, Nicolas Marchesotti, Kirsty Fielding, Daniele Magazzeni, Manuela Veloso
Critical Section Macros - New Results (Extended Abstract)
Lukáš Chrpa, Mauro Vallati
RAILGUN: A Unified Convolutional Policy for Multi-Agent Path Finding Across Different Environments and Tasks (Extended Abstract)
Yimin Tang, Xiao Xiong, Jingyi Xi, Jiaoyang Li, Erdem Bıyık, Sven Koenig
Uncertainty in Real-World Vehicle Routing (Extended Abstract)
Václav Sobotka, Hana Rudová
BLAST: Bit-Blasting Numbers for Classical Planning (Extended Abstract)
Luigi Bonassi, Francesco Percassi, Enrico Scala
Learning Heuristic Functions with Graph Neural Networks for Numeric Planning (Extended Abstract)
Valerio Borelli, Alfonso Emilio Gerevini, Enrico Scala, Ivan Serina
Bidirectional Bounded-Suboptimal Heuristic Search with Consistent Heuristics (Extended Abstract)
Shahaf Shperberg, Natalie Morad, Lior Siag, Ariel Felner, and Dor Atzmon
SoCS
Posters 2
JMS Foyer
Each Spotlights 2 talk will also have a poster.
 
A Preprocessing Framework for Efficient Approximate Bi-Objective Shortest-Path Computation in the Presence of Correlated Objectives
Yaron Halle, Ariel Felner, Sven Koenig and Oren Salzman
Finding All Optimal Solutions in Multi-Agent Path Finding
Shahar Bardugo, Daniel Koyfman and Dor Atzmon
Reevaluation of Large Neighborhood Search for MAPF: Findings and Opportunities
Jiaqi Tan, Yudong Luo, Jiaoyang Li and Hang Ma
A Problem with the Current Methodology for Comparing Search Algorithms and a Proposed Solution
Vidal Alcázar, Michael Barley, Natasha de Kriek, Santiago Franco, Angel Garcia-Olaya, Tim Hartill, Patricia Riddle, Chris Triggs and Henry Zwart
Minimizing Fuel in Multi-Agent Pathfinding
Daniel Koyfman, Dor Atzmon, Shahaf Shperberg and Ariel Felner
Should Multi-Agent Path Finding Algorithms Coordinate Target Arrival Times?
Jonathan Morag, Noy Gabay, Daniel Koyfman and Roni Stern
Real-Time LaCAM for Real-Time MAPF
Runzhe Liang, Rishi Veerapaneni, Daniel Harabor, Jiaoyang Li and Maxim Likhachev
A Bucket-Based Priority Queue for Bounded-suboptimal and Anytime A* Search
Garrett Fereday and Eric Hansen
Heuristics for Bounded-Suboptimal Search
Lior Siag, Ariel Felner and Shahaf S. Shperberg
Lazy Heuristic Search for Solving POMDPs with Expensive-to-Compute Belief Transitions
Muhammad Suhail Saleem, Rishi Veerapaneni and Maxim Likhachev
New Mechanisms in Flex Distribution for Bounded Suboptimal Multi-Agent Path Finding
Shao-Hung Chan, Thomy Phan, Jiaoyang Li and Sven Koenig
Augmenting Exploration with Locally Greedy Probes
Dawson Brown and Rick Valenzano
Sorting Colored Balls in Colored Tubes
Ernst Althaus, Markus Blumenstock, Nick Rassau, Felix Martin Schuhknecht and Anton Quentin Zimdars