Boolean satisfiability (or SAT problem) plays a key role in CS and in our many real-life applications. The most well-known algorithm of SAT problem is DPLL (Davis-Putnam-Logemann-Loveland), and people are trying to apply various kinds of Machine learning algorithms for optimizing problems. We investigated all ML algorithms on DPLL and found that some specific ML algorithms show more efficient results. Furthermore, applying Neural-Networks to determine Literal selection gives us an insight into Formal Hardware-Verification processes.