QBF is the problem of deciding the satisfiability of quantified boolean formulae in which variables can be either universally
or existentially quantified. QBF generalizes SAT (SAT is QBF under the restriction all variables are existential) and is in
practice much harder to solve than SAT. One of the sources of added complexity in QBF arises from the restrictions quantifier
nesting places on the variable orderings that can be utilized during backtracking search. In this paper we present a technique
for alleviating some of this complexity by utilizing an order unconstrained SAT solver during QBF solving. The innovation
of our paper lies in the integration of SAT and QBF. We have developed methods that allow information obtained from each solver
to be used to improve the performance of the other. Unlike previous attempts to avoid the ordering constraints imposed by
quantifier nesting, our algorithm retains the polynomial space requirements of standard backtracking search. Our empirical
results demonstrate that our techniques allow improvements over the current state-of-the-art in QBF solvers.