Many existing boundedly-suboptimal heuristic search algorithms are variants of best-first search. Due to memory limitations, these algorithms are unable to solve problems with extremely large search spaces. In this paper, we present a framework that allows best-first search algorithms to solve problems with such large search spaces given a (reasonable) memory bound while also preserving optimality guarantees in tree-structured search spaces. In our framework, a given algorithm is run several times. In each search episode, the algorithm expands up to a user-defined number of states. After each episode, unless the goal has been found, the heuristic values of the generated states are updated using a linear-time algorithm that preserves consistency in tree-structured search spaces. In subsequent search episodes, only the heuristic values of the states generated in the previous episode need to be kept in memory. We present experimental results where we plug A*, GBFS, and wA* into our framework to solve traveling salesman problems and compare them against benchmark linear-memory algorithms like DFBnB and wDFBnB.

Partially Observable Markov Decision Processes (POMDPs) are a popular formalism for sequential decision making in partially observable environments. Since solving POMDPs to optimality is a difficult task, point-based value iteration methods are widely used. These methods compute an approximate POMDP solution, and in some cases they even provide guarantees on the solution quality, but these algorithms have been designed for problems with an infinite planning horizon. In this paper we discuss why state-of-the-art point-based algorithms cannot be easily applied to finite-horizon problems that do not include discounting. Subsequently, we present a general point-based value iteration algorithm for finite-horizon problems which provides solutions with guarantees on solution quality. Furthermore, we introduce two heuristics to reduce the number of belief points considered during execution, which lowers the computational requirements. In experiments we demonstrate that the algorithm is an effective method for solving finite-horizon POMDPs.

Multi-agent pathfinding is the problem of finding a non-interfering paths for a set of agents, such that if the agents follow these paths then each agent will reach its desired destination. Recent years have shown tremendous advances in this field, with optimal and suboptimal algorithms that are able to plan paths for over 100 agents in reasonable time. However, autonomous mobile agents are prime targets for cyber-security attacks, where an adversary may take control over an agent to disrupt the agents execution of their plan. This threat raises two questions. The first question is how much damage can an agent do if it does not follow its plan. The second question is how can one plan a-priori to be as robust as possible to such cyber-attacks. In this work, We provide an answer to both questions. To compute the maximal amount of damage that an adversary agent can do, we define a corresponding graph search problem and solve this problem with A*. Then, we provide a very simple method to choose a solution that is robust to such damages. We demonstrate both algorithms in simulation over standard multi-agent pathfinding domains.

In this paper, we present Satgen, the first implicit generative model of real-world Boolean Satisfiability (SAT) formulas. Our approach uses unsupervised machine learning techniques to generate new formulas by mimicking the structural properties of a given input formula Phi. We proceed in two phases: first, we construct the Literal-Incidence Graph (LIG) of Phi. This is used by a Generative Adversarial Network (GAN) to generate new LIGs that exhibit graph-theoretic properties similar to those of the LIG of Phi. In the second phase, we extract a formula whose LIG would correspond to the generated graph. We show that generating such a formula is equivalent to finding a minimal clique edge cover of the given graph, which we tackle efficiently using a greedy hill-climbing algorithm. We verify experimentally that our approach generates formulas that closely resemble a given real-world SAT instance, as measured by a range of different metrics.

Conflict-Based Search (CBS) is a state of the art algorithm for multi-agent pathfinding (MAPF). CBS has been studied in many domains, however, most research has focused on classic domains with point agents that move with unit time steps and unit costs. In this work, we are interested in MAPF solutions for classic domains and complex domains, that is, domains which include shaped agents, actions with non-unit costs, non-uniform action durations and/or non-holonomic or kinodynamic movement constraints. Prior work on sub-optimal formulations of CBS has focused on heuristics. Instead, our work introduces new types of constraints. We show that certain constraint formulations have properties that can cause CBS to run orders of magnitude faster, but may cause the algorithm to be incomplete and yield sub-optimal results. We introduce new conditional constraints which allow CBS to exploit constraint properties which cause it to run faster and still retain algorithmic completeness. We additionally formulate a new constraint accumulation technique called constraint overloading which utilizes conditional constraints in order to achieve further performance gains.

