Dear Wolframers, regarding the problem of Quantified Boolean Formula satisfiability checking, how are the capabilities of the Wolfram Language best harnessed ?

On the one hand, we have Resolve that performs quantifier elimination, for example :

And and the other hand, we have the SatisfiableQ and TautologyQ builtin functions dealing with (non quantified) boolean formula satisfiability.

I surmise then that the correct way of checking the satisfiability of Quantified Boolean Formula is to perform quantifier elimination using Resolve, and to then check the satisfiability of the resulting formula using SatisfiableQ.

Could anyone give some advice about the best way to deal with Quantified Boolean Formula in the Wolfram Language ?

Thanks for your much appreciated help.