Μονάδα:
Τμήμα Πληροφορικής & ΤηλεπικοινωνιώνΠληροφορική
Ημερομηνία κατάθεσης:
2017-06-15
Συγγραφέας:
ΑΛΕΞΗΣ ΚΩΝΣΤΑΝΤΙΝΟΣ
Στοιχεία επιβλεπόντων καθηγητών:
Παναγιώτης Σταματόπουλος, Επίκουρος Καθηγητής, Τμήμα Πληροφορικής και Τηλεπικοινωνιών, Εθνικό και Καποδιστριακό Πανεπιστήμιο Αθηνών
Πρωτότυπος Τίτλος:
Προβλήματα Ικανοποίησης Περιορισμών: Επιλυτές Περιορισμών ή Επιλυτές Ικανοποιησιμότητας;
Γλώσσες εργασίας:
Ελληνικά
Μεταφρασμένος τίτλος:
Προβλήματα Ικανοποίησης Περιορισμών: Επιλυτές Περιορισμών ή Επιλυτές Ικανοποιησιμότητας;
Περίληψη:
Σκοπός αυτής της εργασίας είναι να πραγματοποιηθεί μια έρευνα πάνω στην επίλυση προβλημάτων ικανοποίησης περιορισμών (CSP – Constraint Satisfaction Problem). Συγκεκριμένα, αντικείμενο της μελέτης είναι η παράλληλη σύγκριση δύο διαφορετικών προσεγγίσεων για την επίλυση CSP προβλημάτων. Η πρώτη προσέγγιση αφορά την απευθείας επίλυση του προβλήματος από ένα εξειδικευμένο λογισμικό επίλυσης CSP προβλημάτων (CSP Solver). Η δεύτερη προσέγγιση εξετάζει αρχικά την κωδικοποίηση του προβλήματος σε ένα ισοδύναμο πρόβλημα SAT (Boolean Satisfiability Problem) και στη συνέχεια την επίλυση αυτού μέσω ενός λογισμικού επίλυσης SAT προβλημάτων (SAT Solver).
Για να γίνει αυτή η σύγκριση, επιλέχθηκαν τρία κλασσικά CSP προβλήματα (N queens, Map Coloring, Car Sequencing) τα οποία εξετάστηκαν και με τις δυο προσεγγίσεις. Τα προβλήματα αυτά μοντελοποιήθηκαν ως CSP και SAT και στη συνέχεια επιλύθηκαν από τους αντίστοιχους CSP και SAT Solvers. Για την περίπτωση των CSP, η μοντελοποίηση έγινε με τη χρήση του λογισμικού MiniZinc και η επίλυση καλώντας εσωτερικά τον Gecode solver. Αντίστοιχα, για την περίπτωση των SAT, υλοποιήθηκαν τα προβλήματα σε C++ περιβάλλον και επιλύθηκαν με τη βοήθεια του πακέτου MiniSat.
Από τα αποτελέσματα που προέκυψαν, φαίνεται πως η γνήσια CSP προσέγγιση υπερέχει της αντίστοιχης SAT. Αν και το συμπέρασμα αυτό δεν είναι απόλυτο και καθολικό, ωστόσο σημειώνεται πως το ιδιαίτερο πλεονέκτημα της CSP στρατηγικής είναι η συνέπεια και η αξιοπιστία της σε σχέση με την αντίστοιχη SAT.
Κύρια θεματική κατηγορία:
Τεχνητή Νοημοσύνη
Λέξεις-κλειδιά:
προβλήματα ικανοποίησης περιορισμών, SAT στιγμιότυπα, SAT κωδικοποιήσεις, CSP επιλυτές, SAT επιλυτές
Αρ. σελίδων ευρετηρίου:
2
Αρ. βιβλιογραφικών αναφορών:
6
