FG1 Seminar talk

Michael Kompatscher
A complexity dichotomy for Poset-SAT

Let Phi be a finite set of quantifier-free formulas in the language of orders. Then an instance of the computational problem Poset-SAT(Phi) consists of a conjunction of equations and formulas from Phi. The task is to decide whether there is a partial order that satisfies this conjunction. We show that Poset-SAT(Phi) is NP-complete or solvable in polynomial time, depending on the set Phi.

We first restate the Poset-SAT problems as constraint satisfaction problems of reducts of the random partial order. We then study these reducts, analysing their polymorphism clones with the help of methods developed by Bodirsky and Pinsker. In the course of this analysis we establish a structural dichotomy regarding the clones that corresponds to the complexity dichotomy.

This is a joint work with Trung Van Pham.