Binary Classification as a Complementary Tool for Solving SAT Problems

Satisfiability problem is a classical NP-complete task, that is of great interest both in academia and industry. Some articles about applying machine learning techniques for solving SAT problems were published recently. The object of this work is using binary classification as a complementary tool in DPLL algorithm for its performance increase. The main idea of the thesis is that solution search time should be reduced selecting the value of the branching variable that is more probably lead to the satisfiable formula. Probability prediction of formula satisfiability for two different values of the branching variable at each iteration of the DPLL algorithm is done by using binary classifiers in this work. So, different binary classifiers were trained and the best one was chosen to use in DPLL algorithm for further experiments. The result of this work is that it was shown that applying binary classifiers for choosing branching variables’ values in DPLL algorithm increases its time performance. However, it was also shown that the threshold value of the number of variables in formulas, for which use of the binary classification makes sense, is different for different branching rules of the DPLL algorithm.