Graph functional dependency checking

A computer implemented method for detecting errors in data includes obtaining one or more graph functional dependency (GFD) rules comprising a set of GFD rules, obtaining a set of GFDs representative of the data, building a canonical graph for the GFD rules, and determining that one or more GFD of the set of GFDs conflict based on the set of GFD rules and the canonical graph and, based thereon, determining an error in the set of GFDs.

TECHNICAL FIELD

The present disclosure is related to functional dependency checking, and in particular to graph functional dependency checking.

BACKGROUND

When receiving unstructured data, such as social media data or other data from non-relational database sources, there may be inconsistencies in the data, such as an object having a top speed, but the data reflecting two different top speeds for the same object, or a domain expert stating one thing as true, but a non-expert in the domain stating the same thing as false. In a relational database, functional dependencies are constraints between two sets of attributes in a relation. Conflicts may be found without much difficulty. However, unstructured data may be represented by graphs. It is difficult to determine inconsistencies or conflicts in data represented by graphs.

SUMMARY

According to one aspect of the present disclosure, a computer implemented method for detecting errors in data includes obtaining one or more graph functional dependency (GFD) rules comprising a set of GFD rules, obtaining a set of GFDs representative of the data, building a canonical graph for the GFD rules, and determining that one or more GFD of the set of GFDs conflict based on the set of GFD rules and the canonical graph and, based thereon, determining an error in the set of GFDs.

Optionally, in any of the preceding aspects, a further implementation of the aspect includes wherein the canonical graph includes an empty graph and wherein a conflict comprises a literal assigned two distinct constants.

Optionally, in any of the preceding aspects, a further implementation of the aspect includes populating the empty graph by an Expand( ) operation prior to determining if any one of the GFDs conflicts iteratively for each rule.

Optionally, in any of the preceding aspects, a further implementation of the aspect includes wherein the canonical graph comprises a first graph pattern Q6and a second graph pattern Q7, wherein the canonical graph includes two distinct copies of the first graph pattern.

Optionally, in any of the preceding aspects, a further implementation of the aspect includes wherein the set of GFD rules include a first rule: φ7=Q6[x, y, z, w](Ø→x.A=0 ∧y.B=1), a second rule: φ9=Q6[x](y.B=1→w.C=1), and third rule: φ10=Q7[x](w.C=1→x.A=1), wherein x, y, z, and w are vertices, and A, B, and C are attribute names

Optionally, in any of the preceding aspects, a further implementation of the aspect includes creating work units for each graph pattern and graph pattern copy for each GFD rule, coordinating execution of the work units on multiple processors, sharing results from each processor in response to applying the rule associated with each work unit, and assigning remaining work units to processors in response to sharing results to the multiple processors.

Optionally, in any of the preceding aspects, a further implementation of the aspect includes creating a priority queue with the work units, processing the work units on different processors, and sharing changes with other processors.

Optionally, in any of the preceding aspects, a further implementation of the aspect includes receiving a new GFD rule and determining if the set of GFD rules implies the new GFD rule.

Optionally, in any of the preceding aspects, a further implementation of the aspect includes wherein determining if the set of GFD rules implies the new rule comprises enforcing GFDs on matches in the canonical graph one by one and terminating the method with true when either an equivalence relation is conflicting or when an implied attribute name is a part of the equivalence relation.

According to one aspect of the present disclosure, a device includes a memory storage comprising instructions and one or more processors in communication with the memory, wherein the one or more processors execute the instructions to obtain one or more graph functional dependency (GFD) rules comprising a set of GFD rules, obtain a set of GFDs representative of data, build a canonical graph for the GFD rules, determine that one or more GFD of the sets of GFDs conflicts based on the GFD rules and the canonical graph, and based thereon, determine an error in the set of GFDs.

Optionally, in any of the preceding aspects, a further implementation of the aspect includes wherein the canonical graph includes an empty graph and wherein the one or more processors execute the instructions to populate the empty graph by an Expand( ) operation prior to determining if any one of the GFDs conflicts iteratively for each rule, and wherein a conflict comprises a literal assigned two distinct constants.

Optionally, in any of the preceding aspects, a further implementation of the aspect includes wherein the canonical graph comprises a first graph pattern Q6and a second graph pattern Q7, wherein the canonical graph includes two distinct copies of the first graph pattern, wherein the GFD rules include a first rule: φ7=Q6[x, y, z, w](Ø→x.A=0∧y.B=1), a second rule: φ9=Q6[x](y.B=1→w.C=1), and third rule: φ10=Q7[x](w.C=1→x.A=1), wherein x, y, z, and w are vertices, and A, B, and C are attribute names.

Optionally, in any of the preceding aspects, a further implementation of the aspect includes wherein the one or more processors execute the instructions to create work units for each graph pattern and graph pattern copy for each GFD rule, coordinate execution of the work units on multiple processors, share results from each processor in response to applying the rule associated with each work unit, and assign remaining work units in response to sharing results to the multiple processors.

Optionally, in any of the preceding aspects, a further implementation of the aspect includes wherein the one or more processors execute the instructions to upon determining the set of GFDs does not conflict, receive a new GFD rule and determine if the set of rules implies the new GFD rule.

Optionally, in any of the preceding aspects, a further implementation of the aspect includes wherein determining if the set of rules implies the new rule comprises enforcing GFDs on matches in the canonical graph one by one and terminating with true when either an equivalence relation is conflicting or when the implied attribute name is a part of the equivalence relation.

Optionally, in any of the preceding aspects, a further implementation of the aspect includes wherein the one or more processors execute the instructions to create a priority queue with work units, process the work units on different processors, and share changes with other processors.

According to one aspect of the present disclosure, a computer-readable media stores computer instructions for detecting errors in data, that when executed by one or more processors cause the one or more processors to perform operations comprising obtaining a set of GFDs representative of the data, building a canonical graph for the GFD rules, and determining that one or more GFD of the set of GFDs conflict based on the set of GFD rules and the canonical graph and, based thereon, determining an error in the set of GFDs.

Optionally, in any of the preceding aspects, a further implementation of the aspect includes wherein the canonical graph comprises a first graph pattern Q6and a second graph pattern Q7, wherein the canonical graph includes two distinct copies of the first graph pattern, and wherein the GFD rules include a first rule: φ7=Q6[x, y, z, w](Ø→x.A=0∧y.B=1), a second rule: φ9=Q6[x](y.B=1→w.C=1), and third rule: φ10=Q7[x](w.C=1→x.A=1), wherein x, y, z, and w are vertices, and A, B, and C are attribute names.

Optionally, in any of the preceding aspects, a further implementation of the aspect includes wherein the operations further comprise creating work units for each graph pattern and copy for each GFD rule, coordinating execution of the work units on multiple processors, sharing results from each processor in response to applying the rule associated with each work unit, and assigning remaining work units in response to sharing results to the multiple processors.

