Arrow Research search

Author name cluster

Peter J. Stuckey

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

103 papers
2 author rows

Possible papers

103

AAMAS Conference 2026 Conference Paper

Flow-Based Task Assignment for Large-Scale Online Multi-Agent Pickup and Delivery

  • Yue Zhang
  • Zhe Chen
  • Daniel Harabor
  • Pierre Le Bodic
  • Peter J. Stuckey

We study the online Multi-Agent Pickup and Delivery (MAPD) problem, where a team of agents must repeatedly serve dynamically appearing tasks on a shared map. Existing methods either rely on simple heuristics, which result in poor decisions, or employ complex reasoning, which suffers from limited scalability under real-time constraints. In this work, we focus on the task assignment subproblem and formulate it as a minimum-cost flow over the environment graph. This eliminates the need for pairwise distance computations and allows agents to be simultaneously assigned to tasks and routed toward them. The resulting flow network also supports guide path extraction which accelerates planning under real-time constraints. This approach supports real-time execution and scales to 20, 000 agents and 30, 000 tasks within 1-second planning time, outperforming existing works in terms of computational efficiency, assignment quality and scalability.

AAAI Conference 2025 Short Paper

Acoustic-to-Hyper-Spectral: Hyper-Spectral Image Construction from Frequency Spectrums Through Simulated Annealing (Student Abstract)

  • Ruth-Emely Pierau
  • Alaster Meehan
  • Hamid Rezatofighi
  • Peter J. Stuckey

This abstract presents a simulated annealing based approach that constructs hyper-spectral images from the frequency spectrums of a distributed acoustic sensing system and iteratively improves them through the training of learnable filters. The aim is to construct an image that represents features of signals from events while repressing noise. Hyper-spectral images are specifically created for downstream computer vision tasks such as object detection. Hyper-spectral images are images with more than three channels that are derived from a frequency spectrum to obtain the spectrum for each image pixel. Simulated annealing is used to train the filters to automatically select frequencies and bin them into frequency bands. Each frequency band is mapped into an image channel. We fully integrate our filtering method with an object detection network so that filters are trained in conjunction with the neural network. The detection model serves as both the measure and the selector. Our simulated annealing approach significantly outperforms current state-of-the-art methods by a margin of 22%. Limitations include a dependency on randomness and excluding parts of the search space prematuraly due to the design of the local moves.

AAAI Conference 2025 Conference Paper

Concurrent Planning and Execution in Lifelong Multi-Agent Path Finding with Delay Probabilities

  • Yue Zhang
  • Zhe Chen
  • Daniel Harabor
  • Pierre Le Bodic
  • Peter J. Stuckey

In multi-agent systems, when we account for the possibility of delays during execution, online planning becomes more complicated, as both execution and planning should be able to handle delays when agents are moving. Lifelong Multi-Agent Path Finding (LMAPF) is the problem of (re)planning the collision-free moves of agents to their goals in a shared space, while agents continuously receive new goals. PIE (Planning and Improving while Executing) is a recent approach to LMAPF which concurrently replans later parts of agents' trajectories while execution occurs. However, the execution is assumed to be perfect. Existing approaches either use policy-based methods to quickly coordinate agents every timestep with instant delay feedback, or deploy an execution policy to adjust a solution for delays on the fly. These approaches may introduce large amounts of unnecessary delays to agents due to their planner guarantees or simple delay-handling policies. In this paper, we extend PIE to define a framework for solving the lifelong MAPF problem with execution delays. We instantiate our framework with different execution and replanning strategies, and experimentally evaluate them. Overall, we find that this framework can substantially improve the throughput by up to a factor 3 for lifelong MAPF, compared to approaches that handle delays with simple execution policies.

IJCAI Conference 2025 Conference Paper

Dynamic Replanning for Improved Public Transport Routing

  • Abdallah Abuaisha
  • Bojie Shen
  • Daniel D. Harabor
  • Peter J. Stuckey
  • Mark Wallace

Delays in public transport are common, often impacting users through prolonged travel times and missed transfers. Existing solutions for handling delays remain limited; backup plans based on historical data miss opportunities for earlier arrivals, while snapshot planning accounts for current delays but not future ones. With the growing availability of live delay data, users can adjust their journeys in real-time. However, the literature lacks a framework that fully exploits this advantage for system-scale dynamic replanning. To address this, we formalise the dynamic replanning problem in public transport routing and propose two solutions: a "pull" approach, where users manually request replanning, and a novel "push" approach, where the server proactively monitors and adjusts journeys. Our experiments show that the push approach outperforms the pull approach, achieving significant speedups. The results also reveal substantial arrival time savings enabled by dynamic replanning.

IJCAI Conference 2025 Conference Paper

Most General Explanations of Tree Ensembles

  • Yacine Izza
  • Akexey Ignatiev
  • Sasha Rubin
  • Joao Marques-Silva
  • Peter J. Stuckey

Explainable Artificial Intelligence (XAI) is critical for attaining trust in the operation of AI systems. A key question of an AI system is ``why was this decision made this way''. Formal approaches to XAI use a formal model of the AI system to identify abductive explanations. While abductive explanations may be applicable to a large number of inputs sharing the same concrete values, more general explanations may be preferred for numeric inputs. So-called inflated abductive explanations give intervals for each feature ensuring that any input whose values fall withing these intervals is still guaranteed to make the same prediction. Inflated explanations cover a larger portion of the input space, and hence are deemed more general explanations. But there can be many (inflated) abductive explanations for an instance. Which is the best? In this paper, we show how to find a most general abductive explanation for an AI decision. This explanation covers as much of the input space as possible, while still being a correct formal explanation of the model's behaviour. Given that we only want to give a human one explanation for a decision, the most general explanation gives us the explanation with the broadest applicability, and hence the one most likely to seem sensible.

AAAI Conference 2025 Conference Paper

Online Guidance Graph Optimization for Lifelong Multi-Agent Path Finding

  • Hongzhi Zang
  • Yulun Zhang
  • He Jiang
  • Zhe Chen
  • Daniel Harabor
  • Peter J. Stuckey
  • Jiaoyang Li

We study the problem of optimizing a guidance policy capable of dynamically guiding the agents for lifelong Multi-Agent Path Finding based on real-time traffic patterns. Multi-Agent Path Finding (MAPF) focuses on moving multiple agents from their starts to goals without collisions. Its lifelong variant, LMAPF, continuously assigns new goals to agents. In this work, we focus on improving the solution quality of PIBT, a state-of-the-art rule-based LMAPF algorithm, by optimizing a policy to generate adaptive guidance. We design two pipelines to incorporate guidance in PIBT in two different ways. We demonstrate the superiority of the optimized policy over both static guidance and human-designed policies. Additionally, we explore scenarios where task distribution changes over time, a challenging yet common situation in real-world applications that is rarely explored in the literature.

SAT Conference 2024 Conference Paper

Anytime Approximate Formal Feature Attribution

  • Jinqiang Yu
  • Graham Farr
  • Alexey Ignatiev
  • Peter J. Stuckey

Widespread use of artificial intelligence (AI) algorithms and machine learning (ML) models on the one hand and a number of crucial issues pertaining to them warrant the need for explainable artificial intelligence (XAI). A key explainability question is: given this decision was made, what are the input features which contributed to the decision? Although a range of XAI approaches exist to tackle this problem, most of them have significant limitations. Heuristic XAI approaches suffer from the lack of quality guarantees, and often try to approximate Shapley values, which is not the same as explaining which features contribute to a decision. A recent alternative is so-called formal feature attribution (FFA), which defines feature importance as the fraction of formal abductive explanations (AXp’s) containing the given feature. This measures feature importance from the view of formally reasoning about the model’s behavior. Namely, given a system of constraints logically representing the ML model of interest, computing an AXp requires finding a minimal unsatisfiable subset (MUS) of the system. It is challenging to compute FFA using its definition because that involves counting over all AXp’s (equivalently, counting over MUSes), although one can approximate it. Based on these results, this paper makes several contributions. First, it gives compelling evidence that computing FFA is intractable, even if the set of contrastive formal explanations (CXp’s), which correspond to minimal correction subsets (MCSes) of the logical system, is provided, by proving that the problem is #P-hard. Second, by using the duality between MUSes and MCSes, it proposes an efficient heuristic to switch from MCS enumeration to MUS enumeration on-the-fly resulting in an adaptive explanation enumeration algorithm effectively approximating FFA in an anytime fashion. Finally, experimental results obtained on a range of widely used datasets demonstrate the effectiveness of the proposed FFA approximation approach in terms of the error of FFA approximation as well as the number of explanations computed and their diversity given a fixed time limit.

SoCS Conference 2024 Conference Paper

Avoiding Node Re-Expansions Can Break Symmetry Breaking

  • Mark Carlson
  • Daniel Harabor
  • Peter J. Stuckey

Symmetry breaking and weighted-suboptimal search are two popular speed up techniques used in pathfinding search. It is a commonly held assumption that they are orthogonal and easily combined. In this paper we illustrate that this is not necessarily the case when combining a number of symmetry breaking methods, based on Jump Point Search, with Weighted A*, a bounded suboptimal search approach which does not require node re-expansions. Surprisingly, the combination of these two methods can cause search to fail, finding no path to a target node when clearly such paths exist. We demonstrate this phenomena and show how we can modify the combination to always succeed with low overhead.

AAAI Conference 2024 Conference Paper

Delivering Inflated Explanations

  • Yacine Izza
  • Alexey Ignatiev
  • Peter J. Stuckey
  • Joao Marques-Silva

In the quest for Explainable Artificial Intelligence (XAI) one of the questions that frequently arises given a decision made by an AI system is, ``why was the decision made in this way?'' Formal approaches to explainability build a formal model of the AI system and use this to reason about the properties of the system. Given a set of feature values for an instance to be explained, and a resulting decision, a formal abductive explanation is a set of features, such that if they take the given value will always lead to the same decision. This explanation is useful, it shows that only some features were used in making the final decision. But it is narrow, it only shows that if the selected features take their given values the decision is unchanged. It is possible that some features may change values and still lead to the same decision. In this paper we formally define inflated explanations which is a set of features, and for each feature a set of values (always including the value of the instance being explained), such that the decision will remain unchanged, for any of the values allowed for any of the features in the (inflated) abductive explanation. Inflated formal explanations are more informative than common abductive explanations since e.g. they allow us to see if the exact value of a feature is important, or it could be any nearby value. Overall they allow us to better understand the role of each feature in the decision. We show that we can compute inflated explanations for not that much greater cost than abductive explanations, and that we can extend duality results for abductive explanations also to inflated explanations.

NeurIPS Conference 2024 Conference Paper

Multi-Stage Predict+Optimize for (Mixed Integer) Linear Programs

  • Xinyi Hu
  • Jasper C. Lee
  • Jimmy H. Lee
  • Peter J. Stuckey

The recently-proposed framework of Predict+Optimize tackles optimization problems with parameters that are unknown at solving time, in a supervised learning setting. Prior frameworks consider only the scenario where all unknown parameters are (eventually) revealed simultaneously. In this work, we propose Multi-Stage Predict+Optimize, a novel extension catering to applications where unknown parameters are revealed in sequential stages, with optimization decisions made in between. We further develop three training algorithms for neural networks (NNs) for our framework as proof of concept, both of which handle all mixed integer linear programs. The first baseline algorithm is a natural extension of prior work, training a single NN which makes a single prediction of unknown parameters. The second and third algorithms instead leverage the possibility of updating parameter predictions between stages, and trains one NN per stage. To handle the interdependency between the neural networks, we adopt sequential and parallelized versions of coordinate descent for training. Experimentation on three benchmarks demonstrates the superior learning performance of our methods over classical approaches.

SoCS Conference 2024 Conference Paper

Planning and Exection in Multi-Agent Path Finding: Models and Algorithms (Extended Abstract)

  • Yue Zhang 0048
  • Zhe Chen 0016
  • Daniel Harabor
  • Pierre Le Bodic
  • Peter J. Stuckey

In applications of Multi-Agent Path Finding (MAPF), it is often the sum of planning and execution times that needs to be minimised (i. e. , the Goal Achievement Time). Yet current methods seldom optimise for this objective. Optimal algorithms reduce execution time, but may require exponential planning time. Non-optimal algorithms reduce planning time, but at the expense of increased path length. To address these limitations we introduce PIE (Planning and Improving while Executing), a new framework for concurrent planning and execution in MAPF. We first show how PIE for one-shot MAPF improves practical performance compared to sequential planning and execution. We then adapt PIE to Lifelong MAPF, a popular application setting where agents are continuously assigned new goals and where additional decisions are required to ensure feasibility. We examine a variety of different approaches to overcome these challenges and we conduct comparative experiments vs. recently proposed alternatives. Results show that PIE substantially outperforms existing methods for One-shot and Lifelong MAPF.

