On-line algorithms for satisfiability problems with uncertainty

In this paper the problem of the on-line satisfiability of a Horn formula with uncertainty is addressed; we show how to represent a significant class of formulae by weighted directed hypergraphs and we present two algorithms that solve the on-line Horn-SAT problem and find a minimum model for the formula working on the dynamic weighted hypergraph representation. These algorithms make increasing assumptions on the formula and we find that the second one solves the on-line Horn-SAT problem with a total time linear in the size of the formula, matching the optimal result for Boolean Horn formulae.