Program Synthesis as Dependency Quantified Formula Modulo Theory
Authors: Priyanka Golia, Subhajit Roy, Kuldeep S. Meel
IJCAI 2021 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | The objective of our experimental evaluation was to study the feasibility of solving BV-constrained synthesis via the state-of-the-art DQBF solvers. To this end, we perform an evaluation over an extensive suite of benchmarks and tools, which we describe in detail below. ... Table 2 represents the instances solved by the virtual best solver for Sy Gu S, BV constrained, and DQBF tools. |
| Researcher Affiliation | Academia | Priyanka Golia1,2 , Subhajit Roy1 , Kuldeep S. Meel2 1Indian Institute of Technology Kanpur 2National University of Singapore |
| Pseudocode | Yes | Algorithm 1: Reducing a single-callsign instance ϕ to DQF(T) ... Algorithm 2: Reducing multiple-callsign to single-callsign instance |
| Open Source Code | Yes | The open source tool De Qu S based on this work is available at https://github.com/meelgroup/De Qu S |
| Open Datasets | Yes | The benchmark suite consisted of instances from two sources: Sy Gu S competition and QBF competition. We use 645 general-track bitvector (BV) theory benchmarks from Sy Gu S competition 2018, 2019 https://sygus.org/ ... Furthermore, we considered 609 QBF benchmarks from QBFEval competition 17,184, disjunctive decomposition and arithmetic set http://www.qbflib.org/index_eval.php |
| Dataset Splits | No | The paper mentions using instances from Sy Gu S and QBF competitions as benchmarks for evaluation but does not specify any training, validation, or test dataset splits explicitly created or used by the authors for their experiments. |
| Hardware Specification | Yes | All our experiments were conducted on a high-performance computer cluster with each node consisting of a E5-2690 v3 CPU with 24 cores and 96GB of RAM, with a memory limit set to 4GB per core. |
| Software Dependencies | No | The paper mentions using Z3, CADET, Manthan, Dep QBF, DCAQE, and DQBDD but does not provide specific version numbers for any of these software dependencies. |
| Experiment Setup | Yes | All tools were run in a single-threaded mode on a single core with a timeout of 900s. ... with a memory limit set to 4GB per core. |