Validating QBF Decisions

About -- Download -- Statistics


All benchmarks were done using these versions of the tools:

qbv 1.03 (2007-01-28) link download
squolem 1.03 (2007-01-28) link download
qbfi 1.0 (2006-11-27) link download
quantor 2.11 link download
sKizzo 0.8.2-beta link download

The instances that we used were from the 2006 QBF-Eval preliminary and fixed set, which is available for download here. We also provide a local copy here. The generated certificate files are available in two versions:
Test Parameters: A time limit of 600 seconds, and a memory limit of 1 GB.

Certificate Generation Time
The following chart shows the overhead in terms of time, introduced by turning on certificate generation in squolem. This has been tested for all instances from the testset that squolem, with certificate generation turned off, returns within 600 seconds. This test was run on an Intel Xeon, 3.0 GHz, 4 GB.

Result Files: GTvsST-valid.csv, GTvsST-invalid.csv, qbc-valid.tgz (certificates for valid QBFs), qbc-invalid.tgz (certificates for invalid QBFs).

Certificate Validation Time
The following chart illustrates that the time needed to validate a certificate is significantly less than the time to generate a certificate. However, it can be seen that certificates of validity are a little bit harder to validate. This test was run on an Intel Xeon, 3.0 GHz, 4 GB.

Result Files: GTvsVT-valid.csv, GTvsVT-invalid.csv.

Inverted Instances
One idea to generate certificates of validity is to invert the instance and then generate a certificate of invalidity for the inverted instance. The data that we acquired by inverting all the instances that the solvers could solve within 600 seconds, shows that this approach is not feasible. This test was run on an Intel Xeon, 2.8 GHz, 4 GB.

This chart cleary shows that the time needed to solve an inverted instance is almost always considerably longer than the time to solve the non-inverted instance. Actually, a lot of instances that took almost no time to solve normally (<1 sec), timed out when inverted (as seen in the top left of the chart).

Result Files: isat.tgz (inverted instances), compstatsQUANTOR-i.csv (Quantor on inverted), compstatsQUANTOR-ni.csv (Quantor on original), compstatsSKIZZO-i.csv (sKizzo on inverted), compstatsSKIZZO-ni.csv (sKizzo on original), compstatsSQUOLEM-i.csv (Squolem on inverted), compstatsSQUOLEM-ni.csv (Squolem on original),