Optionally, in any of the preceding aspects, a further implementation of the aspect includes wherein the operations further comprise creating a priority queue with the work units, processing the work units on different processors, and sharing changes with other processors.

DETAILED DESCRIPTION

When receiving unstructured data, such as social media data or other data from non-relational database sources, there may be inconsistencies in the data, such as an object having a top speed, but the data reflecting two different top speeds for the same object, or a domain expert stating one thing as true, but a non-expert in the domain stating the same thing as false. In a relational database, functional dependencies are constraints between two sets of attributes in a relation. Conflicts may be found without much difficulty. However, unstructured data may be represented by graphs. It is difficult to determine inconsistencies or conflicts in data represented by graphs.

Several classes of graph dependencies have recently been proposed to extend functional dependencies (FDs) from relations to graphs, referred to as graph functional dependencies (GFDs). The need for GFDs is evident in inconsistency detection, knowledge acquisition, knowledge base enrichment, and spam detection, among other things.

There are two fundamental problems for GFDs. One is the satisfiability problem, to decide whether a set Σ of GFDs has a model, i.e., a nonempty graph that satisfies all GFDs in Σ. The other is the implication problem, to decide whether a GFD φ is entailed by a set Σ of GFDs, i.e., for any graph G, if G satisfies Σ then G satisfies φ. These are classical problems associated with any dependency class, known as the static analyses.

These problems, satisfiability and implication are coNP-complete and NP-complete, respectively. In various embodiments, errors in data, such as unstructured data, represented by GFDs are detected by using algorithms for detecting satisfiability and implication of the GFDs. Parallel algorithms for both are also provided.

The satisfiability analysis enables checking whether a set Σ of GFDs discovered from (possibly dirty) real-life graphs is “dirty” itself before it is used to detect errors and spam. The implication analysis eliminates redundant GFDs that are entailed by others. That is, the implication analysis provides us with an optimization strategy to speed up, e.g., error detection process.

No matter how important, these problems are hard for GFDs. For relational FDs, the satisfiability problem is trivial: any set of FDs can find a nonempty relation that satisfies the FDs. The implication problem is in linear time. In contrast, for GFDs, the satisfiability and implication problems are coNP-complete and NP-complete, respectively. GFDs on graphs are more complicated than FDs on relations. A GFD is a combination of a graph pattern Q, to identify entities in a graph, and an “attribute dependency” X→Y that is applied to the entities identified. Since graph pattern matching is NP-complete under the semantics of homomorphism, the static analyses of GFDs are inevitably intractable.

In one embodiment, a small model property: a set Σ of GFDs is satisfiable if and only if (iff) there exists a graph G such that G satisfies Σ and the size |G| of G is bounded by the size |Σ| of Σ. This allows inspecting graphs G of a bounded size as candidate models of E. Based on the small model property, a sequential (exact) algorithm referred to as SeqSat, is used to check GFD satisfiability.

A parallel algorithm ParSat, may also used to check GFD satisfiability for large sets of GFD, such a social media data. ParSat is parallel scalable relative to SeqSat: its parallel running time is in O(t(|Σ|)/p), where t(|Σ|) denotes the cost of SeqSat and p is the number of processors used. As a result, ParS at enables reduced running time when more processors are used. Hence it is feasible to scale with large sets of GFDs, Σ, by increasing p, despite the intractability of GFD satisfiability.

In a further embodiment, GFD implication checking is parallelized. A further small model property: to check whether a set Σ of GFDs implies another GFD φ, suffices to inspect graphs of size bounded by the sizes of φ and Σ, and enforce the GFDs of Σ on the small graphs. Based on this, a sequential exact algorithm SeqImp is used to check GFD implication. A ParImp algorithm is obtained by parallelizing SeqImp. ParImp is parallel scalable relative to SeqImp, allowing scaling with large sets Σ of GFDs.

Algorithms ParSat and ParImp use one or more techniques for parallel reasoning by using a combination of datapartitioned parallelism and pipelined parallelism for early termination of checking. Dynamic workload assignment and work unit splitting may be used to handle stragglers. A topological order on work units may be based on a dependency graph.

These algorithms provide tools for reasoning about GFDs, to validate data quality rules and optimize rule-based process for cleaning graph data, among other things.

A computer implemented method for detecting errors in data is first described, followed by a description of example GFDs and supporting information regarding sequential and parallel algorithms for determining satisfiability and implication to detecting errors in data represented by sets of graphs.

FIG. 1is a flowchart illustrating a computer implemented method100for detecting errors in data represented by graphs, such as directed graphs. Method100begins by the computer obtaining one or more graph functional dependency (GFD) rules at operation110and obtaining a set of GFDs at operation120representative of the data. The rules may contain one or more constraints, such as a vertices only having one value, or a value in one vertices implying a value in another vertices. The rules may be represented by edges between verticies in graph theory.

At operation130, a canonical graph (a graph having a notation that is common) is built for each GFD rule. One or more of the sets of GFDs is determined to conflict based on the GFD rules and the canonical graph at operation140. Based on the determination that a conflict exists, operation150determines that an error exists in the set of GFDs.

Once an error is determined, it is known that the set of graphs cannot be used for precise queries or possibly other data mining operations. A different set may then be tried until a set without errors is found. That set may be used for queries and other operations that benefit from known error free data.

The canonical graph includes an empty graph in one embodiment. A conflict is determined to exist when a literal is assigned two distinct constants as described in further detail below. The empty graph is populated by an Expand( ) operation prior to determining if any one of the GFDs conflicts iteratively for each rule. In one embodiment, the canonical graph comprises a first graph pattern Q6and a second graph pattern Q7, and also includes two distinct copies of the first graph pattern Q6.

The GFD rules in one embodiment, include a first rule: φ7=Q6[x, y, z, w](Ø→x.A=0∧y.B=1), a second rule: φ9=Q6[x] B=1→w.C=1), and third rule: φ10=Q7[x](w.C=1→x.A=1), wherein x, y, z, and w are vertices, and A, B, and C are attribute names.

In one embodiment, operation160includes receiving a new GFD rule, and operation170determines if the set of rules implies the new GFD rule. Operation170provides an efficient method of determining if the new GFD rule is satisfiable with the set of GFDs without having to start method100from the beginning.

FIG. 2is a flowchart illustrating a method200of determining if the set of rules implies a new rule. At operation210, GFDs are enforced on matches in the canonical graph one by one. The method is terminated at operation220with true in response to either an equivalence relation is conflicting or the implied attribute name is a part of the equivalence relation. The method is terminated with false at operation230when all GFDs are processed without terminating with true.

FIG. 3is a flowchart illustrating a method300of determining satisfiability of a set of GFDs utilizing parallel processing resources. At operation310, work units are created for each graph pattern for each GFD rule. A work unit is a set of candidate matches of a graph pattern to be checked as described in further detail below. Coordination of execution of each work unit on multiple processors is performed at operation320. At operation330, results from each processor are shared with other processors in response to applying the rule associated with each work unit. Remaining work units are assigned at operation340in response to sharing of the results to the multiple processors via operation330.

