A new Approach for Solving Satisfiability Problems with Qualitative Preferences

摘要: The problem of expressing and solving satisfiability problems (SAT) with qualitative preferences is central in many areas Computer Science Artificial Intelligence. In previous papers, it has been shown that on literals allow for capturing qualitative/quantitative literals/formulas; an optimal model a can be computed via simple modification the Davis-Logemann-Loveland procedure (DLL): Given SAT formula, solution by simply imposing DLL branches according to partial order preferences. Unfortunately, well known introducing ordering branching heuristic may cause exponential degradation its performances. experimental analysis reported these papers hightlights such indeed show up presence significant number preferences. In this paper we propose alternative which does not require any heuristic: Once computed, constraint added input formula new (if any) better than last computed. We implemented idea, resulting system lead improvements wrt original proposal when dealing MIN-ONE/MAX-SAT corresponding structured instances.