Testing for Renamability to Classes of Clause Sets

TL;DR

This paper studies the problem of determining whether clause sets can be renamed to fit certain classes, providing polynomial-time algorithms for some classes and NP-completeness results for others.

Contribution

It introduces decision procedures for renamability to classes like Horn and OCC1N, and establishes NP-completeness for PVD, advancing understanding of clause set classification.

Findings

Polynomial-time decision algorithms for Horn and OCC1N classes

NP-completeness of renamability for class PVD

Renaming can be extracted from saturated clause sets

Abstract

This paper investigates the problem of testing clause sets for membership in classes known from literature. In particular, we are interested in classes defined via renaming: Is it possible to rename the predicates in a way such that positive and negative literals satisfy certain conditions? We show that for classes like Horn or OCC1N, the existence of such renamings can be decided in polynomial time, whereas the same problem is NP-complete for class PVD. The decision procedures are based on hyper-resolution; if a renaming exists, it can be extracted from the final saturated clause set.