Automated Aggregator — Rewriting with the Counting Aggregate

We follow the ASP-Core-2 Input Language Format [4]. We consider rules of the form $head\leftarrow body.$ The head may consist of a single literal or be empty, the latter representing a contradiction, making the rule a constraint. The body may contain one or more literals or be empty, which constitutes a fact. Literals are composed of an atom, which may be preceded by $not$. Negative literals include $not$; positive literals do not. Atoms have the form $p(t_{\_}1,\dots,t_{\_}k)$, where $p$ is a predicate symbol of arity $k$ and each $t_{\_}i$ is a term, that is, a constant, variable, or expression of the form $f(t_{\_}1,\dots,t_{\_}k)$ where $f$ is a function symbol of arity $k>0$ and each $t_{\_}i$ is a term.¹¹1AAgg also accepts other term expressions following the definition used by clingo [6].

Atoms may also take the form of an aggregate expression. In this work, we focus on counting aggregates, that is, expressions of the form:

$$s_{\_}1\prec_{\_}1\#count\{{\it\bf t}_{\_}1:{\it\bf L}_{\_}1{\bf;}\ldots{\bf;}{\it\bf t}_{\_}n:{\it\bf L}_{\_}n\}\prec_{\_}2s_{\_}2$$

(1)

In (1), ${\it\bf t}_{\_}i$ and ${\it\bf L}_{\_}i$ form an aggregate element, which is a non-empty tuple of terms and literals, respectively. The count operation simply counts the number of unique term tuples ${\it\bf t}_{\_}i$ whose corresponding condition ${\it\bf L}_{\_}i$ holds. The result of the count function is compared by the comparison predicates $\prec_{\_}1$ and $\prec_{\_}2$ to the terms $s_{\_}1$ and $s_{\_}2$. These comparison predicates may be one of $\{<,\leq,=,\neq\}$. One or both of these comparisons can be omitted [6].

The aggregate equivalence rewriting takes as input rules of the form:

$$H\leftarrow\bigwedge_{\_}{1\leq i\leq b}F(X_{\_}i,{\bf Y}),\bigwedge_{\_}{1\leq i<j\leq b}X_{\_}i\neq X_{\_}j,\ G.$$

(2)

where

• •

  $H$ is the head of a rule ($H$ may be empty making the rule a constraint)

• •

  $F$ is a predicate of arity $1+\bf{|Y|}$

• •

  $X_{\_}1,\ldots,X_{\_}b$ are variables, all in the same position in $F$

• •

  $\bf{Y}$ is a comma-separated list of variables, identical in variables and variable positions for all $F$ in the rule

• •

  $G$ is the remaining body of the rule, possibly empty,

and the following hold true:

• •

  $b\geq 2$

• •

  $H$, $G$, and ${\bf Y}$ have no occurrences of variables $X_{\_}1,\ldots,X_{\_}b$

• •

  The terms $\bigwedge_{\_}{1\leq i<j\leq b}X_{\_}i\neq X_{\_}j$ may instead be a continuous chain of comparisons:

  $\bigwedge_{\_}{1\leq i\leq b-1}X_{\_}i<X_{\_}{i+1}$ or $\bigwedge_{\_}{1\leq i\leq b-1}X_{\_}i>X_{\_}{i+1}$.

Note that $X_{\_}i$’s need not be in the first position in $F$, so long as they are all in the same position in $F$ and the other variables in $F$ (if any) are identical in all occurrences of $F$ in the rule. Additionally, some other forms logically equivalent to $\bigwedge_{\_}{1\leq i<j\leq b}X_{\_}i\neq X_{\_}j$ are also acceptable. For instance, the condition $X_{\_}1\neq X_{\_}2$ may be expressed as $X_{\_}1+a\neq X_{\_}2+a$, for some integer $a$.

The form of the output depends on the size of ${\bf Y}$. When $|{\bf Y}|=0$, the output form is:

$$H\leftarrow b\leq\#count\{X:F(X)\},G.$$

(3)

where

• •

  $H$, $b$, $F$, and $G$ are as above

• •

  Aggregate element $X:F(X)$ follows the form ${\it\bf term}:{\it\bf literal}$ as defined above. The prior, $X$, is a tuple of one term, which in this case is a variable. The second, $F(X)$, is a literal.

