Solving Exist-Random Quantified Stochastic Boolean Satisfiability via Clause Selection
Authors: Nian-Ze Lee, Yen-Shi Wang, Jie-Hong R. Jiang
IJCAI 2018 | Conference PDF | Archive PDF | Plain Text | 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. |