ICAPS Conference 2024 Conference Paper

Planning and Execution in Multi-Agent Path Finding: Models and Algorithms

  • Yue Zhang 0048
  • Zhe Chen 0016
  • Daniel Harabor
  • Pierre Le Bodic
  • Peter J. Stuckey

In applications of Multi-Agent Path Finding (MAPF), it is often the sum of planning and execution times that needs to be minimised (i. e. , the Goal Achievement Time). Yet current methods seldom optimise for this objective. Optimal algorithms reduce execution time, but may require exponential planning time. Non-optimal algorithms reduce planning time, but at the expense of increased path length. To address these limitations we introduce PIE (Planning and Improving while Executing), a new framework for concurrent planning and execution in MAPF. We show how different instantiations of PIE affect practical performance, including initial planning time, action commitment time and concurrent vs. sequential planning and execution. We then adapt PIE to Lifelong MAPF, a popular application setting where agents are continuously assigned new goals and where additional decisions are required to ensure feasibility. We examine a variety of different approaches to overcome these challenges and we conduct comparative experiments vs. recently proposed alternatives. Results show that PIE substantially outperforms existing methods for One-shot and Lifelong MAPF.

SoCS Conference 2024 Conference Paper

Solving Facility Location Problems via FastMap and Locality Sensitive Hashing

  • Ang Li
  • Peter J. Stuckey
  • Sven Koenig
  • T. K. Satish Kumar

Facility Location Problems (FLPs) arise while serving multiple customers in a shared environment, minimizing transportation and other costs. Hence, they involve the optimal placement of facilities. They are defined on graphs as well as in Euclidean spaces with or without obstacles; and they are typically NP-hard to solve optimally. There are many heuristic algorithms tailored to different kinds of FLPs. However, FLPs defined in Euclidean spaces without obstacles are the most amenable to efficient and effective heuristic algorithms. This motivates the idea of quickly reformulating FLPs on graphs and in Euclidean spaces with obstacles to FLPs in Euclidean spaces without obstacles. Towards this end, we propose a new approach that uses FastMap and Locality Sensitive Hashing. FastMap is a near-linear-time algorithm that embeds the vertices of a graph in a Euclidean space while approximately preserving graph-based distances as Euclidean distances for all pairs of vertices. Through extensive experiments, we show that our approach significantly outperforms other state-of-the-art competing algorithms on a variety of FLPs: the Multi-Agent Meeting, Vertex K-Median (VKM), Weighted VKM, and the Capacitated VKM problems.

AAAI Conference 2024 Conference Paper

Traffic Flow Optimisation for Lifelong Multi-Agent Path Finding

  • Zhe Chen
  • Daniel Harabor
  • Jiaoyang Li
  • Peter J. Stuckey

Multi-Agent Path Finding (MAPF) is a fundamental problem in robotics that asks us to compute collision-free paths for a team of agents, all moving across a shared map. Although many works appear on this topic, all current algorithms struggle as the number of agents grows. The principal reason is that existing approaches typically plan free-flow optimal paths, which creates congestion. To tackle this issue, we propose a new approach for MAPF where agents are guided to their destination by following congestion-avoiding paths. We evaluate the idea in two large-scale settings: one-shot MAPF, where each agent has a single destination, and lifelong MAPF, where agents are continuously assigned new destinations. Empirically, we report large improvements in solution quality for one-short MAPF and in overall throughput for lifelong MAPF.

SoCS Conference 2024 Conference Paper

Traffic Flow Optimisation for Lifelong Multi-Agent Path Finding (Extended Abstract)

  • Zhe Chen 0016
  • Daniel Harabor
  • Jiaoyang Li 0001
  • Peter J. Stuckey

Multi-Agent Path Finding (MAPF) is a fundamental problem in robotics that asks us to compute collision-free paths for a team of agents, all moving across a shared map. Existing scalable approaches struggle as the number of agents grows, as they typically plan free-flow optimal paths, which creates congestion. To tackle this issue, we propose a new approach for MAPF where agents are guided to their destination by following congestion-avoiding paths. Empirically, we report large improvements in overall throughput for lifelong MAPF while coordinating more than ten thousand agents.

ICAPS Conference 2023 Conference Paper

A Constraint Programming Solution to the Guillotine Rectangular Cutting Problem

  • Sergey Polyakovskiy
  • Peter J. Stuckey

The guillotine rectangular cutting problem deals with a single rectangular plate of raw material and a collection of rectangular items to be cut from the plate. Each item is associated with a profit and a demand. The problem searches for a feasible layout of a subset of items on the plate so as to maximize the total profit of selected items. The guillotine constraint restricts feasible layouts to those that can be obtained via guillotine edge-to-edge cuts that run parallel to an edge of the plate. We propose a novel constraint programming model that is suitable for guillotine cutting with an arbitrary number of stages of alternating horizontal and vertical guillotine cuts. This is an assignment-based model that models guillotine cuts using a constant number of rectangular regions, with some regions allocated to items. It treats the entire plate as a primary region and decides on the guillotine cuts required to split the regions recursively till they produce space for the items. To speed the search, the model explores the strength of cumulative scheduling relaxations of the cutting problem. Our model is a successful alternative to more traditional mixed-integer linear programming (MILP) models. It outperforms a number of state-of-the-art MILPs on a set of small and moderate size benchmark instances and proves optimality for several instances that remain challenging for these MILPs.

IJCAI Conference 2023 Conference Paper

A Regular Matching Constraint for String Variables

  • Roberto Amadini
  • Peter J. Stuckey

Using a regular language as a pattern for string matching is nowadays a common -and sometimes unsafe- operation, provided as a built-in feature by most programming languages. A proper constraint solver over string variables should support most of the operations over regular expressions and related constructs. However, state-of-the-art string solvers natively support only the membership relation of a string variable to a regular language. Here we take a step forward by defining a specialised propagator for the match operation, returning the leftmost position where a pattern can match a given string. Empirical evidences show the effectiveness of our approach, implemented within the constraint programming framework, and tested against state-of-the-art string solvers.

ICAPS Conference 2023 Conference Paper

Beyond Pairwise Reasoning in Multi-Agent Path Finding

  • Bojie Shen
  • Zhe Chen 0016
  • Jiaoyang Li 0001
  • Muhammad Aamir Cheema
  • Daniel Harabor
  • Peter J. Stuckey

In Multi-Agent Path Finding (MAPF), we are asked to plan collision-free paths for teams of moving agents. Among the leading methods for optimal MAPF is Conflict-Based Search (CBS), an algorithmic family which has received intense attention in recent years and for which large advancements in efficiency and effectiveness have been reported. Yet all of the recent CBS gains come from reasoning over pairs of agents only. In this paper, we show how to further improve CBS by reasoning about more than two agents at the same time. Our new cluster reasoning techniques allow us to generate stronger bounds for CBS and to identify more bypasses (alternative cost-equivalent paths), which reduce the number of nodes in the CBS conflict tree.

SoCS Conference 2023 Conference Paper

Efficient Multi Agent Path Finding with Turn Actions

  • Yue Zhang 0048
  • Daniel Harabor
  • Pierre Le Bodic
  • Peter J. Stuckey

Current approaches for real-world Multi-Agent Path Finding (MAPF) usually start with a simplified MAPF model and modify the resulting plans so they are kinematically feasible. We investigate one such problem, called MAPF with turn actions MAPF_T, and show that ignoring the kinematic constraints significantly increases solution cost. A first modification of the popular Conflict-Based Search algorithm to MAPF_T yields significantly better plans but comes at the cost of substantial decreases in scalability. We then introduce several techniques that can improve the performance of CBS for MAPF_T, including stronger and generalised versions of existing symmetry-breaking constraints and a novel pruning technique that eliminates redundant branches in the CBS constraint tree. Experimental results on six popular MAPF domains show convincing improvements for CBS success rate and substantial reductions in node expansions and runtime.

AAAI Conference 2023 Conference Paper

Eliminating the Impossible, Whatever Remains Must Be True: On Extracting and Applying Background Knowledge in the Context of Formal Explanations

  • Jinqiang Yu
  • Alexey Ignatiev
  • Peter J. Stuckey
  • Nina Narodytska
  • Joao Marques-Silva

The rise of AI methods to make predictions and decisions has led to a pressing need for more explainable artificial intelligence (XAI) methods. One common approach for XAI is to produce a post-hoc explanation, explaining why a black box ML model made a certain prediction. Formal approaches to post-hoc explanations provide succinct reasons for why a prediction was made, as well as why not another prediction was made. But these approaches assume that features are independent and uniformly distributed. While this means that “why” explanations are correct, they may be longer than required. It also means the “why not” explanations may be suspect as the counterexamples they rely on may not be meaningful. In this paper, we show how one can apply background knowledge to give more succinct “why” formal explanations, that are presumably easier to interpret by humans, and give more accurate “why not” explanations. In addition, we show how to use existing rule induction techniques to efficiently extract background information from a dataset.

ICAPS Conference 2023 Conference Paper

Exact Anytime Multi-Agent Path Finding Using Branch-and-Cut-and-Price and Large Neighborhood Search

  • Edward Lam 0001
  • Daniel Harabor
  • Peter J. Stuckey
  • Jiaoyang Li 0001

Given a set of agents on a grid, the multi-agent path finding problem aims to find a path that moves each agent from its given start location to its target location such that they do not collide and that the sum of arrival times is minimized. LNS2 is a state-of-the-art algorithm for anytime, suboptimal solving. It is an upper-bounding algorithm that repeatedly adjusts an existing solution and, being a local search, is oblivious to optimality. BCP is a state-of-the-art algorithm for exact solving. It is a lower-bounding tree search that attempts to tighten the lower bound until a solution appears. As BCP operates on the lower bound, the first solution it finds is optimal or nearly optimal, and therefore has poor anytime behavior. This paper proposes to tightly couple LNS2 and BCP to achieve better anytime, suboptimal solving while retaining the optimality guarantee of BCP. Experiments indicate that the combination achieves better anytime behavior than BCP in general and better suboptimal performance than LNS2 on congested maps.

AAAI Conference 2023 Conference Paper

Optimal Pathfinding on Weighted Grid Maps

  • Mark Carlson
  • Sajjad K. Moghadam
  • Daniel D. Harabor
  • Peter J. Stuckey
  • Morteza Ebrahimi

In many computer games up to hundreds of agents navigate in real-time across a dynamically changing weighted grid map. Pathfinding in these situations is challenging because the grids are large, traversal costs are not uniform, and because each shortest path has many symmetric permutations, all of which must be considered by an optimal online search. In this work we introduce Weighted Jump Point Search (JPSW), a new type of pathfinding algorithm which breaks weighted grid symmetries by introducing a tiebreaking policy that allows us to apply effective pruning rules in symmetric regions. We show that these pruning rules preserve at least one optimal path to every grid cell and that their application can yield large performance improvements for optimal pathfinding. We give a complete theoretical description of the new algorithm, including pseudo-code. We also conduct a wide-ranging experimental evaluation, including data from real games. Results indicate JPSW is up to orders of magnitude faster than the nearest baseline, online search using A*.

SoCS Conference 2023 Conference Paper

Reducing Redundant Work in Jump Point Search

  • Shizhe Zhao
  • Daniel Harabor
  • Peter J. Stuckey

JPS (Jump Point Search) is a state-of-the-art optimal algorithm for online grid-based pathfinding. Widely used in games and other navigation scenarios, JPS nevertheless can exhibit pathological behaviours which are not well studied: (i) it may repeatedly scan the same area of the map to find successors; (ii) it may generate and expand suboptimal search nodes. In this work, we examine the source of these pathological behaviours, show how they can occur in practice, and propose a purely online approach, called Constrained JPS (CJPS), to tackle them efficiently. Experimental results show that CJPS has low overheads and is often faster than JPS in dynamically changing grid environments: by up to 7x in large game maps and up to 14x in pathological scenarios.

AAAI Conference 2022 Conference Paper

A Divide and Conquer Algorithm for Predict+Optimize with Non-convex Problems

  • Ali Ugur Guler
  • Emir Demirović
  • Jeffrey Chan
  • James Bailey
  • Christopher Leckie
  • Peter J. Stuckey

The predict+optimize problem combines machine learning and combinatorial optimization by predicting the problem coefficients first and then using these coefficients to solve the optimization problem. While this problem can be solved in two separate stages, recent research shows end to end models can achieve better results. This requires differentiating through a discrete combinatorial function. Models that use differentiable surrogates are prone to approximation errors, while existing exact models are limited to dynamic programming, or they do not generalize well with scarce data. In this work we propose a novel divide and conquer algorithm based on transition points to reason over exact optimization problems and predict the coefficients using the optimization loss. Moreover, our model is not limited to dynamic programming problems. We also introduce a greedy version, which achieves similar results with less computation. In comparison with other predict+optimize frameworks, we show our method outperforms existing exact frameworks and can reason over hard combinatorial problems better than surrogate methods.