We describe an attempt to unify search-based and compilation-based approaches to multi-agent path finding (MAPF) through satisfiability modulo theories (SMT). The task in MAPF is to navigate agents in an undirected graph to given goal vertices so that they do not collide. We rephrase Conflict-Based Search (CBS), one of the state-of-the-art algorithms for optimal MAPF solving, in the terms of SMT. This idea combines SAT-based solving known from MDD-SAT, a SAT-based optimal MAPF solver, at the low level with conflict elimination of CBS at the high level. Where the standard CBS branches the search after a conflict occurs, we refine the propositional model with a disjunctive constraint instead. Our novel algorithm called SMT-CBS hence does not branch at the high-level but incrementally extends the propositional model that is consulted with the SAT solver at each iteration. We experimentally compare SMT-CBS with CBS and MDD-SAT.

This paper addresses a variant of multi-agent path finding (MAPF) in continuous space and time. We present a new solving approach based on satisfiability modulo theories (SMT) to obtain makespan optimal solutions. The standard MAPF is a task of navigating agents in an undirected graph from given starting vertices to given goal vertices so that agents do not collide with each other in vertices of the graph. In the continuous version (MAPF-R) agents move in an n-dimensional Euclidean space along straight lines that interconnect predefined positions. For simplicity, we work with circular omni-directional agents having constant velocities in the 2D plane. As agents can have different sizes and move smoothly along lines, a non-colliding movement along certain lines with small agents can result in a collision if the same movement is performed with larger agents. Our SMT-based approach for MAPF-R called SMT-CBS-R reformulates the Conflict-based Search (CBS) algorithm in terms of SMT concepts. We suggest lazy generation of decision variables and constraints. Each time a new conflict is discovered, the underlying encoding is extended with new variables and constraints to eliminate the conflict. We compared SMT-CBS-R and adaptations of CBS for the continuous variant of MAPF experimentally.

In this paper, we study a problem from the realm of multi-criteria decision making in which the goal is to select from a given set S of d-dimensional objects a minimum sized subset S' with bounded regret. Thereby, regret measures the unhappiness of users which would like to select their favorite object from set S but now can only select their favorite object from the subset S'. Previous work focused on bounding the maximum regret which is determined by the most unhappy user. We propose to consider the average regret instead which is determined by the sum of (un)happiness of all possible users. We show that this regret measure comes with desirable properties as supermodularity which allows to construct approximation algorithms. Furthermore, we introduce the regret minimizing permutation problem and discuss extensions of our algorithms to the recently proposed k-regret measure. Our theoretical results are accompanied with experiments on a variety of inputs with d up to 7.

NBS is a non-parametric bidirectional search algorithm, proved to expand at most twice the number of node expansions required to verify the optimality of a solution. We introduce new variants of NBS that are aimed at finding all optimal solutions. We then introduce an algorithmic framework that includes NBS as a special case. Finally, we introduce DVCBS, a new algorithm in this framework that aims to further reduce the number of expansions. Unlike NBS, DVCBS does not have any worst-case bound guarantees, but in practice it outperforms NBS in verifying the optimality of solutions.

In Multi-Agent Path Finding (MAPF), a team of agents needs to find collision-free paths from their starting locations to their respective targets. Combined Target Assignment and Path Finding (TAPF) extends MAPF by including the problem of assigning targets to agents as a precursor to the MAPF problem. A limitation of both models is their assumption that the number of agents and targets are equal, which is invalid in some applications. We address this limitation by generalizing TAPF to allow for (1) unequal number of agents and tasks; (2) tasks to have deadlines by which they must be completed; (3) ordering of groups of tasks to be completed; and (4) tasks that are composed of a sequence of checkpoints that must be visited in a specific order. Further, we model the problem using answer set programming (ASP) to show that customizing the desired variant of the problem is simple -- one only needs to choose the appropriate combination of ASP rules to enforce it. We also demonstrate experimentally that if problem specific information can be incorporated into the ASP encoding then ASP based methods can be efficient and can scale up to solve practical applications.