2020/01/06 by Patrick Rodler, Rodler, Patrick · 1 citation
Computer Science · #Semantic Web and Ontologies #Constraint Satisfaction and Optimization #Advanced Database Systems and Queries
paper · pdf · doi:10.48550/arxiv.2001.01835
In his seminal paper of 2004, Ulrich Junker proposed the QuickXPlain\nalgorithm, which provides a divide-and-conquer computation strategy to find\nwithin a given set an irreducible subset with a particular (monotone) property.\nBeside its original application in the domain of constraint satisfaction\nproblems, the algorithm has since then found widespread adoption in areas as\ndifferent as model-based diagnosis, recommender systems, verification, or the\nSemantic Web. This popularity is due to the frequent occurrence of the problem\nof finding irreducible subsets on the one hand, and to QuickXPlain's general\napplicability and favorable computational complexity on the other hand.\n However, although (we regularly experience) people are having a hard time\nunderstanding QuickXPlain and seeing why it works correctly, a proof of\ncorrectness of the algorithm has never been published. This is what we account\nfor in this work, by explaining QuickXPlain in a novel tried and tested way and\nby presenting an intelligible formal proof of it. Apart from showing the\ncorrectness of the algorithm and excluding the later detection of errors (proof\nand trust effect), the added value of the availability of a formal proof is,≠.g., (i) that the workings of the algorithm often become completely clear only\nafter studying, verifying and comprehending the proof (didactic effect), (ii)\nthe shown proof methodology can be used as a guidance for proving other\nrecursive algorithms (transfer effect), and (iii) the possibility of providing\n"gapless" correctness proofs of systems that rely on (results computed by)\nQuickXPlain, such as numerous model-based debuggers (completeness effect).\n