Satisfiable Formulas Closed Under Replacement

Let Var-SAT be the set of prepositional formulas which are satisfiable for any replacement of any set of literals by their complements. We discuss the complexity of Var-SAT. For 2-CNF -formulas we present a linear-time algorithm, and for DNF⩕ CNF -formulas we show the coNP—hardness of the problem Var-SAT. Further, we show that any satisfiable hitting formula and any proper subformula of a minimal unsatisfiable Horn-formula is in Var-SAT.