Efficient program synthesis using constraint satisfaction in inductive logic programming

被引:231
作者
Ahlgren, John [1 ]
Yuen, Shiu Yin [1 ]
机构
[1] Department of Electronic Engineering, City University of Hong Kong, Hong Kong
关键词
Boolean satisfiability problem; Constraint satisfaction; Inductive logic programming; Program synthesis; Theory induction;
D O I
10.1145/800157.805047
中图分类号
学科分类号
摘要
We present NrSample, a framework for program synthesis in inductive logic programming. NrSample uses propositional logic constraints to exclude undesirable candidates from the search. This is achieved by representing constraints as propositional formulae and solving the associated constraint satisfaction problem. We present a variety of such constraints: pruning, input-output, functional (arithmetic), and variable splitting. NrSample is also capable of detecting search space exhaustion, leading to further speedups in clause induction and optimality. We benchmark NrSample against enumeration search (Aleph's default) and Progol's A* search in the context of program synthesis. The results show that, on large program synthesis problems, NrSample induces between 1 and 1358 times faster than enumeration (236 times faster on average), always with similar or better accuracy. Compared to Progol A*, NrSample is 18 times faster on average with similar or better accuracy except for two problems: one in which Progol A* substantially sacrificed accuracy to induce faster, and one in which Progol A* was a clear winner. Functional constraints provide a speedup of up to 53 times (21 times on average) with similar or better accuracy. We also benchmark using a few concept learning (non-program synthesis) problems. The results indicate that without strong constraints, the overhead of solving constraints is not compensated for. © 2013 John Ahlgren and Shiu Yin Yuen.
引用
收藏
页码:3649 / 3681
页数:32
相关论文
共 26 条
  • [1] Blackburn P., Bos J., Striegnitz K., Learn Prolog Now!, (2006)
  • [2] Camacho R., Inducing Models of Human Control Skills Using Machine Learning Algorithms, (2000)
  • [3] Cook S.A., The complexity of theorem-proving procedures, Proceedings of the Third Annual ACMSymposium on Theory of Computing, STOC '71, pp. 151-158, (1971)
  • [4] Davis M., Logemann G., Loveland D., A machine program for theorem-proving, Communications of the ACM, 5, pp. 394-397, (1962)
  • [5] De Raedt L., Ramon J., Condensed representations for inductive logic programming, Proceedings of the 9th International Conference on Principles of Knowledge Representation and Reasoning, pp. 438-446, (2004)
  • [6] Dowling W.F., Gallier J.H., Linear-time algorithms for testing the satisfiability of propositional horn formulae, Journal of Logic Programming, 1, 3, pp. 267-284, (1984)
  • [7] Flener P., Yilmaz S., Inductive synthesis of recursive logic programs: Achievements and prospects, Journal of Logic Programming, 41, pp. 141-195, (1999)
  • [8] Flener P., Lau K., Ornaghi M., Richardson J., An abstract formalization of correct schemas for program synthesis, Journal of Symbolic Computation, 30, 1, pp. 93-127, (2000)
  • [9] Fonseca N.A., Costa V.S., Silva F.M.A., Camacho R., On avoiding redundancy in inductive logic programming, ILP, pp. 132-146, (2004)
  • [10] Maloberti J., Sebag M., Fast theta-subsumption with constraint satisfaction algorithms, Machine Learning, 55, 2, pp. 137-174, (2004)