Graph problems are fundamental in several areas of research such as Computer Sciences, Physics, Chemistry, Biology, Social Sciences, and many other fields. Recent studies in graph theory are devoted to understanding more complicated versions of the classic problems of colorability and finding cliques. In particular, the Clique Coloring (CC) problem is the problem of deciding whether vertices of every maximal clique can be colored by two different colors. For arbitrary graphs, this problem is known to be Σ p 2 -complete. Answer Set Programming (ASP) is a logic-based declarative programming language able to model this kind of complex problems. In this paper, we provide two modeling into ASP, one using the basic version of ASP and the so-called saturation technique, and another one using a new extension of ASP with quantifiers, named ASP(Q), that is a much more powerful language able to model each computational problem in the polynomial hierarchy. We show that this last modeling is much more intuitive and allows to express the CC problem in a direct and natural way. Finally, we formally prove the soundness and completeness of both approaches. 1
Problems on graphs are fundamental in several sciences such as Computer Sciences, Physics, Chemistry, Biology, Social Sciences, and many other fields, because a lot of problems in these research areas can be translated into graph problems [1]. In the past, great attention has been focused on the study of graph problems about coloring, such as the Vertex Coloring problem and the Chromatic Number problem; about routes, such as the Hamiltonian Path problem and the Travelling Salesman problem; about covering, such as the Vertex Covering problem and the Dominating Set problem; and many others [2]. All these problems we have mentioned are very complex from a computational view point. More precisely, they are NP-hard [3].
Answer Set Programming (ASP) [4,5] is a logic-based declarative language able to model this kind of complex problems in an easy and direct way. It is based on the stable model semantics [6], also called answer set semantics [7]. A classic modeling example concerns the Vertex Coloring problem by using three colors, say red, blue, and green. Note that, also in this case, the problem in standard ASP; in Section 4, we model the CC problem with an ASP(Q) program, by showing soundness and completeness of the enconding; and, finally, in Section 5, we conclude with a brief discussion and future work.
In this section, first, we present the Clique Coloring (CC) problem. Then, we introduce basic notions of Answer Set Programming (ASP), and its extension with quantifiers, namely ASP(Q) [19].
The Clique Coloring (CC) problem is the problem of deciding whether vertices of every maximal clique can be colored by two different colors [20]. More formally, let G = (V, E) be an undirected graph. Recall that a clique H in G is a subset of V of at least 2 vertices, such that every pair of distinct vertices is connected by an edge, that is the subgraph of G induced by H is a complete graph. A maximal clique H in G is a clique in G such that each subset H ′ of V strictly containing H (i.e., H ⊂ H ′ ⊆ V ) is not a clique in G. Intuitively, H is a maximal clique if it cannot be extended to a larger one. Let k be an integer number. A k-clique-coloring of G is a function γ from V to {1, 2, . . . , k} such that every maximal clique of G contains two vertices of different color. Now, we can formally specify the CC decision problem.
INPUT: An undirected graph G and an integer k. QUESTION: Is there a k-clique-coloring of G?
To better understand previous notions and the CC problem, we focus on the case of k = 2, and provide two graph examples: the first of a graph admitting a 2-clique-coloring, and the second of a graph that does not admit it.
Example 1. Let G 1 be the graph reported in Figure 1. Formally, G 1 = (V, E), where V = {a, b, c, d, e, f } and E = {{a, b}, {a, c}, {a, d}, {b, c}, {c, d}, {b, e}, {d, e}, {d, f }}. It is easy to see that the maximal cliques in G 1 are: {a, b, c}, {a, c, d}, {d, e}, {b, e}, and {d, f }. Now, assume that k = 2, and consider the following coloration of vertices of G 1, 1 corresponds to red, and 2 to blue). Hence, each maximal clique in G 1 contains two vertices of different color. Therefore, γ is a 2-clique-coloring of G 1 .
Example 2. Let G 2 be the graph reported in Figure 2. Formally, G 2 = (V, E), where V = {a, b, c, d, e, f } and E = {{a, b}, {b, c}, {b, d}, {a, f }, {c, f }, {d, e}, {e, f }}. Then, the maximal cliques in G 2 are: {a, b}, {b, c}, {b, d}, {a, f }, {c, f }, {d, e}, {e, f }. Now, if we assume that k = 2, it is possible to prove that there is no 2-clique-coloring of G 2 . However, if we assume that k = 3, the following function 2, 1 corresponds to red, 2 to blue, and 3 to green) is a 3-clique-coloring of G 2 .
Note that the CC problem can be also seen as the problem of coloring the clique hypergraph (cf. Duffus et al. [21]). The clique hypergraph C (G) of a graph G = (V, E) is defined on the same vertex set V , and a set V ′ ⊆ V is a hyperedge of C (G) if, and only if, |V ′ | > 1 and V ′ induces an inclusionwise maximal clique of G. The question of k-coloring the hypergraph C (G) concerns into assign k colors to the vertices of C (G) such that every hyperedge contains at least two colors. Clearly, a graph G is k-clique-coloring if, and only if, the hypergraph C (G) is k-colorable.
Concerning computational complexity, it has been proved in [20] that the CC problem is Σ p 2complete for any fixed k ≥ 2 (see Theorem 4 and Corollary 5 in [20]). In the past, many classes of special graphs have been studied. It is known that for perfect graph the 2-clique-coloring problem is NP-hard, but it is open the question if it is NP-complete [24]. Moreover, for planar graph the 2-clique-coloring problem is feasible in polynomial time [24]. More recently, it has been proved that for planar graph the 3-clique-coloring problem is feasible in linear time [28]. Concerning circular-arc graphs, the CC problem is solvable in polynomial time [33], and an optimal clique-coloring is computable in linear time [34]. In the next sections, we will focus on the most general case.
Let P be a set of predicates, C a set of constants, and V set of variables. An element in C ∪ V is called a (standard) term. A (standard) atom a of arity n ≥ 0 has the form p(t 1 , . . . ,t n ), where p is a predicate from P, and t i is a term, for each i ∈ {1, . . . , n}. Whenever n = 0, we just write p instead of p(). If no variable appears in an atom, it is called ground. Moreover, let ⋆ ∈ {+, −, ×, /}, ≺∈ {<, ≤, =, ̸ =, >, ≥}, and let X and Y be variables. We extend the set of terms and atoms as follows. An arithmetic term has form −(X), (X ⋆Y ), −(α) or (α ⋆ β ), where α and β are arithmetic terms, and a built-in atom has form α ≺ β , where α and β are arithmetic terms. A (disjunctive) rule r has form
where m + n + l > 0, and all a i and c k are standard atoms, and b j are standard or built-in atoms. A (disjunctive) ASP program P is a finite set of rules. The head of r is the set H(r) = {a 1 , . . . , a l }, the positive (resp., negative) body of r is the set B + (r) = {b 1 , . . . , b m } (resp., B − (r) = {c 1 , . . . , c n }), and the body is the set B(r) = B − (r) ∪ B + (r). We denote by A(r) the set of built-in atoms. If B(r) = / 0, then the arrow "←" will be omitted. A rule r is normal, if |H(r)| ≤ 1. A fact is normal rule with B(r) = / 0. A constraint is a rule with H(r) = / 0. A normal ASP program P is a finite set of normal rules.
The Herbrand universe of P, denoted by U P , is the set of all integers and all constants appearing in P. The Herbrand base of P, denoted by B P , is the set of all ground standard atoms that can be obtained from the set of predicate symbols appearing in P and the constants in U P . Let r be a rule of P, and let σ be a substitution map from the set of variables occurring in r to U P , such that the arithmetic evaluation, performed in the standard way, of any arithmetic term is well-defined. A ground instance of r is a rule obtained from r by replacing each variable X in r by σ (X). The arithmetic evaluation of a ground instance r is obtained by replacing any arithmetic term appearing in r by its integer value, which is calculated in the standard way. The ground instantiation of r, denoted by ground(r), is the set of all (arithmetically evaluated) ground instances of r. We denote by ground(P) = ⋃︁ r∈P ground(r) the set of all (arithmetically evaluated) ground instances of all rules of P. An interpretation of P is any set I ⊆ B P of standard atoms.
A rule r is ground if each atom in r is ground. A program P is ground if each rule in P is ground. We say that an interpretation I satisfies a ground rule r if B + (r)\A(r) ⊆ I; B − (r) ∩ I = / 0 implies I ∩ H(r) ̸ = / 0; and each built-in atom in A(r) is true according to the standard arithmetic evaluation. If I satisfies every rule r in a ground program P, then I is a model of P. The reduct of P w.r.t. an interpretation I is the program P I such that: (i) for each rule r ∈ P with B − (r) ∩ I = / 0, P I contains the rule r ′ with H(r ′ ) = H(r), B + (r ′ ) = B + (r), and B − (r ′ ) = / 0; (ii) no further rule is in P I . An interpretation I is an answer set of the ground ASP program P if it is a minimal model of P I . For a non ground ASP program P, its answer sets are those of ground(P). The set of all answer sets of P is denoted by AS(P). A program P such that AS(P) ̸ = / 0 is called coherent, otherwise it is called incoherent.
Therefore, its ground version is given by ground
} are (minimal) models of P. Note that M 3 is not an answer set of P. Indeed, ground(P) M 3 = {a(1). a(2). b(1). c(2) ← a(1), b(2).}, thus its minimal model is F. On the other hand, M 1 and M 2 are answer sets of P. Indeed, ground(P (2).}, so M 2 is a minimal model of ground(P) M 2 . Hence, P is coherent.
In the following, we will also use choice rules [35], aggregates [36], and conditional literals [35]. In particular, we will use choice rules of the form h{a 1 ; . . . ; a l }k ← b 1 , . . . , b m , not c 1 , . . . , not c n .
(
where h and k are two natural numbers, l > 0, m + n ≥ 0, and all a i , b j and c k are atoms. The expression h{a 1 ; . . . ; a l }k is satisfied by an interpretation
In particular, a rule of the form 0{a}1 (written also as {a}) can be seen as a synctactic shortcut for the rule a ∨ a F , where a F is a fresh new atom not appearing elsewhere in the program, meaning that a can be chosen as true. Moreover, we will use aggregates of the form
where φ is a conjunction of atoms, and t is a variable occurring in φ . Intuitively, this aggregate counts the number of element of the set of all t for which φ holds. More formally, given an interpretation I, the result of applying I to the aggregate of the form (3) is the cardinality of {t|I satisfies φ }. Finally, we will use conditional literals of the form
where a and b i are atoms for i = 1, . . . , n. Intuitively, a conditional literal can be regarded as the list of elements in the set {a|b 1 , . . . , b n }. Concerning computational complexity properties, we recall that for normal ground programs P, deciding whether AS(P) ̸ = / 0 is NP-complete; while for disjunctive ground programs P, deciding whether AS(P) ̸ = / 0 is Σ p 2 -complete [37].
Let P i be an ASP program, for each i = 1, . . . , n, and let C be a set of constraints. 1 An ASP with Quantifiers (ASP(Q)) program Π is an expression of the form:
where, for each i = 1, . . . , n, □ i ∈ {∃ st , ∀ st }. Symbols ∃ st and ∀ st are named existential and universal answer set quantifiers, respectively. An ASP(Q) program Π of the form ( 5) is called existential whenever □ 1 = ∃ st , otherwise it is called universal.
Let Π be an ASP(Q) program of the form (5). Given an ASP program P and an interpretation I over B P , we denote by fix P (I) the set of facts and constraints {a | a ∈ I} ∪ {← a | a ∈ B P \ I} and by Π P 1 ,I the ASP(Q) program of the form (5), where P 1 is replaced by P 1 ∪ fix P 1 (I). The coherence of an ASP(Q) program is inductively defined on the number of quantifiers in the program: (i) ∃ st P : C is coherent, if there exists M ∈ AS(P) such that C ∪ fix P (M) is coherent; (ii) ∀ st P : C is coherent, if for each M ∈ AS(P), C ∪ fix P (M) is coherent; (iii) ∃ st P Π is coherent, if there exists M ∈ AS(P) such that Π P,M is coherent; (iv) ∀ st P Π is coherent, if for each M ∈ AS(P), Π P,M is coherent. For an existential ASP(Q) program Π of the form (5), we say that M ∈ AS(P 1 ) is a quantified answer set of Π, whenever (□ 2 P 2 • • • □ n P n : C) P 1 ,M is coherent, in case of n > 1, and whenever C ∪ fix P 1 (M) is coherent, in case of n = 1. The set of all quantified answer sets of Π is denoted by QAS(Π).
For instance, an existential ASP(Q) program Π = ∃ st P 1 ∀ st P 2 : C is coherent if there exists an answer set M 1 of P 1 such that for each answer set M 2 of P ′ 2 there is an answer set of C ∪ f ix P ′ 2 (M 2 ), where
If such an answer set M 1 exists, then M 1 is a quantified answer set of Π.
Example 4. Consider the existential ASP(Q) program Π = ∃ st P 1 ∀ st P 2 : C, where
First, note that the program P 1 has two answer sets: M 1 = {a(1), b(1)} and M 2 = {a(1), c(1)}. Now, if we consider M 1 , then fix P 1 (M 1 ) = {a(1). b(1). ← c(1).}. Hence, the program P ′ 2 = P 2 ∪ fix P 1 (M 1 ) has the unique answer set M 1 . Thus, fix P ′ 2 (M 1 ) = {a(1). b(1). ← c(1). ← d (1). ← e(1).}, and so C ∪ fix P ′ 2 (M 1 ) is incoherent. On the other hand, if we consider M 2 , then fix P 1 (M 2 ) = {a(1). c(1). ← b(1).}. Hence, the program P ′ 2 = P 2 ∪ fix P 1 (M 2 ) has two answer sets:
. ← e(1).} and fix P ′ 2 (M 4 ) = {a(1). c(1). e(1). ← b(1). ← d(1).}. Since both C ∪ fix P ′ 2 (M 3 ) and C ∪ fix P ′ 2 (M 4 ) are coherent, then Π is coherent, and M 2 is a quantified answer set of Π. Concerning computational complexity properties, we recall that for normal existential (respectively, universal) ASP(Q) programs Π with n alternating quantifiers in the prefix, deciding whether Π is coherent is Σ p n -complete [respectively, Π p n -complete]. Hence, ASP(Q) can in principle model all problems in the Polynomial Hierarchy [12].
Now, we show how to model the CC problem by using ASP. First of all, note that this representation is theoretically possible as CC is a Σ p 2 -complete problem and ASP is able to model decisional problems in this complexity class. A standard technique used to model this kind of problems is called saturation [32]. It was initially introduced by Eiter and Gottlob [31] in order to provide a complexity reduction from the problem of deciding the validity of a quantified Boolean formula of the form ∃X∀Y φ (X,Y ), where φ (X,Y ) is in disjunctive normal form over atoms in X and Y , to the problem of deciding the coherence of a propositional disjunctive ASP program. Both problems are Σ p 2 -complete. In the following, we exploit the saturation technique to model the CC problem into an ASP program.
Let G = (V, E) be an undirected graph, and let {1, . . . , k} be a set of k colors.
node(a). for each a ∈ V ; (6) edge(a, b). edge(b, a). for each {a, b} ∈ E;
noEdge(a, b). noEdge(b, a). for each {a, b} ̸ ∈ E;
color(i). for each i = 1, ..., k.
This set of facts model the input data, i.e. the graph G = (V, E) by using atoms node(a), for each vertex a ∈ V (6); edge(a, b) and edge(b, a), for each edge {a, b} ∈ E (7); noEdge(a, b) and noEdge(b, a), for each set of two vertices {a, b} ̸ ∈ E (8); and color(i), for each i = 1, . . . , k (9).
1{colors(X,C) : color(C)}1 ← node(X).
Rule ( 10) is a choice rule that selects exactly one atom in the set {colors(a, 1), . . . , colors(a, k)}, for each vertex a ∈ V . Hence, it guesses a possible coloration of the vertices of the graph.
inClique(X) ∨ outClique(X) ← node(X).
Rule ( 11) is a disjunctive rule guessing a subset of vertices by introducing a unary predicate inClique, for selected vertices, and a unary predicate outClique, for non selected ones.
Saturation Check:
The previous three rules model the saturation conditions. First, we saturate whenever the guessed set H is not a clique. Indeed, rule (12) models that two distinct vertices are in the set, but there is no edge between them. Second, we saturate whenever the guessed clique is not maximal. Indeed, rule (13) models that a vertex X is out of the clique, and every vertex Y not adjacent to X is out of the clique. This means that X is connected with every vertex of the clique, so the clique is not maximal. Finally, we saturate whenever the guessed maximal clique has two distinct vertices with two different colors. Indeed, rule ( 14) models that there exists two vertices X and Y belonging to a clique, such that X is colored by C, Y is colored by D, and C and D are different colors.
inClique(X) ← node(X), satur.
outClique(X) ← node(X), satur.
← not satur.
These last three rules represent the classic saturation part. In particular, rules ( 15) and ( 16) impose to infer each atom of the form inClique(X) and outClique(X) for each node X, whenever some saturation condition is satisfied. Finally, rule (17) forces the whole program to return an answer set only if the atom satur has been inferred. Now, we formally prove that our encoding is sound and complete.
Theorem 1. Let G = (V, E) be a graph, k an integer, and P be the program formed by rules ( 6)- (17). Then, P has an answer set if, and only if, there is a k-clique-coloring of G.
Proof. First, assume that γ from V to {1, . . . , k} is a k-clique-coloring of G. We state that the set A containing facts ( 6)-( 9); atoms colors(a, γ(a)), for each a ∈ V ; atoms inClique(a) and outClique(a), for each a ∈ V ; and the atom satur is an answer set of P. It can be easily checked that A is a model P. Now, consider the reduct program of P with respect to A, that is the positive program P A given by P \ {← not satur}. We have to show that A is a minimal model of P A . By contradiction, assume that there is a model A ′ of P A such that A ′ ⊂ A. Clearly, since A ′ is a model of P A contained in A, then at least the facts ( 6)-( 9) and the atoms colors(a, γ(a)), for each a ∈ V , must be also in A ′ . Now, note that satur ̸ ∈ A ′ , otherwise A ′ should be forced to have also atoms inClique(a) and outClique(a), for each a ∈ V (because of rules ( 15) and ( 16)), and so A ′ should be equal to A. Since satur ̸ ∈ A ′ , then no body of the rules among ( 12), ( 13), and ( 14) is satisfied by A ′ . This means that A ′ contains a subset of atoms from {inClique(a)|a ∈ V } (since A ′ satisfies rule (11)) such that the set H = {a|inClique(a) ∈ A ′ } is a clique (since A ′ does not satisfy the body of rule ( 12)), is a maximal clique (since A ′ does not satisfy the body of rule ( 13)), and each node a in H has the same color (since A ′ does not satisfy the body of rule ( 14)). But this is a contradiction, since γ is a k-clique-coloring of G. Therefore, such an A ′ cannot exist, and A is a minimal model of P A , and so it is an answer set of P.
On the other hand, assume that P has an answer set, say A. Then, A must contain the atom satur (otherwise rule (17) would not be satisfied). Moreover, by rules ( 15) and ( 16), each atom of the form inClique(a) and outClique(a), for each node a of the graph, must belong to A. Since A is a minimal model of the reduct of P with respect to A, that is P \ {← not satur}, then there is no model of P A not satisfying at least one of the rules among ( 12), (13), and ( 14). This means that, for each possible choice of the rule (11), the set of atoms of the form inClique(X), corresponding to the set of selected vertices in G, either it was not a clique (whenever rule (12) has been applied), or it was not a maximal clique (whenever rule (13) has been applied), or it was a maximal clique with at least two vertices with two distinct colors (whenever rule (14) has been applied). In other words, there is a coloration choice of the vertices in G (the one corresponding to A), such that each maximal clique in G has two vertices with two distinct colors. Hence, there is a k-clique-coloring of G.
As highlighted by many expert ASP scholars, the saturation technique is not at all easy to use and its meaning is not very intuitive [15,14,13]. So, in the next section, we exploit the modeling capabilities of ASP with quantifiers to provide an encoding of the CC problem.
Let G = (V, E) be a graph and k be an integer. First of all, note that the CC problem can be easily expressed as follow:
1. There exists a k-coloring of G such that 2. for each maximal clique H in G,
This problem has a direct and natural way to be modeled into an ASP(Q) program of the form ∃ st P 1 ∀ st P 2 : C. Intuitively, P 1 has to model the problem of identifying a k-coloring of G, so that an answer set of P 1 will correspond to a k-coloring of G. Then, P 2 models the problem of identify a maximal clique in G, so that an answer set of P 2 will correspond to a maximal clique in G colored with k colors. Finally, the program C will be just a constraint to check that the answer sets of P 2 satisfy the condition of having two vertices of different color.
edge(a, b). edge(b, a). for each {a, b} ∈ E;
.
The ASP program P 1 models the problem of choose a coloration of the vertices of a graph. Indeed, the first three lines model the input data, i.e. the graph G = (V, E) by using a unary predicate node (18) and a binary predicate edge (19); and the set of k colors with a unary predicate color (20). Finally, the choice rule (21) selects exactly one atom in the set {colors(a, 1), . . . , colors(a, k)}, for each vertex a ∈ V .
Hence, an answer set of P 1 is given by the set of facts F union a possible coloration of the vertices. For instance, A = F ∪ {colors(a, 1), colors(b, 1), colors(c, 2), colors(d, 1), colors(e, 2), colors( f , 2)} is an answer set of P 1 .
Program P 2 :
{inClique(X)} ← node(X).
← inClique(X), inClique(Y ), not edge(X,Y ), X ̸ = Y. ( 23)
← lengthClique(X), X < 2.
← node(X), not inClique(X), lengthClique(Z), #count{Y : edge(X,Y ), inClique(Y )} = Z.
The ASP program P 2 models the problem of finding a maximal clique in a graph. Indeed, rule ( 22) is a choice rule guessing a subset of vertices of the graph, collected into the unary predicate inClique. Then, constraint ( 23) is violated whenever in the guessed subset there are two distinct vertices X and Y for which there is no edge between them. Rule (24) computes the cardinality of the guessed subset, by infering an atom of the form lengthClique(n), where n is the cardinality. Constraint (25) forces the cardinality to be greater than 1. Therefore, rules ( 23), ( 24) and ( 25) select a guessed subset of vertices that is a clique of the graph. Finally, the last constraint ( 26) is violated whenever there is a vertex X of the graph, but not of the guessed subset such that the number of edges from X to a vertex Y of the guessed subset is equal to the cardinality of the guessed subset. This means that the guessed subset is not a maximal clique. It can be easily verified that each answer set corresponds to a maximal clique in G with the coloration given by A.
The program C checks that each maximal clique contains at least two vertices of different color. Indeed, the constraint ( 27) is violated in case the number of colors C for which there is a vertex in the maximal clique (inClique(X)) that is colored by C (colors(X,C)) is equal to 1.
Example 7. Consider again the graph G 1 of the Example 1, and the answer sets A 1 , ..., A 5 reported in Example 6. Each answer set does not violate the constraint (27), that is it satisfies the program C. For instance, in A 1 we have atoms colors(a, 1), colors(c, 2), inClique(a), and inClique(c). Hence, the counting aggregate returns 2. Now, we formally prove that our encoding is sound and complete.
Theorem 2. Let G = (V, E) be a graph, k an integer, and Π = ∃ st P 1 ∀ st P 2 : C be the ASP(Q) program described above. Then, Π is coherent if, and only if, there is a k-clique-coloring of G.
Proof. First, assume that γ from V to {1, . . . , k} is a k-clique-coloring of G. We state that the set A containing facts ( 18), (19), and (20); and atoms colors(a, γ(a)), for each a ∈ V is an answer set of P 1 such that for each answer set A ′ of P 2 ∪ fix P 1 (A), A ′ is an answer set of C. Note that fix P 1 (A) = A ∪ {← colors(a, i)|i = 1, . . . , k ∧ i ̸ = γ(a) ∧ a ∈ V }, and each of these constraints is always not violated by P 2 , since atoms of the form colors(a, i) are never inferred by P 2 . Hence, instead of P 2 ∪ fix P 1 (A), we can just consider P 2 ∪ A. By construction, A is an answer set of P 1 . Now, let A ′ be an answer set of P 2 ∪ A. Hence, by rule (22), a subset of {inClique(a)|a ∈ V } must be contained in A ′ , and by rules ( 24) and ( 25) this subset has to have at least two elements. Moreover, also an atom of the form lengthClique(n), with n ≥ 2, belongs to A ′ . Finally, since A ′ satisfy the two constraints of P 2 (rule ( 23) and ( 26)), we have that the set K = {a|inClique(a) ∈ A ′ } is a maximal clique of G. Now, since γ is a k-clique-coloring of G, we have that there exists a and b in K such that γ(a) ̸ = γ(b). Therefore, colors(a, γ(a)) and colors(b, γ(b)) are two atoms in A ′ ⊇ A. Hence, the aggregate appearing in the constraint ( 27) returns a number greater than 1. Thus, A ′ is an answer set of the program C.
On the other hand, assume that Π is coherent. Hence, there exists an answer set A of P 1 such that for each answer set A ′ of P 2 ∪ A, A ′ is an answer set of C. Let γ be a function from V to {1, . . . , k} such that γ(a) = i iff colors(a, i) ∈ A. We state that such a γ is a k-clique-coloring of G. Indeed, let H be a maximal clique of G, and consider the set A ′ = A ∪ {inClique(a)|a ∈ H} ∪ {length(|H|)}. By construction, A ′ satisfies rules (22) and (24). Moreover, since H is a maximal clique, A ′ satisfies also constraints ( 23), ( 25) and (26). Therefore, A ′ is a model of P 2 ∪A, and by construction is also a minimal model of the reduct (P 2 ∪ A) A ′ . Hence, A ′ is an answer set of P 2 ∪ A. Then, by assumption, A ′ is an answer set of C, i.e., A ′ does not violate the constraint (27). This means that the cardinality of the set {i|colors(a, i) ∈ A ′ ∧ inClique(a) ∈ A ′ } is greater than 1. Therefore, by construction of A ′ , we have that there exist at least two vertices in the maximal clique H, say a and b, such that γ(a) = i and γ(b) = j with i ̸ = j. I.e., H is a maximal clique of G containing two vertices of different color. Hence, γ is a k-clique-coloring of G.
This paper focused on modeling the CC problem via ASP. We provided an enconding into standard ASP by using the saturation technique, and an encoding into ASP(Q), an extension of ASP able to quantify over answer sets. We also provided formal proofs of soudness and completeness of both encondings. From a modeling point of view, the comparison of the two encondigs shows that ASP(Q) is able to provide a direct and natural way of modeling the CC problem.
Concerning others logic-based modeling approaches to the CC problem, Zhang et. al. [38] have provided an encoding by using a first-order theory, and then a general reduction from first-order theories to ASP programs. Concerning our ASP encoding based on saturation, we note that a similar encoding has been proposed in [39], where the author is interested to provide a comparison with another saturation encoding in ASP by using recursive non-convex aggregates, to show the efficiency improvements for ASP solvers whenever a program with standard aggregates is rewritten with recursive non-convex aggregates.
Since, to the best of our knowledge, there are currently no solvers to compute ASP(Q) programs, for future work, we plan to provide an implementation of ASP(Q) at least for ASP(Q) programs with two innested quantifiers, that are ∃ st P 1 ∀ st P 2 : C and ∀ st P 1 ∃ st P 2 : C, thus to be able to evaluate problems belonging to the second level of the polynomial hierarchy (i.e., Σ p 2 and Π p 2 ). In this way, we could plan an experimental analysis to compare, also from a practical computational point of view, all these encondings for solving the CC problem.
Finally, given the expressivity and the modeling capability of the ASP(Q) language, we plan to consider other problems related to the CC one. Such as the k-Clique-Choosability problem that has been proved to be a Π p 3 -complete problem for every k ≥ 2 (see Corollary 9 in [20]), and the Hereditary k-Clique-Coloring that has been proved to be a Π p 3 -complete problem for every k ≥ 3 (see Corollary 15 in [20]).