When $|{\bf Y}|>0$, we perform projection to project out the variable $X$ from $F$. This gives us an output form consisting of two rules:

$\displaystyle\begin{split}H&\leftarrow b\leq\#count\{X:F(X,{\bf Y})\},F^{\prime}({\bf Y}),G.\\ F^{\prime}({\bf Y})&\leftarrow F(X,{\bf Y}).\end{split}$

(4)

where

• •

  $H$, $b$, $F$, ${\bf Y}$, and $G$ are as above

• •

  Aggregate element $X:F(X,{\bf Y})$ follows the form ${\it\bf term}:{\it\bf literal}$ as above

• •

  $F^{\prime}$ is a new predicate symbol of arity equal to the size of Y, that is, equal to the arity of $F$ minus one; introducing $F^{\prime}$ ensures that variables in $\mathbf{Y}$ are universally quantified.

The correctness of this rewriting, follows from the results presented in the appendix (Theorem A.3). Specifically, we show there that if a program is obtained from another program by rewriting one of its rules in the way described above, then both programs have the same answer sets (modulo atoms $F^{\prime}(\mathbf{y})$, if $F^{\prime}$ is introduced).

The software relies on the clingo Python module provided by the Potassco suite [8]. The module is written in Python 2.7. As such, Python 2.7 is required to run the Automated Aggregator system. Installation information is provided in the software’s README file. The Automated Aggregator is invoked as follows:

  python  aagg/main.py
          [-h,--help] [-o,--output FILENAME] [--no-rewrite]
          [--no-prompt] [--use-anonymous-variable]
          [--aggregate-form ID] [-d,--debug] [-r,--run-clingo]
          [encoding_1 encoding_2 ...]

The -h flag lists the help options. The encoding(s) are the filename(s) of the input encoding(s), and the output is the desired name for the output file. If no output filename is given, one is generated based on the first input filename given. When a candidate rule is discovered, the user is shown the proposed rewriting and prompted for confirmation. If the --no-rewrite flag is given, no prompts are given and no rewriting is performed. If the --no-prompt flag is given, no prompts are given and rewriting is performed where possible. The ID supplied to the --aggregate-form argument informs the program which aggregate form to use when performing rewrites: its values $1$, $2$, and $3$ correspond to aggregate forms (3/4), (5), and (6), respectively. The -d debug flag directs the application to operate with verbosity, printing details during the rewriting candidate discovery process and printing some statistics after the application’s conclusion. The --r run-clingo flag directs the application to run the resulting program through clingo after any rewritings are performed.

Finally, the --use-anonymous-variable flag indicates an additional modification of the output form to be performed. It uses the anonymous variable ‘_’ in place of the variable $X$ in the output forms listed above, with some additional modifications of the rule to ensure the transformation is correct. Specifically, we replace the aggregate element $X:F(X,{\bf Y})$ with $F(\_,{\bf Y}):F(\_,{\bf Y})$ rather than with $\_:F(\_,{\bf Y})$, because the latter is not a valid gringo syntax. We mention this option for completeness sake, since it is available in our implementation. However, we found that the programs generated when using and when not using the anonymous variable are identical after grounding, so we neither discuss it further nor use these rewritings in our experiments.

By default all boolean flags are disabled and the aggregate-form ID is set to $1$ indicating output form (3). At least one input encoding filename must be specified.

The methodology used for discovering whether a rule is a candidate for the aggregate equivalence rewriting is as follows. The given logic program(s) are parsed by the clingo module, generating an abstract syntax tree for each rule. Each such tree is passed to a transformer class for preprocessing. After preprocessing, some information is gathered from the program as a whole; specifically, predicate dependencies are determined, which in turn determine when output forms (5) and (6) are appropriate for a given rule (see the appendix for more details). Rules are then passed individually to an equivalence transformer class for processing. After processing, and if the requested rewriting is possible and confirmed by the user, the rewritten form of the rule is returned. Otherwise the original rule is returned. All returned rules, rewritten or not, are collected and output to the desired output file location. Optionally, the resulting program is then run using clingo.

