Dynamic analysis of implicit Boolean network for multi-agent pathfinding

Abstract

This paper presents a dynamic analysis of trajectories in an implicit first-order Boolean network that models a multi-agent pathfinding problem on a graph of admissible agent movements. A binary dynamic network model is proposed, capable of solving a number of well-known pathfinding problems for both directed and undirected graphs. This model incorporates two types of constraints (Boolean equations): static and dynamic. Static constraints define the set of admissible network states, while dynamic constraints determine admissible transitions between these states. The core of this formalization is the problem of finding a trajectory (a sequence of transitions) that ensures the reachability of given target states from specified initial states under constraints on the trajectory length. The specifications of the initial and final states are defined in the language of Boolean equations and are incorporated into the dynamics equations of the implicit Boolean network. The solvability of the resulting system of Boolean constraints is verified constructively using a SAT solver. Four practically relevant variants of the reachability property are proposed. Several examples are considered to illustrate the application of the proposed approach to the multi-agent pathfinding problem.