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 --

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.