Combining approaches for solving Satisfiability problems with Preferences and their Evaluation

摘要: The ability to effectively reason in the presence of qualitative preferences on literals or formulas is a central issue in Artificial Intelligence. In the last few years, two procedures have been presented in order to reason with propositional satisfiability (SAT) problems in the presence of additional, partially ordered qualitative preferences on literals or formulas: The first requires a modification of the branching heuristic of the SAT solver in order to guarantee that the first solution is optimal, while the second computes a sequence of solutions, each guaranteed to be better than the previous one. The two approaches have been compared on specific classes of instances—each having an empty partial order—showing that the second has superior performance. In this paper we show that these two approaches can be combined yielding a new effective procedure. In particular, we modify the branching heuristic—as in the first approach—by possibly changing the polarity of the returned literal, and then we continue the search—as in the second approach—looking for better solutions. We extended the experimental analysis conducted in previous papers by considering a wide variety of problems, having both an empty and a non-empty partial order: The results show that the new procedure performs better than the two previous approaches on average, and especially on the “hard” problems.