An -partition of a finite undirected simple graph is a labeling of 's vertices such that the constraints expressed by the model graph are satisfied. These constraints concern the adjacency or nonadjacency of vertices depending on their label. For every model graph , it can be decided in non-deterministic polynomial time whether a given input graph admits an -partition. Moreover, it has been shown in [1] that for most model graphs, this decision problem is in deterministic polynomial time. In this paper, we show that these polynomialtime algorithms for finding -partitions can be expressed in Datalog with stratified negation. Moreover, using the answer set solver Clingo [2, 3], we have conducted experiments to compare straightforward guess-and-check programs with Datalog programs. Our experiments indicate that in Clingo, guess-and-check programs run faster than their equivalent Datalog programs.
We will test this scenario on the problem of finding -partitions in undirected graphs [1]. All undirected graphs in this paper are understood to be finite and simple. Given an undirected graph , this problem consists in deciding whether there exists a partition of ’s vertices such that this partition respects some constraints encoded in another graph with exactly four vertices, called model graph. Each class of the partition is labeled by a vertex in . There are two types of constraints: • if contains a full edge between two vertices, and , then each vertex in the class labeled by must be adjacent to each vertex in the class labeled by ; and • if contains a dotted edge between two vertices, and , then each vertex in the class labeled by must be nonadjacent to each vertex in the class labeled by .
Note that there are no constraints between two vertices in the same class. All possible model graphs, up to isomorphism, are presented in Figures 1 and 2. The -partitioning problem for 2 + 2, also known as finding a skew partition, is in polynomial time [ 5, 6]. The -partitioning problem for 22 is NP-complete [7]. For each model graph in Figure 2, Dantas et al. [1] provide a polynomial-time algorithm, of low polynomial degree, for deciding whether an undirected graph admits an -partition. In this paper, we show how these polynomial-time algorithms can be encoded in Datalog with stratified negation. We then experimentally compare these Datalog programs with a guess-and-check ASP program. In theory, the computational complexity of Datalog is in P, while guess-and-check ASP programs can solve NP-complete problems.
This paper is organized as follows. Section 2 formalizes the problem of finding -partitions and paraphrases the polynomial-time method of Dantas et al. [1]. Sections 3 and 4 focus on finding partitions in logic programming, first in ASP, and then in Datalog with stratified negation. In our experimental validation of Section 5, we first generate undirected graphs of diferent sizes on which our programs can be executed. We distinguish between those input graphs that admit an -partition, called yes-instances, and those that do not, called no-instances. We show diferent methods for generating yes-instances and no-instances, for a fixed model graph , and then compare the running times of our logic programs in the answer set solver Clingo [2, 3]. Finally, Section 6 concludes the paper. Due to space limitations, some proofs have been omitted, which can be found in the extended version [8].
In this section, we formally define the problem H-PARTITION and sketch an algorithm borrowed from [1]. In Section 4, this algorithm will be written in Datalog with stratified negation.
A model graph is an undirected graph with four vertices, called , , and (sometimes written in lowercase letters). The vertices are called , , , and in anticlockwise order, starting with the top-left vertex. Every edge is of exactly one of two types: full or dotted. All possible model graphs, up to isomorphisms, are presented in Figures 1 and 2. We define H-PARTITION as the following decision problem.
Question: Is it possible to partition () into four pairwise disjoint, non-empty subsets, , , , and such that, for all , ∈ {, , , } with ̸= : • if (, ) is a full edge of , then every vertex in is adjacent to every vertex in ; and • if (, ) is a dotted edge of , then every vertex in is nonadjacent to every vertex in .
We call a pair (, ) a yes-instance if H-PARTITION returns yes on input and ; otherwise (, ) is a no-instance. H-PARTITION() denotes the H-PARTITION problem for a fixed model graph .
The partitions , , , and are commonly denoted by , , , and , respectively. One can view such a partition of () as a labeling of () with the labels , , , and . From here on, we will often omit curly braces and commas in the denotation of subsets of {, , , }. For example, denotes the set {, , }.
Definition 1. This definition is relative to a fixed model graph . Let ⊆ { , , , }. We define NF() as the set of vertices of that are adjacent, through a full edge, to some vertex of . Similarly, ND() is the set of vertices of that are adjacent, through a dotted edge, to some vertex of . We say that is trivial if || = 1.
Informally, given a model graph , each label among , , , and imposes a constraint that can be read from . For example, for the model graph = (19) given in Figure 2, the label imposes “being adjacent to and nonadjacent to ,” and imposes “being adjacent to and nonadjacent to .” A list of two or more labels imposes all the constraints of each label in the list. For example, for = (19), the list imposes “being adjacent to , nonadjacent to , adjacent to , and nonadjacent to .” A list is called conflicting if it imposes an unsatisfiable constraint. For example, for = (20), the list is conflicting, because imposes “being nonadjacent to ,” while imposes “being adjacent to .” We will call a list non-maximal1 if it can be extended into a longer list that imposes the same constraint. For
example, for = (33), the lists and impose the same constraint, namely “being adjacent to , nonadjacent to , and nonadjacent to ,” and therefore is non-maximal.
Definition 2. This definition is relative to a fixed model graph . Let ⊆ { , , , }. is conflicting if NF() ∩ ND() ̸= ∅. is non-maximal if there exists ′ ⊆ { , , , } such that ⊊ ′ with NF() = NF(′) and ND() = ND(′).
For example, let be model graph (13) of Figure 2. The list is non-maximal because for the set , we have that NF() = = NF() and ND() = = ND(). The list is conflicting because ∈ ND() ∩ NF().
Dantas et al. [1] have shown that H-PARTITION() is in polynomial time for all model graphs in Figure 2. Our algorithmic approach slightly difers from theirs because, unlike [ 1], we will not use non-maximal or conflicting lists. We now describe our approach.
Definition 3. Let be a model graph, and an undirected graph. Let , , , and be four distinct vertices of . We say that the quadruplet (, , , ) is -isomorphic if the subgraph of induced by these vertices is a yes-instance of H-PARTITION() for a labeling where , , , and are respectively labeled by , , , and .
For instance, in the graph of Figure 3a, the quadruplet (
Our algorithmic approach loops over all -isomorphic quadruplets (, , , ). Each such quadruplet yields an initial partial labeling. Given such an initial partial labeling, we test whether it can be extended into a complete labeling, i.e., into a solution. To this end, we repeatedly pick an unlabeled vertex, and compute its possible labels. When we say that a label ∈ {, , , } is possible for a vertex, we mean that the model graph does not forbid us to label that vertex with , given the vertices that have already been labeled. If only one label is possible for an unlabeled vertex, we label that vertex with that label. If no label is possible for some unlabeled vertex, we conclude that the current labeling cannot be extended to a complete labeling. If for every unlabeled vertex at least two labels remain possible, then we conclude that is a yes-instance for H-PARTITION() (except for model graphs (7), (10) and (11) where some additional tests are needed).
In [1], refined lists are obtained by removing conflicting and non-maximal lists. The description on [DdFGK05, page 141] might suggest that we must be careful to only consider refined lists. However, the following lemma implies that conflicting or non-maximal lists will not occur in our algorithmic approach.
Lemma 1. Let be a model graph, and an undirected graph. Assume that, during the execution of the previously described algorithm for H-PARTITION() with input , there is a vertex ∈ () whose set of all possible labels is with || ⩾ 2. Then, is neither conflicting nor non-maximal.
In Section 4, we show how to encode our algorithmic approach in Datalog with stratified negation. However, we will first provide a straightforward guess-and-check program for H-PARTITION.
In all logic programs of this paper, the constants are in lowercase and the variables are in uppercase to match with Clingo syntax. We use the binary predicate e to store the edges of the input graph , while the unary predicate vertex stores vertices. The binary predicates full and dotted encode, respectively, full and dotted edges of the model graph. The labels are provided to the program as partition(a), partition(b), partition(c), and partition(d).
The following program follows the generate-and-test (or guess-and-check) methodology that is classical for problems in NP: generate a candidate solution, and test whether it is a true solution, i.e., whether it satisfies all constraints. In the following program, the generating part is the rule 1 { placedIn(X,P) : partition(P) } 1 :- vertex(X)., which places every vertex in exactly one partition. The testing part imposes that every partition must contain at least one vertex, and that the constraints of the model graph must be satisfied. Moreover, we suppose that e is symmetric, i.e., e(t,s) is stored whenever e(s,t) is stored. % Every vertex goes in exactly one partition. 1 { placedIn(X,P) : partition(P) } 1 :- vertex(X). % No partition is empty. filled(P) :- placedIn(X,P). :- partition(P), not filled(P). % Constraints of the model graph. :- placedIn(X,P), placedIn(Y,Q), full(P,Q), not e(X,Y). :- placedIn(X,P), placedIn(Y,Q), dotted(P,Q), e(X,Y).
In this section, we show how to encode H-PARTITION() in Datalog with stratified negation, for model graphs in Figure 2. Section 4.1 encodes the approach of [1] in general. We argue that this general encoding is correct for every model graph in Figure 2 that is distinct from (7), (10), and (11). We then show how to adjust the general encoding for these three model graphs. Finally, we show that for model graphs with an isolated vertex, non-recursive Datalog with negation sufices to check the existence of -partitions.
Dantas et al. [1] showed that H-PARTITION() can be solved in polynomial time for all model graphs in Figure 2. Following our previously described method, we check whether some initial valid labeling of four vertices, called a base, can be extended to a complete labeling of all vertices. Finding a base. The algorithm loops over all quadruplets of distinct vertices and checks whether a quadruplet is -isomorphic. Our Datalog rules are as follows: base(X,Y,Z,T) :- distinct(X,Y,Z,T), not problematic_base(X,Y,Z,T).
Here, the predicate distinct(X,Y,Z,T) checks whether , , , and are four distinct vertices of , and problematic_base is defined, for each possible edge in the model graph , with two rules. For example, if we consider the edge (, ), the rules are: problematic_base(X,Y,Z,T) :- dotted(a,b), e(X,Y), vertex(Z), vertex(T). problematic_base(X,Y,Z,T) :- full(a,b), not e(X,Y), vertex(X), vertex(Y), vertex(Z), vertex(T). Similar rules are added for edges (, ), (, ), (, ), (, ), and (, ). inPart(I,a,I,J,K,L) :- base(I,J,K,L). inPart(J,b,I,J,K,L) :- base(I,J,K,L). inPart(K,c,I,J,K,L) :- base(I,J,K,L). inPart(L,d,I,J,K,L) :- base(I,J,K,L).
We keep track that a vertex that has been labeled in a base must not be re-labeled later on. Extension to a complete labeling. First, for every base (, , , ) of four vertices, we label with , with , with , and with .
Next, rather than computing the set of possible labels for a yet unlabeled vertex , we use the predicate imp(X,P,I,J,K,L) with the meaning that the vertex cannot be labeled by ∈ {, , , }, relative to the fixed base (, , , ). The Datalog rules are straightforward. The second rule, for example, expresses that for a full edge (, ) in the model graph, if a vertex has been labeled with , then a vertex that is nonadjacent to cannot be labeled with . One should read “prob” as a shorthand for “problematic.” imp(X,P,I,J,K,L) :- vertex(X), full_prob(X,P,I,J,K,L), not done(X,I,J,K,L). full_prob(X,P,I,J,K,L) :- full(P,Q), inPart(Y,Q,I,J,K,L), not e(X,Y), vertex(X). imp(X,P,I,J,K,L) :- vertex(X), dot_prob(X,P,I,J,K,L), not done(X,I,J,K,L). dot_prob(X,P,I,J,K,L) :- dotted(P,Q), inPart(Y,Q,I,J,K,L), e(X,Y).
For every vertex of that is not in the fixed base (, , , ), we now consider two possibilities:
(
Finally, if some base never encounters the second case, the answer to H-PARTITION() is “yes”; otherwise the answer is “no”. Note incidentally that in a “yes”-instance, there may be vertices that are not labeled by the first case. % First case. inPart(X,a,I,J,K,L) :- imp(X,b,I,J,K,L), imp(X,c,I,J,K,L), imp(X,d,I,J,K,L). inPart(X,b,I,J,K,L) :- imp(X,a,I,J,K,L), imp(X,c,I,J,K,L), imp(X,d,I,J,K,L). inPart(X,c,I,J,K,L) :- imp(X,a,I,J,K,L), imp(X,b,I,J,K,L), imp(X,d,I,J,K,L). inPart(X,d,I,J,K,L) :- imp(X,a,I,J,K,L), imp(X,b,I,J,K,L), imp(X,c,I,J,K,L). % Second case. bad_init(I,J,K,L) :- vertex(X), base(I,J,K,L), imp(X,a,I,J,K,L),
imp(X,b,I,J,K,L), imp(X,c,I,J,K,L), imp(X,d,I,J,K,L). yes_instance() :- base(I,J,K,L), not bad_init(I,J,K,L). no_instance() :- not yes_instance().
We have the following result.
Theorem 2. If is one of the model graphs of Figure 2 such that is distinct from model graphs (7), (10), and (11), then H-PARTITION() is expressible in Datalog with stratified negation. (a) Counterexample for the model graph (7).
(b) Counterexample for the model graph (10).
In [1], the model graph (7) of Figure 2 is reduced to the model graph 2. This is possible because the constraints for and are identical (i.e., being adjacent to both and ), and the constraints for and are identical. Then, every non-base vertex labeled by can also be labeled by , and every non-base vertex labeled by can also be labeled by . Our previous Datalog program would fail, however, for the reason that the set of possible labels for a non-base vertex is never a singleton.
For example, consider the graph in Figure 3a with the base (
We adjust our Datalog program as follows: if the set of possible labels of a vertex has size 2, the new program will label with one of these two possibilities, arbitrarily chosen. The rest of the program remains unchanged. That is, in the box that immediately precedes Theorem 2, we replace the four rules for the predicate inPart by the following two rules: inPart(X,a,I,J,K,L) :- imp(X,b,I,J,K,L), imp(X,d,I,J,K,L). inPart(X,b,I,J,K,L) :- imp(X,a,I,J,K,L), imp(X,c,I,J,K,L).
As in [1], the model graphs (10) and (11) of Figure 2 need a special treatment. We illustrate the issue
by the model graph (10) and the graph given in Figure 3b. For the base (
It can be verified that for the model graph (10), the lists of possible labels are and ; for the model graph (11), the lists of possible labels are and . We have the following result. Lemma 3. (Cf. [1]) Let be one of the model graphs (10) or (11) in Figure 2. If there exists a solution to H-PARTITION() with a base (, , , ), then there is also a solution with the same base such that: • each vertex having in its list of possible labels is labeled ; and • each vertex having in its list of possible labels is labeled .
We now use Lemma 3 to adjust our previous Datalog program of Section 4.1. First, we copy the labeled vertices. label(X,a,I,J,K,L) :- inPart(X,a,I,J,K,L). label(X,b,I,J,K,L) :- inPart(X,b,I,J,K,L). label(X,c,I,J,K,L) :- inPart(X,c,I,J,K,L). label(X,d,I,J,K,L) :- inPart(X,d,I,J,K,L).
Next, if is an impossible label for a vertex but is not, the vertex is labeled by . Symmetrically, if is an impossible label for a vertex but is not, the vertex is labeled by . label(X,a,I,J,K,L) :- not imp(X,a,I,J,K,L), imp(X,b,I,J,K,L). label(X,b,I,J,K,L) :- imp(X,a,I,J,K,L), not imp(X,b,I,J,K,L).
We now have to check that this labeling is correct according to the model graph. If not, we reject the initial base. problem(X,P,I,J,K,L) :- label(X,P,I,J,K,L), full(P,Q), label(Y,Q,I,J,K,L), not e(X,Y). problem(X,P,I,J,K,L) :- label(X,P,I,J,K,L), dotted(P,Q), label(Y,Q,I,J,K,L), e(X,Y). bad_base(I,J,K,L) :- problem(X,P,I,J,K,L).
Finally, the definition of yes_instance() is changed as follows: yes_instance() :- base(I,J,K,L), not bad_base(I,J,K,L), not bad_init(I,J,K,L). no_instance() :- not yes_instance().
Along the lines of Theorem 2, we obtain the following result.
Theorem 4. If is one of the model graphs (10) or (11) in Figure 2, then H-PARTITION() is expressible in Datalog with stratified negation.
A vertex in a model graph is isolated if it is not adjacent to a full or dotted edge. The model graphs in
Figure 2 with at least one isolated vertex are (
Lemma 5. Let be an undirected graph. Let be a model graph with an isolated vertex. Then the following are equivalent: 1. contains an -isomorphic quadruplet of distinct vertices; and 2. is a yes-instance of the problem H-PARTITION().
From Section 4.1, it follows that non-recursive Datalog sufices to test the existence of an -isomorphic quadruplet of distinct vertices. Thus, we obtain the following result.
Theorem 6. If is a model graph with an isolated vertex, then H-PARTITION() is expressible in non-recursive Datalog with negation.
To compare the eficiency of our programs in an existing answer set solver, we need a generator for yes-instances and no-instances of arbitrary size. The motivation for distinguishing between yes- and no-instances comes from the asymmetry of NP-problems: on a yes-instance, an algorithm can stop as soon as the first -partition is found; but on no-instances no such early stopping is possible. In this section, we discuss generators for yes- and no-instances, and then we report on execution times of our programs on these instances.
Let , be two positive integers, and a model graph. We want to build a graph with vertices and edges that is a yes-instance for the problem H-PARTITION(). Necessarily, ⩾ 4 and ≤ (2− 1) , where the latter is the number of edges in the complete graph with vertices.
We denote N0 = {1, 2, 3, . . .}. Let , , , ∈ N0 such that + + + = . One can wonder if there exists a yes-instance with edges where the numbers of vertices labeled by , , , and are, respectively, , , , and .
Definition 4. We define min (, , , ) as the smallest number such that some graph with |()| = admits an -partition (, , , ) such that || = , || = , | | = , and || = . Analogously, we define max (, , , ) as the largest number such that some graph with |()| = admits an -partition (, , , ) such that || = , || = , | | = , and || = .
We write for a label and also for the number of vertices labeled with this label. If the context is not clear, we write # for the number of vertices labeled by . We have the following result. Lemma 7. Let be a model graph. Let , , , ∈ N0 such that + + + = . Then, min (, , , ) = max (, , , ) =
∑︁
(,)∈Full()
where Full() is the set of the full edges of , and Dotted() is the set of the dotted edges of .
Proof. We give a proof of (
Since for each full edge (, ) in , each vertex labeled with is connected to each vertex labeled with , there are # · # such edges. Moreover, there are no other edges than those described here. As we sum up these values for each full edge (, ), we obtain the desired number of edges in min .
We claim that this labeling satisfies all the constraints. The full constraints are satisfied by construction. The dotted constraints are also satisfied because min contains only edges connecting two vertices whose labels are adjacent through a full edge in .
It remains to be shown that there exists no graph with strictly less than ∑︀(,)∈Full() # · # edges
that is a yes-instance where the number of vertices labeled by , , , and are, respectively, , , ,
and . Assume for the sake of contradiction that there exists such a graph ′. We can assume without
loss of generality that ′ and min have the same set of vertices. Since ′ has strictly less edges than
min , there is an edge (, ) in min that is not in ′. Since ′ is a yes-instance, it has a solution. Let
be the label of in this solution, and the label of . Since (, ) is an edge of min , we have that
(, ) is a full edge of . So, we have two vertices and that are labeled by and respectively, but
there is no edge in ′ between and . This is a contradiction with the fact that ′ is a yes-instance.
This concludes the proof of (
The proof of (
For example, let us fix , , , ∈ N0 with the model graph (23) of Figure 2 and = + + + . According to the Figure 4, we have:
(m2i3n)(, , , ) = + (m2a3x) (, , , ) = Moreover, we claim that, for all such that (m2i3n)(, , , ) ⩽ ⩽ (m2a3x) (, , , ), there exists a graph with vertices and edges such that is a yes-instance for a labeling where the numbers of vertices labeled by , , , and are, respectively, , , , and . The idea is that we can extend the graph for (m2i3n)(, , , ) by adding edges until we reach edges such that every added edge does not violate any dotted constraint. We will now formalize this construction.
Definition 5. Let and ′ be two undirected graphs, We say that is an extension of ′, denoted ′ ⊆ , if (′) = () and (′) ⊆ (). If ′ ⊆ , we also say that ′ is extended by .
In other words, is an extension of ′ if it is possible to obtain from ′ by adding some edges. One can easily see that min ⊆ max . Indeed, we take min and consider the labeling induced by the construction of min . We can add all possibles edges that do not violate any dotted constraint. In this way, we obtain max by definition.
Theorem 8. Let be a model graph. Let , , , ∈ N0 and = + + + . Let min and max be the graphs with vertices and respectively min (, , , ) and max (, , , ) edges defined in (the proof of) Lemma 7. Every graph such that min ⊆ ⊆ max has a solution (, , , ) where || = , || = , | | = , and || = .
1 2 3
Proof. Let us consider the same labeling of the vertices in as in min . So the number of vertices labeled by , , , and are, respectively, , , , and . It remains to be shown that this labeling satisfies all the constraints.
• Let (, ) be a full edge of . We have to show that all the vertices labeled by are adjacent to all vertices labeled by . This holds true because is an extension of min and min already satisfies this constraint. • Let (, ) be a dotted edge of . We have to show that all the vertices labeled by are nonadjacent to all vertices labeled by . This holds true because max is an extension of and max already satisfies this constraint.
Corollary 9. Let be a model graph, and , , , ∈ N0 such that = + + + . Let be an integer such that min (, , , ) ⩽ ⩽ max (, , , ). There is an undirected graph with vertices and edges such that has a solution where the numbers of vertices labeled by , , , and are, respectively, , , , and .
Generator for yes-instances
Generator: For every quadruplet (, , , ) of positive integers such that + + + = and min (, , , ) ⩽ ⩽ max (, , , ), build a yes-instance from min by randomly adding edges that do not violate any dotted constraint, until the number of edges reaches ; if no such quadruplet exists, return “there is no such yes-instance.”
Given an integer ⩾ 4 and a model graph , we want to build a graph with vertices that is a no-instance for the problem H-PARTITION(). The following proposition tells us when this is possible.
Proposition 10. Let be a model graph and an integer such that ⩾ 4. There is an undirected
graph with vertices that is a no-instance for H-PARTITION() if and only if is not the model
graph (
Proof. Assume that is the model graph (
For the opposite direction, assume that is not the model graph (
• If contains at least one full edge, the empty graph with vertices and no edge is a no-instance because the full constraint will never be satisfied for any labeling of the vertices. • If contains at least one dotted edge, the complete graph with vertices and (2− 1) edges is a no-instance because the dotted constraint will never be satisfied for any labeling of the vertices.
The undirected graphs in the proof of Proposition 10 are of little interest in an experimental validation, because they do not admit an -isomorphic quadruplet of vertices, and therefore the Datalog program would not even enter its recursive part. Instead, for a model graph , we would like to generate no-instances that contain an -isomorphic quadruplet. Note here that, by Lemma 5, such no-instances do not exist if has an isolated vertex.
It would be interesting to develop an approach similar to that for yes-instances: start with a small no-instance and extend it until some desired number of vertices is reached. Nevertheless, this seems a dificult task, because the addition of edges for new vertices can turn no-instances into yes-instances, and vice versa. For example, in Figure 5, 1 is extended by 2, and 2 is extended by 3. For the model graph (6), we have that 2 is a no-instance, while 1 and 3 are yes-instances.
In view of the aforementioned dificulties, we have decided to generate no-instances in a randomized
fashion. Given ⩾ 4 and model graph that is not the model graph (
For the model graphs (
We have used the answer set solver Clingo [2, 3] to compare the execution times of ASP guess-and-check programs with programs in Datalog with stratified negation. Figure 6 shows execution times on input graphs of diferent small sizes that were generated as previously explained. The execution times reported in Figure 6 are average execution times over the 34 model graphs of Figure 2. It is immediately clear from this figure that when executed by Clingo, the guess-and-check program is much more eficient than our Datalog programs with stratified negation. The diference in eficiency was even more striking for larger graphs. In fact, on graphs with more than 50 vertices, we encountered memory problems when executing our Datalog programs in Clingo, which seem to be due to the size of the grounded program. In search for an explanation, we displayed and investigated the grounded rules in Clingo. The grounded Datalog programs only contain true atoms, i.e., rules whose body has already been evaluated as true and therefore left empty. Figure 7 shows that the Datalog programs yield significantly more grounded rules than the guess-and-check programs. Datalog often yields more than 250 000 true atoms while guess-and-check never results in more than 5000 ground rules.
We presented a logical programming approach to the problem of finding -partitions in undirected graphs. In particular, we showed how the polynomial-time solutions given in [1] can be encoded in Datalog with stratified negation. In an experimental validation, we found that in the answer set solver Clingo, these Datalog programs execute much slower than a simple guess-and-check program. We also studied the problem of generating yes- and no-instances for H-PARTITION with a fixed number of vertices or edges.
Our experiments indicate that when using an answer set solver, there may be no benefit in writing programs that are theoretically more eficient than guess-and-check programs. It would be interesting to investigate execution times of our Datalog programs on a dedicated Datalog engine. It would also be interesting to find systematic methods for generating no-instances with a fixed number of vertices or edges.