Determine independence ratio for benchmark formulas

[lhstrh]

The idea is to report the degree of independence in benchmark formulas that our approach can benefit from exploiting. The conjecture is that there is such independence. We can verify this by simply, for a sufficiently large time bound, run our code on formulas, and, instead of invoking the model counter, report the ratio between the number of APs in the formula passed to the SAT solver and the total number of APs in the AST. We only care about the first time the solver is invoked because that will be the call with the largest number of variables. Once we have obtained these ratios we can present them in a histogram. It appears that the ratio should converge with an increasing time bound.