Search

Generally, the negation-limited inverters problem is a puzzle of constructing an inverter with AND gates and OR gates, and a few inverters. This paper introduces a curious new result about the effectiveness of two powerful ATP (Automated Theorem Proving) strategies in tackling negation-limited inverter problems. Two resolution strategies are UR (Unit Resulting) resolution and Hyper-Resolution. In the experiment, we cope with two kinds of automated circuit construction: three input/output inverters and four 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 cause a considerable difference in computation cost between UR resolution and Hyper-Resolution. [ABSTRACT FROM AUTHOR]