......We decided to start testing our program (code) by using 2-SAT problems -- because the results of executions of such problems are well known. So we can apply 2-SAT problem solving (even though the linear algirithm for such problems exists) to our coding and see if it works corectly and has all needed functionality. I designed some
simple input file the content of which looked like this:

30 50 10000
40 50 10000
50 50 10000
60 50 10000
70 50 10000

Where the first column -- M(number of clauses), second-N(number of variables), third-# of randomly generated formulae. Therefore, we have alpha (M/N)= 0.6, 0.8, 1.0, 1.2, 1.4
respectively. It should be that a cross-over point is somewhere around alpha=1. Let's see...