SAT-Based Strategy Extraction in Reachability Games
Authors: Niklas Een, Alexander Legg, Nina Narodytska, Leonid Ryzhyk
AAAI 2015 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Our experimental results show that our approach performs well on a number of software synthesis benchmarks. Figure 5 summarises our results. For each family, we show strategy generation time as a function of the number of state variables in the speciļ¬cation for 5 hardest instances of the family solved by EVASOLVER. |
| Researcher Affiliation | Academia | Niklas Een UC Berkeley Alexander Legg NICTA and UNSW Australia Nina Narodytska University of Toronto and NICTA Leonid Ryzhyk Carnegie Mellon University |
| Pseudocode | Yes | Algorithm 1 Computing a winning strategy, Algorithm 2 Partitioning winning states, Algorithm 3 Successor set, Algorithm 4 Compiling the winning strategy |
| Open Source Code | No | The paper states "We implemented our strategy generation algorithm as an extension on top of EVASOLVER," but does not provide any concrete access information (e.g., a specific repository link, explicit code release statement, or code in supplementary materials) for the source code of their described methodology. |
| Open Datasets | Yes | We evaluate our implementation on driver synthesis benchmarks from (Narodytska et al. 2014). |
| Dataset Splits | No | The paper evaluates on "driver synthesis benchmarks" but does not provide specific dataset split information (exact percentages, sample counts, citations to predefined splits, or detailed splitting methodology) needed to reproduce the data partitioning into training, validation, and test sets. |
| Hardware Specification | No | The paper does not provide specific hardware details (exact GPU/CPU models, processor types with speeds, memory amounts, or detailed computer specifications) used for running its experiments, only mentioning "We implemented our strategy generation algorithm as an extension on top of EVASOLVER." |
| Software Dependencies | No | The paper mentions software components like "EVASOLVER," "Pe RIPLO (Rollini et al. 2014)," and "BDDs" used with "CUDD (Somenzi 2014)," but does not provide specific version numbers for these ancillary software dependencies needed to replicate the experiment. |
| Experiment Setup | No | The paper does not contain specific experimental setup details such as concrete hyperparameter values, training configurations, or system-level settings in the main text. |