Solving satisfiability problems with preferences
Solving satisfiability problems with preferences
复制标题
解决偏好的满意度问题
作者：
E. Rosa;E. Giunchiglia;M. Maratea
命题满意度（SAT）是计算机科学和人工智能中的成功故事：SAT求解器目前用于解决许多不同的应用程序域中的问题，包括计划和正式验证。由于有数百万个变量的问题。 DLL是一个决策过程，但是可以很容易地修改它，以返回满足输入子句集的一个或所有分配，但假设存在至少一个。条款：实际上，返回的作业在某种意义上也必须是“最佳”，例如，他们必须满足许多其他约束（如偏好）。从文字上的定性偏好开始，定义为这样一个poset的部分有序集（POSET）。我们显示的（i）如何扩展DLL，以返回一个或所有最佳模型（一旦在子句中转换并假设ψ是满足的），以及（ii）如何使用相同的过程来计算最佳模型对公式和/或WRT的定性偏好是对文字或公式的定量偏好。 - 艺术系统，针对我们考虑的特定问题量身定制。
Propositional satisfiability (SAT) is a success story in Computer Science and Artificial Intelligence: SAT solvers are currently used to solve problems in many different application domains, including planning and formal verification. The main reason for this success is that modern SAT solvers can successfully deal with problems having millions of variables. All these solvers are based on the Davis–Logemann–Loveland procedure (dll). In its original version, dll is a decision procedure, but it can be very easily modified in order to return one or all assignments satisfying the input set of clauses, assuming at least one exists. However, in many cases it is not enough to compute assignments satisfying all the input clauses: Indeed, the returned assignments have also to be “optimal” in some sense, e.g., they have to satisfy as many other constraints—expressed as preferences—as possible. In this paper we start with qualitative preferences on literals, defined as a partially ordered set (poset) of literals. Such a poset induces a poset on total assignments and leads to the definition of optimal model for a formula ψ as a minimal element of the poset on the models of ψ. We show (i) how dll can be extended in order to return one or all optimal models of ψ (once converted in clauses and assuming ψ is satisfiable), and (ii) how the same procedures can be used to compute optimal models wrt a qualitative preference on formulas and/or wrt a quantitative preference on literals or formulas. We implemented our ideas and we tested the resulting system on a variety of very challenging structured benchmarks. The results indicate that our implementation has comparable performances with other state-of-the-art systems, tailored for the specific problems we consider.