SAT-Solving the Poset Cover Problem

TL;DR

The poset cover problem asks for a minimal collection of partial orders whose linear extensions cover a given set of linear orders, recognizing its NP-completeness. The paper contributes a non-trivial SAT reduction based on swap graphs to avoid naive encoding blow-up, enabling efficient solving with SAT solvers such as the Z3 theorem prover. It introduces a moat-based insulation around strongly connected components to bound constraints and demonstrates the approach with randomized experiments, showing practical performance for moderate universe sizes and hinting at a divide-and-conquer parallelizable strategy. The work highlights potential applications to partial-order analyses and formal concept analysis, and suggests future optimizations for handling larger instances.

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.