SAT-Solving the Poset Cover Problem

TL;DR

This paper introduces a novel SAT-based approach using swap graphs to efficiently solve the NP-complete poset cover problem, demonstrating practical effectiveness with modern SAT solvers on random instances.

Contribution

The paper presents a new reduction technique to SAT for the poset cover problem that avoids naive complexity explosion and leverages modern SAT solvers for practical solutions.

Findings

Effective reduction to SAT using swap graphs

Successful application of Z3 solver on random instances

Demonstrated efficiency and practicality of the approach

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.