Migrating Techniques from Search-based Multi-Agent Path Finding Solvers to SAT-based Approach
Authors: Pavel Surynek, Roni Stern, Eli Boyarski, Ariel Felner
JAIR 2022 | Venue PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Experimental evaluation on several domains shows that there are many scenarios where our SAT-based methods outperform state-of-the-art sum-of-costs search-based solvers, such as variants of the ICTS and ICBS algorithms. The experimental evaluation has been extended significantly, including experiments not reported in the conference papers that explore: (i) The impact of using a newer SAT solver on the ability of our algorithms to solve more MAPF problems; (ii) The relation between the computed makespan and the number of time expansions needed to prove its optimality; (iii) The distribution of runtime spent in each time expansion. |
| Researcher Affiliation | Collaboration | Pavel Surynek EMAIL Faculty of Information Technology, Czech Technical University in Prague Th akurova 9, 160 00 Praha 6, Czechia Roni Stern EMAIL Ben Gurion University, Beer-Sheva 84105, Israel Palo Alto Research Center, CA, USA Eli Boyarski EMAIL Ariel Felner EMAIL Ben Gurion University, Beer-Sheva 84105, Israel |
| Pseudocode | Yes | All SAT-based algorithms and encodings are described here in greater details, including detailed pseudo-codes. Detailed proofs of important properties such as completeness and time/space complexity are given. Algorithm 1: Framework of makespan-optimal SAT-based MAPF solving Algorithm 2: Basic SAT-based sum-of-costs optimal MAPF solving. Algorithm 3: Construction of the time expansion graph. Algorithm 4: MAPF solving algorithm based on independence detection technique. Algorithm 5: Independence detection in the sum-of-cost optimal SAT-based solver MDDSAT. Algorithm 6: e MDD-SAT, an (1 + ϵ)-bounded suboptimal version of the MDD-SAT MAPF solver |
| Open Source Code | Yes | The implementation is available as part of a MAPF experimental project on: https://github.com/surynek/reLOC. |
| Open Datasets | Yes | We experimented on 4-connected grids with randomly placed obstacles (Silver, 2005) and on Dragon Age maps (Sharon et al., 2015; Sturtevant, 2012). Both settings are a standard MAPF benchmarks. |
| Dataset Splits | No | The paper describes the generation of random instances for experiments but does not provide specific training/test/validation splits of a fixed dataset. For example, it states: "For each number of agents 10 random instances were generated." and describes how initial positions and goals were selected randomly based on average distance. |
| Hardware Specification | Yes | All experiments were performed on a system with Xeon 2.8Ghz core with 32 Gb of memory. |
| Software Dependencies | Yes | We used Glucose 3.0 (Audemard & Simon, 2009; Audemard, Lagniez, & Simon, 2013), which is a top-performing SAT solver in the recent editions of the SAT Competition... a new SAT solver appeared, namely Maple COMSPS (Liang, 2018; Liang, Oh, Mathew, Thomas, Li, & Ganesh, 2018) |
| Experiment Setup | Yes | We first experimented on 8x8, 16x16, and 32x32 grids with 10% obstacles while increasing the number of agents from 1 up to the last number... For each number of agents 10 random instances were generated. Figure 10 presents success rate results where each algorithm was given a time limit of 300 seconds... The mean distance from initial positions is varied from 8 up to 320 using step 8. Ten random instance were generated per distance. The maximum mean distance was set so that no of the tested algorithms was able to solve instances for the maximum average distance given the time limit of 300 seconds. In test of the bounded variants we used ϵ = 0.01 |