Linear Arithmetic Satisfiability via Strategy Improvement
Authors: Azadeh Farzan, Zachary Kincaid
IJCAI 2016 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Experimental results demonstrate that the proposed procedure is competitive with existing solvers. We evaluated SIMSAT on a suite of benchmarks drawn from SMT-LIB2 [Barrett et al., 2010] and Mjollnir [Monniaux, 2010]. |
| Researcher Affiliation | Academia | Azadeh Farzan University of Toronto azadeh@cs.toronto.edu Zachary Kincaid Princeton University zkincaid@cs.princeton.edu |
| Pseudocode | Yes | Algorithm 1: Check if a strategy has a counter-strategy; Algorithm 2: Counter-strategy synthesis; Algorithm 3: Satisfiability modulo LRA |
| Open Source Code | No | The paper states, 'We have implemented Algorithm 3 in a prototype tool called SIMSAT,' but it does not provide a specific link or explicit statement about the source code being open or publicly available. |
| Open Datasets | Yes | We evaluated SIMSAT on a suite of benchmarks drawn from SMT-LIB2 [Barrett et al., 2010] and Mjollnir [Monniaux, 2010]. |
| Dataset Splits | No | The paper discusses 'industrial benchmarks' and 'random benchmarks' for evaluation but does not specify any train, validation, or test dataset splits (e.g., percentages or sample counts). |
| Hardware Specification | Yes | The experimental evaluation was performed on a Linux machine with Intel Core i5 2.80GHz processors and 4GB of memory. |
| Software Dependencies | No | The paper mentions that the tool 'is implemented in OCaml and uses Z3 to solve ground formulas,' but it does not provide specific version numbers for OCaml or Z3. |
| Experiment Setup | No | The paper mentions a 'time limit was set to 300 seconds' for experiments but does not provide specific details on hyperparameters, model initialization, or other training configurations. |