否定受限反相器问题中归结策略的一个有趣新结果
人工智能
2020-11-03 v1
摘要
通常,否定受限反相器问题被称为一种用与门、或门及少量反相器构造反相器的谜题。本文介绍关于两种强大的 ATP(自动定理证明)策略在处理否定受限反相器问题上的有效性的一项有趣新结果。两种归结策略分别为 UR(单元归结)归结与超归结。在实验中,我们给出两类自动电路构造:3 输入/输出反相器与 4 输入/输出 BCD 计数器电路。两类电路均用少量受限反相器构造。有趣的是,结果表明在 SOS(支持集)规模的度量上,UR 归结比超归结显著更快。此外,我们讨论了可能导致 UR 归结与超归结之间计算代价显著差异的句法与语义准则。
引用
@article{arxiv.2011.00775,
title = {A Curious New Result of Resolution Strategies in Negation-Limited Inverters Problem},
author = {Ruo Ando and Yoshiyasu Takefuji},
journal= {arXiv preprint arXiv:2011.00775},
year = {2020}
}