 |
Here we collect experimental results over many QBF families, most of which in the public domain.
-
Which QBF instances do we consider?
We target all the non-random benchmarks from the QBFLIB's archive
(maintained by the STAR-lab group
at the University of
Genova, Italy), plus some QBF families
we have been collecting from sKizzo's users who kindly contributed them (the instances themselves are not available from this site).
Overall, we consider more than 2000 instances, organized in 115 families,
contributed from 17 different sources (authors). They have been obtained by directly
encoding into QBF some formal verification, conformant planning, or game related problem, or
indirectly by compiling instances from another language/formalism (e.g. modal logic) into QBF.
-
What are the experimental conditions?
For the experiments, we used sKizzo v0.8.2
on a 2.66GHz Xeon processor equipped with 2Gb of main memory, running Mandriva Linux, kernel version 2.6.
Given that sKizzo is a hybrid and highly customizable solver, we give results
for different settings of the parameters. Each configuration of settings is called a
"personality" (see the solver manual for details).
-
|
