# Second Order QBF

Consider a universe with two elements 0,1 and a second order formula, i.e. of the form "forall R exists S ... such that F", where R,S are relation symbols of some given arity, and F is some first order formula e.g. "exists x forall y R(x,y)&S(y,x)".

Further for simplicity assume that the quantifier-free part (the "matrix") of F is given in disjunctive normal form, and everything is in prenex normal form.

What would be an algorithm to decide satisfiability (or better, list all solutions namely if the formula begins with "exists R" to list all relations that satisfy it) of such second order boolean formula, anything better than brute force in the average case (as probably no one knows to do it better than brute force in the worst case if that's even possible)? Surely just a reference would be great as well.

Alternatively, if one can point me to a second-order version of the resolution method.