SoCS Conference 2022 Conference Paper

Dual Euclidean Shortest Path Search (Extended Abstract)

  • Ryan Hechenberger
  • Peter J. Stuckey
  • Pierre Le Bodic
  • Daniel Harabor

The Euclidean Shortest Path Problem (ESPP) asks us to find a minimum length path between two points on a 2D plane while avoiding a set of polygonal obstacles. Existing approaches for ESPP, based on Dijkstra or A* search, are primal methods that gradually build up longer and longer valid paths until they reach the target. In this paper we define an alternative algorithm for ESPP which can avoid this problem. Our approach starts from a path that ignores all obstacles, and generates longer and longer paths, each avoiding more obstacles, until eventually the search finds an optimal valid path.

AIJ Journal 2022 Journal Article

Fast optimal and bounded suboptimal Euclidean pathfinding

  • Bojie Shen
  • Muhammad Aamir Cheema
  • Daniel D. Harabor
  • Peter J. Stuckey

We consider optimal and suboptimal algorithms for the Euclidean Shortest Path Problem (ESPP) in two dimensions. For optimal path planning, Our approach leverages ideas from two recent works: Polyanya, a mesh-based ESPP planner which we use to represent and reason about the environment, and Compressed Path Databases (CPD), a speedup technique for pathfinding on grids and spatial networks, which we exploit to efficiently compute candidate paths, in order to construct a completely novel ESPP algorithm, End Point Search (EPS). In a range of experiments and empirical comparisons we show that: (i) the auxiliary data structures required by EPS are cheap to build and store; (ii) for optimal search, the new algorithm is faster than a range of recent ESPP planners, with speedups ranging from several factors to over one order of magnitude; (iii) for anytime search, where feasible solutions are needed fast, we report even better performance. For suboptimal path planning, we extend the CPD such that it computes and compresses first move data of a larger number of selected candidate nodes covering every point in the Euclidean space. Our approach is search-free, simultaneously fast, and returns a path within a fixed bound of the optimal solution. In a range of empirical results, we show that: (i) our approach outperforms both offline/online optimal and suboptimal ESPP algorithms proposed in the literature; (ii) our approach demonstrates excellent path quality, better than all existing suboptimal ESPP algorithms; and (iii) the approach offers flexibility by allowing a trade-off between the CPD construction cost (space and time) and the suboptimality bound.

AAAI Conference 2022 Conference Paper

Flex Distribution for Bounded-Suboptimal Multi-Agent Path Finding

  • Shao-Hung Chan
  • Jiaoyang Li
  • Graeme Gange
  • Daniel Harabor
  • Peter J. Stuckey
  • Sven Koenig

Multi-Agent Path Finding (MAPF) is the problem of finding collision-free paths for multiple agents that minimize the sum of path costs. EECBS is a leading two-level algorithm that solves MAPF bounded-suboptimally, that is, within some factor w of the minimum sum of path costs C∗. It uses focal search to find bounded-suboptimal paths on the low level and Explicit Estimation Search (EES) to resolve collisions on the high level. EES keeps track of a lower bound LB on C∗ to find paths whose sum of path costs is at most w · LB in order to solve MAPF bounded-suboptimally. However, the costs of many paths are often much smaller than w times their minimum path costs, meaning that the sum of path costs is much smaller than w ·C∗. In this paper, we therefore propose Flexible EECBS (FEECBS), which uses a flex(ible) distribution of the path costs (that relaxes the requirement to find bounded-suboptimal paths on the low level) in order to reduce the number of collisions that need to be resolved on the high level while still guaranteeing to solve MAPF bounded suboptimally. We address the drawbacks of flex distribution via techniques such as restrictions on the flex distribution, restarts of the high-level search with EECBS, and low-level focal-A* search. Our empirical evaluation shows that FEECBS substantially improves the efficiency of EECBS on MAPF instances with large maps and large numbers of agents.

ICAPS Conference 2022 Conference Paper

Improving Time-Dependent Contraction Hierarchies

  • Bojie Shen
  • Muhammad Aamir Cheema
  • Daniel Harabor
  • Peter J. Stuckey

Computing time-optimal shortest paths, in road networks, is one of the most popular applications of Artificial Intelligence. This problem is tricky to solve because road congestion affects travel times. The state-of-the-art in this area is an algorithm called Time-dependent Contraction Hierarchies (TCH). Although fast and optimal, TCH still suffers from two main drawbacks: (1) the usual query process uses bi-directional Dijkstra search to find the shortest path, which can be time-consuming; and (2) the TCH is constructed w. r. t. the entire time domain T, which complicates the search process for queries q that start and finish in a smaller time period Tq ⊂ T. In this work, we improve TCH by making use of time-independent heuristics, which speed up optimal search, and by computing TCHs for different subsets of the time domain, which further reduces the size of the search space. We give a full description of these methods and discuss their optimality-preserving characteristics. We report significant query time improvements against a baseline implementation of TCH.

AAAI Conference 2022 Conference Paper

MAPF-LNS2: Fast Repairing for Multi-Agent Path Finding via Large Neighborhood Search

  • Jiaoyang Li
  • Zhe Chen
  • Daniel Harabor
  • Peter J. Stuckey
  • Sven Koenig

Multi-Agent Path Finding (MAPF) is the problem of planning collision-free paths for multiple agents in a shared environment. In this paper, we propose a novel algorithm MAPF- LNS2 based on large neighborhood search for solving MAPF efficiently. Starting from a set of paths that contain collisions, MAPF-LNS2 repeatedly selects a subset of colliding agents and replans their paths to reduce the number of collisions until the paths become collision-free. We compare MAPF- LNS2 against a variety of state-of-the-art MAPF algorithms, including Prioritized Planning with random restarts, EECBS, and PPS, and show that MAPF-LNS2 runs significantly faster than them while still providing near-optimal solutions in most cases. MAPF-LNS2 solves 80% of the random-scenario instances with the largest number of agents from the MAPF benchmark suite with a runtime limit of just 5 minutes, which, to our knowledge, has not been achieved by any existing algorithms.

ICAPS Conference 2022 Conference Paper

Multi-Agent Path Finding with Temporal Jump Point Search

  • Shuli Hu
  • Daniel Harabor
  • Graeme Gange
  • Peter J. Stuckey
  • Nathan R. Sturtevant

Temporal Jump Point Search (JPST) is a recently introduced algorithm for grid-optimal pathfinding among dynamic temporal obstacles. In this work we consider JPST as a low-level planner in Multi-Agent Path Finding (MAPF). We investigate how the canonical ordering of JPST can negatively impact MAPF performance and we consider several strategies which allow us to overcome these limitations. Experiments show our new CBS/JPST approach can substantially improve on CBS/SIPP, a contemporary and leading method from the area.

SoCS Conference 2022 Conference Paper

Multi-Train Path Finding Revisited

  • Zhe Chen 0016
  • Jiaoyang Li 0001
  • Daniel Harabor
  • Peter J. Stuckey
  • Sven Koenig

Multi-Train Path Finding (MTPF) is a coordination problem that asks us to plan collision-free paths for a team of moving agents, where each agent occupies a sequence of locations at any given time. MTPF is useful for planning a range of real-world vehicles, including rail trains and road convoys. MTPF is closely related to another coordination problem known as k-Robust Multi-Agent Path Finding (kR-MAPF). Although similar in principle, the performance of optimal MTPF algorithms in practice lags far behind that of optimal kR-MAPF algorithms. In this work, we revisit the connection between them and reduce the performance gap. First, we show that, in many cases, a valid kR-MAPF plan is also a valid MTPF plan, which leads to a new and faster approach for collision resolution. We also show that many recently introduced improvements for kR-MAPF, such as lower-bounding heuristics and symmetry reasoning, can be extended to MTPF. Finally, we explore a new type of pairwise symmetry specific to MTPF. Our experiments show that these improvements yield large efficiency gains for optimal MTPF.

JMLR Journal 2022 Journal Article

MurTree: Optimal Decision Trees via Dynamic Programming and Search

  • Emir Demirović
  • Anna Lukina
  • Emmanuel Hebrard
  • Jeffrey Chan
  • James Bailey
  • Christopher Leckie
  • Kotagiri Ramamohanarao
  • Peter J. Stuckey

Decision tree learning is a widely used approach in machine learning, favoured in applications that require concise and interpretable models. Heuristic methods are traditionally used to quickly produce models with reasonably high accuracy. A commonly criticised point, however, is that the resulting trees may not necessarily be the best representation of the data in terms of accuracy and size. In recent years, this motivated the development of optimal classification tree algorithms that globally optimise the decision tree in contrast to heuristic methods that perform a sequence of locally optimal decisions. We follow this line of work and provide a novel algorithm for learning optimal classification trees based on dynamic programming and search. Our algorithm supports constraints on the depth of the tree and number of nodes. The success of our approach is attributed to a series of specialised techniques that exploit properties unique to classification trees. Whereas algorithms for optimal classification trees have traditionally been plagued by high runtimes and limited scalability, we show in a detailed experimental study that our approach uses only a fraction of the time required by the state-of-the-art and can handle datasets with tens of thousands of instances, providing several orders of magnitude improvements and notably contributing towards the practical use of optimal decision trees. [abs] [ pdf ][ bib ] [ code ] &copy JMLR 2022. ( edit, beta )

AAAI Conference 2022 Conference Paper

Using MaxSAT for Efficient Explanations of Tree Ensembles

  • Alexey Ignatiev
  • Yacine Izza
  • Peter J. Stuckey
  • Joao Marques-Silva

Tree ensembles (TEs) denote a prevalent machine learning model that do not offer guarantees of interpretability, that represent a challenge from the perspective of explainable artificial intelligence. Besides model agnostic approaches, recent work proposed to explain TEs with formally-defined explanations, which are computed with oracles for propositional satisfiability (SAT) and satisfiability modulo theories. The computation of explanations for TEs involves linear constraints to express the prediction. In practice, this deteriorates scalability of the underlying reasoners. Motivated by the inherent propositional nature of TEs, this paper proposes to circumvent the need for linear constraints and instead employ an optimization engine for pure propositional logic to efficiently handle the prediction. Concretely, the paper proposes to use a MaxSAT solver and exploit the objective function to determine a winning class. This is achieved by devising a propositional encoding for computing explanations of TEs. Furthermore, the paper proposes additional heuristics to improve the underlying MaxSAT solving procedure. Experimental results obtained on a wide range of publicly available datasets demonstrate that the proposed MaxSAT-based approach is either on par or outperforms the existing reasoning-based explainers, thus representing a robust and efficient alternative for computing formal explanations for TEs.

AAAI Conference 2021 Conference Paper

A Scalable Two Stage Approach to Computing Optimal Decision Sets

  • Alexey Ignatiev
  • Edward Lam
  • Peter J. Stuckey
  • Joao Marques-Silva

Machine learning (ML) is ubiquitous in modern life. Since it is being deployed in technologies that affect our privacy and safety, it is often crucial to understand the reasoning behind its decisions, warranting the need for explainable AI. Rulebased models, such as decision trees, decision lists, and decision sets, are conventionally deemed to be the most interpretable. Recent work uses propositional satisfiability (SAT) solving (and its optimization variants) to generate minimumsize decision sets. Motivated by limited practical scalability of these earlier methods, this paper proposes a novel approach to learn minimum-size decision sets by enumerating individual rules of the target decision set independently of each other, and then solving a set cover problem to select a subset of rules. The approach makes use of modern maximum satisfiability and integer linear programming technologies. Experiments on a wide range of publicly available datasets demonstrate the advantage of the new approach over the state of the art in SAT-based decision set learning.

IJCAI Conference 2021 Conference Paper

Anytime Multi-Agent Path Finding via Large Neighborhood Search

  • Jiaoyang Li
  • Zhe Chen
  • Daniel Harabor
  • Peter J. Stuckey
  • Sven Koenig

Multi-Agent Path Finding (MAPF) is the challenging problem of computing collision-free paths for multiple agents. Algorithms for solving MAPF can be categorized on a spectrum. At one end are (bounded-sub)optimal algorithms that can find high-quality solutions for small problems. At the other end are unbounded-suboptimal algorithms that can solve large problems but usually find low-quality solutions. In this paper, we consider a third approach that combines the best of both worlds: anytime algorithms that quickly find an initial solution using efficient MAPF algorithms from the literature, even for large problems, and that subsequently improve the solution quality to near-optimal as time progresses by replanning subgroups of agents using Large Neighborhood Search. We compare our algorithm MAPF-LNS against a range of existing work and report significant gains in scalability, runtime to the initial solution, and speed of improving the solution.

