sQueezeBF: an effective preprocessor for QBFs based on equivalence reasoning In this paper we present sQueezeBF, an effective preprocessor for QBFs that combines various techniques for eliminating variables and/or redundant clauses. In particular sQueezeBF combines (i) variable elimination via Q-resolution, (ii) variable elimination via equivalence substitution and (iii) equivalence breaking via equivalence rewriting. The experimental analysis shows that sQueezeBF can produce significant reductions in the number of clauses and/or variables -- up to the point that some instances are solved directly by sQueezeBF -- and that it can significantly improve the efficiency of a range of state-of-the-art QBF solvers -- up to the point that some instances cannot be solved without sQueezeBF preprocessing.