|
In the tests a problem set is characterized by
N and p: d is fixed to 1, C is equal
to L, and L
is varied in such a way to cover the ``100\% satisfiable
-- 100\% unsatisfiable'' transition.
100 3CNF(E) formulas are randomly generated
for each point L in a problem set.
For each run, we consider the CPU time the systems take
for the main processing of the formula (excluding parsing and
normalization) and we plot the median value.
For practical reasons, a timeout mechanism stops the execution of the
system on a formula after 1000 seconds of CPU time. For any point
the execution of *SAT, *SAT+GH and TA+GH is
stopped after the system exceeds the timeout on 51
of the 100 samples.
DLP+GH instead, stops its execution
if a super-majority of the first tests exceeds the timeout.
|
