Tackling Satisfiability: SAT Instances Classification Using Several Machine Learning Approaches

The Boolean Satisfiability Problem (SAT) is a computationally challenging and fundamental problem in computer science, with extensive applications in cryptography, artificial intelligence, and hardware verification. This paper examines the application of machine learning techniques to categorize Conjunctive Normal Form (CNF) instances as either satisfiable (SAT) or unsatisfiable (UNSAT). We investigate a variety of models, such as Naive Bayes (NB), Support Vector Machines (SVM), Logistic Regression (LR), and Neural Networks (NN), by utilizing features that encapsulate the intrinsic properties of CNF formulas. We have demonstrated the high accuracy of these models' ability to predict satisfiability by conducting extensive experiments to analyze their performance. Our findings demonstrate that machine learning can provide a scalable and efficient alternative to conventional SAT solvers, thereby introducing new opportunities for the future to address intricate satisfiability problems.