A Curious New Result of Resolution Strategies in Negation-Limited Inverters Problem

TL;DR

This paper investigates the effectiveness of two automated theorem proving strategies, UR resolution and hyper-resolution, in solving negation-limited inverter circuit construction problems, revealing UR resolution's superior speed.

Contribution

It introduces a comparative analysis of UR resolution and hyper-resolution strategies on negation-limited inverter problems, highlighting UR resolution's efficiency in automated circuit synthesis.

Findings

UR resolution is significantly faster than hyper-resolution.

The size of the set of support influences resolution speed.

Syntactic and semantic factors affect computational costs.

Abstract

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.