Το πρόβλημα ικανοποιησιμότητας

Abstract

Η παρούσα πτυχιακή εργασία επικεντρώνεται στο πρόβλημα ικανοποιησιμότητας (satisfiability problem - SAT). Στο κεφάλαιο της εισαγωγής, δίνονται μια ιστορική αναδρομή για το πρόβλημα SAT και η επεξήγηση βασικών όρων που αφορούν αυτό. Στο δεύτερο κεφάλαιο, αναλύονται κάποια από τα προβλήματα που ανάγονται στο SAT και παρουσιάζονται οι αντίστοιχες αναγωγές καθώς και οι υλοποιήσεις τους. Τέλος, στο τρίτο κεφάλαιο, περιγράφονται διάφοροι αλγόριθμος επίλυσης του SAT. Πιο συγκεκριμένα, παρουσιάζονται τρεις βασικές προσεγγίσεις σχεδίασης αλγορίθμων επίλυσης του SAT: με τη βοήθεια της αρχής της απόφασης (DPP), με χρήση της τεχνικής backtracking (DPLL) και με εκμάθηση παρενθέσεων μέσω συγκρούσεων (CDCL). Επίσης εξετάζεται ή αποτελεσματικότητα και η ικανότητά τους στην επίλυση προβλημάτων SAT. Αυτή η πτυχιακή εργασία ανοίγει το δρόμο για περαιτέρω έρευνα του συγκεκριμένου θέματος.