DRAFT Schedule

This schedule is a work in progress. Please take a look and report any errors (but requests to have your talk moved will need to go to the relevant conference or workshop chairs instead). However, this is all subject to change, and in particular some of the rooms might switch around based upon estimated attendance.

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

Sunday 10th August   ▶
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.
09:00 – 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
ExCoS
ExCoS Workshop
JMS 430
ML4SP
ML4SP Workshop
JMS 630
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
JMS 745
ExCoS
ExCoS Workshop
JMS 430
ML4SP
ML4SP Workshop
JMS 630
12:30 – 13:30
All
Lunch
JMS Foyer
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
CP / SAT Doctoral Programme
JMS 745
ExCoS
ExCoS Workshop
JMS 430
ML4SP
ML4SP Workshop
JMS 630
15:00 – 15:30
All
Coffee Break
JMS Foyer
15:30 – 17:30
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
JMS 745
ExCoS
ExCoS Workshop
JMS 430
ML4SP
ML4SP Workshop
JMS 630
◀   Monday 11th August   ▶
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 + Optimization Modulo Theory
BO LT1
Invited Talk: SAT Reasoning in CDCL(T) Solvers
Katalin Fazekas
09:00 – 10:00
An Optimization Modulo Theories-based Approach to Cumulative Scheduling with Delays
Antton Kasslin
10:00 – 10:30
DP
CP / SAT Doctoral Programme
JMS 745
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 Workshop
WMB Gannochy
ModRef
ModRef Workshop
JMS 743
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
10:30 – 11:00
All
Coffee Break
JMS Foyer
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
CP / SAT Doctoral Programme
JMS 745
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 Workshop
WMB Gannochy
ModRef
ModRef Workshop
JMS 743
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
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
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
JMS 745
LLM-Solve
Joint Talk with PTHG
WMB Yudowitz
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
ModRef
ModRef Workshop
JMS 743
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
MC
Model Counting 2
WMB Hugh Fraser
Cara: An Isomorphism-Based #SAT Solver
Petr Illner
13:30 – 14:00
Johannes K. Fichte, Markus Hecher and Arijit Shaw
Surveying the Model Counting Competition 2025
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
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
JMS 745
LLM-Solve
Benchmarking LLMs
WMB Yudowitz
Benchmarking LLMs for CP model generation
Kostis Michailidis, Dimos Tsouros, Tias Guns
15:30 – 16:00
LLM-Solve
Joint Panel with PTHG
WMB Yudowitz
Are LLMs the missing piece to get us to the Holy Grail?
16:00 – 17:30
PTHG
PTHG Workshop
WMB Gannochy
ModRef
ModRef Workshop
JMS 743
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
19:30 – late
◀   Tuesday 12th August   ▶
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
Privacy-preserving SAT Solving
09:30 – 10:30
10:30 – 11:00
All
Coffee Break
JMS Foyer
11:00 – 12:30
CP A
Applications 1
BO LT1
Constraint-based In-Station Train Dispatching
Andreas Schutt, Matteo Cardellini, Jip J. Dekker, Daniel Harabor, Marco Maratea, and Mauro Vallati
11:00 – 11:30
Cargo Routing Optimization in Liner Shipping Networks
Yousra El Ghazi, Djamal Habet, and Cyril Terrioux
11:30 – 12:00
Aircraft Resource-Constrained Assembly Line Balancing with Learning Effect: a Constraint Programming Approach
Duc Anh Le, Stéphanie Roussel, and Christophe Lecoutre
12:00 – 12:30
CP B
Solver Tuning / Selection / Parallelisation
JMS 745
DynamicSAT: Dynamic Configuration Tuning for SAT Solving
Zhengyuan Shi, Wentao Jiang, Xindi Zhang, Jin Luo, Yun Liang, Zhufei Chu, and Qiang Xu
11:00 – 11:30
Parallel MIP Solving with Dynamic Task Decomposition
Peng Lin, Shaowei Cai, Mengchuan Zou, and Shengqi Chen
11:30 – 12:00
Transformer-based Feature Learning for Algorithm Selection in Combinatorial Optimisation
Alessio Pellegrino, Özgür Akgün, Nguyen Dang, Zeynep Kiziltan, and Ian Miguel
12:00 – 12:30
SoCS
Best Paper
JMS 743
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
11:00 – 11:20
SoCS
Multi-Agent Pathfinding 1
JMS 743
Lightweight and Effective Preference Construction in PIBT for Large-Scale Multi-Agent Pathfinding
Keisuke Okumura and Nagai Hiroki
11:20 – 11:40
Low-Level Search on Time Intervals in Branch-and-Cut-and-Price for Multi-Agent Path Finding
Edward Lam and Peter J. Stuckey
11:40 – 12:00
New Mechanisms in Flex Distribution for Bounded Suboptimal Multi-Agent Path Finding
Shao-Hung Chan, Thomy Phan, Jiaoyang Li and Sven Koenig
12:00 – 12:20
Guiding the Search for the Euclidean Shortest Path Problem
Daniel Koch and Stefan Funke
12:20 – 12:30
SAT
QBF
BO LT2
Semi-Algebraic Proof Systems for QBF
Olaf Beyersdorff, Ilario Bonacina, Kaspar Kasche, Meena Mahajan, and Luc Spachmann
11:00 – 11:30
Better Extension Variables in DQBF via Independence
Leroy Chew and Tomáš Peitl
11:30 – 12:00
Fine-Grained Complexity Analysis of Dependency Quantified Boolean Formulas
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
14:00 – 15:00
CP A
Model Counting to the Rescue
BO LT1
Reducing Quantum Circuit Synthesis to #SAT
Dekel Zak, Jingyi Mei, Jean-Marie Lagniez, and Alfons Laarman
14:00 – 14:30
Scalable Counting of Minimal Trap Spaces and Fixed Points in Boolean Networks
Mohimenul Kabir, Van-Giang Trinh, Samuel Pastva, and Kuldeep S Meel
14:30 – 15:00
CP B
Applications 2
JMS 745
From Prediction to Action: A Constraint-Based Approach to Predictive
Younes Mechqrane and Ismail Elabbassi
14:00 – 14:30
Balancing Latin Rectangles with LLM-generated Streamliners
Florentina Voboril, Vaidyanathan Peruvemba Ramaswamy, and Stefan Szeider
14:30 – 15:00
SoCS
SoCS Tutorial 1
JMS 743
SAT
Tool and Short Papers
BO LT2
QRP+Gen: A Framework for Checking Q-Resolution Proofs with Generalized Axioms
Mark Peyrer and Martina Seidl
14:00 – 14:20
RustSAT: A Library for SAT Solving in Rust
Christoph Jabs
14:20 – 14:40
On Top-Down Pseudo-Boolean Model Counting
Suwei Yang, Yong Lai, and Kuldeep S. Meel
14:40 – 15:00
15:00 – 15:30
All
Coffee Break
JMS Foyer
15:30 – 17:00
CP A
Verification / Certification / Testing
BO LT1
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
15:30 – 16:00
An Efficient and Uniform CSP Solution Generator Generator
Ghiles Ziat and Martin Pépin
16:00 – 16:30
Guess and Prove: A Hybrid Approach to Linear Polynomial Recovery in Circuit Verification
Clemens Hofstadler and Daniela Kaufmann
16:30 – 17:00
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
Task and Motion Planning Using Infinite Completion Tree and Agnostic Skills
Matan Sudry, Tom Jurgenson and Erez Karpas
15:30 – 15:50
Lazy Heuristic Search for Solving POMDPs with Expensive-to-Compute Belief Transitions
Muhammad Suhail Saleem, Rishi Veerapaneni and Maxim Likhachev
15:50 – 16:10
SoCS
Satisfiability
JMS 743
From Scalable SAT to MaxSAT: Massively Parallel Solution Improving Search
Dominik Schreiber, Christoph Jabs and Jeremias Berg
16:10 – 16:30
Multi-armed Bandit Algorithms for the Boolean Satisfiability Problem: A Survey
Zhihui Xie, Xu Liu and Shuai Li
16:30 – 16:50
Extracting Problem Structure with LLMs for Optimized SAT Local Search
Andre Schidler and Stefan Szeider
16:50 – 17:00
SAT
Sampling and Model Counting
BO LT2
SAT-Metropolis: Combining Markov Chain Monte Carlo with SAT/SMT sampling
Maja Aaslyng Dall, Raúl Pardo, Thomas Lumley, and Andrzej Wasowski
15:30 – 16:00
Scalable Precise Computation of Shannon Entropy
Yong Lai, Haolong Tong, Zhenghang Xu, and Minghao Yin
16:00 – 16:30
Random local access for sampling k-SAT solutions
Dingding Dong and Nitya Mani
16:30 – 17:00
19:00 – 20:30
◀   Wednesday 13th August   ▶
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
All
Invited Talk: Christine Solnon
BO LT1
Anytime and exact search for planning problems: How to explore a DP-based state transition graph with A*, CP and LS?
09:00 – 10:00
10:00 – 10:30
All
Coffee Break
JMS Foyer
10:30 – 12:00
CP A
Best Papers
BO LT1
Modeling and Explaining an Industrial Workforce Allocation and Scheduling Problem
Ignace Bleukx, Ryma Bouzazouma, Tias Guns, Nadine Laage, and Guillaume Poveda
10:30 – 11:00
Transition Dominance in Domain-Independent Dynamic Programming
J. Christopher Beck, Ryo Kuroiwa, Jimmy H.M. Lee, Peter J. Stuckey, and Allen Z. Zhong
11:00 – 11:30
Symmetric Core Learning for Pseudo-Boolean Optimization by Implicit Hitting Sets
Hannes Ihalainen, Jeremias Berg, Matti Järvisalo, and Bart Bogaerts
11:30 – 12:00
SoCS
Heuristic Search 1
JMS 743
A Bucket-Based Priority Queue for Bounded-Suboptimal and Anytime A* Search
Garrett Fereday and Eric Hansen
10:30 – 10:50
Real-time Cost-algebraic Heuristic Search
Devin Wild Thomas and Wheeler Ruml
10:50 – 11:10
Sorting Colored Balls in Colored Tubes
Ernst Althaus, Markus Blumenstock, Nick Rassau, Felix Martin Schuhknecht and Anton Quentin Zimdars
11:10 – 11:30
Heuristics for Bounded-Suboptimal Search
Lior Siag, Ariel Felner and Shahaf S. Shperberg
11:30 – 11:50
Decoupling Generation and Evaluation for Parallel Greedy Best-First Search
Takumi Shimoda and Alex Fukunaga
11:50 – 12:00
SAT
Lots of Solutions
BO LT2
Enumerating All Boolean Matches
Alexander Nadel and Yogev Shalmon
10:30 – 11:00
CNFs and DNFs with exactly k solutions
L. Sunil Chandran, Rishikesh Gajjala, and Kuldeep S. Meel
11:00 – 11:30
Towards Practical First-Order Model Counting
Ananth Kidambi, Guramrit Singh, Paulius Dilkas, and Kuldeep S. Meel
11:30 – 12:00
12:00 – 13:30
All
Lunch
JMS Foyer
13:30 – 15:00
CP A
Modelling Languages / Interfaces
BO LT1
Unit Types for MiniZinc
Jip J. Dekker, Jason Nguyen, Peter J. Stuckey, and Guido Tack
13:30 – 14:00
RPID: Rust Programmable Interface for Domain-Independent Dynamic Programming
Ryo Kuroiwa and J. Christopher Beck
14:00 – 14:30
PrintTalk: A Language for Constraint-based 3D Modelling
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
When Models Meet the Real World: Lessons from Applied AI Research
Mauro Vallati
13:30 – 14:30
SoCS
Best Student Paper
JMS 743
Sub-Microsecond Grid Path Planning, at What Cost?
Mark Carlson, Daniel Harabor and Peter J. Stuckey
14:30 – 14:50
SoCS
Heuristic Search 2
JMS 743
Augmenting Exploration with Locally Greedy Probes
Dawson Brown and Rick Valenzano
14:50 – 15:00
SAT
Pseudo-Boolean and Bit-Vectors
BO LT2
Symbolic Conflict Analysis in Pseudo-Boolean Optimization
Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez Carbonell, and Rui Zhao
13:30 – 14:00
Improving Reduction Techniques in Pseudo-Boolean Conflictct Analysis
Orestis Lomis, Jo Devriendt, Hendrik Bierlee, and Tias Guns
14:00 – 14:30
Bit-precise Reasoning with Parametric Bit-vectors
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
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
15:30 – 16:15
SoCS
Posters 1
JMS Foyer
16:15 – 17:30
SAT
Synthesis and Solvers
BO LT2
Depth-Optimal Quantum Layout Synthesis as SAT
Anna B. Jakobsen, Anders B. Clausen, Jaco van de Pol, and Irfansha Shaik
15:30 – 16:00
CNOT-Optimal Clifford Synthesis as SAT
Irfansha Shaik and Jaco van de Pol
16:00 – 16:30
Streamlining Distributed SAT Solver Design
Dominik Schreiber, Niccolò Rigi-Luperti, and Armin Biere
16:30 – 17:00
Reencoding Unique Literal Clauses
Aeacus Sheng, Joseph Reeves, and Marijn Heule
17:00 – 17:30
◀   Thursday 14th August   ▶
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
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
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
SoCS
Multi-Agent Pathfinding 2
JMS 743
Minimizing Fuel in Multi-Agent Pathfinding
Daniel Koyfman, Dor Atzmon, Shahaf Shperberg and Ariel Felner
10:30 – 10:50
On Path Selection for Reduction-Based Solving of Multi-Agent Pathfinding Using Graph Pruning
Matej Husár, Jiří Švancara and Roman Barták
10:50 – 11:00
Should Multi-Agent Path Finding Algorithms Coordinate Target Arrival Times?
Jonathan Morag, Noy Gabay, Daniel Koyfman and Roni Stern
11:00 – 11:10
Real-Time LaCAM for Real-Time MAPF
Runzhe Liang, Rishi Veerapaneni, Daniel Harabor, Jiaoyang Li and Maxim Likhachev
11:10 – 11:20
Finding All Optimal Solutions in Multi-Agent Path Finding
Shahar Bardugo, Daniel Koyfman and Dor Atzmon
11:20 – 11:40
Reevaluation of Large Neighborhood Search for MAPF: Findings and Opportunities
Jiaqi Tan, Yudong Luo, Jiaoyang Li and Hang Ma
11:40 – 12:00
SAT
MaxSAT
BO LT2
Analyzing Reformulation Performance in Core-Guided MaxSAT Solving
Andre Schidler and Stefan Szeider
10:30 – 11:00
Redundancy rules for MaxSAT
Ilario Bonacina, María-Luisa Bonet, Sam Buss and Massimo Lauria
11:00 – 11:30
Core-Guided Linear Programming-based Maximum Satisfiability
George Katsirelos
11:30 – 12:00
12:00 – 13:00
All
Lunch
JMS Foyer
13:00 – 15:10
CP A
More Lunch
JMS Foyer
13:00 – 13:30
CP A
Applications 3
BO LT1
Multi-League Sports Scheduling with Team Interdependencies: An Optimization Model
Nils Weidmann
13:30 – 14:00
Optimizing 2D Cutting: A Bin Packing Approach to Minimize Scraps and Maximize their Reusability
Manuel Chastenay, Xavier Zwingmann, Claude-Guy Quimper, and Jonathan Gaudreault
14:00 – 14:30
Modeling and Solving a Composite Structure Design Problem with Constraint Programming
Miguel Antoons, Augustin Delecluse, Samih Zein, and Pierre Schaus
14:30 – 15:00
CP A
Extra Coffee
JMS Foyer
15:00 – 15:10
CP B
More Lunch
JMS Foyer
13:00 – 13:30
CP B
Constraints / QIP / Core-Boosted LS
JMS 745
SLS-Enhanced Core-Boosted Linear Search for Anytime Maximum Satisfiability
Ole Lübke and Jeremias Berg
13:30 – 14:00
Unite and Lead: Finding Disjunctive Cliques for Scheduling Problems
Konstantin Sidorov, Imko Marijnissen, and Emir Demirović
14:00 – 14:30
An Expansion-Based Approach for Quantified Integer Programming
Michael Hartisch and Leroy Chew
14:30 – 15:00
CP B
Extra Coffee
JMS Foyer
15:00 – 15:10
SoCS
More Lunch
JMS Foyer
13:00 – 13:30
SoCS
SoCS Tutorial 2
JMS 743
13:30 – 14:30
SoCS
Heuristic Search 3
JMS 743
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
14:30 – 14:50
Position Paper: On the Impact of Direction-Selection in BAE*
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
Bridging Language Models and Symbolic Solvers via the the Model Context Protocol
Stefan Szeider
13:00 – 13:20
SAT
Awards
BO LT2
13:20 – 14:20
SAT
PBO and MC Competitions
BO LT2
14:20 – 15:10
15:10 – 15:30
All
Coffee Break
JMS Foyer
15:30 – 17:30
CP A
Applications 4
BO LT1
The Work Task Variation Problem
Mikael Z. Lagerkvist and Magnus Rattfeldt
15:30 – 16:00
Solving the Agile Earth Observation Satellite Scheduling Problem with CP and Constraint-Based Local Search
Valentin Antuori, Damien T. Wojtowicz, and Emmanuel Hebrard
16:00 – 16:30
Scheduling Telescope Observations for the European Southern Observatory
Michael Prümm, Peter Nightingale, and Felix Ulrich-Oltean
16:30 – 17:00
CP B
Learning Solvers
JMS 745
Conflict Analysis Based on Cutting Planes for Constraint Programming
Robbin Baauw, Maarten Flippo, and Emir Demirović
15:30 – 16:00
Disjunctive Scheduling in Tempo
Emmanuel Hebrard
16:00 – 16:30
Towards Modern and Modular SAT for LCG
Jip J. Dekker, Alexey Ignatiev, Peter J. Stuckey, and Allen Z. Zhong
16:30 – 17:00
SoCS
Spotlights 2
JMS 743
15:30 – 16:15
SoCS
Posters 2
JMS Foyer
16:15 – 17:30
SAT
SAT Competition
BO LT2
15:30 – 16:00
SAT
SAT General Assembly
BO LT2
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
Breaking Symmetries with Involutions
Michael Codish and Mikolas Janota
09:00 – 09:30
BFS-based canonical codes for generating graphs with CP
Xiao Peng and Christine Solnon
09:30 – 10:00
CP B
Applications 5
JMS 745
Analysing Self-stabilization of Synchronous Unison via Propositional Satisfiability
Asma Khoualdia, Sami Cherif, Stéphane Devismes, and Léo Robert
09:00 – 09:30
Constraint Models for Klondike
Nguyen Dang, Ian P. Gent, Peter Nightingale, Felix Ulrich-Oltean, and Jack Waller
09:30 – 10:00
SoCS
Heuristic Search 4
JMS 743
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
09:00 – 09:20
Bi-Objective Search for the Traveling Salesman Problem with Time Windows and Vacant Penalties
Shizhe Zhao, Yancheng Wu and Zhongqiang Ren
09:20 – 09:40
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
09:40 – 10:00
SAT
Short Talks 2
BO LT2
An application of SAT solvers in Integer Programming Games
Pravesh Koirala, Aditya Shrey, and Forrest Laine
09:00 – 09:20
Learn to Unlearn
Bernhard Gstrein, Florian Pollitt, André Schidler, Mathias Fleury, and Armin Biere
09:20 – 09:40
SAT-based CEGAR Method for the Hamiltonian Cycle Problem Enhanced by Cut-Set Constraints
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
BO LT2
An Algebraic Approach to MaxCSP
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
Exact Methods for the Travelling Salesperson Problem with Self-Deleting Graphs
Daniel Pekar and J. Christopher Beck
11:00 – 11:30
The 3-Decomposition Conjecture: A SAT-Based Approach with Specialized Propagators
Tianwei Zhang and Stefan Szeider
11:30 – 12:00
Greed is slow on sparse graphs of oriented valued constraints.
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
Dependency-Curated Large Neighbourhood Search
Frej Knutar Lewander, Pierre Flener, and Justin Pearson
11:00 – 11:30
Understanding the Impact of Value Selection Heuristics in Scheduling Problems
Tim Luchterhand, Emmanuel Hebrard, and Sylvie Thiebaux
11:30 – 12:00
Learning to Bound for Maximum Common Subgraph Algorithms
Buddhi W. Kothalawala, Henning Koehler, and Qing Wang
12:00 – 12:30
SoCS
Learning and Search
JMS 743
Hierarchical DeepPruner: A Novel Framework for Search Space Reduction
Ankur Nath and Alan Kuhnle
10:30 – 10:50
A Conflict-Driven Approach for Reaching Goals Specified with Negation as Failure
Forest Agostinelli
10:50 – 11:10
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
11:10 – 11:20
SoCS
SoCS Community Meeting
JMS 743
11:20 – 12:30
SAT
Coffee Break
JMS Foyer
10:30 – 11:00
SAT
SAT Talks
BO LT2
Certifying Projected Knowledge Compilation
Randal Bryant, Yong Kiam Tan, and Marijn Heule
11:00 – 11:30
Efficient Certified Reasoning for Binarized Neural Networks
Jiong Yang, Yong Kiam Tan, Mate Soos, Magnus O. Myreen, and Kuldeep S. Meel
11:30 – 12:00
Problem Partitioning via Proof Prefixes
Zachary Battleman, Joseph Reeves, and Marijn Heule
12:00 – 12:30
12:30 – 12:50
All
Closing
BO LT1
12:30 – 12:50
12:50 – 14:00
All
Packed Lunch (Stay and Socialise, or Take Away)
JMS Foyer