Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2507.05044 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866911042593882112 |
|---|---|
| author | Brandl, Albert Fermüller, Christian G. Salzer, Gernot |
| author_facet | Brandl, Albert Fermüller, Christian G. Salzer, Gernot |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2507_05044 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Testing for Renamability to Classes of Clause Sets Brandl, Albert Fermüller, Christian G. Salzer, Gernot Logic in Computer Science Computational Complexity 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. |
| title | Testing for Renamability to Classes of Clause Sets |
| topic | Logic in Computer Science Computational Complexity |
| url | https://arxiv.org/abs/2507.05044 |