On quantified weighted MAX-SAT

In this paper, we introduce quantified weighted MAX-SAT (Q-W-MAX-SAT) as the problem of assigning values to existentially quantified variables permitted by order of quantification, so that the sum of the weights of satisfied clauses equals or exceeds a given threshold, for all combinations of all values of universally quantified variables. Q-W-MAX-SAT serves as a prototypical conditional decision-making problem in which satisfying all constraints is either impossible or unnecessary or satisfying some constraints is more important than satisfying some other constraints. We report on two branching heuristics and four simplification rules to solve Q-W-MAX-SAT efficiently, along with an empirical evaluation.