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.
['John Ahlgren', 'Shiu Yin Yuen']
A Constraint Satisfaction Approach to Tractable Theory Induction