Document Open Access Logo

A Dichotomy Theorem for the Inverse Satisfiability Problem

Authors Victor Lagerkvist, Biman Roy

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2017.39.pdf
  • Filesize: 0.55 MB
  • 14 pages

Document Identifiers

Author Details

Victor Lagerkvist
Biman Roy

Cite AsGet BibTex

Victor Lagerkvist and Biman Roy. A Dichotomy Theorem for the Inverse Satisfiability Problem. In 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 93, pp. 39:1-39:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
https://doi.org/10.4230/LIPIcs.FSTTCS.2017.39

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.
Keywords
  • Complexity Theory
  • Inverse Satisfiability
  • Clone Theory

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. L. Barto. Constraint satisfaction problem and universal algebra. ACM SIGLOG News, 1(2):14-24, 2014. Google Scholar
  2. M. Bodirsky, M. Pinsker, and T. Tsankov. Decidability of definability. Journal of Symbolic Logic, 78(4):1036-1054, 2013. Google Scholar
  3. V. G. Bodnarchuk, L. A. Kaluzhnin, V. N. Kotov, and B. A. Romov. Galois theory for Post algebras. I. Cybernetics, 5:243-252, 1969. Google Scholar
  4. V. G. Bodnarchuk, L. A. Kaluzhnin, V. N. Kotov, and B. A. Romov. Galois theory for Post algebras. II. Cybernetics, 5:531-539, 1969. Google Scholar
  5. E. Böhler, N. Creignou, S. Reith, and H. Vollmer. Playing with Boolean blocks, part I: Post’s lattice with applications to complexity theory. ACM SIGACT-Newsletter, 34(4):38-52, 2003. Google Scholar
  6. E. Böhler, N. Creignou, S. Reith, and H. Vollmer. Playing with Boolean blocks, part II: Constraint satisfaction problems. ACM SIGACT-Newsletter, 35(1):22-35, 2004. Google Scholar
  7. H. Chen. Inverse NP problems. Computational Complexity, 17(1):94-118, 2008. Google Scholar
  8. N. Creignou and H. Vollmer. Boolean constraint satisfaction problems: When does Post’s lattice help? In N. Creignou, P. G. Kolaitis, and H. Vollmer, editors, Complexity of Constraints, volume 5250 of Lecture Notes in Computer Science, pages 3-37. Springer Berlin Heidelberg, 2008. Google Scholar
  9. Nadia Creignou, Phokion G. Kolaitis, and Bruno Zanuttini. Structure identification of boolean relations and plain bases for co-clones. J. Comput. Syst. Sci., 74(7):1103-1115, 2008. URL: http://dx.doi.org/10.1016/j.jcss.2008.02.005.
  10. Creignou, N. and Hebrard, J.-J. On generating all solutions of generalized satisfiability problems. RAIRO-Theor. Inf. Appl., 31(6):499-511, 1997. Google Scholar
  11. D. Geiger. Closed systems of functions and predicates. Pacific Journal of Mathematics, 27(1):95-100, 1968. Google Scholar
  12. P. Jonsson, V. Lagerkvist, and G. Nordh. Constructing np-intermediate problems by blowing holes with parameters of various properties. Theoretical Computer Science, 581:67-82, 2015. Google Scholar
  13. P. Jonsson, V. Lagerkvist, G. Nordh, and B. Zanuttini. Strong partial clones and the time complexity of SAT problems. Journal of Computer and System Sciences, 84:52-78, 2017. Google Scholar
  14. D. Kavvadias and M. Sideri. The inverse satisfiability problem. SIAM Journal on Computing, 28:152-163, 1998. Google Scholar
  15. R. Ladner. On the structure of polynomial time reducibility. Journal of the ACM, 22:155-171, 1975. Google Scholar
  16. V. Lagerkvist. Weak bases of Boolean co-clones. Information Processing Letters, 114(9):462-468, 2014. Google Scholar
  17. V. Lagerkvist and M. Wahlström. The power of primitive positive definitions with polynomially many variables. Journal of Logic and Computation, 27(5):1465-1488, 2017. Google Scholar
  18. V. Lagerkvist, M. Wahlström, and B. Zanuttini. Bounded bases of strong partial clones. In Proceedings of the 45th International Symposium on Multiple-Valued Logic (ISMVL-2015), pages 189-194, 2015. Google Scholar
  19. E. Post. The two-valued iterative systems of mathematical logic. Annals of Mathematical Studies, 5:1-122, 1941. Google Scholar
  20. B.A. Romov. The algebras of partial functions and their invariants. Cybernetics, 17(2):157-167, 1981. Google Scholar
  21. T. Schaefer. The complexity of satisfiability problems. In Proceedings of the 10th Annual ACM Symposium on Theory Of Computing (STOC-78), pages 216-226. ACM Press, 1978. Google Scholar
  22. H. Schnoor and I. Schnoor. Enumerating all solutions for constraint satisfaction problems. In Proceedings of the 24th Annual Symposium on Theoretical Aspects of Computer Science (STACS-2007), volume 4393, pages 694-705. Springer, 2007. Google Scholar
  23. H. Schnoor and I. Schnoor. Partial polymorphisms and constraint satisfaction problems. In N. Creignou, P. G. Kolaitis, and H. Vollmer, editors, Complexity of Constraints, volume 5250 of Lecture Notes in Computer Science, pages 229-254. Springer Berlin Heidelberg, 2008. Google Scholar
  24. R. Willard. Testing expressibility is hard. In Proceedings of the 16th International Conference Principles and Practice of Constraint Programming (CP-2010), volume 6308 of Lecture Notes in Computer Science, pages 9-23. Springer, 2010. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact