Final report
.........I am very pleased that I was selected to be a CRA participant
this summer. This is the
greatest honor that can be given to a student who wish to put all his efforts
and deeds
into the Computer Research.
..........I have had a wonderful summer doing the research with Prof Paula Whitlock
at Brooklyn
College, CUNY. I have gained a very nice and interesting experience in Computer
Science,
Research, and in life in general.
..........Our summer research covered the most interesting and enigmatic area
of the computer
science - SAT problems. To look at the complete description of a problem click
here .
.........First we started testing our code by using 2-SAT problems.
It was a very good determination of the correctness of our program (because
the results of running 2-SAT are well known).
When we got read of all the "memory faults", incorectnesses, and just
errors(+I proposed
and wrote flaCheck -- to determine if we have (A) and (~A) in the same formula
at the same time +
trying different kinds of random number generators), we moved to examining 3-SAT
problems and their properties.
...........These are graphs I got using "gnuplot"
features (week 10):
I tested alpha in the range from 4 to 5 (n=50,number of instances=100 --
before using multithresding advantures)
Here I was trying to take a closer look at the crossover point(the
number of instances is
1000 ) --range of alpha is from 3.6 to 4.8
..........Then we moved to "backbone size" determination.
The backbone of a satisfiable
SAT instsance is the set of entailed literals (a literal l is entailed
by a satisfiable
SAT instance C iff C AND (NOT l) is unsatisfiable). And so the backbone size
is the number of entailed literals. The backbone fraction if the backbone size
over
the number of variables.
.........Therefore, in determining some backbone size first we should consider
formulae that are satisfiable. Then go through each literal l and add (NOT l)
to the formula. If the formula is unsatisfiable - l is in the backbone. If the
formula is satisfiable - add (l) to the formula, if it is unsatisfiable ~l is
in the backbone;
etc(repeat for all literals). If it the formula is satissfiable in both cases
neither l nor ~l is
in the backbone. I wrote all the code associated with the backbone sizes (week
6).
........ But I could run only a relatively small number of instances.
Therefore, we decided to
pot all our efforts, code writing, and experiments to MULTITHREADING (weeks
7-9).
It was a very interesting and challenging period in our research. We tried a
lot of
aThreadFunction interpretations . + we used mutex_lock() and mutex_unlock()
functions to prevent accessing some glabal variables by multiple processors
at
the same time, and then we tried to avoid using those locks and unlocks!
They slow down the execution of the code. It was a lot of fun and new knowledge.
if you are interested and want to look at our activity closer go to
my journal and
find weeks 7-9.
This graph was produced by using multithreading applications.
The number of instances
is 8000 + a wide range of alpha -- from 2 to 5
This graph represents the relationship of the values of alpha to the backbone
fractions.
........Finally I studied and used GNUPLOT to convert the most interesting of
our results to
graphs (As you have seen before). I found gnuplot very friendly and easy to
us
(thank to my Mentor).
I want to thank my mentor -- Professor Paula Whitlock(at Brooklyn
College, CUNY)
for her brilliant mind, patience, and all the knowledge she gave me. Also --
CRA
organization for the greatest honor to participate in this increadable and wonderful
summer reserach! I am very proud that I was a part of this greatest development
of
Computer Science. Thank you! You gave me the great opportunity to realize myself,
to plan my activities for the graduate school, and to have the BEST EXPERIENCE
IN MY LIFE.
P.S. Special "thank you" - for Professor Scott Dexter
(Brooklyn College, CUNY )- for the huge
part of his life that was given in a name of our research, beautiful and quick
mind, all the advice,
and everything he has done for me.