IMPLEMENTATION AND PARALLELIZATION OF A SAT SOLVER ALGORITHM

Simple item page
dc.contributor.authorMOHAMMED, ABDULLAHI,
dc.date.accessioned2014-03-10T06:53:49Z
dc.date.available2014-03-10T06:53:49Z
dc.date.issued2011-06
dc.descriptionDEPARTMENT OF MATHEMATICS AHMADU BELLO UNIVERSITY, ZARIA NIGERIA.en_US
dc.description.abstractvii ACKNOWLEDGEMENT Most importantly, I owe all what I have been obtaining to Allah, who has always been shining my life. Now I can only reaffirm the following words – “Allah, whatever grace we have, it is from you. No god but you”. I would like to thank my supervisor Prof. S. B. Junaidu for his guidance and insight he provided throughout this thesis work, and in teaching the course unit on High Performance Computing which formed the basis of this work. His dedication to research and patience for students and colleagues will always be an example for me to follow. I would like to thank my minor supervisor, Dr. Seyed M. I. Buhari for his support and encouragement on this thesis. I will also like to thank all the staff of Mathematics Department for their various contributions towards making this course a success. To my fellow academics and friends, for helping me to make this dream come true. Thanks also to my parents who have been extremely understanding and supportive of my studies. I feel very lucky to have parents that share my enthusiasm for academic pursuits. Thank you to my parents for bringing me up and supporting my decisions all the way along. Thanks to my brothers and sisters, who are my best friends. Thanks to my wife and daughter, Amina and Asiyah for their unquantifiable encouragement over the years. This dissertation has been completed with support from the ABU MacArthur Foundation Project. viii ABSTRACT There have been remarkable progresses in propositional satisfiability (SAT) in recent years, with significant theoretical and practical contributions. The problem of determining whether a propositional Boolean formula can be true is called the Boolean Satisfiability Problem or SAT. In practice, SAT is a core problem in many applications such as Electronic Design Automation (EDA) and Artificial Intelligence (AI). In this thesis, an implementation of a SAT solver algorithm proposed by Bagais (2008) using C programming language is presented. The performance of the sequential SAT solver is independent of the nature of Boolean formula for efficiency. The algorithm belongs to the class of complete search procedures which determine whether the given formula is satisfiable or not. It keeps all the satisfying assignments of previous clauses before moving forward thereby avoiding backtracking which consumes much time before a decision is reached and this is the case of other algorithms in the literature. A parallel version of the SAT solver algorithm which can be implemented on 2-Dimentional mesh architecture was proposed and a theoretical analysis of the proposed algorithm was carried out.en_US
dc.identifier.urihttp://hdl.handle.net/123456789/3499
dc.language.isoenen_US
dc.subjectIMPLEMENTATION,en_US
dc.subjectPARALLELIZATION,en_US
dc.subjectSAT SOLVER,en_US
dc.subjectALGORITHM.en_US
dc.titleIMPLEMENTATION AND PARALLELIZATION OF A SAT SOLVER ALGORITHMen_US
dc.typeThesisen_US
Files
Original bundle
Now showing 1 - 1 of 1
No Thumbnail Available
Name:
IMPLEMENTATION AND PARALLELIZATION OF A SAT SOLVER ALGORITHM.pdf
Size:
53.09 MB
Format:
Adobe Portable Document Format
Description:
Download
License bundle
Now showing 1 - 1 of 1
No Thumbnail Available
Name:
license.txt
Size:
1.58 KB
Format:
Item-specific license agreed upon to submission
Description:
Download
Collections
SCIENCE