SAT-Solving the Poset Cover Problem
Logic in Computer Science
2025-05-08 v1 Discrete Mathematics
Abstract
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.
Cite
@article{arxiv.2505.04013,
title = {SAT-Solving the Poset Cover Problem},
author = {Chih-Cheng Rex Yuan and Bow-Yaw Wang},
journal= {arXiv preprint arXiv:2505.04013},
year = {2025}
}