Statistics

• Original, as used in the statistics: qbc-valid.tgz (certificates for valid QBFs), qbc-invalid.tgz (certificates for invalid QBFs).

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.

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.

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