nach oben

Erschienen in:

2017 | OriginalPaper | Buchkapitel

Logic-Based Encodings for Ricochet Robots

verfasst von : Filipe Gouveia, Pedro T. Monteiro, Vasco Manquinho, Inês Lynce

Erschienen in: Progress in Artificial Intelligence

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

Studying the performance of logic tools on solving a specific problem can bring new insights on the use of different paradigms. This paper provides an empirical evaluation of logic-based encodings for a well known board game: Ricochet Robots. Ricochet Robots is a board game where the goal is to find the smallest number of moves needed for one robot to move from the initial position to a target position, while taking into account the existing barriers and other robots. Finding a solution to the Ricochet Robots problem is NP-hard. In this work we develop logic-based encodings for the Ricochet Robots problem to feed into Boolean Satisfiability (SAT) solvers. When appropriate, advanced techniques are applied to further boost the performance of a solver. A comparison between the performance of SAT solvers and an existing ASP solution clearly shows that SAT is by far the more adequate technology to solve the Ricochet Robots problem.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Iterative Variable Elimination in ASP

Nächstes Kapitel An Achilles’ Heel of Term-Resolution

For the sake of clarity, some of the clauses are not written in CNF. In any case, the translation to CNF is trivial.

This encoding is available from https://potassco.org/doc/apps/2016/09/20/ricochet-robots.html. Note that the more recent encoding described in [13] is not publicly available.

http://potassco.sourceforge.net/.

http://www.labri.fr/perso/lsimon/glucose/.

https://github.com/Z3Prover/z3.

http://www.minizinc.org/index.html.

Ansótegui, C., Manyà, F.: Mapping problems with finite-domain variables into problems with Boolean variables. In: International Conference on Theory and Applications of Satisfiability Testing, pp. 1–15 (2004)

Audemard, G., Lagniez, J.-M., Simon, L.: Improving glucose for incremental SAT solving with assumptions: application to MUS extraction. In: Järvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol. 7962, pp. 309–317. Springer, Heidelberg (2013). doi:10.1007/978-3-642-39071-5_23CrossRefMATH

Audemard, G., Simon, L.: Lazy clause exchange policy for parallel SAT solvers. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 197–205. Springer, Cham (2014). doi:10.1007/978-3-319-09284-3_15CrossRefMATH

Baral, C.: Knowledge Representation, Reasoning and Declarative Problem Solving. Cambridge University Press, Cambridge (2003)CrossRef

Barták, R., Dovier, A., Zhou, N.F.: Multiple-origin-multiple-destination path finding with minimal arc usage: complexity and models. In: International Conference on Tools with Artificial Intelligence (ICTAI), pp. 91–97. IEEE (2016)

Butko, N., Lehmann, K.A., Ramenzoni, V.: Ricochet robots-a case study for human complex problem solving. Project thesis from the Complex System Summer School, Santa Fe Institute (2006)

Chen, J.: A new SAT encoding of the at-most-one constraint. In: International Workshop on Modelling and Reformulating Constraint Satisfaction Problems (2010)

Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). doi:10.1007/978-3-540-78800-3_24CrossRef

Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004). doi:10.1007/978-3-540-24605-3_37CrossRef

10.

Engels, B., Kamphans, T.: Randolphs robot game is NP-hard!. Electron. Notes Discret. Math. 25, 49–53 (2006)MathSciNetCrossRef

11.

Frisch, A.M., Peugniez, T.J., Doggett, A.J., Nightingale, P.: Solving non-Boolean satisfiability problems with stochastic local search: a comparison of encodings. J. Autom. Reason. 35(1–3), 143–179 (2005)MathSciNetMATH

12.

Gebser, M., Jost, H., Kaminski, R., Obermeier, P., Sabuncu, O., Schaub, T., Schneider, M.: Ricochet robots: a transverse ASP benchmark. In: Cabalar, P., Son, T.C. (eds.) LPNMR 2013. LNCS, vol. 8148, pp. 348–360. Springer, Heidelberg (2013). doi:10.1007/978-3-642-40564-8_35CrossRef

13.

