Linear Planar 3-SAT and Its Applications in Planning

TL;DR

This paper introduces Linear Planar 3-SAT, a new NP-complete fragment combining linear and planar constraints, and demonstrates its applications in proving complexity results for multi-agent pathfinding problems.

Contribution

It defines and proves NP-completeness of Linear Planar 3-SAT, and explores its reconfiguration complexity, applying these results to multi-agent pathfinding problems.

Findings

Linear Planar 3-SAT is NP-complete.

Reconfiguration of Linear Planar 3-SAT is PSPACE-complete.

Complexity results for multi-agent pathfinding are established.

Abstract

Several fragments of the satisfiability problem have been studied in the literature. Among these, Linear 3-SAT is a satisfaction problem in which each clause (viewed as a set of literals) intersects with at most one other clause; moreover, any pair of clauses have at most one literal in common. Planar 3-SAT is a fragment which requires that the so-called variable-clause graph is planar. Both fragments are NP-complete and have applications in encoding NP-hard planning problems. In this paper, we investigate the complexity and applications of the fragment obtained combining both features. We define Linear Planar 3-SAT and prove its NP-completeness. We also study the reconfiguration problem of Linear Planar 3-SAT and show that it is PSPACE-complete. As an application, we use these new results to prove the NP-completeness of Bounded Connected Multi-Agent Pathfinding and the PSPACE-completeness of Connected Multi-Agent Pathfinding in two-dimensional grids.