IMPLEMENTATION AND PARALLELIZATION OF A SAT SOLVER ALGORITHM
IMPLEMENTATION AND PARALLELIZATION OF A SAT SOLVER ALGORITHM
No Thumbnail Available
Date
2011-06
Authors
MOHAMMED, ABDULLAHI,
Journal Title
Journal ISSN
Volume Title
Publisher
Abstract
vii
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.
Description
DEPARTMENT OF MATHEMATICS
AHMADU BELLO UNIVERSITY, ZARIA
NIGERIA.
Keywords
IMPLEMENTATION,, PARALLELIZATION,, SAT SOLVER,, ALGORITHM.