SAT 3 CNF in polynomial time Files

Code to generate large 3 CNF equations
Code to solve large 3 CNF equations

Solving does not employ VSAT, but VSAT is optional at the end to check the solution
L - # of 3CNF clauses      N - # of terms     R - L/N - ratio of clauses to terms     T - run time
N     R    T      R    T      R    T      R     T      R     T     R   T
2^8   1    .016s  2    .034s  4    .070s  4.2  --      4.25  .054  5   -    
2^10  1    .030s  2    .114s  4    -----  4.2  --      4.25  --    5   -
2^12  1    .086s  2    .122s  4   ------  4.2  2.830s  4.25  --    5   -
2^14  1    .404s  2    .526s  4   ------
2^16  1   1.711s  2   7.679s  4   ------
2^18  1   6.162s  2  42.825s
2^20  1  29.515s  

different times come from different equations, but order of magnitude remains the same.

times to beat (based on Sat09 competition)
N       R      T  
2000    4.2    .08s      
4000    4.2    1.8s      
10000   4.2    5s        
12000   4.2    20s
14000   4.2    20s
16000   4.2    20s

The equations are stored in files so that the generation time does impact the solving time.
The bottlenecks so far are: loading the file, GSAT-like selections (especially in large equations).
Linear performance has been acheived for large (2^16+) equations but it is slow linear performance.

Previously, fruitless entailments posed a problem.  I greatly restricted this by reducing the entailment queue based on the literals' 2CNF membership.
I also add a threshold value that imposes further limits and increases when entailment increases so as to dampen it (severely after 8000).


To do: add stack features to climb up tree

farther off to do:
       convert file format to a binary file to save space and speed load time
               
       write this in C++ (ugh)