AAMAS Conference 2021 Conference Paper

Anytime Multi-Agent Path Finding via Large Neighborhood Search

  • Jiaoyang Li
  • Zhe Chen
  • Daniel Harabor
  • Peter J. Stuckey
  • Sven Koenig

Multi-Agent Path Finding (MAPF) is the challenging problem of computing collision-free paths for a cooperative team of moving agents. Algorithms for solving MAPF can be categorized on a spectrum. At one end are (bounded-sub)optimal algorithms that can find high-quality solutions for small problems. At the other end are unbounded-suboptimal algorithms (including prioritized and rule-based algorithms) that can solve very large practical problems but usually find low-quality solutions. In this paper, we consider a third approach that combines both advantages: anytime algorithms that quickly find an initial solution, including for large problems, and that subsequently improve the solution to near-optimal as time progresses. To improve the solution, we replan subsets of agents using Large Neighborhood Search, a popular meta-heuristic often applied in combinatorial optimization. Empirically, we compare our algorithm MAPF-LNS to the state-of-the-art anytime MAPF algorithm anytime BCBS and report significant gains in scalability, runtime to the first solution, and speed of improving solutions.

ICAPS Conference 2021 Conference Paper

Contracting and Compressing Shortest Path Databases

  • Bojie Shen
  • Muhammad Aamir Cheema
  • Daniel Harabor
  • Peter J. Stuckey

Compressed Path Databases (CPD) are powerful database-driven methods for shortest path extraction in grids and in spatial networks. Yet CPDs have two main drawbacks: (1) constructing the database requires an offline all-pairs precompute, which can sometimes be prohibitive and; (2) extracting a path requires a number of database lookups equal to its number of edges, which can be costly in terms of time. In this work, we consider how CPD methods can be improved and enhanced by: (i) contracting the input graph before preprocessing and; (ii) limiting the preprocessing step to only a selected subset of graph nodes. We also describe a new bi-directional path extraction algorithm which we call CH-CPD. In a range of experiments on road networks, we show that CH-CPD substantially improves on conventional CPDs in terms of preprocessing costs and online performance. We also report convincing query time improvements against a range of methods from the recent literature.

SoCS Conference 2021 Conference Paper

Customised Shortest Paths Using a Distributed Reverse Oracle

  • Arthur Mahéo
  • Shizhe Zhao
  • Hassan Afzaal
  • Daniel Harabor
  • Peter J. Stuckey
  • Mark Wallace 0001

We consider the design and implementation of a centralised oracle that provides commuters with customised and congestion-aware driving directions. Computing directions for a single journey is straightforward, but doing so at city-scale, in real-time, and under changing conditions is extremely challenging. In this work we describe a new type of centralised oracle which combines fast database-driven path planning with a query management system that distributes work across a small commodity cluster of networked machines. Our system allows large-scale changes to the underlying graph metric, from one query to the next, and it supports a variety of query types including optimal, bounded suboptimal, time-budgeted and k-prefix. Simulated experiments show strong results: we can provide real-time routing for all peak-hour commuter trips in the city of Melbourne, Australia.

AAAI Conference 2021 Conference Paper

Cutting to the Core of Pseudo-Boolean Optimization: Combining Core-Guided Search with Cutting Planes Reasoning

  • Jo Devriendt
  • Stephan Gocht
  • Emir Demirović
  • Jakob Nordström
  • Peter J. Stuckey

Core-guided techniques have revolutionized Boolean satisfiability approaches to optimization problems (MaxSAT), but the process at the heart of these methods, strengthening bounds on solutions by repeatedly adding cardinality constraints, remains a bottleneck. Cardinality constraints require significant work to be re-encoded to SAT, and SAT solvers are notoriously weak at cardinality reasoning. In this work, we lift core-guided search to pseudo-Boolean (PB) solvers, which deal with more general PB optimization problems and operate natively with cardinality constraints. The cutting planes method used in such solvers allows us to derive stronger cardinality constraints, which yield better updates to solution bounds, and the increased efficiency of objective function reformulation also makes it feasible to switch repeatedly between lower-bounding and upper-bounding search. A thorough evaluation on applied and crafted benchmarks shows that our core-guided PB solver significantly improves on the state of the art in pseudo-Boolean optimization.

SoCS Conference 2021 Conference Paper

ECBS with Flex Distribution for Bounded-Suboptimal Multi-Agent Path Finding

  • Shao-Hung Chan
  • Jiaoyang Li 0001
  • Graeme Gange
  • Daniel Harabor
  • Peter J. Stuckey
  • Sven Koenig

Multi-Agent Path Finding (MAPF) is the problem of finding collision-free paths for multiple agents. CBS is a leading optimal two-level MAPF solver whose low level plans optimal paths for single agents and whose high level runs a best-first search on a Constraint Tree (CT) to resolve the collisions between the paths. ECBS, a bounded-suboptimal variant of CBS, speeds up CBS by reducing the number of collisions that need to be resolved on the high level. It achieves this by generating bounded-suboptimal paths with fewer collisions with the paths of the other agents on the low level and expanding bounded-suboptimal CT nodes that contain fewer collisions on the high level. In this paper, we propose Flexible ECBS (FECBS) that further reduces the number of collisions that need to be resolved on the high level by using looser suboptimal bounds on the low level while still providing bounded-suboptimal solutions. Instead of requiring the cost of each path to be bounded-suboptimal, FECBS requires only the overall cost of the paths to be bounded-suboptimal, which gives us the freedom to distribute the cost leeway among different agents according to their needs. Our empirical results show that FECBS can solve more MAPF instances than state-of-the-art ECBS variants within 5 minutes.

AAAI Conference 2021 Conference Paper

f-Aware Conflict Prioritization & Improved Heuristics For Conflict-Based Search

  • Eli Boyarski
  • Ariel Felner
  • Pierre Le Bodic
  • Daniel D. Harabor
  • Peter J. Stuckey
  • Sven Koenig

Conflict-Based Search (CBS) is a leading two-level algorithm for optimal Multi-Agent Path Finding (MAPF). The main step of CBS is to expand nodes by resolving conflicts (where two agents collide). Choosing the ‘right’ conflict to resolve can greatly speed up the search. CBS first resolves conflicts where the costs (g-values) of the resulting child nodes are larger than the cost of the node to be split. However, the recent addition of high-level heuristics to CBS and expanding nodes according to f = g + h reduces the relevance of this conflict prioritization method. Therefore, we introduce an expanded categorization of conflicts, which first resolves conflicts where the f-values of the child nodes are larger than the f-value of the node to be split, and present a method for identifying such conflicts. We also enhance all known heuristics for CBS by using information about the cost of resolving certain conflicts with only a small computational overhead. Finally, we experimentally demonstrate that both the expanded categorization of conflicts and the improved heuristics contribute to making CBS even more efficient.

SoCS Conference 2021 Conference Paper

Further Improved Heuristics For Conflict-Based Search

  • Eli Boyarski
  • Ariel Felner
  • Pierre Le Bodic
  • Daniel Harabor
  • Peter J. Stuckey
  • Sven Koenig

Conflict-Based Search (CBS) is a leading two-level algorithm for optimal Multi-Agent Path Finding (MAPF). At its high level, CBS expands nodes by resolving conflicts. In recent years, admissible heuristics were added to the high level of CBS. We enhance all known heuristic functions for CBS by using information about the cost of resolving certain conflicts, with only a small computational overhead. We experimentally demonstrate that the improved heuristics contribute to making CBS even more efficient.

ICAPS Conference 2021 Conference Paper

Jump Point Search with Temporal Obstacles

  • Shuli Hu
  • Daniel Harabor
  • Graeme Gange
  • Peter J. Stuckey
  • Nathan R. Sturtevant

In 4-connected grid-based path planning one often needs to account for temporal and moving obstacles: ones that appear, disappear and which can prevent the agent from reaching its target. Such problems are common in a variety of settings (games, robotics etc.) and they can be surprisingly challenging to solve. First, because the temporal aspect increases the size of the search space; second because the search space contains many symmetric paths, indistinguishable from one another except by the order in which grid moves appear. To tackle such problems we consider a new optimal algorithm – in the style of Jump Point Search – which can identify and break these symmetries and thus improves performance; from several factor to more than one order of magnitude vs. SIPP, arguably the gold standard baseline in the area.

JAIR Journal 2021 Journal Article

Learning Optimal Decision Sets and Lists with SAT

  • Jinqiang Yu
  • Alexey Ignatiev
  • Peter J. Stuckey
  • Pierre Le Bodic

Decision sets and decision lists are two of the most easily explainable machine learning models. Given the renewed emphasis on explainable machine learning decisions, both of these machine learning models are becoming increasingly attractive, as they combine small size and clear explainability. In this paper, we define size as the total number of literals in the SAT encoding of these rule-based models as opposed to earlier work that concentrates on the number of rules. In this paper, we develop approaches to computing minimum-size “perfect” decision sets and decision lists, which are perfectly accurate on the training data, and minimal in size, making use of modern SAT solving technology. We also provide a new method for determining optimal sparse alternatives, which trade off size and accuracy. The experiments in this paper demonstrate that the optimal decision sets computed by the SAT-based approach are comparable with the best heuristic methods, but much more succinct, and thus, more explainable. We contrast the size and test accuracy of optimal decisions lists versus optimal decision sets, as well as other state-of-the-art methods for determining optimal decision lists. Finally, we examine the size of average explanations generated by decision sets and decision lists.

SoCS Conference 2021 Conference Paper

Multi-Target Search in Euclidean Space with Ray Shooting

  • Ryan Hechenberger
  • Daniel Harabor
  • Muhammad Aamir Cheema
  • Peter J. Stuckey
  • Pierre Le Bodic

The shortest path problem (SPP) asks us to find a minimum length path between two points, usually on a graph. In a Euclidean environment the points are in a 2D plane and here the path must avoid a set of polygonal obstacles. Solution methods for this Euclidean SPP (ESPP) typically convert the continuous 2D map into a discretised representation, like a graph or navigation mesh. RayScan is a recent and fast ESPP algorithm which avoids the preprocessing step by using a combination of "ray shooting" and polygon scanning. In this paper we improve the performance of RayScan using spatial reasoning and ray caching techniques. We also extend the algorithm, from single-target search to a multi-target setting. Comparative game map experiments show a substantial speedup.

AAAI Conference 2021 Conference Paper

Optimal Decision Trees for Nonlinear Metrics

  • Emir Demirović
  • Peter J. Stuckey

Nonlinear metrics, such as the F1-score, Matthews correlation coefficient, and Fowlkes–Mallows index, are often used to evaluate the performance of machine learning models, in particular, when facing imbalanced datasets that contain more samples of one class than the other. Recent optimal decision tree algorithms have shown remarkable progress in producing trees that are optimal with respect to linear criteria, such as accuracy, but unfortunately nonlinear metrics remain a challenge. To address this gap, we propose a novel algorithm based on bi-objective optimisation, which treats misclassifications of each binary class as a separate objective. We show that, for a large class of metrics, the optimal tree lies on the Pareto frontier. Consequently, we obtain the optimal tree by using our method to generate the set of all nondominated trees. To the best of our knowledge, this is the first method to compute provably optimal decision trees for nonlinear metrics. Our approach leads to a trade-off when compared to optimising linear metrics: the resulting trees may be more desirable according to the given nonlinear metric at the expense of higher runtimes. Nevertheless, the experiments illustrate that runtimes are reasonable for majority of the tested datasets.

AIJ Journal 2021 Journal Article

Pairwise symmetry reasoning for multi-agent path finding search

  • Jiaoyang Li
  • Daniel Harabor
  • Peter J. Stuckey
  • Hang Ma
  • Graeme Gange
  • Sven Koenig

Multi-Agent Path Finding (MAPF) is a challenging combinatorial problem that asks us to plan collision-free paths for a team of cooperative agents. In this work, we show that one of the reasons why MAPF is so hard to solve is due to a phenomenon called pairwise symmetry, which occurs when two agents have many different paths to their target locations, all of which appear promising, but every combination of them results in a collision. We identify several classes of pairwise symmetries and show that each one arises commonly in practice and can produce an exponential explosion in the space of possible collision resolutions, leading to unacceptable runtimes for current state-of-the-art (bounded-sub)optimal MAPF algorithms. We propose a variety of reasoning techniques that detect the symmetries efficiently as they arise and resolve them by using specialized constraints to eliminate all permutations of pairwise colliding paths in a single branching step. We implement these ideas in the context of a leading optimal MAPF algorithm CBS and show that the addition of the symmetry reasoning techniques can have a dramatic positive effect on its performance — we report a reduction in the number of node expansions by up to four orders of magnitude and an increase in scalability by up to thirty times. These gains allow us to solve to optimality a variety of challenging MAPF instances previously considered out of reach for CBS.

