Unifying Decision and Function Queries in Stochastic Boolean Satisfiability
Authors: Yu-Wei Fan, Jie-Hong R. Jiang
AAAI 2024 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | To evaluate the SSAT(Θ) solver, experiments were conducted to study the applicability in solving application benchmarks and to investigate the effect of the threshold quantifier on solving efficiency. The experiments were conducted on a Linux machine with 2.2 GHz Intel Xeon CPU and 128 GB RAM. Two benchmark sets were experimented for evaluation. |
| Researcher Affiliation | Academia | Yu-Wei Fan1, Jie-Hong R. Jiang1,2 1Graduate Institute of Electronics Engineering, National Taiwan University, Taipei, Taiwan 2Department of Electrical Engineering, National Taiwan University, Taipei, Taiwan |
| Pseudocode | Yes | Algorithm 1: SSAT(Θ) Evaluation |
| Open Source Code | Yes | 1Available at https://github.com/NTU-ALCom Lab/Clau SSat Theta. |
| Open Datasets | Yes | The first set includes instances from the case study of parameter synthesis on the DTMC Crowds (Shmatikov 2004). The second set includes instances converted from SSAT formulas, taken from (Chen, Huang, and Jiang 2021). |
| Dataset Splits | No | The paper mentions using 'Two benchmark sets were experimented for evaluation' and refers to existing benchmarks, but it does not provide specific details on how the data was split into training, validation, or test sets. |
| Hardware Specification | Yes | The experiments were conducted on a Linux machine with 2.2 GHz Intel Xeon CPU and 128 GB RAM. |
| Software Dependencies | No | We implemented our SSAT(Θ) solver, named Clau SSat(Θ), in the C++ language by extending Clau SSat (Chen, Huang, and Jiang 2021). A DTMC model was first specified in the prism model format (Kwiatkowska, Norman, and Parker 2002), then converted to a transition relation in a bit-vector form of the QF-BV SMT format, then further bit-blasted using the SMT solver Boolector (Niemetz, Preiner, and Biere 2014). The paper mentions C++ and names other tools but does not provide specific version numbers for the software dependencies required to reproduce their solver's environment. While Boolector's version (2.0) is in its citation, it's not directly stated as a required dependency with that version for their solver. |
| Experiment Setup | Yes | A 1000-second time limit was imposed on solving each instance. In the experiment, we checked safe0 under m = 5. A DTMC model was first specified in the prism model format (Kwiatkowska, Norman, and Parker 2002), then converted to a transition relation in a bit-vector form of the QF-BV SMT format, then further bit-blasted using the SMT solver Boolector (Niemetz, Preiner, and Biere 2014). |