A practical algorithm for structure embedding

Charlie Murphy, Zachary Kincaid

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

This paper presents an algorithm for the structure embedding problem: given two finite first-order structures over a common relational vocabulary, does there exist an injective homomorphism from one to the other? The structure embedding problem is NP-complete in the general case, but for monadic structures (each predicate has arity ≤ 1) we observe that it can be solved in polytime by reduction to bipartite graph matching. Our algorithm, MatchEmbeds, extends the bipartite matching approach to the general case by using it as the foundation of a backtracking search procedure. We show that MatchEmbeds outperforms state-of-the-art SAT, CSP, and subgraph isomorphism solvers on difficult random instances and significantly improves the performance of a client model checker for multi-threaded programs.

Original languageEnglish (US)
Title of host publicationVerification, Model Checking, and Abstract Interpretation - 20th International Conference, VMCAI 2019, Proceedings
EditorsRuzica Piskac, Constantin Enea
PublisherSpringer Verlag
Pages342-362
Number of pages21
ISBN (Print)9783030112448
DOIs
StatePublished - Jan 1 2019
Event20th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2019 - Cascais, Portugal
Duration: Jan 13 2019Jan 15 2019

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume11388 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other20th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2019
CountryPortugal
CityCascais
Period1/13/191/15/19

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'A practical algorithm for structure embedding'. Together they form a unique fingerprint.

  • Cite this

    Murphy, C., & Kincaid, Z. (2019). A practical algorithm for structure embedding. In R. Piskac, & C. Enea (Eds.), Verification, Model Checking, and Abstract Interpretation - 20th International Conference, VMCAI 2019, Proceedings (pp. 342-362). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11388 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-030-11245-5_16