FIG. 4is a flowchart illustrating method400of implementing implication checking for a set of GFDs utilizing parallel processing resources. A priority queue with work units is created at operation410, and the work units are processed at operation420on different processors. At operation430, the results on each processor are shared with other processors.

The sequential and parallel algorithms for both satisfiability and implication are now described in further detail. Some definitions of terms notations are first provided. Assume two countably infinite alphabets Γ and θ for labels and attributes, respectively.

Directed graphs are defined as G=(V, E, L, FA), where (1) V is a finite set of vertices, also referred to as nodes; (2) E⊆V×V, in which (v, v′) denotes an edge from node v to v′; (3) each node v∈V is labeled L(v)∈Γ; similarly L(e) is defined for edge e∈E; and (4) for each node v, FA(v) is a tuple (A1=a1, . . . , An=an), where a is a constant, Ai∈θ is an attribute of v, written as v.Ai=ai, and Ai≠Ajif i≠j; the attributes carry content as in property graphs.

A graph (V′, E′, L′, F′A) is a subgraph of (V, E, L, FA) if V′⊆V, E′⊆E, for each node v∈V′, L′(v)=L(v) and F′A(v)=FA(v), and for each edge e∈E′, L′(e)=L(e).

A graph pattern is a graph Q[x]=(VQ, EQ, LQ), where (1) VQ(resp. EQ) is a finite set of pattern nodes (resp. edges); (2) LQis a function that assigns a label LQ(u) (resp. LQ(e)) to nodes u∈VQ(resp. edges e∈EQ); and (3)xis a list of distinct variables denoting nodes in V.

Labels LQ(u) and LQ(e) are taken from F and moreover, we allow LQ(u) and LQ(e) to be wildcard

A match of pattern Q[x] in a graph G is a homomorphism h from Q to G such that (a) for each node u∈VQ, LQ(u)=L(h(u)); and (b) for each edge e=(u, u′) in Q, e′=(h(u), h(u′)) is an edge in G and LQ(e)=L(e′). In particular, LQ(u)=L(h(u)) if LQ(u) is ‘_’, i.e., wildcard indicates generic entities and can match any label in F.

The match is denoted as a vector h(x) if it is clear from the context, where h(x) consists of h(x) for each x∈x. Intuitively,xis a list of entities to be identified by Q, and h(x) is such an instantiation in G, one node for each entity.

Graph functional dependencies are referred to as GFDs, from syntax to semantics.

A GFD φ is a pair Q[x](X→Y) [1], where

Q[x] is a graph pattern, called the pattern of φ; and

X and Y are two (possibly empty) sets of literals ofx.

A literal ofxis either x.A=c or x.A=y. B, where x and y are variables in x (denoting nodes in Q), A and B are attributes in θ (not specified in Q), and c is a constant.

GFD φ specifies two constraints: (a) a topological constraint Q, and (b) an attribute dependency X→Y. Pattern Q specifies the scope of the GFD: it identifies subgraphs of G on which X→Y is enforced. As observed in [2], attribute dependencies X→Y subsume relational EGDs and CFDs, in which FDs are a special case. In particular, literals x.A=c carry constant bindings along the same lines as CFDs [16]. Following [1], we refer to Q[x](X→Y) as graph functional dependencies (GFDs).

For a match h(x) of Q in a graph G and a literal x.A=c ofx, we say that h(x) satisfies the literal if there exists attribute A at the node v=h(x) and v.A=c; similarly for literal x.A=y.B. We denote by h(x)|=X if h(x) satisfies all the literals in X; similarly for h(x)|=Y.
h(x)|=X→Yifh(x)|=Ximpliesh(x)|=Y.

A graph G satisfies GFD φ, denoted by G|=φ, if for all matches h(x) of Q in G, h(x)|=X→Y.

Intuitively, G|=φ if for each match h(x) identified by Q, the attributes of the entities in h(x) satisfy X→Y.

Consider GFDs defined with patterns Q1, Q2, Q3, and Q4shown inFIGS. 5A, 5B, 5C, and 5Drespectively. These GFDs are able to catch semantic inconsistencies in real-life knowledge bases and social graphs. (1) GFD φ1=Q1[x, y](Ø→false). It states that for any place x510, if x is located in (edge512) another place y515, then y should not be part of (edge517) x. Here X is Ø, and Boolean constant false is a syntactic sugar for, e.g., x.A=c and x.A=d with distinct constants c and d. The GFD is defined with a cyclic pattern Q1.

In DBpedia, Bamburi_airport is located in city Bamburi, but at the same time, Bamburi is put as part of Bamburi airport. Hence DBpedia does not satisfy φ1, and the violation is caught by match h:xBamburi_airport and yBamburi of Q1. The inconsistency is detected by φ1.

(2) GFD φ2=Q2[x, y, z](Ø>y.val=z.val), where val is an attribute of y520and z525. It says that the topSpeed is a functional property, i.e., an object x530has at most one top speed. Note that x is labeled wildcard ‘_’, and may denote, e.g., car, plane.

The GFD catches the following error in DBpedia: tanks are associated with two topSpeed values, 24.076 and 33.336.

(3) GFD φ3=Q3[x, y, z, w](x.c=y.c→z.val=w.val), where c is an attribute of person x535and person y540indicating country, and val is an attribute of z545and w550indicating value, in this case, country as shown inFIG. 5C. The GFD states if person x535and person y540are the president and vice president of the same country as indicated by edges542and544, then x and y must have the same nationality. It catches the following inconsistency in DBpedia: the president and vice-president of Botswana have nationality Botswana and Tswana, respectively, while Tswana is ethnicity, not nationality

Graphs are considered in some embodiments that typically do not have a schema, as found in the real world. Hence a node v may not necessarily have a particular attribute. For a literal x.A=c in X, if h(x) has no attribute A, then h(x) trivially satisfies X→Y by the definition of h(x)|=X. In contrast, if x.A=c is in Y and h(x)|=Y, then h(x) must have attribute A by the definition of satisfaction; similarly for x.A=y.B.

In particular, if X is Ø, then h(x)|=X for any match h(x) of Q in G, and Y has to be enforced on h(x). In this case, if Y includes a literal x.A=c, then h(x) must carry attribute A. If Y=Ø, then Y is true, and φ is trivially satisfied.

The following notations may be used to describe the satisfiability problem for GFDs.

A model of a set of GFDs (E) is a (finite) graph G such that (a) G|=Σ, i.e., G satisfies all GFDs in Σ, and (b) for each GFD Q[x](X→Y) in Σ, there exists a match of Q in G.

Intuitively, if Σ has a model, then the GFDs in Σ are consistent, i.e., they do not conflict with each other, since all of them can be applied to the same graph. Σ is satisfiable iff Σ has a model. The satisfiability problem is to decide, given a set Σ of GFDs, whether Σ is satisfiable.

