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 Σ2p-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 is NP-hard. However, with just the two following rules, whose meaning is very intuitive, the problem is solved:
← color(X , red) ∨ color(X , blue) ∨ color(X , green) ← node(X ).
edge(X ,Y ), col(C), color(X ,C), color(Y,C).
Indeed, the first rule is a guess of the color for a given node of the graph; and the second rule is a constraint forcing the chosen coloration to have different colors for nodes connected by an edge, i.e., it is not possible that there is an edge between two nodes, X and Y , and both are colored by the same color C.
In the past, for solving problems in ASP a very useful methodology has been identified and developed. It is known as generate-define-test [ 7] or as guess-and-check [8]. Basically, the guess part selects candidate solutions by using disjunctive rules, and the check part uses constraints to force admissible ones, like in the Vertex Coloring modeling example. Moreover, several ASP solvers have been designed and implemented, such as DLV [9] and Clasp [10], to show the effectivity in solving problems [11]. However, ASP in its basic version is not able to solve complex problems beyond the second level of the Polynomial Hierarchy [12], and it loses its ease of use when already dealing with problems that are Σ2p-complete [13, 14, 15]. To overcome these limitations, several attempts have been developed in the past [16, 14, 17, 13, 15, 18]. More recently, it has been proposed an extension of ASP with Quantifiers , named ASP(Q) [19]. Basically, ASP(Q) programs extends ASP program in a similar way to how Quantified Boolean formulas extend propositional logic formulas. Intuitively, the ASP(Q) language allows to quantify (existentially or universally) over answer sets of standard ASP programs. So that, ASP(Q) is a much more powerful language able to model, in a direct and natural way, problems belonging to the Polynomial Hierarchy.
Now, recent studies in graph theory are devoted to understanding more complicated versions of the classic graph problems mentioned above. In this paper, we will focus on the so-called Clique Coloring (CC) problem [20]. Intuitively, it is the problem of deciding whether vertices of every inclusionwise maximal clique of a graph can be colored by (at least) two different colors from a set of k colors. In this case, the graph is said to have a k-clique-coloring. Originally, the CC problem was formulated in terms of the clique hypergraph [21], that is defined on the same set of vertices of the starting graph, while an hyperedge is a subset of vertices that is an inclusionwise maximal clique. The problem is now to decide the existence of a coloring of the vertices of the hypergraph with k colors such that every hyperedge contains at least two colors. In this case, the hypergraph is said to be k-colorable. Clearly, a graph has a k-clique-coloring if, and only if, the corresponding hypergraph is k-colorable. The CC problem has been addressed for restricted classes of graphs in [22, 23, 24, 25, 26, 27, 28, 29], and in its general version in [20, 30]. For arbitrary graphs, this problem is Σ2p-complete already for k = 2 [20].
In this paper, we provide two modeling of the CC problem into ASP programs, one using the basic version of ASP and the so-called saturation technique [31, 32], and another one using ASP(Q). 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.
The paper is structured as follows. In Section 2, we introduce preliminary notions about the CC problem, ASP, and ASP(Q); in Section 3, we develop and study an encoding of the CC problem a b b c d e a d c f e f b b c a d d e c f e 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.
CC 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 G1 be the graph reported in Figure 1. Formally, G1 = (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 G1 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 G1: γ(a) = γ(b) = γ(d) = 1 and γ(c) = γ(e) = γ( f ) = 2 (in Figure 1, 1 corresponds to red, and 2 to blue). Hence, each maximal clique in G1 contains two vertices of different color. Therefore, γ is a 2-clique-coloring of G1. Example 2. Let G2 be the graph reported in Figure 2. Formally, G2 = (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 G2 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 G2. However, if we assume that k = 3, the following function γ such that γ(a) = γ(c) = γ(d) = 1, γ(b) = γ(e) = 2, and γ( f ) = 3 (in Figure 2, 1 corresponds to red, 2 to blue, and 3 to green) is a 3-clique-coloring of G2.
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 Σp2 complete 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(t1, . . . , tn), where p is a predicate from P, and ti 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 a1 ∨ . . . ∨ al ← where m + n + l > 0, and all ai and ck 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) = {a1, . . . , al}, the positive (resp., negative) body of r is the set B+(r) = {b1, . . . , bm} (resp., B− (r) = {c1, . . . , cn}), 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 UP, is the set of all integers and all constants appearing in P. The Herbrand base of P, denoted by BP, 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 UP. Let r be a rule of P, and let σ be a substitution map from the set of variables occurring in r to UP, 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 ⊆ BP 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 PI such that: (i) for each rule r ∈ P with B− (r) ∩ I = 0/ , PI contains the rule r′ with H(r′) = H(r), B+(r′) = B+(r), and B− (r′) = 0/ ; (ii) no further rule
I is in P . An interpretation I is an answer set of the ground ASP program P if it is a minimal model of PI. 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.
⎧ a(
P = ⎨ c(X ) ∨ d(X ) ← a(X ), not b(X ).
⎩ c(Y ) ← a(X ), b(Y ), not c(X ), X ̸= Y. ⎭
⎧ a(
⎪⎪⎪⎪⎩ cc((
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
(
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 Σ2p-complete [37].
Let Pi 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:
□ 1P1 □ 2P2 · · · □ nPn : C
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 (
Let Π be an ASP(Q) program of the form (
For instance, an existential ASP(Q) program Π = ∃st P1∀st P2 : C is coherent if there exists an answer set M1 of P1 such that for each answer set M2 of P2′ there is an answer set of C ∪ f ixP2′ (M2), where P2′ = P2 ∪ fix P1 (M1). If such an answer set M1 exists, then M1 is a quantified answer set of Π.
Example 4. Consider the existential ASP(Q) program Π = ∃st P1∀st P2 : C, where
P1 = {︁ a(
P2 = {︁ d(X ) ∨ e(X ) ←
c(X ). }︁ ; C = {︁ ←
b(X ), not d(X ). }︁ .
First, note that the program P1 has two answer sets: M1 = {a(
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 Σnp-complete [respectively, Πnp-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 Σ2p-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 Σ2p-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. Guess: noEdge(a, b). noEdge(b, a). for each {a, b} ̸∈ E;
color(i). for each i = 1, ..., k.
Saturation Guess: inClique(X) ∨ outClique(X) ←
Rule (
Rule (
outClique(X ), outClique(Y ) : noEdge(X ,Y ) : X ̸= Y.
satur ← inClique(X ), inClique(Y ), colors(X ,C), colors(Y, D),C ̸= D.
The previous three rules model the saturation conditions. First, we saturate whenever the guessed
set H is not a clique. Indeed, rule (
node(X ), satur.
not satur.
←
These last three rules represent the classic saturation part. In particular, rules (
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
(
On the other hand, assume that P has an answer set, say A. Then, A must contain the atom
satur (otherwise rule (
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, 3. H cointains two vertices of different color?
This problem has a direct and natural way to be modeled into an ASP(Q) program of the form ∃st P1∀st P2 : C. Intuitively, P1 has to model the problem of identifying a k-coloring of G, so that an answer set of P1 will correspond to a k-coloring of G. Then, P2 models the problem of identify a maximal clique in G, so that an answer set of P2 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 P2 satisfy the condition of having two vertices of different color.
Program P1:
node(a). for each a ∈ V ; edge(a, b). edge(b, a). for each {a, b} ∈ E;
color(i). for each i = 1, ..., k;
1{colors(X ,C) : color(C)}1 ←
The ASP program P1 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 (
Example 5. Let G1 be the graph considered in Example 1, and let k = 2. The first three rules of program P1 identify the following set of facts F = ⎧ node(a), node(b), node(c), node(d), node(e), node( f ), ⎫ ⎪⎪⎨ edge(a, b), edge(a, c), edge(b, c), edge(c, d), edge(b, e), edge(d, e), edge(d, f ), ⎬⎪⎪ ⎪⎪⎩ edge(b, a), edge(c, a), edge(c,cbo)l,oerd(g1e)(,dc,oclo),re(d2g)e(e, b), edge(e, d), edge( f , d), ⎪⎭⎪ . Hence, an answer set of P1 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 P1.
Program P2: {inClique(X)} ← ← inClique(X ), inClique(Y ), not edge(X ,Y ), X ̸= Y.
lengthClique(Y ) ←
#count{X : inClique(X )} = Y.
← lengthClique(X ), X < 2.
←
node(X ), not inClique(X ), lengthClique(Z),
#count{Y : edge(X ,Y ), inClique(Y )} = Z.
(
Example 6. Consider again the graph G1 of the Example 1, and the answer set A of the program P1 reported in Example 5. Based on the facts in A, the ASP program P2 produces exactly the following 5 answer sets:
A1 = A ∪ {inClique(a), inClique(b), inClique(c), lengthClique(
A3 = A ∪ {inClique(d), inClique(e), lengthClique(
A5 = A ∪ {inClique(d), inClique( f ), lengthClique(
It can be easily verified that each answer set corresponds to a maximal clique in G with the coloration given by A.
Program C:
#count{C : colors(X ,C), inClique(X )} = 1.
←
The program C checks that each maximal clique contains at least two vertices of different color.
Indeed, the constraint (
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 P1∀st P2 : 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 (
On the other hand, assume that Π is coherent. Hence, there exists an answer set A of P1 such that
for each answer set A′ of P2 ∪ 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 (
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. (see Corollary 15 in [20]).
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 P1∀st P2 : C and ∀st P1∃st P2 : C, thus to be able to evaluate problems belonging to the second level of the polynomial hierarchy (i.e., Σ2p and Π2 ). In this way, p 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 Hhaesrebdeietanrpyrko-vCeldiqtuoeb-CeoalΠor3pin-cgotmhaptlehtaespbreoebnlepmrovfoerdetvoebrye ak Π≥3p-complete problem for every k ≥ 3 2 (see Corollary 9 in [20]), and the 119–124. [37] E. Dantsin, T. Eiter, G. Gottlob, A. Voronkov, Complexity and expressive power of logic programming, ACM Comput. Surv. 33 (2001) 374–425. [38] H. Zhang, Y. Zhang, M. Ying, Y. Zhou, Translating first-order theories into logic programs, in: IJCAI, IJCAI/AAAI, 2011, pp. 1126–1131. [39] M. Alviano, Evaluating answer set programming with non-convex recursive aggregates, Fundam. Informaticae 149 (2016) 1–34.