Construction of an ROBDD for a PB-Constraint in Band Form and Related Techniques for PB-Solvers
Construction of an ROBDD for a PB-Constraint in Band Form and Related Techniques for PB-Solvers
复制标题
DOI：
10.1587/transinf.2014fop0007
复制
发表时间：
2015-06-01
影响因子：
0.7
通讯作者：
Nabeshima, Hidetomo
中科院分区：
文献类型：
--
作者：
Sakai, Masahiko;Nabeshima, Hidetomo
伪树状（PB）问题是整数线性问题，仅限于0-1变量。本文讨论了PB - 索引的加速技术，这些技术采用了CNF的SAT解决，每种CNF通过二进制决策图（BDD）从每个PB-constraint产生。具体而言，我们显示（i）从带形式的约束L中有效地构造了有序的BDD（ROBDD）
Pseudo-Boolean (PB) problems are Integer Linear Problem restricted to 0-1 variables. This paper discusses on acceleration techniques of PB-solvers that employ SAT-solving of combined CNFs each of which is produced from each PB-constraint via a binary decision diagram (BDD). Specifically, we show (i) an efficient construction of a reduced ordered BDD (ROBDD) from a constraint in band form l