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 ZeroSuppressed Binary Decision Diagrams to concisely store and process very large clause sets. Our study considers both the full prime implicate task and applications of consequence-finding for restricted target languages in abduction, model-based and faulttree diagnosis, and polynomially-bounded knowledge compilation. We show that the ZBDD implementation can push consequence-finding to a new limit, solving problems which generate over 1070 clauses.

• Type: Conference
• Year: 2001
• Where: IJCAI
• Authors: Laurent Simon, Alvaro del Val
• Keywords: Binary Decision Diagrams, IJCAI 2001, IJCAI 2007, Large Clause Sets, Prime Implicate Task