000 02274cam a2200337 a 4500
003 EG-GiCUC
005 20250223032350.0
008 190902s2018 ua d f m 000 0 eng d
040 _aEG-GiCUC
_beng
_cEG-GiCUC
041 0 _aeng
049 _aDeposite
097 _aM.Sc
099 _aCai01.12.17.M.Sc.2018.Mu.I
100 0 _aMunira Abdelfatah Abdelmaksoud
245 1 3 _aAn improvement and implementation of the DPLL satisfiability algorithm /
_cMunira Abdelfatah Abdelmaksoud ; Supervised Laila Fahmy Abdelal , Areeg Abdalla
246 1 5 _aDPLLتحسين وتطبيق خوارزم التحقق
260 _aCairo :
_bMunira Abdelfatah Abdelmaksoud ,
_c2018
300 _a64 P. :
_bcharts ;
_c25cm
502 _aThesis (M.Sc.) - Cairo University - Faculty of Science - Department of Mathematics
520 _aThe 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
530 _aIssued also as CD
653 4 _aDPLL
653 4 _aMINISAT
653 4 _aSatisfiability
700 0 _aAreeg Abdalla ,
_eSupervisor
700 0 _aLaila Fahmy Abdelal ,
_eSupervisor
856 _uhttp://172.23.153.220/th.pdf
905 _aAsmaa
_eCataloger
905 _aNazla
_eRevisor
942 _2ddc
_cTH
999 _c73603
_d73603