header
Local cover image
Local cover image
Image from OpenLibrary

An improvement and implementation of the DPLL satisfiability algorithm / Munira Abdelfatah Abdelmaksoud ; Supervised Laila Fahmy Abdelal , Areeg Abdalla

By: Contributor(s): Material type: TextTextLanguage: English Publication details: Cairo : Munira Abdelfatah Abdelmaksoud , 2018Description: 64 P. : charts ; 25cmOther title:
  • DPLLتحسين وتطبيق خوارزم التحقق [Added title page title]
Subject(s): Online resources: Available additional physical forms:
  • Issued also as CD
Dissertation note: Thesis (M.Sc.) - Cairo University - Faculty of Science - Department of Mathematics Summary: 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
Tags from this library: No tags from this library for this title. Log in to add tags.
Star ratings
    Average rating: 0.0 (0 votes)
Holdings
Item type Current library Home library Call number Copy number Status Barcode
Thesis Thesis قاعة الرسائل الجامعية - الدور الاول المكتبة المركزبة الجديدة - جامعة القاهرة Cai01.12.17.M.Sc.2018.Mu.I (Browse shelf(Opens below)) Not for loan 01010110078995000
CD - Rom CD - Rom مخـــزن الرســائل الجـــامعية - البدروم المكتبة المركزبة الجديدة - جامعة القاهرة Cai01.12.17.M.Sc.2018.Mu.I (Browse shelf(Opens below)) 78995.CD Not for loan 01020110078995000

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

Issued also as CD

There are no comments on this title.

to post a comment.

Click on an image to view it in the image viewer

Local cover image