Source-linked AI summary
SyGuS-Comp 2016: Results and Analysis
Rajeev Alur, Dana Fisman, Rishabh Singh, Armando Solar-Lezama
TL;DR
SyGuS-Comp addresses the need to evaluate synthesis techniques under both semantic specifications and grammar restrictions. The paper analyzes the 2016 competition, including its new Programming By Examples track and solver results across benchmark categories. EUSOLVER solved 787 of 858 PBE benchmarks, while the competition overall showed substantial progress over its first iteration.
Problem
SyGuS-Comp provides an objective basis for comparing algorithms that synthesize programs satisfying logical specifications within grammar-defined spaces.
Method
The paper describes the 2016 benchmarks, solver strategies, specialized tracks, and comparative competition analyses, including the new Programming By Examples track.
Results
EUSOLVER solved 787 of 858 Programming By Examples benchmarks, while the combined-track results identify EUSOLVER as solving the highest percentage overall.
Takeaways & Limitations
The competition facilitated objective comparison and revealed algorithmic strengths across synthesis tracks while showing substantial progress over earlier competitions.
Abstract
from arXiv · showhide
Syntax-Guided Synthesis (SyGuS) is the computational problem of finding an implementation f that meets both a semantic constraint given by a logical formula $\varphi$ in a background theory T, and a syntactic constraint given by a grammar G, which specifies the allowed set of candidate implementations. Such a synthesis problem can be formally defined in SyGuS-IF, a language that is built on top of SMT-LIB. The Syntax-Guided Synthesis Competition (SyGuS-Comp) is an effort to facilitate, bring together and accelerate research and development of efficient solvers for SyGuS by providing a platform for evaluating different synthesis techniques on a comprehensive set of benchmarks. In this year's competition we added a new track devoted to programming by examples. This track consisted of two categories, one using the theory of bit-vectors and one using the theory of strings. This paper presents and analyses the results of SyGuS-Comp'16.
1 Introduction
SyGuS-Comp provides a standardized basis for comparing synthesis algorithms, where solvers find grammar-constrained programs satisfying logical specifications. The 2016 competition extended this framework with specialized tracks and new solver evaluations, including programming by examples.
- Competition purpose: SyGuS-Comp compares synthesis approaches by requiring a grammar-expressible implementation that makes a logical specification valid.The specification is given in a background theory, while the grammar defines the permitted program space.
- Formalism and tracks: The SyGuS format extends SMT-LIB with grammars and supports specialized problem classes including invariant synthesis and integer linear arithmetic.The 2016 competition also included dedicated invariant-synthesis and PBE tracks.
- Applications: SyGuS has supported applications including motion planning, compiler optimization, and cybersecurity, with one generated circuit using 13 gates versus 41 in a handcrafted mitigation circuit.The generated circuit also had a 3-unit-delay critical path versus 6 unit delays for the handcrafted and original circuits.
- General Track: In the general track, benchmark instances combine logical constraints with grammars that restrict synthesized functions to permitted operations.The QCC example uses integer constants, arithmetic, and a conditional primitive to synthesize loop-decrement functions.
- Invariant Synthesis Track: Invariant-synthesis instances expose preconditions, transitions, and postconditions so solvers can synthesize an invariant satisfying the full verification condition.The specialized format represents primed variables and packages the invariant obligation through inv-constraint.
- Programming By Examples Track: The 2016 competition added a Programming By Examples track alongside new submissions from CVC4-1.5.1 and EUSolver.The paper reports benchmark categories, solver strategies, and competition results for the third iteration.
2 Competition Settings
The 2016 competition expanded evaluation with a PBE track covering string and bitvector transformations, alongside new solver submissions and standardized resource-controlled validation. Its benchmarks used domain-specific grammars, including generated compositions of minimal k-nuggets for harder bitvector tasks.
- Participating Benchmarks: The PBE track added 858 benchmarks across 108 string-transformation and 750 bitvector-transformation tasks.The bitvector total combines 450 benchmarks from the 2013 ICFP Programming Competition with 300 additional submissions.
- Participating Benchmarks: String benchmarks encode spreadsheet-style transformations through concatenated constants and substrings, with -long variants containing 100 examples and -repeat variants repeating input-output examples.The grammar uses string operations such as concatenation and substring extraction; it currently excludes loops and regular-expression constructs.
- Participating Benchmarks: Bitvector benchmarks were generated by composing sampled k-nuggets, whose minimality reduces the chance that a smaller equivalent DSL expression solves the resulting programs.The DSL provides the constants needed for each desired transformation.
- Participating Solvers: CVC4-1.5.1 and EUSolver were the two new submissions, and both participated in all four tracks.The competition also included seven solvers from the previous year, with six competing in General, five in Invariant Synthesis, and five in CLIA.
- Participating Solvers: CVC4-1.5.1 combines refutation-based synthesis with single-invocation and syntax-guided strategies, while EUSolver combines enumeration, unification, predicates, and decision-tree learning.CVC4-1.5.1 introduced improvements to both its single-invocation recognition and syntax-guided restriction mechanisms; EUSolver supports specialized generation and unification algorithms.
- Evaluation Setup: Runs used StarExec with 128GB memory and a 3600-second wallclock limit, and post-processors checked both grammar adherence and semantic correctness.The dedicated cluster had 12 nodes, each with two 4-core 2.4GHz processors and 256GB RAM; semantic checking invoked an SMT solver.
3 Competition Results and Analysis
Across SyGuS-Comp'16, EUSOLVER achieved the strongest combined benchmark coverage, while solver leadership varied by track, category, speed, and expression size. The new PBE track showed the largest performance gap, with EUSOLVER solving nearly all bit-vector and many string benchmarks.
- Overall results: EUSOLVER solved the highest percentage of benchmarks across all four tracks, followed by CVC4-1.5.1.The combined result sums solver coverage across categories.
- Evaluation criteria: The competition ranked tracks primarily by solved-benchmark count and additionally analyzed solve-time buckets, expression-size buckets, and uniquely solved benchmarks.Benchmark-level figures encode solver counts, time ranges, expression-size ranges, fastest solvers, and smallest expressions.
- General Track: EUSOLVER solved 206 of 309 General-track benchmarks, while CVC4-1.5.1 solved 195 and the previous CVC4-1.5 solved 179.EUSOLVER also solved 59 benchmarks uniquely, compared with 22 for CVC4-1.5.1.
- Conditional Linear Arithmetic Track: CVC4-1.5.1 solved all 73 Conditional Linear Integer Arithmetic benchmarks, compared with 72 for EUSOLVER and 70 for CVC4-1.5.CVC4-1.5.1 also solved 72 benchmarks among the fastest, versus 33 for EUSOLVER.
- Invariant Synthesis Track: ICE-DT led invariant synthesis by solving 57 of 67 benchmarks, while CVC4-1.5.1 solved 56 and was fastest on 50.ICE-DT solved 44 benchmarks among the fastest, and its two uniquely solved benchmarks were the only unique solutions in this comparison.
- Programming By Example Track: EUSOLVER solved 787 of 858 PBE benchmarks, including 742 of 745 bit-vector and 45 of 108 string tasks, while CVC4-1.5.1 solved 39.EUSOLVER solved 751 benchmarks uniquely; no other solver solved more than one PBE problem, and CVC4-1.5.1 solved four uniquely.
- Category analysis: General-track category winners were distributed across solvers: CVC4-1.5.1 won four categories, while ENUMERATIVE and EUSOLVER each won three.CVC4-1.5.1 led Arrays, Let & Motion Planning, Hackers’ Delight, and Integers; ENUMERATIVE led three invariant/compiler categories; EUSOLVER led Multiple Functions and ICFP.
- General-track observations: CVC4-1.5.1 was fastest on more General-track benchmarks, whereas CVC4-1.5.1 and EUSOLVER produced much larger average expressions than several other solvers.The reported averages were 31580.5 for CVC4-1.5.1 and 30595.7 for EUSOLVER, versus 11.9 to 17.1 for ENUMERATIVE, SKETCH-AC, and STOCHASTIC; the comparison is qualified as unfair because the former solvers solved more benchmarks.
4 Discussion
Across three years, SyGuS-Comp expanded from a single General track to multiple tracks, adding PBE in 2016 alongside new solvers. The 2016 competition solved a much higher fraction of General-track benchmarks than the first competition and addressed many previously challenging instances.
- Progress across competitions: A much higher fraction of General-track benchmarks was solved in the third competition than in the first.
- Progress across competitions: Many benchmarks that were challenging in earlier competitions were solved by newer solvers.