SAT-Solving the Poset Cover Problem
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , |
|---|---|
| Format: | Preprint |
| Publié: |
2025
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866913824137805824 |
|---|---|
| author | Yuan, Chih-Cheng Rex Wang, Bow-Yaw |
| author_facet | Yuan, Chih-Cheng Rex Wang, Bow-Yaw |
| contents | The poset cover problem seeks a minimum set of partial orders whose linear extensions cover a given set of linear orders. Recognizing its NP-completeness, we devised a non-trivial reduction to the Boolean satisfiability problem using a technique we call swap graphs, which avoids the complexity explosion of the naive method. By leveraging modern SAT solvers, we efficiently solve instances with reasonable universe sizes. Experimental results using the Z3 theorem prover on randomly generated inputs demonstrate the effectiveness of our method. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2505_04013 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | SAT-Solving the Poset Cover Problem Yuan, Chih-Cheng Rex Wang, Bow-Yaw Logic in Computer Science Discrete Mathematics The poset cover problem seeks a minimum set of partial orders whose linear extensions cover a given set of linear orders. Recognizing its NP-completeness, we devised a non-trivial reduction to the Boolean satisfiability problem using a technique we call swap graphs, which avoids the complexity explosion of the naive method. By leveraging modern SAT solvers, we efficiently solve instances with reasonable universe sizes. Experimental results using the Z3 theorem prover on randomly generated inputs demonstrate the effectiveness of our method. |
| title | SAT-Solving the Poset Cover Problem |
| topic | Logic in Computer Science Discrete Mathematics |
| url | https://arxiv.org/abs/2505.04013 |