Schedule
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
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?
11:00 – 11:20
From MBQI to Enumerative Instantiation and Back
11:20 – 11:40
Being polite is not enough (and other limits of theory combination)
11:40 – 12:00
A Few Exercises on the Complexity of Congruence Closure with Cardinality Constraints
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
11:20 – 11:27
Practically Feasible Proof Logging for Pseudo-Boolean Optimization
11:30 – 11:39
Certified Implicit Hitting Set Solving with Local Search for Pseudo-Boolean Optimization
11:39 – 11:57
Efficient Certified Reasoning for Binarized Neural Networks
12:00 – 12:09
Proof logging the Generalized Totalizer Encoding
12:09 – 12:27
ExCoS
ExCoS 1
JMS 743
Welcome
10:50 – 11:00
Proving and Explaining the Equivalence of Constraint Formulations
11:00 – 11:22
Explaining SAT Solving Using Causal Reasoning
11:22 – 11:45
Using Certifying Constraint Solvers for Generating Step-Wise Explanations
11:45 – 12:07
Counterfactual Explanations for Unsatisfiable Producer/Consumer Problems
12:07 – 12:30
ML4SP
ML4SP Workshop
JMS 630
Machine Learning Guidance for an Automatic Theorem Prover
11:00 – 11:45
Automated Streamliner Selection via Algorithm Configuration and Selection
11:45 – 12:30
12:30 – 13:30
All
Lunch
JMS Foyer
13:30 – 15:00
SMT
SMT 3: Theories
JMS 641
Evaluating Binary Polynomials using Subpolynomials
13:30 – 14:00
Satisfiability Modulo Exponential Integer Arithmetic
14:00 – 14:20
Constraint Propagation for Bit-Vectors in Alt-Ergo
14:20 – 14:40
Boosting MCSat Modulo Nonlinear Integer Arithmetic via Local Search
14:40 – 15:00
DP
Invited Talk
JMS 745
How Not To Do It
13:30 – 14:30
DP
CP / SAT Doctoral Programme 2
JMS 745
Certified Grounding of Extensions of First-Order Logic
14:30 – 14:48
ExCoS
ExCoS 2
JMS 743
Creating Pen and Paper Puzzles with a Unique Solution
13:30 – 13:52
Understanding How Players Solve Puzzles
13:52 – 14:15
Preference Elicitation for Explanations in Logic Puzzles
14:15 – 14:37
Explanations for Planning via CSP: Application to a Concrete Use Case
14:37 – 15:00
ML4SP
ML4SP Workshop
JMS 630
Machine Learning for Quantifiers
13:30 – 14:15
Applying Machine Learning to Improve SAT Solvers: Some Highlights
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
15:30 – 15:50
Space Explanations of Neural Network Classification
15:30 – 16:10
Approximate SMT Counting Beyond Discrete Domains
16:10 – 16:30
Syntax-Guided Synthesis with CounterExample Guided E-graphs: A Work-In-Progress Report
16:30 – 16:50
On Writing SMT-LIB Scripts: Metrics and a new Dataset
16:50 – 17:10
DP
CP / SAT Doctoral Programme 3
JMS 745
Analyzing Self-stabilization of Synchronous Unison via Propositional Satisfiability
15:30 – 15:39
An Evaluation of Constraint-Based Approaches to Cumulative Scheduling with Delays
15:39 – 15:57
Optimizing 2D Cutting: A Bin Packing Approach to Minimize Scraps and Maximize their Reusability
16:00 – 16:09
Improved Energetic Reasoning Checker for Cumulative Constraint with Profile
16:09 – 16:27
Exact Methods for the Travelling Salesperson Problem with Self-Deleting Graphs
16:30 – 16:39
Preemptive jobshop scheduling with maximum workload constraints
16:39 – 16:57
ExCoS
ExCoS 3
JMS 743
A Framework for Data-driven Explainability in Mathematical Optimization
15:30 – 15:52
Explanations for Hierarchical Neuro-Symbolic AI
15:52 – 16:15
Explaining Mismatches in Expected versus Perceived Behavior for Interacting Digital Systems
16:15 – 16:37
Explainable Rational Synthesis in Multi-Agent Systems
16:37 – 17:00
ML4SP
ML4SP Workshop
JMS 630
ML-guided search for Mixed Integer Linear Programming
15:30 – 16:15
Panel
16:15 – 17:00
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
09:00 – 10:00
SMT
SMT 5: Optimization Modulo Theory
BO LT1
An Optimization Modulo Theories-based Approach to Cumulative Scheduling with Delays
10:00 – 10:30
DP
CP / SAT Doctoral Programme 4
JMS 745
Machine Learning Model for Selecting Assignments of Variables for SAT Problems
09:00 – 09:18
Dependency-Curated Large Neighbourhood Search
09:18 – 09:27
Do LLMs Understand Constraint Programming? Zero-Shot Constraint Programming Model Generation Using LLMs
09:30 – 09:48
Transformer-based Feature Learning for Algorithm Selection in Combinatorial Optimisation
09:48 – 09:57
Approximate SMT Counting Beyond Discrete Domains
10:00 – 10:18
Learning to Bound for Maximum Common Subgraph Algorithms
10:18 – 10:27
ModRef
Invited Talk
JMS 743
Automated Reasoning in Discrete Geometry: Discovery, Verification, and Symmetry
09:00 – 10:00
ModRef
ModRef 1
JMS 743
Machine Learning Model for Selecting Assignments of Variables for SAT Problems
10:00 – 10:15
STRIPS-2-DyPDL: Translating Automated Planning Problems into Domain-Independent Dynamic Programming Problems
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
10:00 – 10:30
LLM-Solve
Invited Talk
WMB Yudowitz
Neurosymbolic CP
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
09:40 – 10:05
Automated Constraint Model Modification with Large Language Models
10:05 – 10:30
QBF
QBF 1
WMB Gannochy
Welcome
09:00 – 09:05
Quantified Integer Programming --- a tutorial
09:05 – 09:50
Computationally Hard Problems Are Hard for QBF Proof Systems Too
09:50 – 10:10
Model Counting for Dependency Quantified Boolean Formulas
10:10 – 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
11:00 – 11:20
A Conjecture Regarding SMT Instability
11:20 – 11:40
A Catalog of SMT-LIB Benchmarks
11:40 – 12:00
A Proposal for an OMT Extension to SMT-LIB
12:00 – 12:20
DP
Invited Talk
JMS 745
In the Reviewer’s Eye
11:00 – 12:00
DP
CP / SAT Doctoral Programme 5
JMS 745
Circuit Learning for Boolean Satisfiability Problem
12:00 – 12:18
ModRef
ModRef 2
JMS 743
Undefinedness in Planning with Arrays
11:00 – 11:25
Asymptotically Smaller Encodings for Graph Problems and Scheduling
11:25 – 11:50
Declarative pearl: I put a SAT solver in your SAT solver so you can find backdoors slowly
11:50 – 12:05
Evaluating the Impact of Encoding on SAT Based Constraint Solving in Exchequer
12:05 – 12:20
PoS
Pragmatics of SAT 2 (Optimization)
BO LT2
Certifying Pareto Optimality in Multi-Objective Maximum Satisfiability
11:00 – 11:30
Improving Watched Pseudo-Boolean Propagation with Significant Literals
11:30 – 12:00
Ordered Objectives in MaxSAT
12:00 – 12:30
LLM-Solve
LLMs and Solvers
WMB Yudowitz
LLMs as Translators, Not Thinkers: Structured Output Enables Stronger NP-Hard Problem Solving
11:00 – 11:30
HiGHS-MCP: Enabling Large Language Models to Solve Optimization Problems with HiGHS
11:30 – 12:00
From Portfolio Solvers to Agentic Solvers
12:00 – 12:30
QBF
QBF 2
WMB Gannochy
Breaking Symmetries in Quantified Graph Search: A Comparative Study
11:00 – 11:20
Graph Choosability via SAT: Beyond the Nullstellensatz
11:20 – 11:40
PyQBF: A Python Framework for Solving Quantified Boolean Formulas
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
11:10 – 11:40
Numerical Considerations in Weighted Model Counting
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
13:30 – 13:50
SMT-COMP presentation
13:50 – 14:00
DP
CP / SAT Doctoral Programme 6
JMS 745
Problem Partitioning via Proof Prefixes
13:30 – 13:39
Workload Balancing in a Food Distribution Center Comparing Constraint Programming and Mixed-Integer Linear Programming
13:39 – 13:57
Streamlining Distributed SAT Solver Design
14:00 – 14:09
Beyond Core-Guided MaxSAT
14:09 – 14:27
Enumerating All Boolean Matches
14:30 – 14:39
MaxSAT and pseudo-Boolean Solutions for the Multi-Skill Project Scheduling Problem
14:39 – 14:57
ModRef
ModRef 3
JMS 743
Solver-Aided Expansion of Loops to Avoid Generate-and-Test
13:30 – 13:55
Integer Linear Programming Techniques for Enhancing Branch and Bound MaxSAT Solvers
13:55 – 14:20
Modeling the p-Dispersion Problem with Distance Constraints
14:20 – 14:45
Mutual B refinements as a justification for constraints model reformulations
14:45 – 15:00
PoS
Pragmatics of SAT 3 (SAT)
BO LT2
Conflict-Driven SAT Solving using XOR-OR-AND Normal Forms
13:30 – 14:00
Revisiting Clause Vivification
14:00 – 14:30
Incremental Inprocessing Rules beyond Resolution
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
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
14:10 – 14:35
LLM-as-a-Judge For Combinatorial Optimization Modelisations from Natural Language
14:35 – 15:00
PTHG
PTHG Workshop
WMB Gannochy
Progress towards the Holy Grail: Solving
14:15 – 15:00
MC
Model Counting 2
WMB Hugh Fraser
Cara: An Isomorphism-Based #SAT Solver
13:30 – 14:00
Surveying the Model Counting Competition 2025
14:00 – 14:30
Towards Real-Time Approximate Counting
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
15:30 – 16:15
Business Meeting
16:15 – 17:00
DP
CP / SAT Doctoral Programme 7
JMS 745
Integer Linear Programming Preprocessing for Maximum Satisfiability
15:30 – 15:48
Fine-Grained Complexity Analysis of Dependency Quantified Boolean Formulas
15:48 – 15:57
Symmetry Breaking in the Subgraph Isomorphism Problem
16:00 – 16:18
Reencoding Unique Literal Clauses
16:18 – 16:27
Modelling Multi-dimensional Arrays in Unified Planning
16:30 – 16:48
Learn to Unlearn
16:48 – 16:57
ModRef
ModRef 4
JMS 743
Modeling the Inglenook Shunting Puzzle
15:30 – 15:55
A new Constraint Programming model for the Multiple Constant Multiplication
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
15:30 – 16:00
Certified Implicit Hitting Set Solving with Local Search for Pseudo-Boolean Optimization
16:00 – 16:30
Faster Certified Symmetry Breaking using Orders with Auxiliary Variables
16:30 – 17:00
LLM-Solve
Benchmarking LLMs
WMB Yudowitz
Benchmarking LLMs for CP model generation
15:30 – 16:00
PTHG
PTHG Workshop
WMB Gannochy
ML-guided and Robust Constraint Acquisition
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 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
09:30 – 10:30
10:30 – 11:00
All
Coffee Break
JMS Foyer
11:00 – 12:30
CP A
Applications 1
BO LT1
Jimmy Lee
11:00 – 11:30
11:30 – 12:00
CP B
Solver Tuning / Selection / Parallelisation
JMS 745
Laurent Michel
11:00 – 11:30
11:30 – 12:00
SoCS
Best Paper
JMS 743
SoCS
Multi-Agent Pathfinding 1
JMS 743
Jiří Švancara
11:20 – 11:40
11:40 – 12:00
SAT
QBF
BO LT2
Clemens Hofstadler
11:00 – 11:30
11:30 – 12:00
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
Michael Codish
14:00 – 14:30
CP B
Applications 2
JMS 745
Hélène Verhaeghe
SoCS
Tutorial
JMS 743
Hana Rudová
Heuristic Search vs. Constraint Programming for Single Machine Scheduling
14:00 – 15:00
SAT
Tool and Short Papers
BO LT2
Daniel Le Berre
14:00 – 14:20
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
CP B
Tutorial
JMS 745
Modelling for Scheduling and Rostering Problems with Constraint Programming
15:30 – 17:00
SoCS
Single Agent Motion Planning
JMS 743
Oren Salzman
SoCS
Satisfiability
JMS 743
Rishi Veerapaneni
SAT
Sampling and Model Counting
BO LT2
Johannes Fichte
15:30 – 16:00
16:00 – 16:30
16:30 – 17:00
19:00 – 20:30
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
10:00 – 10:30
All
Coffee Break
JMS Foyer
10:30 – 12:00
CP A
Best Papers
BO LT1
Maria Garcia de la Banda
SoCS
Heuristic Search 1
JMS 743
Rick Valenzano
10:50 – 11:10
11:10 – 11:30
11:30 – 11:50
SAT
Lots of Solutions
BO LT2
Stefan Szeider
10:30 – 11:00
11:00 – 11:30
12:00 – 13:30
All
Lunch
JMS Foyer
13:30 – 15:00
CP A
Modelling Languages / Interfaces
BO LT1
Özgür Akgün
13:30 – 14:00
14:30 – 15:00
CP B
Tutorial
JMS 745
Parallel Constraint Solving
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
13:30 – 14:30
SoCS
Best Student Paper
JMS 743
Maxim Likhachev
14:30 – 14:50
SoCS
Heuristic Search 2
JMS 743
Maxim Likhachev
14:50 – 15:00
SAT
Pseudo-Boolean and Bit-Vectors
BO LT2
Marc Vinyals
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
15:30 – 16:00
16:00 – 16:30
16:30 – 17:00
17:00 – 17:30
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
10:30 – 11:00
ACP ECR Award
11:00 – 11:30
ACP Doctoral Research Award
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
10:30 – 10:50
10:50 – 11:00
11:10 – 11:20
SAT
MaxSAT
BO LT2
Matti Järvisalo
11:00 – 11:30
12:00 – 13:00
All
Lunch
JMS Foyer
13:00 – 15:10
CP A
Competitions
BO LT1
13:00 – 13:30
CP A
Applications 3
BO LT1
Helmut Simonis
14:05 – 14:35
CP B
Constraints / QIP / Core-Boosted LS
JMS 745
Louis-Martin Rousseau
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
13:30 – 14:30
SoCS
Heuristic Search 3
JMS 743
Mauro Vallati
14:30 – 14:50
SoCS
Extra Coffee
JMS Foyer
15:00 – 15:10
SAT
Short Talks 1
BO LT2
Marijn Heule
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
15:30 – 16:00
CP B
Learning Solvers
JMS 745
Tias Guns
15:30 – 16:00
16:30 – 17:00
SoCS
Spotlights 2
JMS 743
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
09:00 – 09:30
CP B
Applications 5
JMS 745
Christine Solnon
09:30 – 10:00
SoCS
Heuristic Search 4
JMS 743
Nathan Sturtevant
09:20 – 09:40
SAT
Short Talks 2
JMS 641
Katalin Fazekas
09:20 – 09:40
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
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
11:30 – 12:00
CP B
Coffee Break
JMS Foyer
10:30 – 11:00
CP B
Search
JMS 745
Ian Gent
11:00 – 11:30
12:00 – 12:30
SoCS
Learning and Search
JMS 743
Shahaf Shperberg
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
11:00 – 11:30
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)
Multi-Agent Path Finding for Schedule Constrained Automation (Extended Abstract)
Object Packing and Scheduling for Sequential 3D Printing: A Linear Arithmetic Model and a CEGAR-Inspired Optimal Solver (Extended Abstract)
You May Split but You Might Work It Out Later: First Steps Toward Merging Nodes in MAPF (Extended Abstract)
Bidirectional Heuristic Search in Longest Path Problems (Extended Abstract)
Prioritised Planning with Guarantees
New Directions in Bidirectional Search (Student Abstract)
Binarized Nested Rollout Policy Adaptation for the Optimization of the Grain Boundary Problem
Multi-Agent Path Finding: Policies Instead of Plans
Independence Detection in SAT-based MAPF under Time Uncertainty
A Formalism for Optimal Search with Dynamic Heuristics
15:30 – 16:15
SoCS
Posters 1
JMS Foyer
Each Spotlights 1 talk will also have a poster.
Real-time Cost-algebraic Heuristic Search
Bi-Objective Search for the Traveling Salesman Problem with Time Windows and Vacant Penalties
Lightweight and Effective Preference Construction in PIBT for Large-Scale Multi-Agent Pathfinding
From Agent Centric to Obstacle Centric Planning: A Makespan-Optimal Algorithm for the Multi-Agent Warehouse Rearrangement Problem
Guiding the Search for the Euclidean Shortest Path Problem
A Conflict-Driven Approach for Reaching Goals Specified with Negation as Failure
Decoupling Generation and Evaluation for Parallel Greedy Best-First Search
Using Action-Policy Testing in RL to Reduce the Number of Bugs
Hierarchical DeepPruner: A Novel Framework for Search Space Reduction
Efficient Primal Heuristics for Mixed Binary Quadratic Programs Using Suboptimal Rounding Guidance
Sub-microsecond grid path planning, at what cost?
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)
Suboptimal Search with Dynamic Distribution of Suboptimality (Extended Abstract)
Surrogate-Assisted Monte-Carlo Tree Search in Facility Location and Beyond (Extended Abstract)
Hierarchical Seating Allocation (Extended Abstract)
Critical Section Macros - New Results (Extended Abstract)
RAILGUN: A Unified Convolutional Policy for Multi-Agent Path Finding Across Different Environments and Tasks (Extended Abstract)
Uncertainty in Real-World Vehicle Routing (Extended Abstract)
BLAST: Bit-Blasting Numbers for Classical Planning (Extended Abstract)
Learning Heuristic Functions with Graph Neural Networks for Numeric Planning (Extended Abstract)
Bidirectional Bounded-Suboptimal Heuristic Search with Consistent Heuristics (Extended Abstract)
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
Finding All Optimal Solutions in Multi-Agent Path Finding
Reevaluation of Large Neighborhood Search for MAPF: Findings and Opportunities
A Problem with the Current Methodology for Comparing Search Algorithms and a Proposed Solution
Minimizing Fuel in Multi-Agent Pathfinding
Should Multi-Agent Path Finding Algorithms Coordinate Target Arrival Times?
Real-Time LaCAM for Real-Time MAPF
A Bucket-Based Priority Queue for Bounded-suboptimal and Anytime A* Search
Heuristics for Bounded-Suboptimal Search
Lazy Heuristic Search for Solving POMDPs with Expensive-to-Compute Belief Transitions
New Mechanisms in Flex Distribution for Bounded Suboptimal Multi-Agent Path Finding
Augmenting Exploration with Locally Greedy Probes
Sorting Colored Balls in Colored Tubes