Πλοήγηση ανά Συγγραφέας "Tsiakalos, Sofoklis-Evangelos"

Τώρα δείχνει 1 - 1 of 1
  • Μικρογραφία εικόνας
    Τεκμήριο
    Efficient SAT-Solver implementation
    (ΕΛΜΕΠΑ, Σχολή Μηχανικών (ΣΜΗΧ), Τμήμα Ηλεκτρολόγων Μηχανικών και Μηχανικών Υπολογιστών, 2025-10-01) Tsiakalos, Sofoklis-Evangelos; Τσιάκαλος, Σοφοκλής-Ευάγγελος; Batsakis, Sotirios; Μπατσάκης, Σωτήριος
    This 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