Advances in SAT-Based planning

Abstract

Ο σχεδιασμός δράσης είναι ένα δύσκολο πρόβλημα. Ακόμα και οι πιο απλές του μορφές είναι υπολογιστικά δυσεπίλυτες ('intractable'). Παρόλο που είναι απίθανος ο αποτελεσματικός (ως προς χρόνο) σχεδιασμός δράσης στη γενική περίπτωση, εντούτοις αποτελεσματικές ευρετικές μέθοδοι και αποδοτικοί αλγόριθμοι διάχυσης περιορισμών είναι πολύτιμες τεχνικές για την επίλυση μεγάλων προβλημάτων σχεδιασμού δράσης. Πράγματι, πολλά μοντέρνα συστήματα σχεδιασμού δράσης μετατρέπουν το πρόβλημα λογική, και στη συνέχεια το λύνουν με αλγορίθμους προτασιακής λογικής (SAT solvers), περιορισμών ή ψευδό-προτασιακης λογικής ('Pseudo-boolean'). Πολλά άλλα συστήματα λογισμικού επιλύουν το πρόβλημα κατευθύνοντας την αναζήτηση με αποτελεσματικές ευρετικές μεθόδους που εξάγονται αυτόματα από το ίδιο το κωδικοποίησης των προβλημάτων σχεδιασμού δράσης σε προτασιακή λογική (SAT). Αποδεικνύουμε τόσο θεωρητικά αλλά και πειραματικά ότι οι μηχανισμοί διάχυσης περιορισμών των μοντέρνων επιλυτών προτασιακής λογικής διαχέουν τους περιορισμούς πολύ αποδοτικότερα στο SMP από άλλους τρόπους κωδικοποίησης. Επιπλέον, με τη χρήση λογισμικού που υλοποιήσαμε, βρίσκουμε επιπρόσθετους δυαδικούς περιορισμούς που ισχύουν σε προβλήματα σχεδιασμού δράσης για τους οποίους παραθέτουμε ισχυρές πειραματικές ενδείξεις η προσθήκη τους στο SMP δεν προσφέρει υπολογιστικά οφέλη. Στη συνέχεια η κωδικοποίηση του SMP χρησιμοποιήθηκε σαν βάση στην ανάπτυξη του συστήματος σχεδιασμού δράσης PSP. Το σύστημα PSP μεγιστοποιεί το πλήθος των στόχων (goals) που επιτυγχάνονται σε ένα περιορισμένο χρονικό ορίζοντα, επαναλαμβάνοντας τη διαδικασία για διαδοχικά μεγαλύτερους ορίζοντες. Παρά την αδυναμία του PSP να εγγυηθεί ότι οι λύσεις είναι βέλτιστές (ως προς το μήκος τους) όπως το σύστημα SMP, εντούτοις υπολογίζει σχέδια δράσης καλής ποιότητας για προβλήματα που δεν μπορούν να επιλυθούν από τον SMP ή άλλα συστήματα σχεδιασμού δράσης (που που παράγουν βέλτιστες λύσεις) τα οποία βασίζονται σε προτασιακούς επιλυτές. Ένα βασικό μειονέκτημα του συστήματος PSP είναι η περιορισμένη του αποδοτικότητα σε προβλήματα μεγάλου μεγέθους. Αυτό οφείλεται στο ότι οι κωδικοποιήσεις μεγάλων προβλημάτων σχεδιασμού δράσης είναι συχνά πολύ δύσκολες για τους προτασιακούς επιλυτές. Αυτό ισχύει για όλα τα συστήματα σχεδιασμού δράσης που βασίζονται στην μέθοδο της διαδοχικής επέκτασης του ορίζοντα δράσης, αφού το μέγεθος των κωδικοποιήσεων μεγαλώνει όσο μεγαλώνει και ο ορίζοντας. Η αδυναμία αυτή αντιμετωπίζεται από το σύστημα PSP-H το οποίο επεκτείνει το σύστημα PSP με δύο αποδοτικές τεχνικές που αποσυνθέτουν το πρόβλημα σε μικρότερα υποπροβλήματα ώστε τα προβλήματα προτασιακής ικανοποιησιμότητας που προκύπτουν να μην είναι υπερβολικά μεγάλα. Η πρώτη τεχνική μετατρέπει το πρόβλημα σχεδιασμού δράσης σε μια σειρά προβλημάτων δυαδικής βελτιστοποίησης, σε κάθε ένα από τα οποία ο στόχος είναι να μεγιστοποιηθεί το πλήθος των στόχων (goals) που μπορούν να ικανοποιηθούν εντός ενός περιορισμένου ορίζοντα (μήκος πλάνου). Αυτή η τεχνική συνδυάζεται με μια δεύτερη τεχνική που κατευθύνει την αναζήτηση για κάθε υποπρόβλημα σε μια κατάσταση όπου ικανοποιούνται όλοι οι στόχοι του αρχικού προβλήματος. Τα πειραματικά μας αποτελέσματα αποδεικνύουν ότι το PSP-H είναι ένας ανταγωνιστικός αλγόριθμος σχεδιασμού δράσης.

Planning is a difficult problem. Even in its simplest forms it is computationally intractable. Although it is unlikely to be able to plan efficiently in the general case, good heuristics and strong constraint propagation methods are valuable techniques for tackling large planning problems. Indeed some modern planners transform planning into a constraint satisfaction problem, such as a boolean formula, and then solve it by invoking a satisfiability, constraint or pseudo-boolean solver. Many other planners solve the problem by guiding the search using powerful heuristics that are automatically extracted from the planning domain. In the context of this work we first implemented SMP, a novel way of transforming a planning domain into a propositional boolean formula (SAT). We prove both theoretically and experimentally that the constraint propagation engines of the modern SAT solvers propagate the constraints much more efficiently in SMP than in previous transformations. We also provide strong experimental evidence that the addition of more implied non-redundant binary constraints to SMP does not improve the planning times. We then use the SAT encoding of SMP in the PSP planner. PSP seeks to maximize the number of goals that can be achieved using the solve and expand method. Although PSP cannot guarantee optimality as SMP, it often generates sub-optimal plans of high quality for planning problems that are beyond the reach of SMP and other optimal SAT-based planners. A drawback of the PSP planner is its limited scalability, as the instances that arise from large planning problems are often too hard for SAT solvers. This holds true for all planners based on the solve and expand method, as the size of the SAT instance grows monotonically with the planning horizon. To address this problem we developed the PSP-H planning system, that extends PSP by combining two powerful techniques that aim at decomposing a planning problem into smaller subproblems, so that the instances that need to be solved do not grow prohibitively large. The first technique turns planning into a series of boolean optimization problems, each seeking to maximize the number of goals that are achieved within a limited planning horizon. This is coupled with a second technique that directs search towards a state that satisfies all goals. Experimental results demonstrate that PSP-H is a competitive planning algorithm.