Solving Stochastic Boolean Satisfiability under Random-Exist Quantification
Authors: Nian-Ze Lee, Yen-Shi Wang, Jie-Hong R. Jiang
IJCAI 2017 | Conference PDF | Archive PDF | Plain Text | 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 {d04943019, b03901116, jhjiang}@ntu.edu.tw |
| 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." |