Some dichotomy theorems on constant-free quantified Boolean formulas

Abstract

In this paper we study the satisfiability of constant-free quantified boolean formulas. We consider the following classes of quantified boolean formulas. Fix a finite set of basic boolean logical functions. Take conjunctions of these basic functions applied to variables in arbitrary way. Finally, quantify existentially or universally some of the variables.

Schaefer earlier studied the satisfiability of quantified boolean formulas with constants. He showed that every such problem is either in P or PSPACE-complete and he gave a complete classification of the tractable cases. We extend the PSPACE-hardness results to constant-free quantified boolean formulas obtaining a dichotomy theorem for the satisfiability of constant-free quantified boolean formulas. We find that, in fact, constants do not make a difference when considering the satisfiability of quantified boolean formulas. We also prove a dichotomy theorem that allows us to improve a previous result on the learnability of quantified boolean formulas getting rid of the constants.