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).

  • Select the benchmark/personality of interest, then to see the results :

    Select one (or more) set of families:
        Formal Verification (44 families, 339 instances)
        Planning (14 families, 249 instances)
        Games (27 families, 249 instances)
        Compilation into QBF(31 families, 1179 instances)

    Now select the solving personality (choose multiple ones for a comparison):
       ground (SAT-solve the combintorial core)
       light (Use a light symbolic simplification scheme)
       noRES (The full solver but missing SRES)
       noSPLE (Avoid computing symbolically the pure literals)
       resolving (Do it via resolution)
       standard (The default solver)
    In addition to the above personalities, we construct the "envelope solver".It is not a real solver configuration, but a performance profile made up by selecting, for each instance, the personality that solved it faster:
       envelope (The envelope solver)