Towards feasible solutions of the tautology problem

Abstract

This paper studies the problem of testing Boolean validity in polynomial time. A number of hitherto unnoticed elegant properties of Boolean expressions are established in Section 3 to yield generally more efficient methods for many expressions. Combinatorial metatheorems concerning the tautology problem are proved in Section 4. Special partial methods are developed in Sections 6 and 7 which yield efficient solutions to two sets of hard examples which defeat existing methods in the literature. Finally, two general approaches in terms of size calculations and composite expressions with symbolic abbreviations which are under investigation are briefly indicated in Section 7. © 1976.