When a rule is passed to the equivalence transformer for processing, it first undergoes a process of exploration, which traverses the rule’s abstract syntax tree, recording comparison literals between two variables as well as other pertinent information found along the way. These comparison literals are scrutinized to determine whether a subset of the comparisons follows the form given in (2) or some equivalent format as detailed in the section 2.2. The process also identifies those variables that play the role of $X_{\_}1,\ldots,X_{\_}b$ as in (2). The rule is then analyzed to determine whether there are $b$ occurrences of some positive literal of predicate $F$ with the arguments $X_{\_}i$ and $\bf{Y}$, where each $X_{\_}i$, $1\leq i\leq b$, exists at least once in the set of occurrences, and $\bf{Y}$ is the same for each occurrence and contains no variables $X_{\_}1,\ldots,X_{\_}b$. Let us call this set of $b$ literals combined with the corresponding comparisons following the form given in (2) or equivalent, the rule’s counting literals. Similarly, we denote the variables playing the role of the variables $X_{\_}i$ as given in (2) as the rule’s counting variables.

After gathering counting literals and counting variables, the equivalence transformer verifies that the counting variables are not used within literals anywhere in the rule excluding literals within the set of counting literals. If this verification fails or if any of the constraints for the counting literals cannot be satisfied or if no such set of counting variables can be obtained, then the rule is not fit for rewriting. As a result, no rewriting is performed on the rule and the original rule is returned.

In the other case, if the verification succeeds (the counting literals and the counting variables satisfy all the required constraints), then we proceed as follows. If the requested output form is (3/4), then we check whether $|\mathbf{Y}|>0$ and rewrite the rule accordingly using (3) or (4). If the requested output form is (5) or (6), then the predicate dependency condition related to splitting must be verified (see the appendix for details). If it holds, then we check whether $|\mathbf{Y}|>0$ and rewrite the rule into the desired form (5) or (6), adding the second of the two rules in (4) when $|\mathbf{Y}|>0$.

Note that the user is first prompted for confirmation for each rewritten rule before the rule is added to the final program. If the user denies a rewriting, then the original rule is used.

Here we discuss the limitations of the Automated Aggregator in its current form.

1. 1.

   The rewriting is one-directional. The software will only rewrite rules from the form (2) into rules of the forms (3/4), (5), and (6). As it stands, the system will not rewrite rules given in any of the forms (3/4), (5), or (6) into rules of any of other form.

2. 2.

   In the cases when multiple rewritings are possible for a single rule, only one rewriting will be detected and performed. To illustrate, if the form given in (2) occurs twice in one rule over a disjoint set of variables and predicates, where both sets of counting literals consider the other set as part of $G$ and all conditions hold, then only the set of counting literals with the highest number of counting variables will be used for rewriting. If both sets contain the same number of counting variables, then one is chosen based on the order in which the comparisons using those variables occur in the rule.

3. 3.

   There are some cases in which the software will not recognize a valid rewriting when one exists. These cases mostly lie in the many obscure ways of representing a chain of comparisons equivalent to that in (2). However, there are no known cases in which an incorrect rewriting will be proposed when no valid rewriting is possible. More details are given in the software’s README document.

The Automated Aggregator system was applied to logic programs in gringo syntax submitted to the 2009, 2014, and 2015 Answer Set Programming Competitions. Of the 58 encodings given to the application, five contained rules which were candidates for the rewriting described. Table 1 lists the encoding problem names and the ASP Competitions for which they were developed.

Additionally, to provide an example of the functionality of AAgg, the system was applied to an encoding for the Hamiltonian Cycle problem. The original program is shown in Figure 1. The rewritten program, as output by AAgg, is shown in Figure 2. We see that the first two constraints in the program are both rewritten with the necessary projection performed as in (4). Experimental results for these encodings when applied to a generated set of hard instances are given in the following section.

node(X) :- edge(X,Y).
node(X) :- edge(Y,X).

{ hc(X,Y) } :- edge(X,Y).
:- hc(X,Y), hc(X,Z), Y!=Z.
:- hc(X,Y), hc(Z,Y), X!=Z.

reach(X,Y) :- hc(X,Y).
reach(X,Y) :- hc(X,Z), reach(Z,Y).

:- node(X), node(Y), not reach(X,Y).

node(X) :- edge(X,Y).
node(X) :- edge(Y,X).

{ hc(X,Y) } :- edge(X,Y).
:- 2 <= #count{ Y : hc(X,Y) }, hc_project_Z(X).
hc_project_Z(X) :- hc(X,Y).
:- 2 <= #count { X : hc(X,Y) }, hc_project_Z1(Y).
hc_project_Z1(Y) :- hc(X,Y).

