The Boolean Satisfiability Problem (SAT) remains a cornerstone of computer science, with applications spanning formal verification, artificial intelligence, operations research, and cybersecurity. Despite significant advances in SAT solving techniques, the exponential nature of the search space continues to pose challenges, particularly for large-scale instances encountered in real-world applications. This thesis presents two approaches to enhance SAT solvers' efficiency.
The first contribution introduces ESBP_SEL, a novel hybrid approach that combines Effective Symmetry Breaking Predicates (ESBP) with Symmetric Explanation Learning (SEL) through the concept of local symmetries. Experimental results demonstrate that ESBP_SEL significantly outperforms existing methods on highly symmetric instances, particularly unsatisfiable ones.
The second contribution addresses the initialization problem in CDCL SAT solvers through a series of genetic algorithm-based approaches. The base approach, GASPI (Genetic Algorithm for SAT Polarity Initialization), employs evolutionary computation to identify promising initial variable assignments. This is further enhanced in GASPI-ML, which uses machine learning techniques to predict optimal genetic algorithm parameters based on formula characteristics; and in GASPI+, a self adaptive genetic algorithm. These techniques show marked improvement over traditional initialization methods, particularly on satisfiable instances.
By pushing the boundaries of symmetry exploitation and solver initialization, this thesis opens new avenues for tackling complex SAT problems efficiently, with potential impacts across multiple domains. The insights and techniques developed herein contribute to the ongoing quest for expanding the horizons of computational capability in SAT solving.