Skip to main content

A Practical Algorithm for Structure Embedding

Author(s): Murphy, Charlie; Kincaid, Zachary

To refer to this page use:
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.
Publication Date: 2019
Citation: Murphy, Charlie, and Zachary Kincaid. "A Practical Algorithm for Structure Embedding." In International Conference on Verification, Model Checking, and Abstract Interpretation (2019), pp. 342-362. doi:10.1007/978-3-030-11245-5_16
DOI: 10.1007/978-3-030-11245-5_16
ISSN: 0302-9743
Pages: 342 - 362
Type of Material: Conference Article
Journal/Proceeding Title: International Conference on Verification, Model Checking, and Abstract Interpretation
Version: Author's manuscript

Items in OAR@Princeton are protected by copyright, with all rights reserved, unless otherwise indicated.