qTrees
As a pre-processing step, sKizzo extracts a quantifier tree out of each flat prenex CNF instance.

Quantifier tree reconstruction allows us to recover ex-post a portion of the internal structure of QBF instances which was hidden as a consequence of the cast to prenex normal form. The recovered information is leveraged by sKizzo in a number of ways, including (a) the production of simpler skolem functions, (b) the extension of DPLL-like reasoning towards a divide-et-impera behavior and (c) generalization of ordering heuristics for resolution-based reasoning.

Below you find a few examples of quantifier trees extracted from instances in the QBFLIB's archive. The trees have been produced by the qTree utility, dumped to a DOT textual representation for graphs, then rendered using Graphiviz. Depending on the size and on the internal structure of instances, specific settings have been used in the rendering process: with/without clauses attached to leaves, with/without pre-processing, with/without linear branch compression (qTree's options), with/without energy-minimized layout (Graphviz's option).
adder-2-sat
toilet_g_04_01.2
conjuncts: 4
branches: 4
depth: 27
A-nodes: 23
E-nodes: 35
max A-d.: 10
avg A-d.: 7.06
[pdf] [dot]
adder-6-sat
toilet_g_04_01.2
conjuncts: 12
branches: 12
depth: 107
A-nodes: 201
E-nodes: 381
max A-d.: 38
avg A-d.: 21.63
[pdf] [dot]

cf_2_2x3_w_
toilet_g_04_01.2
conjuncts: 1
branches: 49
depth: 290
A-nodes: 6
E-nodes: 470
max A-d.: 6
avg A-d.: 3.77
[pdf] [dot]
cf_2_3x2_r_
toilet_g_04_01.2
conjuncts: 1
branches: 58
depth: 334
A-nodes: 12
E-nodes: 538
max A-d.: 9
avg A-d.: 4.12
[pdf] [dot]

flipflop-3-c
toilet_g_04_01.2
conjuncts: 1
branches: 31
depth: 32
A-nodes: 15
E-nodes: 98
max A-d.: 15
avg A-d.: 13.01
[pdf] [dot]
flipflop-4-c
toilet_g_04_01.2
conjuncts: 11
branches: 303
depth: 76
A-nodes: 96
E-nodes: 747
max A-d.: 12
avg A-d.: 10.82
[pdf] [dot]

mutex-2-s
toilet_g_04_01.2
conjuncts: 1
branches: 37
depth: 25
A-nodes: 8
E-nodes: 96
max A-d.: 8
avg A-d.: 8.00
[pdf] [dot]
mutex-8-s
toilet_g_04_01.2
conjuncts: 1
branches: 247
depth: 61
A-nodes: 32
E-nodes: 617
max A-d.: 32
avg A-d.: 32.00
[pdf] [dot]

toilet_g_02_01.2
toilet_g_04_01.2
conjuncts: 2
branches: 4
depth: 5
A-nodes: 2
E-nodes: 10
max A-d.: 1
avg A-d.: 0.40
[pdf] [dot]
toilet_g_10_01.2
toilet_g_04_01.2
conjuncts: 10
branches: 20
depth: 8
A-nodes: 40
E-nodes: 50
max A-d.: 4
avg A-d.: 1.60
[pdf] [dot]

tree-exa10-10
toilet_g_04_01.2
conjuncts: 9
branches: 9
depth: 4
A-nodes: 18
E-nodes: 9
max A-d.: 2
avg A-d.: 2.00
[pdf] [dot]
tree-exa10-20
toilet_g_04_01.2
conjuncts: 19
branches: 19
depth: 4
A-nodes: 38
E-nodes: 19
max A-d.: 2
avg A-d.: 2.00
[pdf] [dot]

tree-exa2-10
toilet_g_04_01.2
conjuncts: 1
branches: 1
depth: 20
A-nodes: 9
E-nodes: 10
max A-d.: 9
avg A-d.: 4.50
[pdf] [dot]
tree-exa2-30
toilet_g_04_01.2
conjuncts: 1
branches: 1
depth: 60
A-nodes: 29
E-nodes: 30
max A-d.: 29
avg A-d.: 14.50
[pdf] [dot]




back