论文标题
否定逆变器问题解决方案策略的奇怪新结果
A Curious New Result of Resolution Strategies in Negation-Limited Inverters Problem
论文作者
论文摘要
通常，否定的逆变器问题被称为用与大门和大门以及一些逆变器构建逆变器的难题。在本文中，我们介绍了两个强大的ATP（自动化定理证明）策略在解决否定逆变器问题上的有效性。两种解决方案策略是UR（单位）分辨率和超分辨率。在实验中，我们进行了两种自动电路结构：3个输入/输出逆变器和4个输入/输出BCD计数器电路。这两个电路均使用一些有限的逆变器构建。奇怪的是，事实证明，在测量SOS（一组支持）的测量中，UR分辨率的速度要快于高分辨率。此外，我们讨论了句法和语义标准，这可能会导致UR分辨率和超分辨率之间的计算成本差异。
Generally, negation-limited inverters problem is known as a puzzle of constructing an inverter with AND gates and OR gates and a few inverters. In this paper, we introduce a curious new result about the effectiveness of two powerful ATP (Automated Theorem Proving) strategies on tackling negation limited inverter problem. Two resolution strategies are UR (Unit Resulting) resolution and hyper-resolution. In experiment, we come two kinds of automated circuit construction: 3 input/output inverters and 4 input/output BCD Counter Circuit. Both circuits are constructed with a few limited inverters. Curiously, it has been turned out that UR resolution is drastically faster than hyper-resolution in the measurement of the size of SOS (Set of Support). Besides, we discuss the syntactic and semantic criteria which might causes considerable difference of computation cost between UR resolution and hyper-resolution.
