An improvement and implementation of the DPLL satisfiability algorithm /
DPLLتحسين وتطبيق خوارزم التحقق
Munira Abdelfatah Abdelmaksoud ; Supervised Laila Fahmy Abdelal , Areeg Abdalla
- Cairo : Munira Abdelfatah Abdelmaksoud , 2018
- 64 P. : charts ; 25cm
Thesis (M.Sc.) - Cairo University - Faculty of Science - Department of Mathematics
The propositional satisfiability problem (SAT) is a central problem in theoretical computer science. Given a propositional (boolean) formula, SAT searches for an assignment of variables such that the formula evaluates to 1 (True), or a proof that no such assignment exists. Due to its importance, there have been many algorithms for testing the satisfiability. The most well-known one was introduced by (M. Davis, H. Putnam, G.Logemann and D. Loveland) (DPLL) in 1962 is still developed to date. It is considered the basis for almost all modern SAT solvers. SAT has several applications in computer science as well as in mathematics. One of which is computing Van der Waerden numbers, which are known to be very hard to compute. Coding combinatorics problems as SAT was the road to modify modern SAT solvers. In this thesis, we have proposed two new solvers as modifications of the well-known SAT solver, MINISAT. They are applied in computing the Van der Waerden numbers. For all the known measures, experiments showed that the new solvers outperformed the MINISAT in computing many of Van der Waerden numbers