Finding hardness reductions automatically using SAT solvers
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2024
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866909100089016320 |
|---|---|
| author | Bergold, Helena Scheucher, Manfred Schröder, Felix |
| author_facet | Bergold, Helena Scheucher, Manfred Schröder, Felix |
| contents | In this article, we show that the completion problem, i.e. the decision problem whether a partial structure can be completed to a full structure, is NP-complete for many combinatorial structures. While the gadgets for most reductions in literature are found by hand, we present an algorithm to construct gadgets in a fully automated way. Using our framework which is based on SAT, we present the first thorough study of the completion problem on sign mappings with forbidden substructures by classifying thousands of structures for which the completion problem is NP-complete. Our list in particular includes interior triple systems, which were introduced by Knuth towards an axiomatization of planar point configurations. Last but not least, we give an infinite family of structures generalizing interior triple system to higher dimensions for which the completion problem is NP-complete. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2402_06397 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Finding hardness reductions automatically using SAT solvers Bergold, Helena Scheucher, Manfred Schröder, Felix Computational Complexity Artificial Intelligence Data Structures and Algorithms Logic in Computer Science Combinatorics In this article, we show that the completion problem, i.e. the decision problem whether a partial structure can be completed to a full structure, is NP-complete for many combinatorial structures. While the gadgets for most reductions in literature are found by hand, we present an algorithm to construct gadgets in a fully automated way. Using our framework which is based on SAT, we present the first thorough study of the completion problem on sign mappings with forbidden substructures by classifying thousands of structures for which the completion problem is NP-complete. Our list in particular includes interior triple systems, which were introduced by Knuth towards an axiomatization of planar point configurations. Last but not least, we give an infinite family of structures generalizing interior triple system to higher dimensions for which the completion problem is NP-complete. |
| title | Finding hardness reductions automatically using SAT solvers |
| topic | Computational Complexity Artificial Intelligence Data Structures and Algorithms Logic in Computer Science Combinatorics |
| url | https://arxiv.org/abs/2402.06397 |