reach(X,Y) :- hc(X,Y).
reach(X,Y) :- hc(X,Z), reach(Z,Y).

:- node(X), node(Y), not reach(X,Y).

Results were gathered by systematically grounding and solving each instance-encoding pair within families of encodings for each problem type. The data sets of instances we used are available together with the AAgg tool (see the url listed earlier).⁴⁴4We thank Daniel Houston and Liu Liu for providing us with the data sets of instances for the Latin Square and the Hamiltonian Cycle problems, respectively. The data sets for the remaining problems were generated by software tools we developed for the purpose. These tools and descriptions of instance sets used in experiments can be found at the AAgg site. Each encoding in each family of encodings was run for each instance. The total grounding plus solving time of instance-encoding pairs were recorded and compared.

The precise encodings used as input to the AAgg software for gathering results are listed in Table 2. Two output encodings are generated for each input encoding and together they form the encoding family for that problem domain. The two output forms used were those shown in equations (3/4) and (6); previous experiments showed extreme similarity between forms (3/4) and (5), so (5) was left out to preserve machine time. The machine used for testing contained an Intel(R) Core(TM) i7-7700 CPU @ 3.60GHz with 16GB RAM.

Result statistics are shown in Table 3. Data is grouped by problem domain. The first line of each grouping shows statistics for the input encoding. The second line shows statistics for the encoding output by the AAgg software using the first line as input and the output rule form (3/4) as the selected output form. The third and final line of each grouping shows statistics for the encoding output by the AAgg software again using the first line as input but now selecting the output form (6) as the chosen output form.

A win is when an encoding grounds and solves for an instance in the shortest amount of time as compared with the other two encoding in its grouping. The percentage value beside the win count is the proportion of instances which that encoding won relative to the number of instances in the instance set for which at least one of the three encodings terminated within the total time limit set for grounding and solving. This time limit was set to 200 seconds in all experiments, except those with encodings of the Hamiltonian Cycle problem that used a timeout value of 400 seconds due to the relative difficulty of the instance set (in all problem domains except for the Hamiltonian Cycle domain, the number of instances for which no encoding computed an answer within the time limit was very small; for the Hamiltonian Cycle problem, even with the increased time limit, it was significant).

An exclusive win is when the encoding is the only encoding in its grouping to find a solution (or determine there is no solution) for an instance while both of the other two encodings failed to do so within the time limit. The column shows the number and the percentage of wins which were exclusive wins for the encoding. The next column shows the number and the percentage of wins by a margin of at least 20% (this is when the best encoding runs at least 20% faster than the second one; in case the of exclusive wins, we count a win as by at least 20%, if it is faster by at least 20% than the time limit used). The data in the last column shows the numbers and percentages of wins by at least 50% (it is to be interpreted similarly to the data in the previous column).

Results indicate that in some cases, the rewriting can provide complementary performance of encodings. Specifically, the results for the Wire Routing, Graceful Graphs, and Hamiltonian Cycle problems support the claim. This is shown first by the fact that for each problem, each of the encodings scores a significant proportion of wins, and that among those wins a significant proportion are exclusive wins, and an even greater proportion (about 50% or more) are wins by at least 50%. This means that about half of the times when an encoding outperforms the two other encodings, it outperforms both by a factor of at least two.

The Steiner Tree results indicate that sometimes the rewriting produces little to no effect at all. While each encoding for the problem registers a similar proportion of wins, there are very few instances (just eleven out of 283) when the best encoding outperforms the other two by 20% or more, and no instances when the best encoding would outperform the other two by 50% or more. The Latin Squares results are mixed in the sense that for the most part the original encoding works best. However, one of the rewritings registers almost 20% of wins. Moreover, about 45% of those wins are by 20% or more and 6% by 50% or more.

In summary, we see that the rewriting can provide programs that perform complementary to the original. This complementarity is perhaps somewhat surprising, because aggregates are assumed to lead to better performance. Our results show that the picture is more complicated and whether rewriting with aggregates yields better performance is instance-dependent. It is also interesting to note that for some encodings replacing simple counting, like that used in the Latin Square encodings (no two identical elements in a row or column), with the count aggregates does not lead to substantial improvements. Finally, for some problems (in our experiments for the Steiner Tree problem) where complementary behavior does emerge, the differences in performance are relatively small.