It is known that the problem is coNP-complete. However, there is no known way to develop a deterministic polynomial to check GFD satisfiability. In light of the absence of a deterministic polynomial, a small model property of the problem is established as described in further detail below. Based on the small model property, an exact algorithm for satisfiability checking is provided.

As opposed to relational FDs, a set Σ of GFDs may not be satisfiable. In fact, even if each GFD in Σ is satisfiable, Σ may not have a model, because the GFDs in Σ may interact with each other.

Consider two GFDs defined with the same pattern Q5600depicted inFIG. 6A: φ5=Q5[x](Ø→x.A=0) and φ6=Q5[x](Ø→x.A=1), where Q5600has a single node or vertices x602labeled ‘_’. No nonempty graph G satisfies both φ5and φ6. For if such G exists, φ5and φ6require h(x).A to be 0 and 1, respectively, which is impossible; here h(x) is a match of x.

GFDs defined with distinct patterns may also interact with each other. Consider GFDs: φ7=Q6[x, y, z, w](Ø→x.A=0∧y.B=1) and φ8=Q7[x, y, z, w](y.B=1→x.A=1), with Q6604and Q7630shown inFIGS. 6B and 6C. Q6604has a node x605labeled “a” with edges610,614,617having a label “p” coupled to nodes y620, z622, and w624with attribute values of b, b and c respectively. Q7630has the same structure as Q6604with attribute values for y, z, w, of b, c, c. One can easily see that each of φ7and φ8has a model. However, there exists no model G for both φ7and φ8. Indeed, if such G exists, then Q6604has a match h in G: h(x)v, h(y)vb, h(z)vz, h(w)vc. Hence φ7applies to the match and enforces vb.B=1. A match h′ of Q7in G can be given as h′(x)v, h′(y)vb, h′(z)vc, h′(w)vc, and φ8applies to the match since h′(x, y, z, w)|=h′(y).B=1. As a result, φ7and φ8require node v.A to be 1 and 0, respectively.

As shown by Example 2, while Q7630is not homomorphic to Q6604and vice versa, φ7and φ8can be enforced on the same node. Thus GFD satisfiability is nontrivial. It is shown coNP-hard by reduction from the complement of 3-colorability.

A Small Model Property

To find a model of a set Σ of GFDs, one cannot afford to enumerate all (infinitely many) finite graphs G and check whether G|=Σ. A small model property is established to reduce the search space.

A canonical graph GΣof Σ is defined to be (VΣ, EΣ, LΣ, FAΣ), where VΣis the union of Vi's, EΣis the union of Ei's, and LΣis the union of Li's; but (d) FAΣis empty. It is assumed without loss of generality (w.l.o.g.) that patterns in Σ are pairwise disjoint, i.e., their nodes are denoted by distinct variables by renaming.

Intuitively, GΣis the union of all graph patterns in Σ, in which patterns from different GFDs are disjoint. A wildcard _ of Q in GQis kept and treated as a “normal” label such that only _ in a pattern can match _ in G.

A population of GΣis a graph G=(VΣ, EΣ, LΣ, FA), where FAis a function that for each node v∈ VΣ, assigns FA(y)=(A1=a1, . . . , Am=am), a (finite) tuple of attributes from θ and their corresponding constant values.

Population G of GΣis said to be Σ-bounded if all attribute values in FAhave total size bounded by O(|Σ|), i.e., the values of all attributes in G are determined by Σ alone.

Intuitively, G and GΣhave the same topological structure and labels, and G extends GΣwith attributes and values. It is Σ-bounded if its size |G| is in O(|Σ|), including nodes, edges, attributes and all constant values in G.

Small model property. To check the satisfiability of Σ, it suffices to inspect Σ-bounded populations of the canonical graph GΣof Σ. A satisfiability checking algorithm is based on this small model property.

A set Σ of GFDs is satisfiable iff there exists a model G of Σ that is an Σ-bounded population of G.

If there exists an Σ-bounded population of GΣthat is a model of Σ, then obviously Σ is satisfiable. Conversely, if Σ has a model G, then there exists a homomorphism h from GΣto G. Employing h, a Σ-bounded population G′ of GΣis constructed. Attributes of G′ are populated by taking only relevant attributes from G, and by normalizing these attributes to make them Σ-bounded. The population preserves the constant values that appear in Σ and the equality on the attributes. G′|=Σ is shown by contradiction.

As an immediate corollary, an alternative proof is provided for the upper bound of the satisfiability problem for GFDs, instead of revising and using the chase.

The GFDs satisfiability problem is in coNP.

An NP algorithm is used to check whether a set Σ of GFDs is not satisfiable, as follows: (a) guess an Σ-bounded attribute population G of GsΣ, and a match hifor each pattern Qiof Σ in G; (b) check whether each himakes a match; if so, (c) check whether the matches violate any GFD in Σ in G. The correctness follows from Theorem 1. The algorithm is in NP since steps (b) and (c) are in PTIME (polynomial time). Thus the satisfiability problem is in coNP. G cannot be guessed as above and checked whether G|=Σ, since checking G|=Σ is already coNP-complete itself.

A Sequential Algorithm for Satisfiability

FIG. 7is a flowchart illustrating a computer executable exact algorithm SeqSat700for determining satisfiability of a set of GFDs. Based on the small model property, SeqSat700, takes as input a set Σ of GFDs, and returns true if and only if Σ is satisfiable as indicated at710. The set of GFDs Σ is received as input at operation720.

SeqSat700first, at operation725builds the canonical graph GΣ=(VΣ, EΣ, LΣ, FAΣ) of Σ. It then processes each GFD (rule) φ=Q[x](X→Y) in Σ and populates FAΣby invoking procedure Expand at operation730. Expand finds matches h(x) of Q in GsΣ, and checks whether h(x)|=X. If so, SeqSat700adds attributes x.A to FE and/or instantiates attributes x.A with constants for each literal x.A=c or x.A=y.B in Y, i.e., it “enforces” φ on the match h(x). If a conflict emerges as checked at operation735, i.e., if there exists x.A such that x.A is assigned two distinct constants, SeqSat700terminates with false at operation740. The process iterates as indicated by decision operation750until all GFDs in Σ are processed. If no conflict occurs, SeqSat700returns true at operation755.

Algorithm SeqSat700supports early termination. It terminates with false at operation740as soon as a conflict is detected. Moreover, when a match h(x) is found, it expands FAΣby enforcing φ at match h(x), instead of waiting until all matches of Q are in place.

The correctness of SeqSat700is assured by the following: (a) it suffices to inspect populations of GΣby Theorem 1, and (b) attributes are populated by enforcing GFD φ on each match h(x) of Q, which is necessary for any population of GΣto satisfy Σ, by the semantics of GFD satisfaction.

