A Curious New Result of Resolution Strategies in Negation-Limited Inverters Problem
This work addresses a specific puzzle in circuit design for researchers in automated theorem proving, but it appears incremental as it compares existing strategies without introducing new methods.
The paper tackled the negation-limited inverters problem by evaluating two ATP strategies, UR resolution and hyper-resolution, for automated circuit construction, finding that UR resolution was drastically faster in terms of SOS size for 3 and 4 input/output circuits.
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.