An Empirical Study of QBF Encodings: from Treewidth Estimation to Useful Preprocessing