Toward Verifying Nonlinear Integer Arithmetic
Toward Verifying Nonlinear Integer Arithmetic
复制标题
验证非线性整数算术
DOI：
10.1145/3319396
复制
发表时间：
2019
影响因子：
2.5
通讯作者：
Liew, Vincent
中科院分区：
文献类型：
--
作者：
Beame, Paul;Liew, Vincent
通过展示如何为最广泛使用的乘法器电路的许多属性构建短分辨率证明，我们消除了使用 CDCL SAT 求解器有效验证非线性整数算术的关键障碍。人们推测这样的简短证明是不存在的。更准确地说，我们给出了数组、对角线和布斯乘子上任意 2 阶恒等式的 O(1) 大小正则分辨率证明，以及华莱士树乘子上这些恒等式的 nO(logn) 大小证明。
We eliminate a key roadblock to efficient verification of nonlinear integer arithmetic using CDCL SAT solvers, by showing how to construct short resolution proofs for many properties of the most widely used multiplier circuits. Such short proofs were conjectured not to exist. More precisely, we givenO(1)size regular resolution proofs for arbitrary degree 2 identities on array, diagonal, and Booth multipliers andnO(logn)size proofs for these identities on Wallace tree multipliers.
登录
查看更多内容
基于电路划分和冲突条款重用特殊方法的 SAT 等价检查
DOI：
--
发表时间：
2007
期刊：
2007 IEEE Design and Diagnostics of Electronic Circuits and Systems
影响因子：
--
作者：
F. V. Andrade;Márcia C. M. Oliveira;A. O. Fernandes;C. Coelho
通讯作者：
C. Coelho
MathSAT 4SMT 求解器
DOI：
--
发表时间：
2008
期刊：
International Conference on Computer Aided Verification
影响因子：
--
作者：
Roberto Bruttomesso;A. Cimatti;Anders Franzén;A. Griggio;R. Sebastiani
通讯作者：
R. Sebastiani
位精确推理的挑战
DOI：
--
发表时间：
2014
期刊：
Formal Methods in Computer-Aided Design
影响因子：
--
作者：
Armin Biere
通讯作者：
Armin Biere
使用通用进行整数乘法的一次读取分支程序 Omega(2 n/4 ) 下界。
DOI：
--
发表时间：
2001
期刊：
Symposium on the Theory of Computing
影响因子：
--
作者：
Beate Bollig;Philipp Woelfel
通讯作者：
Philipp Woelfel
解决组合设计自动化问题的证明引擎方法
DOI：
10.1145/513918.514101
发表时间：
2002
期刊：
Proceedings 2002 Design Automation Conference (IEEE Cat. No.02CH37324)
影响因子：
--
作者：
G. Andersson;Per Bjesse;B. Cook;Z. Hanna
通讯作者：
Z. Hanna