IJCAI Conference 2021 Conference Paper

Reasoning-Based Learning of Interpretable ML Models

  • Alexey Ignatiev
  • Joao Marques-Silva
  • Nina Narodytska
  • Peter J. Stuckey

Artificial Intelligence (AI) is widely used in decision making procedures in myriads of real-world applications across important practical areas such as finance, healthcare, education, and safety critical systems. Due to its ubiquitous use in safety and privacy critical domains, it is often vital to understand the reasoning behind the AI decisions, which motivates the need for explainable AI (XAI). One of the major approaches to XAI is represented by computing so-called interpretable machine learning (ML) models, such as decision trees (DT), decision lists (DL) and decision sets (DS). These models build on the use of if-then rules and are thus deemed to be easily understandable by humans. A number of approaches have been proposed in the recent past to devising all kinds of interpretable ML models, the most prominent of which involve encoding the problem into a logic formalism, which is then tackled by invoking a reasoning or discrete optimization procedure. This paper overviews the recent advances of the reasoning and constraints based approaches to learning interpretable ML models and discusses their advantages and limitations.

ICAPS Conference 2021 Conference Paper

Scalable Rail Planning and Replanning: Winning the 2020 Flatland Challenge

  • Jiaoyang Li 0001
  • Zhe Chen 0016
  • Yi Zheng 0010
  • Shao-Hung Chan
  • Daniel Harabor
  • Peter J. Stuckey
  • Hang Ma 0001
  • Sven Koenig

Multi-Agent Path Finding (MAPF) is the combinatorial problem of finding collision-free paths for multiple agents on a graph. This paper describes MAPF-based software for solving train planning and replanning problems on large-scale rail networks under uncertainty. The software recently won the 2020 Flatland Challenge, a NeurIPS competition trying to determine how to efficiently manage dense traffic on rail networks. The software incorporates many state-of-the-art MAPF or, in general, optimization technologies, such as prioritized planning, large neighborhood search, safe interval path planning, minimum communication policies, parallel computing, and simulated annealing. It can plan collision-free paths for thousands of trains within a few minutes and deliver deadlock-free actions in real-time during execution.

SoCS Conference 2021 Conference Paper

Scalable Rail Planning and Replanning: Winning the 2020 Flatland Challenge

  • Jiaoyang Li 0001
  • Zhe Chen 0016
  • Yi Zheng 0010
  • Shao-Hung Chan
  • Daniel Harabor
  • Peter J. Stuckey
  • Hang Ma 0001
  • Sven Koenig

Multi-Agent Path Finding (MAPF) is the combinatorial problem of finding collision-free paths for multiple agents on a graph. This paper describes MAPF-based software for solving train planning and replanning problems on large-scale railway networks under uncertainty. The software recently won the 2020 Flatland Challenge, a NeurIPS competition trying to determine how to efficiently manage dense traffic on rail networks. The software incorporates many state-of-the-art MAPF, or in general, optimization technologies, such as prioritized planning, large neighborhood search, safe interval path planning, minimum communication policies, parallel computing, and simulated annealing. It can plan collision-free paths for thousands of trains within a few minutes and deliver deadlock-free actions in real-time during execution.

AAAI Conference 2021 Conference Paper

Symmetry Breaking for k-Robust Multi-Agent Path Finding

  • Zhe Chen
  • Daniel D. Harabor
  • Jiaoyang Li
  • Peter J. Stuckey

During Multi-Agent Path Finding (MAPF) problems, agents can be delayed by unexpected events. To address such situations recent work describes k-Robust Conflict-Based Search (k-CBS): an algorithm that produces a coordinated and collision-free plan that is robust for up to k delays for any agent. In this work we introduce a variety of pairwise symmetry breaking constraints, specific to k-robust planning, that can efficiently find compatible and optimal paths for pairs of colliding agents. We give a thorough description of the new constraints and report large improvements to success rate in a range of domains including: (i) classic MAPF benchmarks, (ii) automated warehouse domains, and (iii) on maps from the 2019 Flatland Challenge, a recently introduced railway domain where k-robust planning can be fruitfully applied to schedule trains.

LOPSTR Conference 2020 Conference Paper

Algorithm Selection for Dynamic Symbolic Execution: A Preliminary Study

  • Roberto Amadini
  • Graeme Gange
  • Peter Schachte
  • Harald Søndergaard
  • Peter J. Stuckey

Abstract Given a portfolio of algorithms, the goal of Algorithm Selection ( AS ) is to select the best algorithm(s) for a new, unseen problem instance. Dynamic Symbolic Execution ( DSE ) brings together concrete and symbolic execution to maximise the program coverage. DSE uses a constraint solver to solve the path conditions and generate new inputs to explore. In this paper we join these lines of research by introducing a model that combines DSE and AS approaches. The proposed AS/DSE model is a generic and flexible framework enabling the DSE engine to solve the path conditions it collects with a portfolio of different solvers, by exploiting and extending the well-known AS techniques that have been developed over the last decade. In this way, one can increase the coverage and sometimes even outperform the aggregate coverage achievable by running simultaneously all the solvers of the portfolio.

ICAPS Conference 2020 Conference Paper

Bounded Suboptimal Path Planning with Compressed Path Databases

  • Shizhe Zhao
  • Mattia Chiari
  • Adi Botea
  • Alfonso Emilio Gerevini
  • Daniel Harabor
  • Alessandro Saetti
  • Peter J. Stuckey

Compressed Path Databases (CPDs) are a state-of-the-art method for path planning. They record, for each start position, an optimal first move to reach any target position. Computing an optimal path with CPDs is extremely fast and requires no state-space search. The main disadvantages are overhead related: building a CPD usually involves an all-pairs precomputation, and storing the result often incurs prohibitive space overheads. Previous research has focused on reducing the size of CPDs and/or improving their online performance. In this paper we consider a new type of CPD, which can also dramatically reduce preprocessing times. Our idea involves computing first-move data for only selected target nodes; chosen in such a way as to guarantee that the cost of any extracted path is within a fixed bound of the optimal solution. Empirical results demonstrate that our new bounded suboptimal CPDs improve preprocessing times by orders of magnitude. They further reduce storage costs, and compute paths more quickly – all in exchange for only a small amount of suboptimality.

AIJ Journal 2020 Journal Article

Dashed strings for string constraint solving

  • Roberto Amadini
  • Graeme Gange
  • Peter J. Stuckey

String processing is ubiquitous across computer science, and arguably more so in web programming — where it is also a critical part of security issues such as injection attacks. In recent years, a number of string solvers have been developed to solve combinatorial problems involving string variables and constraints. We examine the dashed string approach to string constraint solving, which represents an unknown string as a sequence of blocks of characters with bounds on their cardinalities. The solving approach relies on propagation of information about the blocks of characters that arise from reasoning about the constraints in which they occur. This approach shows promising performance on many benchmarks involving constraints like string length, equality, concatenation, and regular expression membership. In this paper, we formally review the definition, the properties and the use of dashed strings for string constraint solving, and we provide an empirical validation that confirms the effectiveness of this approach.

AAAI Conference 2020 Conference Paper

Dynamic Programming for Predict+Optimise

  • Emir Demirovi?
  • Peter J. Stuckey
  • Tias Guns
  • James Bailey
  • Christopher Leckie
  • Kotagiri Ramamohanarao
  • Jeffrey Chan

We study the predict+optimise problem, where machine learning and combinatorial optimisation must interact to achieve a common goal. These problems are important when optimisation needs to be performed on input parameters that are not fully observed but must instead be estimated using machine learning. We provide a novel learning technique for predict+optimise to directly reason about the underlying combinatorial optimisation problem, offering a meaningful integration of machine learning and optimisation. This is done by representing the combinatorial problem as a piecewise linear function parameterised by the coefficients of the learning model and then iteratively performing coordinate descent on the learning coefficients. Our approach is applicable to linear learning functions and any optimisation problem solvable by dynamic programming. We illustrate the effectiveness of our approach on benchmarks from the literature.

IJCAI Conference 2020 Conference Paper

Euclidean Pathfinding with Compressed Path Databases

  • Bojie Shen
  • Muhammad Aamir Cheema
  • Daniel Harabor
  • Peter J. Stuckey

We consider optimal and anytime algorithms for the Euclidean Shortest Path Problem (ESPP) in two dimensions. Our approach leverages ideas from two recent works: Polyanya, a mesh-based ESPP planner which we use to represent and reason about the environment, and Compressed Path Databases, a speedup technique for pathfinding on grids and spatial networks, which we exploit to compute fast candidate paths. In a range of experiments and empirical comparisons we show that: (i) the auxiliary data structures required by the new method are cheap to build and store; (ii) for optimal search, the new algorithm is faster than a range of recent ESPP planners, with speedups ranging from several factors to over one order of magnitude; (iii) for anytime search, where feasible solutions are needed fast, we report even better runtimes.

SoCS Conference 2020 Conference Paper

F-Cardinal Conflicts in Conflict-Based Search

  • Eli Boyarski
  • Daniel Harabor
  • Peter J. Stuckey
  • Pierre Le Bodic
  • Ariel Felner

Conflict-Based Search (CBS) is a leading algorithm for optimal Multi-Agent Path Finding (MAPF) which features strong performance. In CBS, one conflict in a high-level node is resolved to generate two child nodes, until a node with no conflicts is found. Choosing the right conflict to resolve can greatly speed up the search. It is currently recommended to resolve cardinal conflicts first, resolving them yields two child nodes with a higher cost than the cost of their parent. However, since the recent addition of high-level heuristics to CBS, when resolving cardinal conflicts, the h-value of high-level child nodes often decreases by the same amount as their cost increases. This diminishes the effectiveness of the cardinal conflicts distinction. We propose an expanded categorization of conflicts into f-cardinal, g-cardinal, and non-cardinal. F-cardinal conflicts should be resolved first. Resolving f-cardinal conflicts generates child nodes with an increased f-value relative to their parent. We propose two methods for identifying f-cardinal conflicts. Finally, we demonstrate on standard benchmarks that choosing conflicts according to this expanded categorization increases the effectiveness of modern CBS.

IJCAI Conference 2020 Conference Paper

Iterative-Deepening Conflict-Based Search

  • Eli Boyarski
  • Ariel Felner
  • Daniel Harabor
  • Peter J. Stuckey
  • Liron Cohen
  • Jiaoyang Li
  • Sven Koenig

Conflict-Based Search (CBS) is a leading algorithm for optimal Multi-Agent Path Finding (MAPF). CBS variants typically compute MAPF solutions using some form of A* search. However, they often do so under strict time limits so as to avoid exhausting the available memory. In this paper, we present IDCBS, an iterative-deepening variant of CBS which can be executed without exhausting the memory and without strict time limits. IDCBS can be substantially faster than CBS due to incremental methods that it uses when processing CBS nodes.

AAAI Conference 2020 Conference Paper

Modelling and Solving Online Optimisation Problems

  • Alexander Ek
  • Maria Garcia de la Banda
  • Andreas Schutt
  • Peter J. Stuckey
  • Guido Tack

Many optimisation problems are of an online—also called dynamic—nature, where new information is expected to arrive and the problem must be resolved in an ongoing fashion to (a) improve or revise previous decisions and (b) take new ones. Typically, building an online decision-making system requires substantial ad-hoc coding to ensure the offline version of the optimisation problem is continually adjusted and resolved. This paper defines a general framework for automatically solving online optimisation problems. This is achieved by extending a model of the offline optimisation problem, from which an online version is automatically constructed, thus requiring no further modelling effort. In doing so, it formalises many of the aspects that arise in online optimisation problems. The same framework can be applied for automatically creating sliding-window solving approaches for problems that have a large time horizon. Experiments show we can automatically create efficient online and sliding-window solutions to optimisation problems.

AAAI Conference 2020 Conference Paper

Modelling Diversity of Solutions

  • Linnea Ingmar
  • Maria Garcia de la Banda
  • Peter J. Stuckey
  • Guido Tack

For many combinatorial problems, finding a single solution is not enough. This is clearly the case for multi-objective optimization problems, as they have no single “best solution” and, thus, it is useful to find a representation of the nondominated solutions (the Pareto frontier). However, it also applies to single objective optimization problems, where one may be interested in finding several (close to) optimal solutions that illustrate some form of diversity. The same applies to satisfaction problems. This is because models usually idealize the problem in some way, and a diverse pool of solutions may provide a better choice with respect to considerations that are omitted or simplified in the model. This paper describes a general framework for finding k diverse solutions to a combinatorial problem (be it satisfaction, single-objective or multi-objective), various approaches to solve problems in the framework, their implementations, and an experimental evaluation of their practicality.

