×

zbMATH — the first resource for mathematics

Time-expanded graph-based propositional encodings for makespan-optimal solving of cooperative path finding problems. (English) Zbl 1423.68474
Summary: This paper deals with solving cooperative path finding (CPF) problems in a makespan-optimal way. A feasible solution to the CPF problem lies in the moving of mobile agents where each agent has unique initial and goal positions. The abstraction adopted in CPF assumes that agents are discrete units that move over an undirected graph by traversing its edges. We focus specifically on makespan-optimal solutions to the CPF problem where the task is to generate solutions that are as short as possible in terms of the total number of time steps required for all agents to reach their goal positions. We demonstrate that reducing CPF to propositional satisfiability (SAT) represents a viable way to obtain makespan-optimal solutions. Several ways of encoding CPFs into propositional formulae are proposed and evaluated both theoretically and experimentally. Encodings based on the log and direct representations of decision variables are compared. The evaluation indicates that SAT-based solutions to CPF outperform the makespan-optimal versions of such search-based CPF solvers such as OD+ID, CBS, and ICTS in highly constrained scenarios (i.e., environments that are densely occupied by agents and where interactions among the agents are frequent). Moreover, the experiments clearly show that CPF encodings based on the direct representation of variables can be solved faster, although they are less space-efficient than log encodings.
MSC:
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
68T42 Agent technology and artificial intelligence
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Ahuja, R.K., Magnanti, T.L., Orlin, J.B.: Network flows: theory, algorithms, and applications. Prentice Hall (1993) · Zbl 1201.90001
[2] Audemard, G., Simon, L.: The Glucose SAT Solver. http://labri.fr/perso/lsimon/glucose/. [accessed in September 2014] (2013) · Zbl 1357.68248
[3] Audemard, G; Simon, L, Predicting learnt clauses quality in modern SAT solvers, 399-404, (2009)
[4] Bailleux, O; Boufkhad, Y, Efficient CNF encoding of Boolean cardinality constraints, (2003) · Zbl 1273.68332
[5] Balint, A., Belov, A., Heule, M., Järvisalo, M.: SAT 2013 competition. http://www.satcompetition.org/. [accessed in April 2015] (2013)
[6] Balint, A., Belov, A., Järvisalo, M., Sinz, C.: Overview and analysis of the SAT Challenge 2012 solver competition. In: Artificial Intelligence, vol. 223, pp. 120-155. Elsevier (2015) · Zbl 1270.68337
[7] Balyo, T.: Relaxing the relaxed exist-step parallel planning semantics. In: Proceedings of the 26th IEEE International Conference on Tools with Artificial Intelligence (ICTAI 2013), pp. 865-871. IEEE Computer Society (2013) · Zbl 1131.68099
[8] Balyo, T., Biere, A., Iser, M., Sinz, C.: SAT Race 2015. Artificial Intelligence. Vol. 241, pp. 45-65, Elsevier (2016) · Zbl 1392.68381
[9] Barahona, P., Hölldobler, S., Nguyen, V. -H.: Representative encodings to translate finite CSPs into SAT. In: Proceedings of the Integration of AI and OR Techniques in Constraint Programming - 11th International Conference (CPAIOR 2014), pp. 251-267. Springer (2014) · Zbl 1407.68445
[10] Biere, A., Brummayer, R.: Consistency checking of all different constraints over bit-vectors within a SAT solver. In: Proceedings of Formal Methods in Computer-Aided Design (FMCAD 2008), pp. 1-4. IEEE Computer Society (2008) · Zbl 1357.68248
[11] Biere, A., Heule, M., Van Maaren, H., Walsh, T.: Handbook of satisfiability. IOS Press (2009) · Zbl 1183.68568
[12] Bixby, R.E., Fenelon, M., Gu, Z., Rothberg, E., Wunderling, R.: MIP: Theory and Practice - Closing the Gap. Proceedings of the System Modelling and Optimization 1999. In: 19th IFIP TC7 Conference on System Modelling and Optimization, pp. 19-50. Kluwer (2000) · Zbl 0986.90025
[13] Bixby R. E., Gu, Z., Rothberg, E.: The Gurobi Team: Gurobi Optimization - The Best Mathematical Programming Solver. http://www.gurobi.com/. [accessed in September 2016] (2016)
[14] Blum, A., Furst, M.L.: Fast planning through planning graph analysis. In: Proceedings of the Fourteenth International Joint Conference on Artificial Intelligence (IJCAI 1995), pp. 1636-1642. Morgan Kaufmann (1995)
[15] Brummayer, R., Biere, A.: Boolector: An efficient SMT solver for bit-vectors and arrays. In: Tools and Algorithms for the Construction and Analysis of Systems, 15th International Conference, (TACAS 2009), pp. 174-177, LNCS 5505, Springer (2009) · Zbl 1273.68332
[16] Chen, J.: A new SAT encoding of the at-most-one constraint. In: Proceedings of the 9th International Workshop of Constraint Modeling and Reformulation (ModRef 2010), the 16th International Conference on the Principles and Practice of Constraint Programming (CP 2010), Uppsala Universitet (2010) · Zbl 1357.68248
[17] Clark, D.A., Frank, J., Gent, I.P., MacIntyre, E., Tomov, N., Walsh, T.: Local search and the number of solutions (1996)
[18] Crawford, J.M., Baker, A.B.: Experimental results on the application of satisfiability algorithms to scheduling problems. In: Proceedings of the 12th National Conference on Artificial Intelligence (AAAI 1994), pp. 1092-1097. AAAI Press (1994)
[19] Cáp, M., Novák, P., Vokrínek, J., Pechoucek, M.: Multi-agent RRT: sampling-based cooperative pathfinding. In: International conference on Autonomous Agents and Multi-Agent Systems (AAMAS 2013), pp. 1263-1264. IFAAMAS (2013)
[20] Cáp, M., Novák, P., Kleiner, A., Selecký, M.: Prioritized planning algorithms for trajectory coordination of multiple mobile robots. In: IEEE Transaction Automation Science and Engineering, Volume 12, Number 3, pp. 835-849, IEEE Computer Society (2015)
[21] Dechter, R.: Constraint processing. Elsevier Morgan Kaufmann (2003) · Zbl 1057.68114
[22] Erdem, E., Kisa, D.G., Öztok, U., Schüller, P.: A general formal framework for pathfinding problems with multiple agents. In: Proceedings of the 27th AAAI Conference on Artificial Intelligence (AAAI 2013). AAAI Press (2013) · Zbl 1328.68235
[23] Gent, I.P.: Arc consistency in SAT. In: Proceedings of the 15th Eureopean Conference on Artificial Intelligence (ECAI 2002), pp. 121-125. IOS Press (2002)
[24] Huang, R., Chen, Y., Zhang, W.: A novel transition based encoding scheme for planning as satisfiability. In: Proceedings of the 24th AAAI Conference on Artificial Intelligence (AAAI 2010). AAAI Press (2010) · Zbl 1183.68590
[25] Iwama, K., Miyazaki, S: SAT-variable complexity of hard combinatorial problems. In: Proceedings of Technology and Foundations - Information Processing ’94, Volume 1, Proceedings of the IFIP 13th World Computer Congress, pp. 253-258, North-Holland (1994)
[26] Järvisalo, M., Le Berre, D., Roussel, O., Simon, L.: The international SAT solver competitions. AI Magazine, Vol. 33, Number 1. AAAI Press (2012) · Zbl 1131.68099
[27] Ježek, M.: Modeling of Cooperative Pathfinding. Bachelor thesis, Charles University (2015)
[28] Kautz, H., Selman, B.: Unifying SAT-based and graph-based planning. In: Proceedings of the 16th International Joint Conference on Artificial Intelligence (IJCAI 1999), pp. 318-325. Morgan Kaufmann (1999) · Zbl 1317.90199
[29] Kim, D; Hirayama, K; Park, G-K, Collision avoidance in multiple-ship situations by distributed local search, J. Adv. Comput. Intell. Intell. Inform. (JACIII), 18, 839-848, (2014)
[30] KIVA Systems. Official web site. http://www.kivasystems.com/, 2015 [accessed in April 2015]
[31] Kornhauser, D., Miller, G.L., Spirakis, P.G.: Coordinating pebble motion on graphs, the diameter of permutation groups, and applications. In: Proceedings of the 25th Annual Symposium on Foundations of Computer Science (FOCS 1984), pp. 241-250. IEEE Computer Society (1984)
[32] Luna, R., Bekris, K.E.: Push and Swap: Fast cooperative path-finding with completeness guarantees. In: Proceedings of the 22nd International Joint Conference on Artificial Intelligence (IJCAI 2011), pp. 294-300. IJCAI/AAAI (2011)
[33] Michael, N; Fink, J; Kumar, V, Cooperative manipulation and transportation with aerial robots, Autonom. Robot., 30, 73-86, (2011) · Zbl 1250.93085
[34] Morgado, A; Heras, F; Liffiton, MH; Planes, J; Marques-Silva, J, Iterative and coreguided maxsat solving: A survey and assessment, Constraints, 18, r8-534, (2013) · Zbl 1317.90199
[35] Nguyen, V. -H., Mai, S.T.: A new method to encode the at-most-one constraint into SAT. In: Proceedings of the 6th International Symposium on Information and Communication Technology (SoICT 2015), pp. 46-53. ACM (2015)
[36] Nguyen, V. -H., Velev, M.N., Barahona, P.: Application of hierarchical hybrid encodings to efficient translation of CSPs to SAT. In: Proceedings of the 25th International Conference on Tools with Artificial Intelligence (ICTAI 2013), pp. 1028-103. IEEE Computer Society (2013)
[37] Petke, J., Jeavons, P.: The order encoding: From tractable CSP to tractable SAT. In: Proceedings of the 14th International Conference on Theory and Applications of Satisfiability Testing (SAT 2011), LNCS 6695, pp. 371-372. Springer (2011)
[38] Petke, J.: Bridging Constraint Satisfaction and Boolean Satisfiability. Artificial Intelligence: Foundations, Theory, and Algorithms, Springer (2015) · Zbl 1410.68008
[39] Ratner, D., Warmuth, M.K.: Finding a shortest solution for the N × N extension of the 15- PUZZLE Is intractable. In: Proceedings of the 5th National Conference on Artificial Intelligence (AAAI 1986), pp. 168-172. Morgan Kaufmann (1986)
[40] Régin, J. -C.: A filtering algorithm for constraints of difference in CSPs. In: Proceedings of the 12th National Conference on Artificial Intelligence (AAAI 1994), pp. 362-367. AAAI Press (1994)
[41] Rintanen, J; Heljanko, K; Niemela, I, Planning as satisfiability: parallel plans and algorithms for plan search, Artif. Intell., 170, 1031-1080, (2006) · Zbl 1131.68099
[42] Ryan, M.R.K.: Graph decomposition for efficient multi-robot path planning. In: Proceedings of the 20th International Joint Conference on Artificial Intelligence (IJCAI 2007), pp. 2003-2008. IJCAI Conference (2007)
[43] Ryan, MRK, Subgraph structure in multi-robot path planning, J. Artif. Intell. Res. (JAIR), 31, 497-542, (2008) · Zbl 1183.68590
[44] Schulte, C., Stuckey, P.J.: Speeding up constraint propagation. In: Principles and Practice of Constraint Programming, 10th International Conference (CP 2004), pp. 619-633, LNCS 3258 (2004) · Zbl 1152.68583
[45] Schulte, C.: The Gecode Team: Gecode - generic constraint development environment. http://www.gecode.org/. [accessed in September 2016] (2016) · Zbl 1328.68236
[46] Silva, J.P.M., Lynce, I.: Towards robust CNF encodings of cardinality constraints. In: Principles and Practice of Constraint Programming, 13th International Conference (CP 2007), pp. 483-497. Springer (2007) · Zbl 1145.68525
[47] Silver, D.: Cooperative pathfinding. In: Proceedings of the 1st Artificial Intelligence and Interactive Digital Entertainment Conference (AIIDE 2005), pp. 117-122. AAAI Press (2005) · Zbl 0285.05110
[48] Soh, T., Banbara, M., Tamura, N.: A hybrid encoding of CSP to SAT integrating order and log encodings. In: Proceedings of the 27th IEEE International Conference on Tools with Artificial Intelligence (ICTAI 2015), pp. 421-428. IEEE Computer Society (2015) · Zbl 1367.68319
[49] Sharon, G; Stern, R; Goldenberg, M; Felner, A, The increasing cost tree search for optimal multi-agent pathfinding, Artif. Intell., 195, 470-495, (2013) · Zbl 1270.68337
[50] Sharon, G; Stern, R; Felner, A; Sturtevant, NR, Conflict-based search for optimal multi-agent pathfinding, Artif. Intell., 219, 40-66, (2015) · Zbl 1328.68235
[51] Standley, T.S., Korf, R.E.: Complete algorithms for cooperative pathfinding problems. In: Proceedings of Proceedings of the 22nd International Joint Conference on Artificial Intelligence (IJCAI 2011), pp. 668-673. IJCAI/AAAI Press (2011) · Zbl 1273.68332
[52] Sturtevant, NR, Benchmarks for grid-based pathfinding, IEEE Trans. Comput. Intell. AI Games, 4, 144-148, (2012)
[53] Surynek, P.: Towards optimal cooperative path planning in hard setups through satisfiability solving. In: Proceedings of 12th Pacific Rim International Conference on Artificial Intelligence (PRICAI 2012), pp. 564-576, LNCS 7458. Springer (2012)
[54] Surynek, P.: On propositional encodings of cooperative path-finding. In: Proceedings of the 24th International Conference on Tools with Artificial Intelligence (ICTAI 2012), pp. 524-531. IEEE Computer Society (2012) · Zbl 1186.68076
[55] Surynek, P.: Mutex reasoning in cooperative pathfinding modeled as propositional satisfiability. In: Proceedings of the 2013 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS 2013), pp. 4326-4331. IEEE Computer Society (2013)
[56] Surynek, P, Solving abstract cooperative path-finding in densely populated environments, Comput. Intell. (COIN), 30, 402-450, (2014) · Zbl 1328.68204
[57] Surynek, P.: Compact representations of cooperative path-finding as sat based on matchings in bipartite graphs. In: Proceedings of the 26th International Conference on Tools with Artificial Intelligence (ICTAI 2014), pp. 875-882. IEEE Computer Society (2014) · Zbl 1328.68204
[58] Surynek, P.: A simple approach to solving cooperative path-finding as propositional satisfiability works well. In: Proceedings of the 13th Pacific Rim International Conference on Artificial Intelligence (PRICAI 2014), pp. 827-833, Lecture Notes in Computer Science, Vol. 8862, Springer (2014)
[59] Surynek, P.: Simple direct propositional encoding of cooperative pathfinding simplified yet more. In: Proceedings of the 13th Mexican International Conference on Artificial Intelligence (MICAI 2014), LNCS, vol. 8857, pp. 410-425. Springer (2014) · Zbl 1186.68076
[60] Surynek, P, On the complexity of optimal parallel cooperative path-finding, Fund. Inform., 137, 517-548, (2015) · Zbl 1357.68248
[61] Tamura, N; Taga, A; Kitagawa, S; Banbara, M, Compiling finite linear CSP into SAT, Constraints, 14, 254-272, (2009) · Zbl 1186.68076
[62] Tanjo, T., Tamura, N., Banbara, M.: Azucar: A SAT-Based CSP solver using compact order encoding - (tool presentation). In: Proceedings of the Theory and Applications of Satisfiability Testing - 15th International Conference (SAT 2012), pp. 456-462. Springer (2012)
[63] Tseitin, G.S.: On the complexity of derivation in propositional calculus. In: Structures in Constructive Mathematics and Mathematical Logic, Part II, Seminars in Mathematics (translated from Russian), pp. 115-125. Steklov Mathematical Institute (1968) · Zbl 0197.00102
[64] Wagner, G; Choset, H, Subdimensional expansion for multirobot path planning, Artif. Intell., 219, 1-24, (2015) · Zbl 1328.68236
[65] Walsh, T.: SAT v CSP. Principles and practice of constraint programming - CP 2000. In: 6th International Conference (CP 2000), pp. 441-456, LNCS 1894. Springer (2000) · Zbl 1044.68808
[66] Wehrle, M., Rintanen, J.: Planning as satisfiability with relaxed exist-step plans. In: Proceedings of the 20th Australian Joint Conference on Artificial Intelligence, pp. 244-253. Springer (2007)
[67] West, D.B.: Introduction to graph theory. Prentice Hall (2000)
[68] De Wilde, B., ter Mors, A., Witteveen, C.: Push and rotate: cooperative multi-agent path planning. In: Proceedings of the International conference on Autonomous Agents and Multi-Agent Systems (AAMAS 2013), pp. 87-94. IFAAMAS (2013) · Zbl 1183.68590
[69] Wilde, B; ter Mors, AW; Witteveen, C, Push and rotate: a complete multi-agent pathfinding algorithm, J. Artif. Intell. Res. (JAIR), 51, 443-492, (2014) · Zbl 1367.68319
[70] Wilson, RM, Graph puzzles, homotopy, and the alternating group, J. Comb. Theory, Ser. B, 16, 86-96, (1974) · Zbl 0285.05110
[71] Yu, J., LaValle, S.M.: Structure and intractability of optimal multi-robot path planning on graphs. In: Proceedings of the 27th AAAI Conference on Artificial Intelligence (AAAI 2013). AAAI Press (2013) · Zbl 1131.68099
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.