The results of a computational experiment on the assessment of the
complexity of proving the unsatisfiability of random 3-CNF logical formulas are
presented. The dependence of the complexity of this proving on the R-ratio of the
number of clauses to the number of variables is demonstrated. The computational
experiment was carried out for the range of the N-number of variables from 256 to
512. An exponential dependence of the median complexity of proving the
unsatisfiability of formulas on the number of variables was revealed for each of R
value: 4.3, 4.6, 5.0, 5.5, 6.0. A formula is constructed that approximates the results
of the experiment. According to this formula the exponential component of the
median complexity of the analysis of random 3-CNF is estimated as 2 to the power
N / (8.4R-17.8).