A Constraint Satisfaction Approach to Tractable Theory Induction

摘要

A novel framework for combining logical constraints with theory induction in Inductive Logic Programming is presented. The constraints are solved using a boolean satisfiability solver (SAT solver) to obtain a candidate solution. This speeds up induction by avoiding generation of unnecessary candidates with respect to the constraints. Moreover, using a complete SAT solver, search space exhaustion is always detectable, leading to faster small clause/base case induction. We run benchmarks using two constraints: input-output specification and search space pruning. The benchmarks suggest our constraint satisfaction approach can speed up theory induction by four orders of magnitude or more, making certain intractable problems tractable.