An empirical study of QBF encodings: from treewidth estimation to useful preprocessing.