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