Super-Solutions
Cristian Molinaro, Amy L. Sliva, V. S. Subrahmanian · ACM Transactions on Computational Logic · 2014
Annotated Probabilistic Temporal (APT) logic programs are a form of logic programs that allow users to state (or systems to automatically learn) rules of the form “formula G becomes true Δ t time units after formula F became true with ℓ to u % probability.” In this article, we deal with abductive reasoning in APT logic: given an APT logic program Π, a set of formulas H that can be “added” to Π, and a (temporal) goal g , is there a subset S of H such that Π ∪ S is consistent and entails the goal g ? In general, there are many different solutions to the problem and some of them can be highly repetitive, differing only in some unimportant temporal aspects. We propose a compact representation called super-solutions that succinctly represent sets of such solutions. Super-solutions are compact, but lossless representations of sets of such solutions. We study the complexity of existence of basic, super-, and maximal super-solutions as well as check if a set is a solution/super-solution/maximal super-solution. We then leverage a geometric characterization of the problem to suggest a set of pruning strategies and interesting properties that can be leveraged to make the search of basic and super-solutions more efficient. We propose correct sequential algorithms to find solutions and super-solutions. In addition, we develop parallel algorithms to find basic and super-solutions.