Efficient Consequence Finding

We present an extensive experimental study of consequence-finding algorithms based on kernel resolution, using both a trie-based and a novel ZBDD-based implementation, which uses Zero- Suppressed Binary Decision Diagrams to concisely store and process very large clause sets. Our study considers both the full prime implicate task and ap- plications of consequence-finding for restricted tar- get languages in abduction, model-based and fault- tree diagnosis, and polynomially-bounded knowl- edge compilation. We show that the ZBDD imple- mentation can push consequence-finding to a new limit, solving problems which generate over clauses.