Decremental maintenance of reachability in hypergraphs and minimum models of Horn formulae

In this paper we present a decremental algorithm for maintaining minimum rank hyperpaths in a directed hypergraph from a source vertex s to all other vertices, under the assumption of unit hyperedge weights. Given a hypergraph H with n vertices and m hyperedges, the total time needed to perform a sequence of m hyperedge deletions is O(n . Size(H)), where Size(H) is the sum of the sizes of the hyperedges of H; the total space needed is O(n + Size(H)). In the case of integer hyperedge weights in [1, C] our solution requires O(C . n . Size(H)) total time and O(C + n + Size(H)) space. Using the algorithm presented in this paper, we also show how to maintain the satisfiability and the minimum model of a Horn formula F with n propositional symbols in total time O(n . Length(F)) over any sequence of clause deletions.