eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2018-02-12
39:1
39:14
10.4230/LIPIcs.FSTTCS.2017.39
article
A Dichotomy Theorem for the Inverse Satisfiability Problem
Lagerkvist, Victor
Roy, Biman
The inverse satisfiability problem over a set of Boolean relations Gamma (Inv-SAT(Gamma)) is the computational decision problem of, given a set of models R, deciding whether there exists a SAT(Gamma) instance with R as its set of models. This problem is co-NP-complete in general and a dichotomy theorem for finite Γ containing the constant Boolean relations was obtained by Kavvadias and Sideri. In this paper we remove the latter condition and prove that Inv-SAT(Gamma) is always either tractable or co-NP-complete for all finite sets of relations Gamma, thus solving a problem open since 1998. Very little of the techniques used by Kavvadias and Sideri are applicable and we have to turn to more recently developed algebraic approaches based on partial polymorphisms. We also consider the case when Γ is infinite, where the situation differs markedly from the case of SAT. More precisely, we show that there exists infinite Gamma such that Inv-SAT(Gamma) is tractable even though there exists finite Delta is subset of Gamma such that Inv-SAT(Delta) is co-NP-complete.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol093-fsttcs2017/LIPIcs.FSTTCS.2017.39/LIPIcs.FSTTCS.2017.39.pdf
Complexity Theory
Inverse Satisfiability
Clone Theory