Sat, 27 Jul 2024

IMPACT AND IMPROVEMENTS OF QUICKXPLAIN

As I had been transferred into the rules RnD team for the new impossible challenge in 2004, things became more complicated as far as scientific work was concerned. This team has been proud of their Java programming skills and attended developer conferences such as JavaOne, but did not follow scientific AI conferences such as AAAI and IJCAI. However, they understood that some problems such as rule analysis may require new scientific results.

In this new environment, I continued my personal project on preferences in my spare time. I even managed to participate in two research projects on preferences in addition to the work on rule analysis. These projects consisted of a European COST action and a French ANR project. Both research projects have been excellent and inspiring. They allowed me to produce a lot of new ideas, but I could only publish workshop papers. The new work environment simply did not allow me to take the time for preparing conference or journal papers. We can say that I filled a time capsule with ideas and thus created a reserve for future work.

In this time, QuickXplain gained in importance even if I didn’t do anything to promote this work. Other researchers adopted it and advocated it in different scientific communities. Gerhard Friedrich and Barry O’Sullivan have been among the first adopters and became fans of Quickxplain. They and their colleagues continued the work that I was not able to continue for the sheer amount of constraints that took over my personal and professional life. In Spring 2009, Barry O’Sullivan told me that he has recommended QuickXplain to Daniel LeBerre. Thanks to this recommendation, QuickXplain found its way into SAT4J and thus into the eclipse p2 package manager. Daniel LeBerre was really happy about QuickXplain as he told me somewhat later.

Based on success stories like this, QuickXplain became a reference for many researchers working on explanations of failure for different kinds of constraints as well as logical theories. It has been used for finding conflicting requirements in product configuration and in knowledge-based recommender systems, for debugging ontological knowledge bases, and for finding infeasible constraints in mathematical programming. Furthermore, it is also useful for methods that use an explanation-based constraint generalization mechanism. One notable example is cut generation in logical Benders decomposition, the other one is invariant generation in program verification. Due to this broad set of applications, QuickXplain has also found attention outside AI communities. Even famous computer science researchers such as Zohar Manna took note of it.

In 2009, the no-longer optimization company got acquired. This changed the rules of business and the scientific part of my job role vanished over night as if it had never existed, leaving only the engineering part. It’s the same effect as when light hits glass. Part of it does not enter the glass and gets reflected, the other part enters the glass and gets refracted. This change was completely disruptive as far as my carrier was concerned. As my life has been quite constrained at that time, I had no other choice than putting my research on hold.

After this time, improvements of QuickXplain showed up. QuickXplain works fine for finding conflicts that contain a fraction of the constraints, but leads to overhead if all or nearly all constraints belong to a minimal conflict. It may double the number of solver calls compared to the sequential explanation detection method. A simple idea to remedy this behavior consists in switching to the sequential method for subproblems smaller than a threshold.

In 2013, João Marques Silva and colleagues came up with an iterative algorithm, which reproduces the effect of QuickXplain in the good cases and has only negligible overhead over the sequential method in the difficult cases. Philippe Laborie had the same idea independently. In 2020, Patrick Rodler published a correctness proof for QuickXplain. The AAAI 2004 paper on QuickXplain already gave a proof invariant, but did not include a correctness proof.

Given all these improvements and refinements, I personally find it very satisfactory that the publication of QuickXplain had an impact on the work of other researchers. When I was asked to give a talk about QuickXplain at a session at Roadef 2019, I took this occasion to discuss some of this newer work as well. ►