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 Stochastic Boolean Satisfiability under Random-Exist Quantification
Authors: Nian-Ze Lee, Yen-Shi Wang, Jie-Hong R. Jiang
IJCAI 2017 | Venue PDF | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Experimental results show that our method outperforms the stateof-the-art algorithm on random k-CNF and AIrelated formulas in both runtime and memory usage, and has effective application to approximate SSAT on VLSI circuit benchmarks. |
| Researcher Affiliation | Academia | Graduate Institute of Electronics Engineering, Department of Electrical Engineering National Taiwan University, Taipei, Taiwan EMAIL |
| Pseudocode | Yes | Figure 1: Algorithm: Solving random-exist quantified SSAT. |
| Open Source Code | No | The paper does not provide any statement or link indicating that the source code for their methodology is open-source or publicly available. |
| Open Datasets | Yes | The random k-CNF formulas are generated using the cnfgen command [Lauria, 2012]." and "We take the strategic companies problem, which was defined in [Cadoli et al., 1997], as an example..." and "In our experiments, we use circuits from ISCAS benchmark suits and set ϵ = 0.125, δ = 0.01." |
| Dataset Splits | No | The paper describes an algorithm for solving SSAT formulas and evaluates it on various problem instances. It does not involve training machine learning models on datasets with explicit train/validation/test splits as is common in many empirical studies. |
| Hardware Specification | Yes | The experiments were conducted on a Linux machine with Intel Xeon 2.1 GHz CPU and 126 GB RAM. |
| Software Dependencies | Yes | The SAT solver Minisat-2.2 and model counter Cachet were used in our program as underlying computational engines. |
| Experiment Setup | Yes | A runtime limit of 1000 seconds was imposed on each formula." and "Since re SSAT has the capability of solving approximate SSAT, we set a relatively short timeout of 60 seconds to evaluate its ability to derive upper and lower bounds for satisfying probability under a strict time constraint." and "In our experiments, we use circuits from ISCAS benchmark suits and set ϵ = 0.125, δ = 0.01." |