============================================================================
2013-05-24 QBF Gallery 2013 preliminary results for showcase "Preprocessing"
============================================================================

Related to incremental preprocessing in multiple rounds, we tried to analyze
the progress that is made between rounds. After some rounds it might happen
that an instance is not modified at all by the preprocessors during a
round. In this case, preprocessing reached a fixpoint and hence can be
stopped.

Notation:

"A" is hiqqer3e
"B" is bloqqer
"C" is hiqqer3p
"D" is squeeze

In the experiments "num-rounds-12-120sec-ABCD-completion" and
"num-rounds-24-120sec-ABCD-completion" reported below, we consider the
execution sequence ABCD and a timeout of 120 seconds for each individual call
of A, B, C, and D. At most 12 rounds / 24 rounds are executed, respectively. A
run terminates early if an instance is solved or a fixpoint is detected.

We detect fixpoints as follows:

At the beginning of each round, first the clause set of the current instance
is normalized. Normalization of the clause set discards tautological clauses
and sorts the literals of all the clauses in the set in ascending order of
their IDs as given by the QDIMACS encoding. Then the set of clauses is sorted
using the Linux tool 'sort'. A hash value is computed for this normalized
clause set. At the end of the current round, a hash value is computed for the
normalized clause set of the respective current instance. If the hash values
at the beginning and at the end of a round are equal then preprocessing in the
current round did not modify the clause set. Hence a fixpoint has been reached
and the run terminates.

This way of detecting fixpoints ignores different orderings of the clauses in
the current instance or of literals in a clause. Normalization of the clause
sets as described is necessary to allow for easy hash value based detection of
fixpoints. Except for sorting the clause set, we used the pretty-print
function of the solver DepQBF for normalization. This pretty-printed formula
is used only for fixpoint detection and is not forwarded to the
preprocessors. Hence DepQBF does not interfere with preprocessing.


------------------------------------------------------------------------------

eval2012r2 (345 formulas)

statistics for num-rounds-12-120sec-ABCD-completion:

108 instances were solved. 93 instances were solved in round 1, 9 in round 2,
3 in round 3, 1 in round 4, 1 in round 5, and 1 in round 7. No instance was
solved in round 6 and in rounds 8 to 12.

For 206 unsolved instances a fixpoint was detected.
fixpoints after round 1: 3
fixpoints after round 2: 25
fixpoints after round 3: 62
fixpoints after round 4: 64
fixpoints after round 5: 38
fixpoints after round 6: 5
fixpoints after round 7: 4
fixpoints after round 8: 2
fixpoints after round 9: 0
fixpoints after round 10: 2
fixpoints after round 11: 0
fixpoints after round 12: 1

For the remaining 31 = (345 - 108 - 206) instances preprocessing terminated after 12 rounds.


statistics for num-rounds-24-120sec-ABCD-completion:

108 instances were solved. The numbers of instances solved in each round are
equal to the numbers reported for "num-rounds-12-120sec-ABCD-completion". No instance was
solved in round 6 and in rounds 8 to 24.

For 207 unsolved instances a fixpoint was detected.
fixpoints after round 1: 3
fixpoints after round 2: 25
fixpoints after round 3: 62
fixpoints after round 4: 64
fixpoints after round 5: 39
fixpoints after round 6: 5
fixpoints after round 7: 3
fixpoints after round 8: 2
fixpoints after round 9: 0
fixpoints after round 10: 2
fixpoints after round 11: 1
fixpoints after round 12: 1

No fixpoints were detected in rounds 13 to 24.

For the remaining 30 = (345 - 108 - 207) instances preprocessing terminated after 24 rounds.