Batsakis, SotiriosΜπατσάκης, ΣωτήριοςTsiakalos, Sofoklis-EvangelosΤσιάκαλος, Σοφοκλής-Ευάγγελος2025-10-012025-10-012025-10-01https://apothesis.hmu.gr/handle/123456789/11428This thesis investigates the implementation and performance evaluation of modern SAT (Boolean Satisfiability Problem) solvers, focusing on the influence of key algorithmic optimizations and heuristics. SAT solvers play a crucial role in fields such as formal verification, artificial intelligence, and combinatorial optimization. The work is centered on the classic Davis-Putnam-Logemann-Loveland (DPLL) algorithm and its modern extensions, including Conflict-Driven Clause Learning (CDCL) and Two-Watched Literals (TWL) mechanisms. The implemented solvers incorporate a range of branching heuristics, Default, DLCS, DLIS, and MOMS, as well as optimizations such as TWL, Pure TWL (TTWL), and CDCL with clause learning and backjumping. These techniques were rigorously tested using standardized 3-SAT benchmark instances from the SATLIB and SAT Competition datasets. Performance was evaluated across multiple dimensions, primarily focusing on average runtime and solver scalability as the problem size increased. The results reveal that, for random 3-SAT instances, branching heuristics significantly enhance solver performance, with MOMS and DLCS delivering the most consistent improvements, especially on large and unsatisfiable problem sets. Conversely, advanced techniques such as Two-Watched Literals and CDCL did not demonstrate a clear performance benefit within this scope of evaluation and, in certain cases, increased computational overhead. These findings suggest that the choice of heuristics and optimizations should be tailored to the nature of the SAT instances being solved. While simple heuristics yield superior results for random 3-SAT problems, more sophisticated methods may offer greater benefits on structured or industrial benchmarks. The thesis concludes with a discussion of limitations and proposes future directions, including the exploration of hybrid solving strategies, structured problem benchmarks, and parallel computing approaches to enhance solver efficiency and generalizabilityΗ παρούσα πτυχιακή εργασία εξετάζει την υλοποίηση και αξιολόγηση της απόδοσης σύγχρονων SAT (Boolean Satisfiability Problem) επιλυτών, εστιάζοντας στην επίδραση βασικών αλγοριθμικών βελτιστοποιήσεων και ευρετικών. Οι SAT solvers παίζουν καθοριστικό ρόλο σε τομείς όπως η τυπική επαλήθευση, η τεχνητή νοημοσύνη και η συνδυαστική βελτιστοποίηση. Η μελέτη επικεντρώνεται στον κλασικό αλγόριθμο Davis-Putnam-Logemann-Loveland (DPLL) και στις σύγχρονες επεκτάσεις του, συμπεριλαμβανομένων του Conflict-Driven Clause Learning (CDCL) και του μηχανισμού Two-Watched Literals (TWL). Οι υλοποιημένοι επιλυτές ενσωματώνουν μια σειρά από ευρετικές επιλογής μεταβλητών, όπως οι Default, DLCS, DLIS και MOMS, καθώς και βελτιστοποιήσεις όπως οι TWL, Pure TWL (TTWL) και CDCL με εκμάθηση ρητρών και backjumping. Οι τεχνικές αυτές δοκιμάστηκαν εκτενώς χρησιμοποιώντας τυποποιημένα σύνολα δοκιμών 3-SAT από τις συλλογές SATLIB και SAT Competition. Η αξιολόγηση της απόδοσης έγινε σε πολλαπλές διαστάσεις, με κύρια έμφαση στον μέσο χρόνο εκτέλεσης και στη δυνατότητα κλιμάκωσης του επιλυτή όσο αυξανόταν το μέγεθος του προβλήματος. Τα αποτελέσματα δείχνουν ότι, σε τυχαία παραδείγματα 3-SAT, οι ευρετικές στρατηγικές βελτιώνουν σημαντικά την απόδοση, με τις MOMS και DLCS να προσφέρουν τις πιο σταθερές βελτιώσεις, ιδιαίτερα σε μεγάλα και μη ικανοποιήσιμα σύνολα. Αντίθετα, πιο προηγμένες τεχνικές, όπως οι Two-Watched Literals και CDCL, δεν παρουσίασαν σαφές όφελος σε αυτό το πλαίσιο αξιολόγησης και σε ορισμένες περιπτώσεις αύξησαν το υπολογιστικό κόστος. Τα ευρήματα αυτά υποδηλώνουν ότι η επιλογή ευρετικών και βελτιστοποιήσεων θα πρέπει να προσαρμόζεται στη φύση των SAT προβλημάτων που επιλύονται. Ενώ απλές ευρετικές αποδίδουν καλύτερα σε τυχαία 3-SAT προβλήματα, πιο σύνθετες μέθοδοι ενδέχεται να αποδειχθούν πιο χρήσιμες σε δομημένα ή βιομηχανικά παραδείγματα. Η εργασία καταλήγει με συζήτηση για τους περιορισμούς και προτείνει μελλοντικές κατευθύνσεις, όπως η διερεύνηση υβριδικών στρατηγικών επίλυσης, η μελέτη δομημένων συνόλων δοκιμών και η αξιοποίηση παραλληλισμού για τη βελτίωση της αποδοτικότητας και της γενικευσιμότητας των επιλυτών.enAttribution-NonCommercial-NoDerivs 3.0 United StatesSAT solversΠτυχιακή Εργασία