Stochastic Local Search for Satisfiability Modulo Theories
Authors: Andreas Fröhlich, Armin Biere, Christoph Wintersteiger, Youssef Hamadi
AAAI 2015 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Experimental results show that our approach can compete with state-of-the-art bit-vector solvers on many practical instances and, sometimes, outperform existing solvers. To evaluate the performance of our algorithm, we ran experiments on two different sets of benchmarks. |
| Researcher Affiliation | Collaboration | Andreas Fr ohlich and Armin Biere Johannes Kepler University Christoph M. Wintersteiger and Youssef Hamadi Microsoft Research |
| Pseudocode | Yes | Figure 1: Pseudo-Code of our SLS architecture for SMT. |
| Open Source Code | No | The paper does not provide any explicit statement or link regarding the availability of its own source code. |
| Open Datasets | Yes | The first benchmark family is the QF BV benchmark set, which can be found in the SMT-LIB and is also part of the SMT Competition. A second benchmark family is given by the SAGE2 benchmark set. Those problems were generated as part of the SAGE project at Microsoft (Godefroid, Levin, and Molnar 2008). |
| Dataset Splits | No | The paper describes the selection of instances for evaluation ('removed all those which Z3 proved to be unsatisfiable within 1200 seconds. From the remaining 11715 instances, we further filtered out those 4543 formulas, that were shown to be satisfiable only by using pre-processing techniques.'), but does not specify distinct training, validation, or testing splits in terms of data partitioning for model training. |
| Hardware Specification | Yes | All experiments were run on a Windows HPC cluster of dual Quad-Xeon (E54xx) machines, 16 GB RAM, and used a time limit of 1200 seconds. |
| Software Dependencies | No | The paper mentions various comparison solvers (e.g., 'most recent version of the state-of-the-art SMT solver Z3') and tools used for preprocessing (e.g., 'bit-blasting component of Z3'), but does not provide specific version numbers for the software dependencies directly used in the implementation of their own BV-SLS algorithm or other ancillary software components. |
| Experiment Setup | Yes | For all benchmarks, we used the default configuration of BV-SLS: All variables are initialized to 0, candidate selection occurs using the UCB scheme, constants are set to c1 = 0.5, c2 = 20, c3 = 0.025, c4 = 100, wp 0.1, sp 0.05, and it uses the extended neighbourhood relation that additionally allows increment by 1, decrement by 1, and bitwise negation. |