Equivalence class. To speedup checking, SeqSat700represents FΣas an equivalence relation Eq. For each node x∈VΣand each attribute A of x, its equivalence class, denoted by [x.A]Eq, is a set of attributes y.B and constants c, such that x.A=y.B and x.A=c are enforced by GFDs in Σ (see below). One can easily verify that Eq is reflexive, symmetric and transitive.

Given a GFD φ=Q[x](X→Y) in Σ, Expand generates matches h(x) of Q in GΣalong the same lines as VF2 [17] for subgraph isomorphism, except enforcing homomorphism rather than isomorphism. Then for each match h(x) found, Expand checks whether h(x)|=X. If so, it expands Eq by enforcing φ at h(x), with the following rules.

(Rule 1) If l is x.A=c, it checks whether [x.A]Eqdoes not yet exist in Eq. If so, it adds [x.A]Eqto Eq and c to [x.A]Eq. If [x.A]Eqhas a constant d≠c, it stops the process and SeqSat700terminates with false immediately.

(Rule 2) If l is x.A=y.B, it checks whether [x.A]Eqand [y.B]Eqare in Eq. If not, it adds the missing ones to Eq, and merges [x.A]Eqand [y.B]Eqinto one. If the merged class includes distinct constants, SeqSat700terminates with false. That is, Expand generates new attributes, instantiates and equalizes attributes as required for the satisfiability of GFDs.

There is a complication when checking h(x)|=X. For a literal x.A=c in X, x.A may not yet exist in FAΣor is not instantiated (i.e., [x.A]Eqdoes not include any constant). To cope with this, the following method may be used.

(a) Algorithm SeqSat700processes GFDs of the form Q[x](Ø→Y) first, if any in Σ. These add an initial batch of attributes.

(b) Expand maintains a list of matches h(x) and an inverted index with attribute h(x).A that appears in X, but either [h(x).A]Eqdoes not exist or is not instantiated. When h(x).A is instantiated in a later stage, h(x) is efficiently retrieved by the inverted index using h(x).A, and is checked again.

(c) At the end of the process of SeqSat700, some attribute x.A in Eq may still not be instantiated. The missing values do not affect the decision of SeqSat700on the satisfiability of Σ, since we can always complete Fiz, by assigning a distinct constant to each of such [x.A]Eq, without inflicting conflicts.

