Deciding Open Definability via Subisomorphisms

Abstract

Given a logic $\varvec{\mathcal {L}}$, the $\varvec{\mathcal {L}}$-Definability Problem for finite structures takes as input a finite structure $\varvec{A}$ and a target relation T over the domain of $\varvec{A}$, and determines whether there is a formula of $\varvec{\mathcal {L}}$ whose interpretation in $\varvec{A}$ coincides with T. In this note we present an algorithm that solves the definability problem for quantifier-free first order formulas. Our algorithm takes advantage of a semantic characterization of open definability via subisomorphisms, which is sound and complete. We also provide an empirical evaluation of its performance.

A An Execution of OpenDef

To illustrate how Algorithm 1 works, we run it for the following instance. The input structure is the graph $\varvec{G}=(\{0,1,2,3\},E)$

and the target relation is

$$ T=\{(a,b,c,d):E(b,c)\wedge (a=b \vee c=d)\}. $$

A brute force algorithm based on Theorem 1 would have to check that every sub-isomorphisms of $\varvec{G}$ preserves T. That is, for each subuniverse S of $\varvec{G}$ compute all sub-isomorphisms with domain S, and check them for preservation. This means going trough every subuniverse listed in the tree below, where the automorphisms of all subuniverses will be calculated and checked for preservation.

The first improvement of Algorithm 1 allows us to prune tree levels whose nodes do not have cardinality in ${{\mathrm{spec}}}(T)$ (this is correct due to Lemma 1). In the current example, it only processes subuniverses with size in ${{\mathrm{spec}}}(T)=\{2,3\}$. This amounts to process only the following subuniverses. (The node Root is not a subuniverse to be processed; we add it to better visualize the tree traversed by the DFS.)

The second improvement is due to the order in which Algorithm 1 computes the subisomorphisms with a given domain S. It first tries to find an isomorphism from S to an already processed subuniverse. In the case where such an isomorphism exists, no other isomorphisms from S are computed, and the subuniverses contained in S are pruned (this is correct by Corollary 1). The subuniverses of $\varvec{G}$ actually processed by Algorithm 1 are shown below. The bold nodes are in $\mathcal {S}$, and therefore are the only ones that are checked for automorphisms and subuniverses.

In view of the strategies Algorithm 1 employs we get a good idea of what makes for a well conditioned instances $\varvec{A},T$:

• Target relations with a small spectrum compared to the power set of A.

• Structures with few isomorphisms types for substructures with cardinality in the spectrum.