ICAPS Conference 2020 Conference Paper

New Techniques for Pairwise Symmetry Breaking in Multi-Agent Path Finding

  • Jiaoyang Li 0001
  • Graeme Gange
  • Daniel Harabor
  • Peter J. Stuckey
  • Hang Ma 0001
  • Sven Koenig

We consider two new classes of pairwise path symmetries which appear in the context of Multi-Agent Path Finding (MAPF). The first of them, corridor symmetry, arises when two agents attempt to pass through the same narrow passage in opposite directions. The second, target symmetry, arises when the shortest path of one agent passes through the target location of a second agent after the second agent has already arrived at it. These symmetries can produce an exponential explosion in the space of possible collision resolutions, leading to unacceptable runtimes even for state-of-the-art MAPF algorithms such as Conflict-Based Search (CBS). We propose to break these symmetries using new reasoning techniques that: (1) detect each class of symmetry and (2) resolve them by introducing specialized constraints. We experimentally show that our techniques can, in some cases, more than double the success rate of CBS and improve its runtime by one order of magnitude.

SoCS Conference 2020 Conference Paper

New Techniques for Pairwise Symmetry Breaking in Multi-Agent Path Finding

  • Jiaoyang Li 0001
  • Graeme Gange
  • Daniel Harabor
  • Peter J. Stuckey
  • Hang Ma 0001
  • Sven Koenig

We consider two new types of pairwise path symmetries which appear in the context of Multi-Agent Path Finding (MAPF). The first of them, corridor symmetry, arises when two agents attempt to pass through the same narrow passage but in opposite directions. The second, target symmetry, arises when the shortest path of one agent requires the target location of a second agent after the second agent has already arrived. These symmetries can produce an exponential blowup in the space of possible collision resolutions, leading to timeout failure even for state-of-the-art algorithms such as Conflict-Based Search. We propose to break symmetries using new reasoning techniques that: (1) detect each type of situation and, (2) resolve them by introducing specialized constraints. We implement our ideas in the context of Conflict-Based Search where, in a range of experiments, we report up to an order-of-magnitude improvement in runtime performance and, in some cases, more than a doubling in success rate.

ICAPS Conference 2020 Conference Paper

Online Computation of Euclidean Shortest Paths in Two Dimensions

  • Ryan Hechenberger
  • Peter J. Stuckey
  • Daniel Harabor
  • Pierre Le Bodic
  • Muhammad Aamir Cheema

We consider the online version of Euclidean Shortest Path (ESP): a problem that asks for distance minimal trajectories between traversable pairs of points in the plane. The problem is made challenging because each trajectory must avoid a set of non-traversable obstacles represented as polygons. To solve ESP practitioners will often preprocess the environment and construct specialised data structures, such as visibility graphs and navigation meshes. Pathfinding queries on these data structures are fast but the preprocessed data becomes invalidated when obstacles move or change. In this work we propose RayScan, a new algorithmic approach for ESP which is entirely online. The central idea is simple: each time we expand a node we also cast a ray toward the target. If an obstacle intersects the ray we scan its perimeter for a turning point; i. e. a vertex from which a new ray can continue unimpeded towards the target. RayScan is fast, optimal and entirely online. Experiments show that it can significantly improve upon current state-of-the-art methods for ESP in cases where the set of obstacles is dynamic.

AAAI Conference 2020 Conference Paper

Smart Predict-and-Optimize for Hard Combinatorial Optimization Problems

  • Jayanta Mandi
  • Emir Demirovi?
  • Peter J. Stuckey
  • Tias Guns

Combinatorial optimization assumes that all parameters of the optimization problem, e. g. the weights in the objective function, are fixed. Often, these weights are mere estimates and increasingly machine learning techniques are used to for their estimation. Recently, Smart Predict and Optimize (SPO) has been proposed for problems with a linear objective function over the predictions, more specifically linear programming problems. It takes the regret of the predictions on the linear problem into account, by repeatedly solving it during learning. We investigate the use of SPO to solve more realistic discrete optimization problems. The main challenge is the repeated solving of the optimization problem. To this end, we investigate ways to relax the problem as well as warm-starting the learning and the solving. Our results show that even for discrete problems it often suffices to train by solving the relaxation in the SPO loss. Furthermore, this approach outperforms the state-of-the-art approach of Wilder, Dilkina, and Tambe. We experiment with weighted knapsack problems as well as complex scheduling problems, and show for the first time that a predict-and-optimize approach can successfully be used on large-scale combinatorial optimization problems.

ECAI Conference 2020 Conference Paper

String Constraint Solving: Past, Present and Future

  • Roberto Amadini
  • Graeme Gange
  • Peter Schachte
  • Harald Søndergaard
  • Peter J. Stuckey

String constraint solving is an important emerging field, given the ubiquity of strings over different fields such as formal analysis, automated testing, database query processing, and cybersecurity. This paper highlights the current state-of-the-art for string constraint solving, and identifies future challenges in this field.

IJCAI Conference 2019 Conference Paper

Branch-and-Cut-and-Price for Multi-Agent Pathfinding

  • Edward Lam
  • Pierre Le Bodic
  • Daniel D. Harabor
  • Peter J. Stuckey

There are currently two broad strategies for optimal Multi-agent Pathfinding (MAPF): (1) search-based methods, which model and solve MAPF directly, and (2) compilation-based solvers, which reduce MAPF to instances of well-known combinatorial problems, and thus, can benefit from advances in solver techniques. In this work, we present an optimal algorithm, BCP, that hybridizes both approaches using Branch-and-Cut-and-Price, a decomposition framework developed for mathematical optimization. We formalize BCP and compare it empirically against CBSH and CBSH-RM, two leading search-based solvers. Conclusive results on standard benchmarks indicate that its performance exceeds the state-of-the-art: solving more instances on smaller grids and scaling reliably to 100 or more agents on larger game maps.

ICAPS Conference 2019 Conference Paper

Cutting the Size of Compressed Path Databases with Wildcards and Redundant Symbols

  • Mattia Chiari
  • Shizhe Zhao
  • Adi Botea
  • Alfonso Emilio Gerevini
  • Daniel Harabor
  • Alessandro Saetti
  • Matteo Salvetti
  • Peter J. Stuckey

Path planning on gridmaps is a common problem in AI and a popular topic in application areas such as computer games. Compressed Path Databases (CPDs) represent a state-of-theart approach to the problem, in terms of the speed of computing full optimal paths and also individual optimal moves. Despite significant improvements in recent years, the memory required to store a CPD can still be a bottleneck for large game maps. In this work we present a new compression approach that can reduce the size of CPDs. Our approach uses an extended notion of wildcards and a novel concept called a redundant symbol. We implement our ideas on top of a state-of-the-art CPD system and, in a range of experiments, we demonstrate a substantial reduction in the size of CPDs.

ICAPS Conference 2019 Conference Paper

Disjoint Splitting for Multi-Agent Path Finding with Conflict-Based Search

  • Jiaoyang Li 0001
  • Daniel Harabor
  • Peter J. Stuckey
  • Hang Ma 0001
  • Sven Koenig

Multi-Agent Path Finding (MAPF) is the planning problem of finding collision-free paths for a team of agents. We focus on Conflict-Based Search (CBS), a two-level tree-search state-of-the-art MAPF algorithm. The standard splitting strategy used by CBS is not disjoint, i. e. , when it splits a problem into two subproblems, some solutions are shared by both subproblems, which can create duplication of search effort. In this paper, we demonstrate how to improve CBS with disjoint splitting and how to modify the low-level search of CBS to take maximal advantage of it. Experiments show that disjoint splitting increases the success rates and speeds of CBS and its variants by up to 2 orders of magnitude.

SoCS Conference 2019 Conference Paper

Extended Abstract: Searching with Consistent Prioritization for Multi-Agent Path Finding

  • Hang Ma 0001
  • Daniel Harabor
  • Peter J. Stuckey
  • Jiaoyang Li 0001
  • Sven Koenig

We study prioritized planning for Multi-Agent Path Finding (MAPF). Existing prioritized MAPF algorithms depend on rule-of-thumb heuristics and random assignment to determine a fixed total priority ordering of all agents a priori. We instead explore the space of all possible partial priority orderings as part of a novel systematic and conflict-driven combinatorial search framework. In a variety of empirical comparisons, we demonstrate state-of-the-art solution qualities and success rates, often with similar runtimes to existing algorithms. We also develop new theoretical results that explore the limitations of prioritized planning, in terms of completeness and optimality, for the first time. This paper was published at AAAI 2019.

ICAPS Conference 2019 Conference Paper

Lazy CBS: Implicit Conflict-Based Search Using Lazy Clause Generation

  • Graeme Gange
  • Daniel Harabor
  • Peter J. Stuckey

Conflict-based Search (CBS) is a effective approach to optimal multi-agent path finding. However, performance of CBS approaches degrade rapidly in highly-contended graphs with many agents. One of the reasons this occurs is that CBS does not detect independent subproblems; i. e. it can re-solve the same conflicts between the same pairs of agents up to exponentially many times, each time along a different branch. Constraint programming approaches with nogood learning avoid this kind of duplication of effort by storing nogoods that record the reasons for conflicts. This can exponentially reduce search in constraint programming. In this work, we present Lazy CBS, a new approach to multi-agent pathfinding which replaces the high-level solver of CBS with a lazily constructed constraint programming model with nogoods. We use core-guided depth-first search to explore the space of conflicts and we detect along each branch reusable nogoods which help to quickly identify feasible solutions. Our experiments show that Lazy CBS can significantly improve on the state-of-the-art for optimal MAPF problems under the sumof-costs metric, especially in cases where there exists significant contention.

IJCAI Conference 2019 Conference Paper

Path Planning with CPD Heuristics

  • Massimo Bono
  • Alfonso E. Gerevini
  • Daniel D. Harabor
  • Peter J. Stuckey

Compressed Path Databases (CPDs) are a leading technique for optimal pathfinding in graphs with static edge costs. In this work we investigate CPDs as admissible heuristic functions and we apply them in two distinct settings: problems where the graph is subject to dynamically changing costs, and anytime settings where deliberation time is limited. Conventional heuristics derive cost-to-go estimates by reasoning about a tentative and usually infeasible path, from the current node to the target. CPD-based heuristics derive cost-to-go estimates by computing a concrete and usually feasible path. We exploit such paths to bound the optimal solution, not just from below but also from above. We demonstrate the benefit of this approach in a range of experiments on standard gridmaps and in comparison to Landmarks, a popular alternative also developed for searching in explicit state-spaces.

IJCAI Conference 2019 Conference Paper

Predict+Optimise with Ranking Objectives: Exhaustively Learning Linear Functions

  • Emir Demirovic
  • Peter J. Stuckey
  • James Bailey
  • Jeffrey Chan
  • Christopher Leckie
  • Kotagiri Ramamohanarao
  • Tias Guns

We study the predict+optimise problem, where machine learning and combinatorial optimisation must interact to achieve a common goal. These problems are important when optimisation needs to be performed on input parameters that are not fully observed but must instead be estimated using machine learning. Our contributions are two-fold: 1) we provide theoretical insight into the properties and computational complexity of predict+optimise problems in general, and 2) develop a novel framework that, in contrast to related work, guarantees to compute the optimal parameters for a linear learning function given any ranking optimisation problem. We illustrate the applicability of our framework for the particular case of the unit-weighted knapsack predict+optimise problem and evaluate on benchmarks from the literature.

IJCAI Conference 2019 Conference Paper

Regarding Jump Point Search and Subgoal Graphs

  • Daniel D. Harabor
  • Tansel Uras
  • Peter J. Stuckey
  • Sven Koenig

In this paper, we define Jump Point Graphs (JP), a preprocessing-based path-planning technique similar to Subgoal Graphs (SG). JP allows for the first time the combination of Jump Point Search style pruning in the context of abstraction-based speedup techniques, such as Contraction Hierarchies. We compare JP with SG and its variants and report new state-of-the-art results for grid-based pathfinding.

AAAI Conference 2019 Conference Paper

Searching with Consistent Prioritization for Multi-Agent Path Finding

  • Hang Ma
  • Daniel Harabor
  • Peter J. Stuckey
  • Jiaoyang Li
  • Sven Koenig

