Delete/Rederive with Marking for Update Streams
摘要
Given a set of facts and inference rules, a materialized dataset is obtained by extending the facts with all logical consequences w.r.t. the rules. Classically, sequential updates of a materialized dataset are processed separately without any direct interference. Effectively dealing with streams of updates where changes may occur in large numbers and high frequencies, however, demands a more sophisticated approach that is able to consider several updates at once, such that we may perform computations in parallel or prevent their repetition to accelerate the overall processing. Driven by this goal, we extend the classical Delete/Rederive (DRed) algorithm with marking: while processing one update, we directly consider also the next update and mark each fact in the dataset that is added or deleted by the latter. A marked fact that is used in a derivation may then conditionally mark the derived fact to indicate that it will change in the next update too. The proposed approach allows for reducing the overall number of applied rules by directly performing some of the computations that are relevant for the next update before it is actively processed. We show the correctness of the algorithm and provide a prototypical implementation that we evaluate for both synthetic and real data. The evaluation demonstrates a reduction of needed CPU time by about 25% in average compared to classical DRed.