I previously wrote about OOAnalyzer-ASP, an experimental reimagining of the OOAnalyzer tool using Answer Set Programming. I have bad news: I have stopped working on it for now. I am not sure that anyone besides me will really care, but I'll post this here because I will almost certainly forget the details of why I stopped working on it if I don't write them down.

Performance Problems

The ASP implementation I was using, clingo, is a tight integration of a grounder and a solver. The grounder converts the ASP program into the constraint language expected by the solver. The solver is similar to a SAT solver, but is specialized for Answer Set Programming. One of the reasons I was interested in using ASP is that it uses a concept from SAT, conflict-driven clause learning (CDCL), to prune the search space. This is something that is sorely missing in OOAnalyzer, which only explores the search space to a depth of one. I was hoping that CDCL would be able to efficiently tease out facts that had to be true in order for the program to be consistent.

Grounding

Sadly, there were a few problems with this. The first problem is the grounding process itself. To oversimplify, grounding is a process that removes variables from logic programs. Let's say that we have the following logic program:

foo(ed).
bar(X) :- foo(X).

The grounded version of this program would be:

foo(ed).
bar(ed) :- foo(ed).

The challenge with grounding is that it can lead to a combinatorial explosion in the size of the grounded program. And to make a long story short, because class identities in OOAnalyzer are variable, each potential class identity would amount to grounded facts. This was a constant tension, as I was often thinking about the impact on grounding when I was designing the ASP rules.

Large Lemmas

The second performance problem was related to the solver. I found that it worked very well for small programs, but for medium-sized programs, the solver would often stop making progress. It was possible to eek out better solutions by tuning parameters, but it always seemed like it was only exploring a limited portion of the search space.

As clingo runs, it tries to solve a formula saying "find a model that satisfies all of these constraints, and has a model reward/score of at least X". Once X reaches a certain magnitude, this becomes very difficult to solve because a small portion of the search space will score at least X. More problematically, the conditions required to reach X are very complex and interdependent. This too is very impacted by OOAnalyzer's dynamic class identities. At the solver level, when it finds a portion of the search space that is unsatisfiable, it mechanically generates a lemma that describes it to prevent the solver from exploring that portion of the search space again.

In OOAnalyzer-ASP, these lemmas were often huge, which means that they were very specific to the particular model being solved. At a high level, they might say that "if you have a class consisting of exactly these methods, then you can't have a reward of X", rather than a more general lemma that says "if method A and B are on different classes, you can't have a reward of X". What is supposed to happen is that over time, the lemmas accumulate and new lemmas become smaller and more general, until the lemmas cover the entire search space.

The problem is that solvers remove lemmas over time to speed up the search process. At a certain point, this is at tension with the overall learning process. If lemmas are removed before the smaller, more general lemmas are learned, then the solver will have to re-learn the same lemmas over and over again. It stops making progress. This is what was happening in OOAnalyzer-ASP. I think it is probably possible to tune the solver to avoid this, but the next problem in OOAnalyzer-ASP was more pressing.

Articulation Challenges

The second major problem with OOAnalyzer-ASP was that it was difficult to adequately express some properties in ASP. More specifically, as I was fighting the above performance problems, I would often convince the solver to find a model with a better score. Unfortunately, when I actually compared the better scoring model with the ground truth, it would often be slightly worse. It was very difficult to actually construct the model scoring to reflect reality.

One of the reasons for this has to do with fixed points. OOAnalyzer represents classes as sets of methods that are iteratively merged. In Prolog, it is possible to reason about the membership of the current class at each step of the iteration. For example, OOAnalyzer has a few rules that are conditioned on one class only containing a single class. In ASP, class membership is represented as a fixed point, which means that class properties must be monotonic over merging. There is not an easy way to express the fact that a class only contains a single method at some point in time, because the rules can only reason about the final fixed point.

Imagine you had a program like this:

merge(A,B) :- class(A), class(B), hasAConstructor(A), hasADestructor(B), size(B) = 1.

In ASP, after merging A and B, size(B) = 1 would become false, and this line of reasoning would vanish.

In theory, it is possible to represent the entire history of the merging process in ASP by modeling the entire sequence of merges, but this would further compound the grounding performance problem!

Conclusion

I don't think that OOAnalyzer-ASP is a complete dead-end, but it's not the slam dunk I was hoping it would be.

As part of this process, I also spent a lot of time looking at the mistakes OOAnalyzer and OOAnalyzer-ASP made. There is less room for improvement than I expected. That doesn't mean that OOAnalyzer is perfect, but rather, after looking at the available evidence, I am not sure how as a human to do much better. I honestly expected that OOAnalyzer's limited searching ability would have a larger impact than it does.