We study prioritized planning for Multi-Agent Path Finding (MAPF). Existing prioritized MAPF algorithms depend on rule-of-thumb heuristics and random assignment to determine a fixed total priority ordering of all agents a priori. We instead explore the space of all possible partial priority orderings as part of a novel systematic and conflict-driven combinatorial search framework. In a variety of empirical comparisons, we demonstrate state-of-the-art solution qualities and success rates, often with similar runtimes to existing algorithms. We also develop new theoretical results that explore the limitations of prioritized planning, in terms of completeness and optimality, for the first time.

AAAI Conference 2019 Conference Paper

Symmetry-Breaking Constraints for Grid-Based Multi-Agent Path Finding

  • Jiaoyang Li
  • Daniel Harabor
  • Peter J. Stuckey
  • Hang Ma
  • Sven Koenig

We describe a new way of reasoning about symmetric collisions for Multi-Agent Path Finding (MAPF) on 4-neighbor grids. We also introduce a symmetry-breaking constraint to resolve these conflicts. This specialized technique allows us to identify and eliminate, in a single step, all permutations of two currently assigned but incompatible paths. Each such permutation has exactly the same cost as a current path, and each one results in a new collision between the same two agents. We show that the addition of symmetry-breaking techniques can lead to an exponential reduction in the size of the search space of CBS, a popular framework for MAPF, and report significant improvements in both runtime and success rate versus CBSH and EPEA* – two recent and state-of-the-art MAPF algorithms.

SoCS Conference 2019 Conference Paper

Symmetry-Breaking Constraints for Grid-Based Multi-Agent Path Finding

  • Jiaoyang Li 0001
  • Daniel Harabor
  • Peter J. Stuckey
  • Hang Ma 0001
  • Sven Koenig

We describe a new way of reasoning about symmetric collisions for Multi-Agent Path Finding (MAPF) on 4-neighbor grids. We also introduce a symmetry-breaking constraint to resolve these conflicts. This specialized technique allows us to identify and eliminate, in a single step, all permutations of two currently assigned but incompatible paths. Each such permutation has exactly the same cost as a current path, and each one results in a new collision between the same two agents. We show that the addition of symmetry-breaking techniques can lead to an exponential reduction in the size of the search space of CBS, a popular framework for MAPF, and report significant improvements in both runtime and success rate versus CBSH and EPEA* – two recent and state-of-the-art MAPF algorithms.

SoCS Conference 2018 Conference Paper

Forward Search in Contraction Hierarchies

  • Daniel Harabor
  • Peter J. Stuckey

Contraction hierarchies are graph-based data structure developed to speed up shortest path search in road networks. Built during an offline pre-processing step, contraction hierarchies are always paired with an online query algorithm which is a variation on bi-directional Dijkstra search. Though effective and highly popular this combination can sometimes be difficult to extend, for example in order to leverage goal-directed heuristics or other forward-driven pruning techniques. In this paper we deconstruct the bi-directional query algorithm of contraction hierarchies and derive a new algorithmic schema which is compatible with standard uni-directional or bi-directional search. We then develop a variety of new uni-directional query algorithms to find optimal paths in contraction hierarchies. These are based on the combination of A* search and Geometric Containers, a well known and successful edge-pruning technique. Empirical results show that our approach can improve search times by an order of magnitude vs bi-directional Dijkstra, albeit at the cost of additional memory and pre-processing time.

IJCAI Conference 2018 Conference Paper

Machine Learning and Constraint Programming for Relational-To-Ontology Schema Mapping

  • Diego de Uña
  • Nataliia Rümmele
  • Graeme Gange
  • Peter Schachte
  • Peter J. Stuckey

The problem of integrating heterogeneous data sources into an ontology is highly relevant in the database field. Several techniques exist to approach the problem, but side constraints on the data cannot be easily implemented and thus the results may be inconsistent. In this paper we improve previous work by Taheriyan et al. [2016a] using Machine Learning (ML) to take into account inconsistencies in the data (unmatchable attributes) and encode the problem as a variation of the Steiner Tree, for which we use work by De Uña et al. [2016] in Constraint Programming (CP). Combining ML and CP achieves state-of-the-art precision, recall and speed, and provides a more flexible framework for variations of the problem.

SAT Conference 2017 Conference Paper

A Benders Decomposition Approach to Deciding Modular Linear Integer Arithmetic

  • Bishoksan Kafle
  • Graeme Gange
  • Peter Schachte
  • Harald Søndergaard
  • Peter J. Stuckey

Abstract Verification tasks frequently require deciding systems of linear constraints over modular (machine) arithmetic. Existing approaches for reasoning over modular arithmetic use bit-vector solvers, or else approximate machine integers with mathematical integers and use arithmetic solvers. Neither is ideal; the first is sound but inefficient, and the second is efficient but unsound. We describe a linear encoding which correctly describes modular arithmetic semantics, yielding an optimistic but sound approach. Our method abstracts the problem with linear arithmetic, but progressively refines the abstraction when modular semantics is violated. This preserves soundness while exploiting the mostly integer nature of the constraint problem. We present a prototype implementation, which gives encouraging experimental results.

TCS Journal 2016 Journal Article

A complete refinement procedure for regular separability of context-free languages

  • Graeme Gange
  • Jorge A. Navas
  • Peter Schachte
  • Harald Søndergaard
  • Peter J. Stuckey

Often, when analyzing the behaviour of systems modelled as context-free languages, we wish to know if two languages overlap. To this end, we present a class of semi-decision procedures for regular separability of context-free languages, based on counter-example guided abstraction refinement. We propose two effective instances of this approach, one that is complete but relatively expensive, and one that is inexpensive and sound, but for which we do not have a completeness proof. The complete method will prove disjointness whenever the input languages are regularly separable. Both methods will terminate whenever the input languages overlap. We provide an experimental evaluation of these procedures, and demonstrate their practicality on a range of verification and language-theoretic instances.

AAMAS Conference 2016 Conference Paper

Discrete Optimization for Agents

  • Peter J. Stuckey

Many an agent needs to make a decision of what do to given a limited amount of resources. This is a discrete optimization problem. Recent advances in discrete optimization modelling technology have made it easier than ever before to model difficult ad hoc optimization problems, and apply off the shelf solving technology rapidly and efficiently, while rapid advances in discrete optimization solving technology have made it faster than ever before to solve such problems. In this talk I will illustrate how • modern languages allow us to capture the combinatorial substructure of discrete optimization problems thus allowing solving to be much more rapid; • how nogood learning can exponentially improve our ability to solve these problems; • and how these combine to allow us to rapidly resolve problems that are slowly changing, a case that seems particularly relevant to agents readjusting their plans in a changing environment My hope is that the agent community will be inspired to learn and use more of the tools and techniques developed by the discrete optimization community. CCS Concepts •Mathematics of computing → Discrete optimization; •Theory of computation → Constraint and logic programming; •Hardware → Theorem proving and SAT solving;

ECAI Conference 2016 Conference Paper

Efficient Computation of Exact IRV Margins

  • Michelle L. Blom
  • Vanessa Teague
  • Peter J. Stuckey
  • Ron Tidhar

Computing the margin of victory (MOV) in an Instant Runoff Voting (IRV) election is NP-hard. In an IRV election with winning candidate w, the MOV defines the smallest number of cast votes that, if modified, result in the election of a candidate other than w. The ability to compute such margins has significant value. Arguments over the correctness of an election outcome usually rely on the size of the electoral margin. Risk-limiting audits use the size of this margin to determine how much post-election auditing is required. We present an efficient branch-and-bound algorithm for computing exact margins that substantially improves on the current best-known approach. Although exponential in the worst case, our algorithm runs efficiently in practice, computing margins in instances that could not be solved by the current state-of-the-art in a reasonable time frame.

LOPSTR Conference 2016 Conference Paper

MiniZinc with Strings

  • Roberto Amadini
  • Pierre Flener
  • Justin Pearson
  • Joseph D. Scott
  • Peter J. Stuckey
  • Guido Tack

Abstract Strings are extensively used in modern programming languages and constraints over strings of unknown length occur in a wide range of real-world applications such as software analysis and verification, testing, model checking, and web security. Nevertheless, practically no constraint programming solver natively supports string constraints. We introduce string variables and a suitable set of string constraints as builtin features of the MiniZinc modelling language. Furthermore, we define an interpreter for converting a MiniZinc model with strings into a FlatZinc instance relying only on integer variables. This conversion is obtained via rewrite rules, and does not require any extension of the existing FlatZinc specification. This provides a user-friendly interface for modelling combinatorial problems with strings, and enables both string and non-string solvers to actually solve such problems.

IJCAI Conference 2016 Conference Paper

Sequencing Operator Counts

  • Toby O. Davies
  • Adrian R. Pearce
  • Peter J. Stuckey
  • Nir Lipovetzky

Operator-counting is a recently developed framework for analysing and integrating many state-of-the-art heuristics for planning using Linear Programming. In cost-optimal planning only the objective value of these heuristics is traditionally used to guide the search. However the primal solution, i. e. the operator counts, contains useful information. We exploit this information using a SAT-based approach which given an operator-count, either finds a valid plan; or generates a generalized landmark constraint violated by that count. We show that these generalized landmarks can be used to encode the perfect heuristic, h*, as a Mixed Integer Program. Our most interesting experimental result is that finding or refuting a sequence for an operator-count is most often empirically efficient, enabling a novel and promising approach to planning based on Logic-Based Benders Decomposition (LBBD).

SAT Conference 2015 Conference Paper

#∃SAT: Projected Model Counting

  • Rehan Abdul Aziz
  • Geoffrey Chu
  • Christian J. Muise
  • Peter J. Stuckey

Abstract Model counting is the task of computing the number of assignments to variables \(\mathcal{V}\) that satisfy a given propositional theory F. The model counting problem is denoted as #SAT. Model counting is an essential tool in probabilistic reasoning. In this paper, we introduce the problem of model counting projected on a subset of original variables that we call priority variables \(\mathcal{P}\subseteq \mathcal{V}\). The task is to compute the number of assignments to \(\mathcal{P}\) such that there exists an extension to non-priority variables \(\mathcal{V}\setminus \mathcal{P}\) that satisfies F. We denote this as \(\#\exists \) SAT. Projected model counting arises when some parts of the model are irrelevant to the counts, in particular when we require additional variables to model the problem we are counting in SAT. We discuss three different approaches to \(\#\exists \) SAT (two of which are novel), and compare their performance on different benchmark problems.

ICAPS Conference 2015 Conference Paper

Sequencing Operator Counts

  • Toby O. Davies
  • Adrian R. Pearce
  • Peter J. Stuckey
  • Nir Lipovetzky

Operator-counting is a recently developed framework for analysing and integrating many state-of-the-art heuristics for planning using Linear Programming. In cost-optimal planning only the objective value of these heuristics is traditionally used to guide the search. However the primal solution, i. e. the operator counts, contains useful information. We exploit this information using a SAT-based approach which given an operator-count, either finds a valid plan; or generates a generalized landmark constraint violated by that count. We show that these generalized landmarks can be used to encode the perfect heuristic, h*, as a Mixed Integer Program. Our most interesting experimental result is that finding or refuting a sequence for an operator-count is most often empirically efficient, enabling a novel and promising approach to planning based on Logic-Based Benders Decomposition (LBBD).

LOPSTR Conference 2014 Conference Paper

Analyzing Array Manipulating Programs by Program Transformation

  • J. Robert M. Cornish
  • Graeme Gange
  • Jorge A. Navas
  • Peter Schachte
  • Harald Søndergaard
  • Peter J. Stuckey

Abstract We explore a transformational approach to the problem of verifying simple array-manipulating programs. Traditionally, verification of such programs requires intricate analysis machinery to reason with universally quantified statements about symbolic array segments, such as “every data item stored in the segment A[i] to A[j] is equal to the corresponding item stored in the segment B[i] to B[j]. ” We define a simple abstract machine which allows for set-valued variables and we show how to translate programs with array operations to array-free code for this machine. For the purpose of program analysis, the translated program remains faithful to the semantics of array manipulation. Based on our implementation in LLVM, we evaluate the approach with respect to its ability to extract useful invariants and the cost in terms of code size.

ICAPS Conference 2014 Conference Paper

Fragment-Based Planning Using Column Generation

  • Toby O. Davies
  • Adrian R. Pearce
  • Peter J. Stuckey
  • Harald Søndergaard

We introduce a novel algorithm for temporal planning in Golog using shared resources, and describe the Bulk Freight Rail Scheduling Problem, a motivating example of such a temporal domain. We use the framework of column generation to tackle complex resource constrained temporal planning problems that are beyond the scope of current planning technology by combining: the global view of a linear programming relaxation of the problem; the strength of search infinding action sequences; and the domain knowledge that can be encoded in a Golog program. We show that our approach significantly outperforms state-of-the-art temporal planning and constraint programming approaches in this domain, in addition to existing temporal Golog implementations. We also apply our algorithm to a temporal variant of blocks-world where our decomposition speeds proof of optimality significantly compared to other anytime algorithms. We discuss the potential of the underlying algorithm being applicable to STRIPS planning, with further work.

