skip to main content


Title: Reconciling enumerative and deductive program synthesis
Syntax-guided synthesis (SyGuS) aims to find a program satisfying semantic specification as well as user-provided structural hypotheses. There are two main synthesis approaches: enumerative synthesis, which repeatedly enumerates possible candidate programs and checks their correctness, and deductive synthesis, which leverages a symbolic procedure to construct implementations from specifications. Neither approach is strictly better than the other: automated deductive synthesis is usually very efficient but only works for special grammars or applications; enumerative synthesis is very generally applicable but limited in scalability. In this paper, we propose a cooperative synthesis technique for SyGuS problems with the conditional linear integer arithmetic (CLIA) background theory, as a novel integration of the two approaches, combining the best of the two worlds. The technique exploits several novel divide-and-conquer strategies to split a large synthesis problem to smaller subproblems. The subproblems are solved separately and their solutions are combined to form a final solution. The technique integrates two synthesis engines: a pure deductive component that can efficiently solve some problems, and a height-based enumeration algorithm that can handle arbitrary grammar. We implemented the cooperative synthesis technique, and evaluated it on a wide range of benchmarks. Experiments showed that our technique can solve many challenging synthesis problems not possible before, and tends to be more scalable than state-of-the-art synthesis algorithms.  more » « less
Award ID(s):
1837023
NSF-PAR ID:
10205026
Author(s) / Creator(s):
; ; ;
Date Published:
Journal Name:
Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation
Page Range / eLocation ID:
1159 - 1174
Format(s):
Medium: X
Sponsoring Org:
National Science Foundation
More Like this
  1. Syntax-guided synthesis has been a prevalent theme in various computer-aided programming systems. However, the domain of bit-vector synthesis poses several unique challenges that have not yet been sufficiently addressed and resolved. In this paper, we propose a novel synthesis approach that incorporates a distinct enumeration strategy based on various factors. Technically, this approach weighs in subexpression recurrence by term-graph-based enumeration, avoids useless candidates by example-guided filtration, prioritizes valuable components identified by large language models. This approach also incorporates a bottom-up deduction step to enhance the enumeration algorithm by considering subproblems that contribute to the deductive resolution. We implement all the enhanced enumeration techniques in our SyGuS solver DryadSynth, which outperforms state-of-the-art solvers in terms of the number of solved problems, execution time, and solution size. Notably, DryadSynth successfully solved 31 synthesis problems for the first time, including 5 renowned Hacker's Delight problems. 
    more » « less
  2. Programming-by-example (PBE) is a synthesis paradigm that allows users to generate functions by simply providing input-output examples. While a promising interaction paradigm, synthesis is still too slow for realtime interaction and more widespread adoption. Existing approaches to PBE synthesis have used automated reasoning tools, such as SMT solvers, as well as works applying machine learning techniques. At its core, the automated reasoning approach relies on highly domain specific knowledge of programming languages. On the other hand, the machine learning approaches utilize the fact that when working with program code, it is possible to generate arbitrarily large training datasets. In this work, we propose a system for using machine learning in tandem with automated reasoning techniques to solve Syntax Guided Synthesis (SyGuS) style PBE problems. By preprocessing SyGuS PBE problems with a neural network, we can use a data driven approach to reduce the size of the search space, then allow automated reasoning-based solvers to more quickly find a solution analytically. Our system is able to run atop existing SyGuS PBE synthesis tools, decreasing the runtime of the winner of the 2019 SyGuS Competition for the PBE Strings track by 47.65% to outperform all of the competing tools. 
    more » « less
  3. The “asymmetry” between spatiotemporally varying passenger demand and fixed-capacity transportation supply has been a long-standing problem in urban mass transportation (UMT) systems around the world. The emerging modular autonomous vehicle (MAV) technology offers us an opportunity to close the substantial gap between passenger demand and vehicle capacity through station-wise docking and undocking operations. However, there still lacks an appropriate approach that can solve the operational design problem for UMT corridor systems with MAVs efficiently. To bridge this methodological gap, this paper proposes a continuum approximation (CA) model that can offer near-optimal solutions to the operational design for MAV-based transit corridors very efficiently. We investigate the theoretical properties of the optimal solutions to the investigated problem in a certain (yet not uncommon) case. These theoretical properties allow us to estimate the seat demand of each time neighborhood with the arrival demand curves, which recover the “local impact” property of the investigated problem. With the property, a CA model is properly formulated to decompose the original problem into a finite number of subproblems that can be analytically solved. A discretization heuristic is then proposed to convert the analytical solution from the CA model to feasible solutions to the original problem. With two sets of numerical experiments, we show that the proposed CA model can achieve near-optimal solutions (with gaps less than 4% for most cases) to the investigated problem in almost no time (less than 10 ms) for large-scale instances with a wide range of parameter settings (a commercial solver may even not obtain a feasible solution in several hours). The theoretical properties are verified, and managerial insights regarding how input parameters affect system performance are provided through these numerical results. Additionally, results also reveal that, although the CA model does not incorporate vehicle repositioning decisions, the timetabling decisions obtained by solving the CA model can be easily applied to obtain near-optimal repositioning decisions (with gaps less than 5% in most instances) very efficiently (within 10 ms). Thus, the proposed CA model provides a foundation for developing solution approaches for other problems (e.g., MAV repositioning) with more complex system operation constraints whose exact optimal solution can hardly be found with discrete modeling methods. 
    more » « less
  4. While mixed integer linear programming (MILP) solvers are routinely used to solve a wide range of important science and engineering problems, it remains a challenging task for end users to write correct and efficient MILP constraints, especially for problems specified using the inherently non-linear Boolean logic operations. To overcome this challenge, we propose a syntax guided synthesis (SyGuS) method capable of generating high-quality MILP constraints from the specifications expressed using arbitrary combinations of Boolean logic operations. At the center of our method is an extensible domain specification language (DSL) whose expressiveness may be improved by adding new integer variables as decision variables, together with an iterative procedure for synthesizing linear constraints from non-linear Boolean logic operations using these integer variables. To make the synthesis method efficient, we also propose an over-approximation technique for soundly proving the correctness of the synthesized linear constraints, and an under-approximation technique for safely pruning away the incorrect constraints. We have implemented and evaluated the method on a wide range of benchmark specifications from statistics, machine learning, and data science applications. The experimental results show that the method is efficient in handling these benchmarks, and the quality of the synthesized MILP constraints is close to, or higher than, that of manually-written constraints in terms of both compactness and solving time.

     
    more » « less
  5. Andrei Ciortea ; Mehdi Dastani ; Jieting Luo (Ed.)
    The Multi-Agent Path Finding (MAPF) is a problem of finding a plan for agents to reach their desired locations without colliding. Distributed Multi-Agent Path Finder (DMAPF) solves the MAPF problem by decomposing a given MAPF problem instance into smaller subproblems and solve them in parallel. DMAPF works in rounds. Between two consecutive rounds, agents may migrate between two adjacent subproblems following their abstract plans, which are pre-computed, until all of them reach the areas that contain their desired locations. Previous works on DMAPF compute an abstract plan for each agent without the knowledge of other agents’ abstract plans, resulting in high congestion in some areas, especially those that act as corridors. The congestion negatively impacts the runtime of DMAPF and prevents it from being able to solve dense MAPF problems. In this paper, we (i) investigate the use of Uniform-Cost Search to mitigate the congestion. Additionally, we explore the use of several other techniques including (ii) using timeout estimation to preemptively stop solving and relax a subproblem when it is likely to get stuck; (iii) allowing a solving process to manage multiple subproblems – aimed to increase concurrency; and (iv) integrating with MAPF solvers from the Conflict-Based Search family. Experimental results show that our new system is several times faster than the previous ones; can solve larger and denser problems that were unsolvable before; and has better runtime than PBS and EECBS, which are state-of-the-art centralized suboptimal MAPF solvers, in problems with a large number of agents. 
    more » « less