Résumé
One of the major benefits of symbolic AI is explainability. When new knowledge is obtained via a reasoning process, it is possible to determine precisely all elements of the knowledge base that yield this knowledge. Typically, one would use a SAT solver to compute the explanations. However, SAT-solving is computationally expensive, and as the knowledge base grows, the time required increases exponentially. This work presents a method for filtering a datalog knowledge base to optimise the time used by a SAT solver. This is achieved by creating a hypergraph representing the grounded knowledge base and pruning the nodes that are not reachable from the fact that we want to explain. This approach proves to be time-effective. Interestingly, one additional benefit of using this hypergraph is that it is possible to encode more information about the rules used in the reasoning process. By using an off-the-shelf group-SAT solver, this extra information allows us to find specific explanations that would be missed if we only considered facts.