ICAPS Conference 2014 Conference Paper

Planning for Mining Operations with Time and Resource Constraints

  • Nir Lipovetzky
  • Christina N. Burt
  • Adrian R. Pearce
  • Peter J. Stuckey

We study a daily mine planning problem where, given a set of blocks we wishto mine, our task is to generate a mining sequence for the excavators suchthat blending resource constraints are met at various stages of thesequence. Such time-oriented resource constraintsare not traditionally handled well by automated planners. On the other hand, the remaining problem involves finding node-disjoint sequences withstate-dependent travel times on the arcs, which are highly challenging for a Mixed-Integer Program (MIP). In this paper, we address the problem of finding feasible sequences using a combined MIP and planning based decomposition approach. The MIP takes care of the resource constraints, and the planner solves the remaining sequence problem. We extend the notion of finding feasible sequences to finding good feasible sequences, by devising a heuristic objective function in the MIP, which improves the resulting search space for the planner. We empirically analyse the scalability of our approach on a benchmark data set, before demonstrating its effectiveness on a real world case study provided by our industry partner. These results demonstrate that by using a heuristic MIP, it is possible to obtain better makespan results with a suboptimal planner than by using an optimal planner with an uninformed MIP.

IJCAI Conference 2013 Conference Paper

Breaking Symmetries in Graph Representation

  • Michael Codish
  • Alice Miller
  • Patrick Prosser
  • Peter J. Stuckey

There are many complex combinatorial problems which involve searching for an undirected graph satisfying a certain property. These problems are often highly challenging because of the large number of isomorphic representations of a possible solution. In this paper we introduce novel, effective and compact, symmetry breaking constraints for undirected graph search. While incomplete, these prove highly beneficial in pruning the search for a graph. We illustrate the application of symmetry breaking in graph representation to resolve several open instances in extremal graph theory.

SAT Conference 2013 Invited Paper

There Are No CNF Problems

  • Peter J. Stuckey

Abstract SAT technology has improved rapidly in recent years, to the point now where it can solve CNF problems of immense size. But solving CNF problems ignores one important fact: there are NO problems that are originally CNF. All the CNF that SAT solvers tackle is the result of modelling some real world problem, and mapping the high-level constraints and decisions modelling the problem into clauses on binary variables. But by throwing away the high level view of the problem SAT solving may have lost a lot of important insight into how the problem is best solved. In this talk I will hope to persuade you that by keeping the original high level model of the problem one can realise immense benefits in solving hard real world problems.

AIJ Journal 2012 Journal Article

A complete solution to the Maximum Density Still Life Problem

  • Geoffrey Chu
  • Peter J. Stuckey

The Maximum Density Still Life Problem (CSPLib prob032) is to find the maximum number of live cells that can fit in an n × n region of an infinite board, so that the board is stable under the rules of Conwayʼs Game of Life. It is considered a very difficult problem and has a raw search space of O ( 2 n 2 ). Previous state of the art methods could only solve up to n = 20. We give a powerful reformulation of the problem into one of minimizing “wastage” instead of maximizing the number of live cells. This reformulation allows us to compute very strong upper bounds on the number of live cells, which dramatically reduces the search space. It also gives us significant insights into the nature of the problem. By combining these insights with several powerful techniques: remodeling, lazy clause generation, bounded dynamic programming, relaxations, and custom search, we are able to solve the Maximum Density Still Life Problem for all n. This is possible because the Maximum Density Still Life Problem is in fact well behaved mathematically for sufficiently large n (around n > 200 ) and if such very large instances can be solved, then there exist ways to construct provably optimal solutions for all n from a finite set of base solutions. Thus we show that the Maximum Density Still Life Problem has a closed form solution and does not require exponential time to solve.

LOPSTR Conference 2012 Conference Paper

An Introduction to Search Combinators

  • Tom Schrijvers
  • Guido Tack
  • Pieter Wuille
  • Horst Samulowitz
  • Peter J. Stuckey

Abstract The ability to model search in a constraint solver can be an essential asset for solving combinatorial problems. However, existing infrastructure for defining search heuristics is often inadequate. Either modeling capabilities are extremely limited or users are faced with a general-purpose programming language whose features are not tailored towards writing search heuristics. As a result, major improvements in performance may remain unexplored. This article introduces search combinators, a lightweight and solver-independent method that bridges the gap between a conceptually simple modeling language for search (high-level, functional and naturally compositional) and an efficient implementation (low-level, imperative and highly non-modular). By allowing the user to define application-tailored search strategies from a small set of primitives, search combinators effectively provide a rich domain-specific language (DSL) for modeling search to the user. Remarkably, this DSL comes at a low implementation cost to the developer of a constraint solver.

SAT Conference 2011 Conference Paper

Reducing Chaos in SAT-Like Search: Finding Solutions Close to a Given One

  • Ignasi Abío
  • Morgan Deters
  • Robert Nieuwenhuis
  • Peter J. Stuckey

Abstract Motivated by our own industrial users, we attack the following challenge that is crucial in many practical planning, scheduling or timetabling applications. Assume that a solver has found a solution for a given hard problem and, due to unforeseen circumstances (e. g. , re-scheduling), or after an analysis by a committee, a few more constraints have to be added and the solver has to be re-run. Then it is almost always important that the new solution is “close” to the original one. The activity-based variable selection heuristics used by SAT solvers make search chaotic, i. e. , extremely sensitive to the initial conditions. Therefore, re-running with just one additional clause added at the end of the input usually gives a completely different solution. We show that naive approaches for finding close solutions do not work at all, and that solving the Boolean optimization problem is far too inefficient: to find a reasonably close solution, state-of-the-art tools typically require much more time than was needed to solve the original problem. Here we propose the first (to our knowledge) approach that obtains close solutions quickly. In fact, it typically finds the optimal (i. e. , closest) solution in only 25% of the time the solver took in solving the original problem. Our approach requires no deep theoretical or conceptual innovations. Still, it is non-trivial to come up with and will certainly be valuable for researchers and practitioners facing the same problem.

IJCAI Conference 2011 Conference Paper

Symmetries and Lazy Clause Generation

  • Geoffrey Chu
  • Peter J. Stuckey
  • Maria Garcia de la Banda
  • Chris Mears

Lazy clause generation is a powerful approach to reducing search in constraint programming. This is achieved by recording sets of domain restrictions that previously led to failure as new clausal propagators. Symmetry breaking approaches are also powerful methods for reducing search by recog- nizing that parts of the search tree are symmetric and do not need to be explored. In this paper we show how we can successfully combine symmetry breaking methods with lazy clause generation. Further, we show that the more precise nogoods generated by a lazy clause solver allow our combined approach to exploit redundancies that cannot be exploited via any previous symmetry breaking method, be it static or dynamic.

ECAI Conference 2008 Conference Paper

Fast Set Bounds Propagation using BDDs

  • Graeme Gange
  • Vitaly Lagoon
  • Peter J. Stuckey

Set bounds propagation is the most popular approach to solving constraint satisfaction problems (CSPs) involving set variables. The use of reduced ordered Binary Decision Diagrams (BDDs) to represent and solve set CSPs is well understood and brings the advantage that propagators for arbitrary set constraints can be built. This can substantially improve solving. The disadvantages of BDDs is that creating and manipulating BDDs can be expensive. In this paper we show how we can perform set bounds propagation using BDDs in a much more efficient manner by generically creating set constraint predicates, and using a marking approach to propagation. The resulting system can be significantly faster than competing approaches to set bounds propagation.

AIJ Journal 2000 Journal Article

A Lagrangian reconstruction of GENET

  • Kenneth M.F. Choi
  • Jimmy H.M. Lee
  • Peter J. Stuckey

GENET is a heuristic repair algorithm which demonstrates impressive efficiency in solving some large-scale and hard instances of constraint satisfaction problems (CSPs). In this paper, we draw a surprising connection between GENET and discrete Lagrange multiplier methods. Based on the work of Wah and Shang, we propose a discrete Lagrangian-based search scheme LSDL, defining a class of search algorithms for solving CSPs. We show how GENET can be reconstructed from LSDL. The dual viewpoint of GENET as a heuristic repair method and a discrete Lagrange multiplier method allows us to investigate variants of GENET from both perspectives. Benchmarking results confirm that first, our reconstructed GENET has the same fast convergence behavior as the original GENET implementation, and has competitive performance with other local search solvers DLM, WalkSAT, and Wsat(oip), on a set of difficult benchmark problems. Second, our improved variant, which combines techniques from heuristic repair and discrete Lagrangian methods, is always more efficient than the reconstructed GENET, and can better it by an order of magnitude.

TCS Journal 1998 Journal Article

Foundations of aggregation constraints

  • Kenneth A. Ross
  • Divesh Srivastava
  • Peter J. Stuckey
  • S. Sudarshan

We introduce a new constraint domain, aggregation constraints, that is useful in database query languages, and in constraint logic programming languages that incorporate aggregate functions. We formally study the fundamental problem of determining if a conjunction of aggregation constraints is satisfiable, and show that, for many classes of aggregation constraints, the problem is undecidable. We describe a complete and minimal axiomatization of aggregation constraints, for the SQL aggregate functions min, max, sum, count and average, over a non-empty, finite multiset on several domains. This axiomatization helps identify classes of aggregation constraints for which the satisfiability check is efficient. We present a polynomial-time algorithm that directly checks for satisfiability of a conjunction of aggregation range constraints over a single multiset; this is a practically useful class of aggregation constraints. We discuss the relationships between aggregation constraints over a non-empty, finite multiset of reals, and constraints on the elements of the multiset. We show how these relationships can be used to push constraints through aggregate functions to enable compile-time optimization of database queries involving aggregate functions and constraints.

TCS Journal 1995 Journal Article

Bottom-up evaluation and query optimization of well-founded models

  • David B. Kemp
  • Divesh Srivastava
  • Peter J. Stuckey

We present a bottom-up operational procedure for computing well-founded models of allowed programs with negation. This procedure provides a practical method of handling programs that involve unstratified negation in a manner that may be mixed with other evaluation approaches, such as semi-naive evaluation and various program transformations. We define classes of programs and sideways information of passing strategies (sips) for which the magic sets transformation preserves well-founded models with respect to the query. The classes of programs and sips we consider strictly subsume those already considered in the literature, and include stratified programs (with any choice of sips), left-to-right modularly stratified programs (with left-to-right sips) and arbitrary programs (with well-founded sips). For these programs and sips, our procedure for computing well-founded models is applicable to the rewritten programs, thus allowing increased efficiency of specializing a program for a query. Finally, we describe an extension of our bottom-up operational procedure that operates on the magic sets transformation of arbitrary programs with arbitrary sips, and computes query answers with respect to the well-founded models of the original program.

TCS Journal 1992 Journal Article

Transforming normal logic programs to constraint logic programs

  • Kanchana Kanchanasut
  • Peter J. Stuckey

A normal logic program P is transformed to another P ω by a bottom-up computation on the positive component of P while the negative counterpart is left untouched. The declarative semantics of P is given by the completion of P ω. The completed predicate definitions in P ω, if they do not contain local variables, can be used as a basis for expanding each negated atom in the bodies of P ω. We show that for a class of programs where every negative subgoal can be expanded, the resultant program P′ is a definite logic program with equality and disequality constraints. If the program falls outside this class, the resultant program may be executed using constructive negation. Our proposed scheme provides an effective sound and complete query-answering system for the well-founded models of a class of programs whose positive part has a finite P ω and whose clauses satisfy the positive groundedness property defined herein.

TCS Journal 1986 Journal Article

Semantics of infinite tree logic programming

  • Joxan Jaffar
  • Peter J. Stuckey

We address the problem of declarative and operational semantics for logic programming in the domain of infinite trees. We consider logic programming semantics based on the now familiar function T P which maps from and into interpretations of the program P. The main point of departure of our work from the literature is that we include unequations in our treatment. Specifically, we prove that the intuitive notions of success and finite failure, defined in terms of T P, exactly correspond to the operational semantics. The corresponding proofs in the case where no unequations are considered are relatively straightforward mainly because the function T P has a closure property with respect to a suitable metric space of infinite trees. When unequations are considered, however, the function loses this property and consequently the proofs become more complex. The key to our treatment is a result about images of T P; we show that these sets have a property analogous to closure. Finally, we also prove certain results pertaining to infinite derivations. These concern the greatest fixpoint of T P and the concept of completed logic programs and negation-as-failure.

v2026.09.13