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.

翻译：偏序集覆盖问题旨在寻找一组最小偏序集，使得其线性扩展能覆盖给定的线性序集合。考虑到该问题的NP完全性，我们设计了一种非平凡归约方法，通过引入称为交换图的技术将问题转化为布尔可满足性问题，从而避免了朴素方法中的复杂度爆炸。借助现代SAT求解器，我们能够高效求解合理规模下宇宙大小的问题实例。使用Z3定理证明器在随机生成输入上的实验结果表明了该方法的有效性。