License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSTTCS.2017.39
URN: urn:nbn:de:0030-drops-83745
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2018/8374/
Go to the corresponding LIPIcs Volume Portal

Lagerkvist, Victor ; Roy, Biman

A Dichotomy Theorem for the Inverse Satisfiability Problem

pdf-format:
LIPIcs-FSTTCS-2017-39.pdf (0.6 MB)

Abstract

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.

BibTeX - Entry

@InProceedings{lagerkvist_et_al:LIPIcs:2018:8374,
  author =	{Victor Lagerkvist and Biman Roy},
  title =	{{A Dichotomy Theorem for the Inverse Satisfiability Problem}},
  booktitle =	{37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017)},
  pages =	{39:39--39:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-055-2},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{93},
  editor =	{Satya Lokam and R. Ramanujam},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2018/8374},
  URN =		{urn:nbn:de:0030-drops-83745},
  doi =		{10.4230/LIPIcs.FSTTCS.2017.39},
  annote =	{Keywords: Complexity Theory, Inverse Satisfiability, Clone Theory}
}

Keywords: Complexity Theory, Inverse Satisfiability, Clone Theory
Collection: 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017)
Issue Date: 2018
Date of publication: 12.02.2018

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI