TY - GEN
T1 - A practical algorithm for structure embedding
AU - Murphy, Charlie
AU - Kincaid, Zachary
N1 - Publisher Copyright:
© Springer Nature Switzerland AG 2019.
PY - 2019
Y1 - 2019
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=85061107611&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85061107611&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-11245-5_16
DO - 10.1007/978-3-030-11245-5_16
M3 - Conference contribution
AN - SCOPUS:85061107611
SN - 9783030112448
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 342
EP - 362
BT - Verification, Model Checking, and Abstract Interpretation - 20th International Conference, VMCAI 2019, Proceedings
A2 - Piskac, Ruzica
A2 - Enea, Constantin
PB - Springer Verlag
T2 - 20th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2019
Y2 - 13 January 2019 through 15 January 2019
ER -