A declarative encoding of telecommunications feature subscription in SAT
A declarative encoding of telecommunications feature subscription in SAT
复制标题
DOI：
10.1145/1599410.1599442
复制
发表时间：
2009-09
期刊：
影响因子：
--
通讯作者：
M. Codish;S. Genaim;Peter James Stuckey
中科院分区：
文献类型：
--
作者：
M. Codish;S. Genaim;Peter James Stuckey
本文描述了一个电信功能订阅配置问题的命题逻辑和解决方案，使用一个国家的最先进的布尔满意度求解器的编码。以陈述式的形式将问题实例转换为相应的合取范式命题公式。实验评估表明，我们的编码是相当快的速度比以前的方法的基础上使用布尔满意度求解器。获得这样一个快速求解器的关键是布尔表示和编码中的基本操作的仔细设计。声明式编程风格的选择使得使用复杂的电路设计相对容易地并入编码器并微调应用。
This paper describes the encoding of a telecommunications feature subscription configuration problem to propositional logic and its solution using a state-of-the-art Boolean satisfaction solver. The transformation of a problem instance to a corresponding propositional formula in conjunctive normal form is obtained in a declarative style. An experimental evaluation indicates that our encoding is considerably faster than previous approaches based on the use of Boolean satisfaction solvers. The key to obtaining such a fast solver is the careful design of the Boolean representation and of the basic operations in the encoding. The choice of a declarative programming style makes the use of complex circuit designs relatively easy to incorporate into the encoder and to fine tune the application.