Consider Σ={(φ7, φ9, φ10}, where φ7is given in Example 2, φ9=Q6[x](y.B=1→w.C=1) and φ10=Q7[x](w.C=1→x.A=1), with Q6604and Q7630ofFIGS. 6B and 6C. Its canonical graph GΣis similar to the one given in Example 3, with Q7630and two distinct copies of Q6604(from φ7and φ9). Assume that SeqSat700checks ω7, φ10, φ9in this order.

(1) For φ7, Expand finds a match of Q6in GΣ: h(x)x, h(y)y, h(z)z, h(w)>w. Since h(x)|=Ø, it adds [x.A]Eq([y.B]Eq) to Eq and “0” (“1”) to [x.A]Eq([y.B]Eq).

(2) When processing φ10, Expand finds a match of Q7in GE: h′(x)x, h′(y)y, h′(z)w, h′(w)w. As [w.C]Eqis not in Eq, it adds (h′(x), φ10) to an inverted index with w.C.

(3) When processing φ9, Expand finds a match of Q6: h1(x)x, h1(y)y, h1(z)y, h1(w)w. It adds w.C to [y.B]Eq. This triggers re-checking of (h′(x), φ10) with the inverted index. Now h′(x)|=w.C=1. Expand adds “1” to [x.A]Eq, to enforce φ10. However, “0” is already in [x.A]Eq, a conflict. Hence SeqSat700stops and returns false.

Algorithm SeqSat700enforces GFDs of Σ by the semantics of GFDs. By Theorem 1, it returns true iff Σ has a model. One can verify that SeqSat700guarantees to converge at the same result no matter in what order the GFDs of Σ are applied, i.e., Church-Rosser, along the same lines as the characterization of GFD satisfiability. SeqSat700terminates early as soon as a conflict is spotted, and does not enumerate all matches by pruning to eliminate irrelevant matches early.

Algorithm SeqSat700is an exact algorithm. When Σ is large, SeqSat700may be costly due to the intractable nature of the satisfiability problem. A parallel algorithm, ParSat800, shown in pseudocode inFIG. 8A, is a parallelized algorithm for determining satisfiability of a set of graphs. ParSat800works with two procedures, HomMatch830inFIG. 8B, and CheckAttr850inFIG. 8C, both of which are shown in pseudocode form and are described in detail below.

A characterization of parallel algorithms is first described, followed by description of the parallel algorithm ParSat800with performance guarantees.

In general, a parallel algorithm for a problem may not necessarily reduce sequential running time. An algorithm Apfor GFD satisfiability checking is parallel scalable relative to sequential algorithm SeqSat700if its running time can be expressed as:

T⁡(Σ,p)=O⁢⁢(t⁡(Σ)p),
where t(|Σ|) denotes the cost of SeqSat700, and p is the number of processors employed by Apfor parallel computation.

Intuitively, a parallel scalable Aplinearly reduces the sequential cost of SeqSat700when p increases. By taking SeqSat700as a yardstick, Apguarantees to run faster when adding more processors, and hence scale with large Σ.

ParSat800is parallel scalable relative to SeqSat700. ParSat800makes use of both data partitioned parallelism and pipelined parallelism to speed up the process and facilitate interactions between GFDs. ParSat800provides dynamic workload balancing and work unit splitting, to handle stragglers, i.e., work units that take substantially longer than the others. ParSat800deduces a topological order on work units to reduce the impact of their interaction, based on a dependency graph, and retains the early termination property of SeqSat700.

FIG. 9is a block diagram illustrating a parallel processing system900for performing parallel satisfiability checking. ParSat800works with a coordinator Sc910and p workers (P1, . . . , Pp)915,916,917. A canonical graph GΣ920is replicated at each worker915,916,917, to reduce graph partition complication and communication costs. This is feasible since GΣ920is much smaller than real-life data graphs925such as social networks, which have billions of nodes and trillions of edges.

Work units: Consider a GFD φ=Q[x](X→Y). To simplify the discussion, assume w.l.o.g. that Q is connected. A node x∈xis designated as a pivot of Q. A work unit w of Σ is a pair (Q[z], φ), where z is a node in GΣthat matches the label of x. Intuitively, w indicates a set of candidate matches of Q to be checked.

A pivot x is used to explore the data locality of graph homomorphism: for any v in GE, if there exists a match h of Q in GΣsuch that h(x)=v, then h(x) consists of only nodes in the dQ-neighbor of v. Here dQis the radius of Q at v, i.e., the longest shortest path from v to any node in Q. The dQneighbor of v includes all nodes and edges within dQhops of v. Thus each candidate match v of x determines a work unit, namely, the dQ-neighbor of v, and the work units may be checked in parallel. Ideally, a pivot x is chosen that is selective, i.e., the pivot x, carries a label that does not occur often in GΣ; nonetheless, any node x inxcan serve as a pivot.

When Q is disconnected, a work unit is (Q[z], φ), wherezincludes a pivot for each connected component of Q.

ParSat800works as follows, with lines of pseudocode numbered and referenced as lines 1-11 inFIG. 8A:

Given Σ925, coordinator Sc910first (a) builds its canonical graph GΣ920and replicates GΣat each worker (line 1), and (b) constructs a priority queue W930of all work units of Σ (line 2), following a topological order based on a dependency graph of Σ (see details below). Coordinator Sc910then activates each worker Piwith one work unit w from the front of W (line 3). In fact, work units can be assigned to worker in a small batch rather than a single w, to reduce the communication cost.

The coordinator910then interacts with workers and dynamically assigns workload, starting from the units of W with the highest priority (lines 4-10). A worker Pimay send two flags to Sc: (a) ficif Pidetects a conflict when expanding equivalence relation Eq; and (b) fidif Piis done with its work unit. If coordinator Sc910receives ficfor any i∈[1, p], ParSat800terminates immediately with false (lines 5-6). If coordinator Sc910receives fid, it assigns the next unit w′ in W to Piand removes w′ from W (lines 7-8). The process iterates until either a conflict is detected, or W becomes empty, i.e., all work units have been processed. At this point algorithm ParSat800concludes that Σ is satisfiable and returns true (line 11).

A worker may split its unit w into a list Liof sub-units if w is a straggler as illustrated at1000inFIG. 10. Upon receiving Li, coordinator Sc910adds Lito the front of the priority queue W (lines 9-10). Putting these together, ParSat800implements data partitioned parallelism (by distributing work units of W), dynamic workload assignment, and early termination.

Each worker Pi915maintains the following: (a) local canonical graph GΣ920in which an equivalence relation Eqirepresents its local FAΣ, and (b) a buffer ΔEqi940that receives and stores updates to Eqifrom other workers. It processes its work unit w locally and interacts with coordinator Scand other workers asynchronously as follows.

Upon receiving a work unit (Q[z], φ), Pi915conducts local checking in the dQ-neighbor of z. This suffices to find matches h(x) of Q in GΣwhen the pivot x of Q is mapped to z, by the data locality of graph homomorphism.

Algorithm ParSat800implements Expand with two procedures: (i) HomMatch830finds matches h(x) of Q in GΣpivoted at z, and (ii) CheckAttr850expands Eq, by enforcing φ at match h(x) based on two expansion rules. ParSat800differs from Expand in the following. Each procedure has lines identified with consecutive line numbers referred to below.

The two procedures work in pipeline: as soon as a match h(x) is generated by HomMatch830, CheckAttr850is triggered to check h(x) in a different thread, instead of waiting for all matches of Q to be found (lines 2-3 of HomMatch830).

If a conflict emerges, i.e., if some class [y.B]Eqi(2)includes distinct constants, worker Pisends flag ficto coordinator Sc and terminates the process (line 4). After all matches of Q pivoted at z are processed, Pisends flag fidto Sc(line 9).

Like procedure Expand, CheckAttr850also maintains an inverted index on matches h(x) that need to be re-checked upon the availability of (instantiated) attributes needed.

Worker Pibroadcasts its local changes ΔEqito other workers (line 5). It keeps receiving changes ΔEqifrom other processors and updates its local Eqiby CheckAttr850. The communication is asynchronous, i.e., there is no need to coordinate the exchange through Sc. This does not affect the correctness of ParSat800since equivalence relation Eq is monotonically expanding, and a conflict ficterminates the process no matter at which worker ficemerges.

Recall Σ={φ7, φ9, φ10} from Example 4. Its canonical graph GΣincludes two copies of Q6[x, y, z, w] and a copy of Q7[x, y, z, w], in which variable x (designated as a pivot) in the three patterns is renamed as x1, x2, x3, respectively; similarly for variables y, z, w.

ParSat800works with coordinator Sc and two workers P1and P2. ParSat800first creates a priority queue W, where W has 9 work units wi=(Q6[xi], φ7), w3+i=(Q6[xi], φ9) and w6+i=(Q7[xi], φ10) in this order, for i∈[1, 3] (see Example 7). Then Scsends w1to P1and w2to P2. It then dynamically assigns the remaining units to P1and P2one by one following the order of W, upon receiving fjdfor j∈[1, 2].

Parallel checking may be sped up in at least two ways, unit splitting, and by the use of a dependency graph.

A work unit w=(Q[z],φ) assigned to a worker Pimay become a straggler and is “skewed”. ParSat800handles stragglers as follows. Recall that matching dominates the cost of w, and HomMatch830computes matches via backtracking like in VF2. When HomMatch830is triggered, it starts keeping track of the time τ spent on w. If τ exceeds a threshold TTL, it picks a set Liof partial match h(y) of Q, i.e.,yis a proper sub-listx. It treats (Q[y], φ) as a work unit, and sends Lito Sc(lines 6-7). Worker Piresets τ=0 and continues with the remaining work of w excluding those in Li(line 8).

Coordinator Scadds Lito the front of W, and distributes the units to workers as usual. Upon receiving such (Q[w],φ), worker Pjresumes the checking from Q[w].

Consider a work unit w=(Q[u11],φ), where φ=Q[x, y, z](X→Y), in which x is pivoted at u11. Suppose that at one point, HomMatch830finds a match h(x, y, z): xu11, yu21and zu32as shown inFIG. 10at1000, and the time spent on w has exceeded TTL. Hence HomMatch830decides to split w. It creates a list Liconsisting of wj=(Q[u11, u2j],φ) for j∈[2, m], where wjcorresponds to a partial match hi[x, y]: xu11and yu2i, and it does not include match for z; here partial matches hiare found by backtracking one step. HomMatch830sends Lito Sc, restarts counter τ and continues to complete the processing of the current match h(x, y, z), to process, e.g., matches in which z ranges over u32and u33.

Upon receiving Li, coordinator Sc910adds its units to the front of the priority queue and assigns them to available workers as usual. When, e.g., wjis sent to a worker Pk, Pkresumes the processing of w1starting from partial match hi[x, y].

A priority queue W of work units is built as indicated at line 2 of ParSat800. A dependency graph Gd=(V,E), is constructed, where V is the set of work units, and (w1,w2) is a directed edge if (a) there exists an attribute x.A that appears in both Y1and X2, where w1=(Q1[z1],ϕ1), w2=(Q2[x2], ϕ2), ϕ1=Q1[x1](X1→Y1), ϕ2=Q2[x2](X2→Y2), i.e., the antecedent X2of ϕ2, may depend on the consequence Y1of ϕ1; and (b) z2is within dQ1hops of z1, i.e., the two pivots are close enough to interact.

ParSat800deduces a topological order from Gdand sorts W accordingly. Note that work units for GFDs Q[x](Ø→Y) are at the front of queue W, with the highest priority.

For the 9 work units of Example 5, the dependency graph Gdis depicted inFIG. 11at1100. There exists an edge (w1,w4) since w1and w4are both pivoted at x1, w1carries φ7=Q6[x, y, z, w](Ø→x.A=0∧y.B=1), w4carries φ9=Q6[w](y.B=1→w.C=1), and y.B is in both the consequence of φ7and the antecedent of φ9; similarly for other edges inFIG. 11. In contrast, there is no edge between w2and w4since their pivots are not close, although they also carry φ7and φ9, respectively. From Gda topological order is deduced, to sort the work units of Example 5.

As another optimization strategy, ParSat800also extracts common sub-patterns that appear in multiple GFDs of Σ, finds matches of the sub-patterns at common pivots early, and reuses the matches when processing relevant GFDs. This is a common practice of multi-query optimization. To avoid the complexity of finding common sub-patterns, following, graph simulation is used to check whether a pattern Q1is homomorphic to a sub-pattern Q2′ of Q2. If Q1does not match Q2′ by simulation, then Q1is not homomorphic to Q2′. Since graph simulation is in O(|Q1|·|Q2′|) time, this method reduces the (possibly exponential) cost of checking homomorphism.

The correctness of ParS at800is warranted by Theorem 1 and the fact that equivalence relation Eq is monotonically increasing, similar to the inflational semantics of fixpoint computation. ParSat800parallelizes SeqSat700, and is parallel scalable relative to SeqSat700by dynamic work unit assignment to balance workload, and work unit splitting to handle stragglers. One can verify by induction on the number of work units that the parallel runtime of ParSat800is in

O⁢⁢(t⁡(Σ)p),
where t(|Σ|) denotes the cost of SeqSat700.

Implication checking may also be performed in a serial or parallel manner A set Σ of GFDs implies another GFD φ, denoted by Σ|=φ, if for all graphs G, if G|=Σ then G|=φ.

The implication problem for GFDs is to decide, given a finite set Σ of GFDs and another GFD φ, whether Σ|=φ. A small model property of the implication problem is used in one embodiment. Capitalizing on the small model property, a sequential exact algorithm SeqImp is used to perform implication checking. SeqImp may be parallelized to provide a parallel scalable algorithm ParImp.

A Small Model Property of GFD Implication

For traditional FDs over relations, the implication analysis takes linear time. When it comes to GFDs, however, the story is more complicated.

Now consider φ14=Q7[x](x.A=0→z.C=2). Again, one can verify that Σ|=φ14. This is because for any graph G and any match h(x) of Q7in G, if G|=Σ then h(x)|≠h(x).A=0, since φ11enforces h(x).A=0. That is, Q7, x.A=0 and Σ are “inconsistent” when put together.

The implication problem may be derived by proving a small model property. This is more involved than its counterpart for satisfiability. Notations include the following.

Consider φ=Q[x](X→Y), where Q=(VQ, EQ, LQ). The canonical graph of φ is GQX=(VQ, EQ, LQ, FAX), where FAXis defined as follows. For each node x∈VQ(i.e., each x∈x), (a) if x.A=c is in X, then FAX(x) has attribute A with x.A=c; (b) if x.A=y.B is in X, then FAX(x) has attributes A and B such that x.A=y.B; and moreover, (c) FAXis closed under the transitivity of equality, i.e., if x.A=y.B and y.B=z.C, then x.A=z.C; similarly if x.A=c and z.C=c, then x.A=z.C.

A wildcard _ of Q is kept in GQjust like in GΣ. A (Σ,φ)-bounded population of GQXfor canonical graph GQXof φ as a population of GQXsuch that its size is in O(|E|+|φ|) is defined. To check whether Σ|=φ, it suffices to populate the canonical graph GQX.

For any set Σ of GFDs and GFD φ=Q[x](X→Y), Σ|=φ iff for all (Σ,φ)-bounded populations G of GQX, either (a) G|≠Σ, or (b) G|=Σ and G|=φ.

If Σ|=φ, then for all graphs G, if G|=Σ then G|=φ. These graphs include (Σ,φ)-bounded populations of GQX. From this it follows that conditions (a) and (b) hold.

Conversely, assume that Σ|≠φ, i.e., there exists a graph G such that G|=Σ but G|≠φ. A (Σ, φ)-bounded population G′ of GQXis constructed such that G′|=Σ but G′|≠φ, violating conditions (a) and (b). The construction makes use of the “witness” of G|≠φ (the match of the pattern of in G that violates φ), and requires attribute value normalization as in the proof of Theorem 1, such that the total size of attributes in G are in O(|E|+|φ|) (see [15] for details).

To check whether Σ|=φ, Theorem 3 allows inspection of (Σ,φ)-bounded populations G of GQXonly. However, all such small graphs are checked, exponentially many in total. To further reduce the search space, a corollary of Theorem 3 is proven.

Notations are provided. Recall equivalence class Eq representing FAΣ. Given a GFD ϕ=Q′[x′](X′→Y′) in Σ and a match h′ of Q′ in GQX, Eq can be expanded by enforcing ϕ at h′ with the two rules.

A list H of such pairs (h′, ϕ) is referred to as a partial enforcement of Σ on GQX. EqHis used to denote the expansion of Eq by H, by enforcing ϕ at h′ one by one.

EqHis conflicting if there exists [x.A]EqHthat includes distinct constants c and d. Intuitively, this means that the GFDs in H and Q, X are inconsistent.

Recall that φ=Q[x](X→Y). Y⊆EqHis written if for any literal u=v, v∈[u]EqHwhere u=v is either x.A=c or x.A=y.B. That is, the literal can be deduced from the equivalence relation EqHvia the transitivity of equality.

For any set Σ of GFDs and φ=Q[x](X→Y), Σ|=φ iff there exists a partial enforcement H of Σ on GQXsuch that either EqHis conflicting, or Y⊆EqH. The two cases of Corollary 4 are illustrated in Example 8.

If Σ|=φ, then such an H exists by Theorem 3, since each EqHis a (Σ,φ)-bounded population of GQX.

Conversely, the following is shown by induction on the length of H. (1) If EqHis conflicting, then for all (Σ,φ)-bounded populations G of GQX. G|≠Σ. (2) If Y⊆EqH, then for all (Σ,φ)-bounded populations G of GQX, if G|=Σ, then G|=φ. From this and Theorem 3 it follows that Σ|=φ.

Corollary 4 allows checking of Σ|=φ by selectively inspecting H, instead of enumerating all (Σ,φ)-bounded populations. Leveraging Corollary 4, the following is verified along the same lines as the proof of Corollary 2.

The GFD implication problem is in NP.

Sequential Algorithm for Implication

Capitalizing on Corollary 4, an exact sequential algorithm, SeqImp, for checking GFD implication is provided.

SeqImp takes as input a set Σ of GFDs and another GFD φ. It returns true if Σ|=φ, and false otherwise. Let φ=Q[x](X→Y). Similar to SeqSat700for satisfiability checking, algorithm SeqImp enforces GFDs of Σ on matches of Q in the canonical graph GQXone by one, and terminates as soon as Σ|=φ can be decided. It has the following subtle differences from SeqImp.

(a) In contrast to SeqSat700that starts with Eq initially empty, SeqImp uses EqHto represent partial enforcement, initialized as EqX, the (nonempty) equivalence relation encoding FAX.

(b) SeqImp terminates with true when either (i) EqHis conflicting, or (ii) Y⊆EqH. It terminates with false when all GFDs are processed, if neither conflict is detected nor YEqHin the entire process, concluding that Σ|≠φ.

Now for φ14. SeqImp starts with FAX′={x.A=0}. After enforcing φ11at h(x) it adds “1” to [x.A]Eq, a conflict with [x.A]Eq={0}. Hence SeqImp returns true and terminates.

The correctness of SeqImp follows from Corollary 4. Its complexity is dominated by generating matches of graph patterns in Σ, while Y⊆EqHand conflicts in EqHcan be checked efficiently. In particular, the equivalence relation EqHcan be computed in linear time with index. Moreover, one can verify that the length of EqHis bounded by |Q|·|Σ|.

Algorithm ParImp is a parallel scalable relative to SeqImp. Hence ParImp is capable of dealing with large set Σ of GFDs by adding processors as needed. ParImp works with a coordinator Scand p workers (P1, . . . , Pp), like ParS at800. It first constructs the canonical graph GQXof φ, initializes EqHas EqX, and replicates GQXand EqHat each worker.

EqHis expanded in parallel by distributing work units across p workers. A work unit (Qϕ[z],ϕ) is defined in the same way as previously described for GFDs ϕ=Qϕ[xϕ](Xϕ→Yϕ) in Σ at pivots z in GQX. The work units are organized in a priority queue W as before, based on a revised notion of dependency graph (see below). Algorithm ParImp dynamically assigns work units of W to workers, starting with the ones with the highest priority, in small batches. Workers process their assigned work units in parallel, broadcast their local EqHexpansions to other workers, and send flags to Sc. The process proceeds until (a) either at a partial enforcement H of G at some worker, EqHhas conflict or Y⊆EqH, or (b) all work units in W have been examined. The process returns true in case (a), and false in case (b), by Corollary 4.

ParImp employs the same dynamic workload assignment and unit splitting strategies of ParS at800to handle stragglers. ParImp also supports a combination of data partitioned parallelism and pipelined parallelism. It differs from ParSat800in the following.

ParImp deduces a topological order on W also based on the dependency graph of work units. The only difference is that a unit (Qϕ[z],ϕ) is associated with the highest priority if ϕ=Qϕ[xϕ](Xϕ→Yϕ) and X subsumes Xϕ, i.e., each literal in Xϕcan be deduced from EqX.

Each worker Pisends flag ficto coordinator if either (i) a conflict is detected in its local copy of EqH, or (ii) Y⊆EqH. Upon receiving fic, algorithm ParImp terminates immediately with true, regardless of what Piis.

Now consider φ14instead of φ13. ParImp creates priority queue W=[w1=(Q9[x], φ12), w2=(Q8[x],φ11)]. Note that W is different from the queue for φ13, since the initial EqHincludes [x.A]EqH={0}. Coordinator Scsends w1to P1and w2to P2. When P2enforces φ11on match h′(x) it adds “1” to [x.A]Eq(H,2), but “0” is already in [x.A]Eq(H,2). Thus P2sends f2cto Scand ParImp stops with true.

The correctness of ParImp is assured by Corollary 4 and monotonic expansion of EqH. ParImp is parallel scalable relative to SeqImp by dynamic workload balancing and unit splitting. Formally, one can show that ParSat800takes

O⁢⁢(t⁢⁢(Σ,φ)p)
time with p workers, where t(|Σ|,|φ|) is the cost of SeqImp, by induction on the number of work units.

FIG. 12is a block diagram illustrating circuitry for executing one or more of the sequential and parallel satisfiability and implication algorithms and for performing methods according to example embodiments. All components need not be used in various embodiments.

One example computing device in the form of a computer1200may include a processing unit1202, memory1203, removable storage1210, and non-removable storage1212. Although the example computing device is illustrated and described as computer1200, the computing device may be in different forms in different embodiments. For example, the computing device may instead be a smartphone, a tablet, smartwatch, or other computing device including the same or similar elements as illustrated and described with regard toFIG. 12. Devices, such as smartphones, tablets, and smartwatches, are generally collectively referred to as mobile devices or user equipment. Further, although the various data storage elements are illustrated as part of the computer1200, the storage may also or alternatively include cloud-based storage accessible via a network, such as the Internet or server-based storage.

Memory1203may include volatile memory1214and non-volatile memory1208. Computer1200may include—or have access to a computing environment that includes—a variety of computer-readable media, such as volatile memory1214and non-volatile memory1208, removable storage1210and non-removable storage1212. Computer storage includes random access memory (RAM), read only memory (ROM), erasable programmable read-only memory (EPROM) or electrically erasable programmable read-only memory (EEPROM), flash memory or other memory technologies, compact disc read-only memory (CD ROM), Digital Versatile Disks (DVD) or other optical disk storage, magnetic cassettes, magnetic tape, magnetic disk storage or other magnetic storage devices, or any other medium capable of storing computer-readable instructions.

Computer1200may include or have access to a computing environment that includes input interface1206, output interface1204, and a communication interface1216. Output interface1204may include a display device, such as a touchscreen, that also may serve as an input device. The input interface1206may include one or more of a touchscreen, touchpad, mouse, keyboard, camera, one or more device-specific buttons, one or more sensors integrated within or coupled via wired or wireless data connections to the computer1200, and other input devices.

The computer may operate in a networked environment using a communication connection to connect to one or more remote computers, such as database servers. The remote computer may include a personal computer (PC), server, router, network PC, a peer device or other common DFD network switch, or the like. The communication connection may include a Local Area Network (LAN), a Wide Area Network (WAN), cellular, WiFi, Bluetooth, or other networks. According to one embodiment, the various components of computer1200are connected with a system bus1220.

Computer-readable instructions stored on a computer-readable medium are executable by the processing unit1202of the computer1200, such as a program1218. The program1218in some embodiments comprises software that, when executed by the processing unit1202, performs operations according to any of the embodiments included herein. A hard drive, CD-ROM, and RAM are some examples of articles including a non-transitory computer-readable medium such as a storage device. The terms computer-readable medium and storage device do not include carrier waves to the extent carrier waves are deemed too transitory. Storage can also include networked storage, such as a storage area network (SAN). Computer program1218may be used to cause processing unit1202to perform one or more methods or algorithms described herein.