Notice: The reproducibility variables underlying each score are classified using an automated LLM-based pipeline, validated against a manually labeled dataset. LLM-based classification introduces uncertainty and potential bias; scores should be interpreted as estimates. Full accuracy metrics and methodology are described in Coakley et alK. L. Coakley, T. Snelleman, H. Hoos, and O. E. Gundersen, "The embrace of open science: An analysis of a decade of AI research and 56 800 conference papers," Under Review, 2026..
Solving Exist-Random Quantified Stochastic Boolean Satisfiability via Clause Selection
Authors: Nian-Ze Lee, Yen-Shi Wang, Jie-Hong R. Jiang
IJCAI 2018 | Venue PDF | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Experiments show that the proposed algorithm achieves significant performance gains and memory savings over the state-of-the-art SSAT solvers on a number of benchmark formulas, and provides useful lower bounds for cases where prior methods fail to compute exact answers. |
| Researcher Affiliation | Academia | 1Graduate Institute of Electronics Engineering, National Taiwan University, Taipei, Taiwan 2Department of Electrical Engineering, National Taiwan University, Taipei, Taiwan |
| Pseudocode | Yes | Figure 1: E-MAJSAT solving with clause containment learning. |
| Open Source Code | Yes | A prototyping program1 of the proposed algorithm Solve EMAJSAT was implemented... 1Available at https://github.com/nianzelee/ssat ABC.git |
| Open Datasets | Yes | The random k-CNF formulas were generated by the cnfgen package [Lauria, 2012]. We collected seven families of application formulas for evaluation. The first two families, Toilet-A and Conformant, are exist-forall-exist quantified QBFs from [Giunchiglia et al., 2005]. The third family Sand-Castle is a probabilistic conformant planning problem, which was encoded as an E-MAJSAT formula in [Majercik and Littman, 1998]. The fourth, fifth, and sixth families are taken from [Fremont et al., 2017]... The last family is taken from [Lee and Jiang, 2014]... |
| Dataset Splits | No | The paper does not explicitly provide training/test/validation dataset splits. It evaluates on benchmark formulas, but does not describe a data splitting methodology for reproducibility. |
| Hardware Specification | Yes | The experiments were conducted on a Linux machine with an Intel Xeon 2.1 GHz CPU and 126 GB RAM. |
| Software Dependencies | Yes | A prototyping program1 of the proposed algorithm Solve EMAJSAT was implemented in the ABC [Mishchenko, 2005] environment with SAT solver Minisat-2.2 [E en and S orensson, 2003a]. For weighted model counting... we adopt the well-developed BDD package CUDD [Somenzi, 1998]... |
| Experiment Setup | Yes | A runtime limit of 1000 seconds was imposed on each formula... We did not impose a memory limit, but recorded the maximum memory usage during execution. |