Solving Hierarchical Soft Constraints with an SMT Solver
Solving Hierarchical Soft Constraints with an SMT Solver
复制标题
使用 SMT 求解器求解分层软约束
DOI：
10.1145/3384613.3384654
复制
发表时间：
2020
期刊：
影响因子：
--
通讯作者：
Hiroshi Hosobe
中科院分区：
文献类型：
--
作者：
Ren Masahiro and Toshiaki Omori;Hiroshi Hosobe
约束允许声明性地规范许多领域中的各种问题。特别是，约束层次结构，使软约束与层次偏好是有用的编程交互式图形应用程序。然而，它仍然是难以处理的约束层次与非线性约束。提出了一种求解可能含有非线性约束的约束层次的算法。它不是直接求解约束层次，而是通过使用外部SMT求解器连续生成并求解普通约束问题。实验结果表明，该算法能够找到精确的约束层次解。
Constraints allow the declarative specification of various problems in many fields. In particular, constraint hierarchies that enable soft constraints with hierarchical preferences are useful for programming interactive graphical applications. However, it is still difficult to handle constraint hierarchies with nonlinear constraints. This paper proposes an algorithm for solving constraint hierarchies possibly with nonlinear constraints. Instead of directly solving a constraint hierarchy, it successively generates and solves ordinary constraint problems by using an external SMT solver. The results of our experiments show that the algorithm is able to find accurate constraint hierarchy solutions.