QBF with Soft Variables

QBF formulae are usually considered in prenex form, i.e. the quantifier block is completely separated from the propositional part of the QBF. Among others, the semantics of the QBF is defined by the sequence of the variables within the prefix, where existentially quantified variables depend on all universally quantified variables stated to the left. In this paper we extend that classical definition and consider a new quantification type which we call soft variable. The idea is to allow a flexible position and quantifier type for these variables. Hence the type of quantifier of the soft variable can also be altered. Based on this concept, we present an optimization problem seeking an optimal prefix as defined by user-given preferences. We state an algorithm based on MaxQBF, and present several applications – mainly from verification area – which can be naturally translated into the optimization problem for QBF with soft variables. We further implemented a prototype solver for this formalism, and compare our approach to previous work, that differently from ours does not guarantee optimality and completeness.