A Moderately Exponential Time Algorithm for k-IBDD Satisfiability
A Moderately Exponential Time Algorithm for k-IBDD Satisfiability
复制标题
k-IBDD 可满足性的中等指数时间算法
DOI：
10.1007/s00453-017-0332-2
复制
发表时间：
2018
期刊：
影响因子：
1.1
通讯作者：
Teruyama Junichi
中科院分区：
文献类型：
--
作者：
Nagao Atsuki;Seto Kazuhisa;Teruyama Junichi
提出了一种叉索引二元决策图的可满足性算法。所提出的指数空间和确定性算法解决了k-IBDD的可满足性，即，k-IBDD SAT，对于具有n个变量和cn个节点的实例，其中。我们还提供了一个多项式空间和确定性算法，解决了ak-IBDD SAT的多项式大小为任何constantintime。此外，该算法适用于两个IBDD的等价性检查。
We present a satisfiability algorithm fork-indexed binary decision diagrams (k-IBDDs). The proposed exponential space and deterministic algorithm solves the satisfiability ofk-IBDDs, i.e.,k-IBDD SAT, for instances withnvariables andcnnodes intime, where. We also provide a polynomial space and deterministic algorithm that solves ak-IBDD SAT of polynomial size for any constantintime. In addition, the proposed algorithm is applicable to equivalence checking of two IBDDs.
登录
查看更多内容
通用 CNF SAT 的精确算法
DOI：
10.1007/978-1-4939-2864-4_133
发表时间：
2008
期刊：
Mathematical systems theory
影响因子：
--
作者：
E. Hirsch
通讯作者：
E. Hirsch
基于汉明球搜索的 SAT 算法
DOI：
10.1007/978-3-540-24749-4_13
发表时间：
2004
期刊：
2011 IEEE 52nd Annual Symposium on Foundations of Computer Science
影响因子：
--
作者：
E. Dantsin;E. Hirsch;A. Wolpert
通讯作者：
A. Wolpert
索引 BDD：表示和验证布尔函数的技术的算法进步
DOI：
10.1109/12.644298
发表时间：
1997
期刊：
IEEE Trans. Computers
影响因子：
--
作者：
J. Jain;J. Bitner;M. Abadir;J. Abraham;D. Fussell
通讯作者：
D. Fussell
对抗 Perebor：公式和 QBF 满足性的新算法和改进算法
DOI：
10.1109/focs.2010.25
发表时间：
2010
期刊：
2010 IEEE 51st Annual Symposium on Foundations of Computer Science
影响因子：
--
作者：
R. Santhanam
通讯作者：
R. Santhanam
完全二元基础公式的可满足性算法和平均情况硬度
DOI：
--
发表时间：
2012
期刊：
Proceedings of the 27th IEEE Conference on Computational Complexity
影响因子：
--
作者：
K.Seto;S.Tamaki
通讯作者：
S.Tamaki