Gebser, M., Kaminski, R., Obermeier, P., Schaub, T.: Ricochet Robots reloaded: a case-study in multi-shot ASP solving. In: Eiter, T., Strass, H., Truszczyński, M., Woltran, S. (eds.) Advances in Knowledge Representation, Logic Programming, and Abstract Argumentation. LNCS, vol. 9060, pp. 17–32. Springer, Cham (2015). doi:10.1007/978-3-319-14726-0_2CrossRefMATH

14.

Gebser, M., Kaufmann, B., Neumann, A., Schaub, T.: clasp: a conflict-driven answer set solver. In: Baral, C., Brewka, G., Schlipf, J. (eds.) LPNMR 2007. LNCS, vol. 4483, pp. 260–265. Springer, Heidelberg (2007). doi:10.1007/978-3-540-72200-7_23CrossRef

15.

Gebser, M., Schaub, T., Thiele, S.: GrinGo: a new grounder for answer set programming. In: Baral, C., Brewka, G., Schlipf, J. (eds.) LPNMR 2007. LNCS, vol. 4483, pp. 266–271. Springer, Heidelberg (2007). doi:10.1007/978-3-540-72200-7_24CrossRef

16.

Gent, I.P., Nightingale, P.: A new encoding of All different into SAT. In: International Workshop on Modelling and Reformulating Constraint Satisfaction Problems (2004)

17.

Klieber, W., Kwon, G.: Efficient CNF encoding for selecting 1 from N objects. In: International Workshop on Constraints in Formal Verification (2007)

18.

Martins, R., Joshi, S., Manquinho, V., Lynce, I.: Incremental cardinality constraints for MaxSAT. In: O’Sullivan, B. (ed.) CP 2014. LNCS, vol. 8656, pp. 531–548. Springer, Cham (2014). doi:10.1007/978-3-319-10428-7_39CrossRef

19.

Nethercote, N., Stuckey, P.J., Becket, R., Brand, S., Duck, G.J., Tack, G.: MiniZinc: towards a standard CP modelling language. In: Bessière, C. (ed.) CP 2007. LNCS, vol. 4741, pp. 529–543. Springer, Heidelberg (2007). doi:10.1007/978-3-540-74970-7_38CrossRef

20.

Prestwich, S.: Variable dependency in local search: prevention is better than cure. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 107–120. Springer, Heidelberg (2007). doi:10.1007/978-3-540-72788-0_14CrossRef

21.

Russell, S.J., Norvig, P.: Artificial Intelligence - A Modern Approach, 3rd edn. Pearson Education, London (2010)MATH

22.

Sharma, A., Sharma, D.: An incremental approach to solving dynamic constraint satisfaction problems. In: Huang, T., Zeng, Z., Li, C., Leung, C.S. (eds.) ICONIP 2012. LNCS, vol. 7665, pp. 445–455. Springer, Heidelberg (2012). doi:10.1007/978-3-642-34487-9_54CrossRef

23.

Shtrichman, O.: Pruning techniques for the SAT-based bounded model checking problem. In: Margaria, T., Melham, T. (eds.) CHARME 2001. LNCS, vol. 2144, pp. 58–70. Springer, Heidelberg (2001). doi:10.1007/3-540-44798-9_4CrossRef

24.

Surynek, P.: Simple direct propositional encoding of cooperative path finding simplified yet more. In: Gelbukh, A., Espinoza, F.C., Galicia-Haro, S.N. (eds.) MICAI 2014. LNCS, vol. 8857, pp. 410–425. Springer, Cham (2014). doi:10.1007/978-3-319-13650-9_36CrossRef

Titel: Logic-Based Encodings for Ricochet Robots
verfasst von: Filipe Gouveia
Pedro T. Monteiro
Vasco Manquinho
Inês Lynce
Verlag: Springer International Publishing
Buch: Progress in Artificial Intelligence
Print ISBN: 978-3-319-65339-6

Electronic ISBN: 978-3-319-65340-2

Copyright-Jahr: 2017
DOI: https://doi.org/10.1007/978-3-319-65340-2_54

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"