Created by W.Langdon from gp-bibliography.bib Revision:1.6561
The key contribution of this dissertation is a new approach to program synthesis that combines the strengths of a counterexample-guided inductive synthesizer with those of a theory solver, exploring the solution space more efficiently without relying on user guidance. We call this approach CEGIS(T), where T is a first-order theory. Notably, since the publication of CEGIS(T), a variant of the algorithm has been implemented inside leading synthesis solver CVC4. CEGIS(T) is as complete (or incomplete) as CEGIS, and it does not affect worst-case run-time complexity considerations.
In combination with the development of CEGIS(T ), we introduced several algorithmic improvements that enhance both the performance of CEGIS(T ) and the baseline CEGIS algorithm. The first of these improvements is a significant change to the way we encode the synthesis problem for the SAT-based synthesis component of CEGIS in order to produce smaller formulae that can be more efficiently solved by SAT and SMT solvers. The second of these improvements is the use of incremental satisfiability solving in the synthesis component of CEGIS. Incremental satisfiability solving allows the SAT solver to re-use clauses learnt in previous CEGIS iterations, thus reducing the time per synthesis iteration.
We evaluate our contributions on a set of benchmarks taken from the Syntax Guided Synthesis Competition, and note that CEGIS(T ) is able to solve benchmarks which elude a standard implementation of CEGIS, specifically benchmarks that contain non-trivial constants. We find that the novel proposed encoding provides a substantial speed-up on all the benchmarks that require synthesising a program of length greater than one instruction. The use of incremental first-order solving in CEGIS decreases the solving time in some cases but not all, and we hypothesise that these are the benchmarks on which SAT-solver pre-processing is less important.",
Supervisor: Alessandro Abate",
Genetic Programming entries for Elizabeth Polgreen