SAT-Solving the Poset Cover Problem

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.

This work was conducted in 2017-2018 while the first author was an undergraduate student at National Taiwan Normal University and an adjunct research assistant at Academia Sinica