SharpSSAT: A Witness-Generating Stochastic Boolean Satisfiability Solver
Authors: Yu-Wei Fan, Jie-Hong R. Jiang
AAAI 2023 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | 6 Experimental Evaluation We implemented the SSAT solver, named Sharp SSAT1 , in C++ based on the model counter Sharp SAT (Thurley 2006). The witness generation algorithms were integrated into Sharp SSAT and Clau SSat. All experiments were conducted on a Linux machine with 2.2 GHz Intel Xeon CPU and 128 GB RAM. A time limit of 1000 seconds and a 64GB memory limit were imposed on solving an instance. We compared our solver with the state-of-the-art SSAT solvers DC-SSAT, Clau SSat, Prime, and Elim SSAT. The benchmark set used in Clau SSat, with 20 families in total of 357 SSAT instances available at https://github. com/NTU-ALCom Lab/Clau SSat, was taken 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 {r11943096, jhjiang}@ntu.edu.tw |
| Pseudocode | Yes | Algorithm 1: solve SSAT Input: An SSAT formula Φ Output: satisfying probability pret |
| Open Source Code | Yes | We implemented the SSAT solver, named Sharp SSAT1 , in C++ based on the model counter Sharp SAT (Thurley 2006). The witness generation algorithms were integrated into Sharp SSAT and Clau SSat. ... 1Available at https://github.com/NTU-ALCom Lab/Sharp SSAT |
| Open Datasets | Yes | The benchmark set used in Clau SSat, with 20 families in total of 357 SSAT instances available at https://github. com/NTU-ALCom Lab/Clau SSat, was taken for evaluation. |
| Dataset Splits | No | No specific details on train/validation/test dataset splits, sample counts, or splitting methodology were provided. The paper uses a benchmark set for evaluation without specifying data partitioning for training, validation, or testing. |
| Hardware Specification | Yes | All experiments were conducted on a Linux machine with 2.2 GHz Intel Xeon CPU and 128 GB RAM. |
| Software Dependencies | No | The paper states that the solver was implemented in C++ and based on the model counter Sharp SAT. However, it does not specify versions for C++ compilers, Sharp SAT, or any other critical software libraries used in the implementation or for running experiments. |
| Experiment Setup | Yes | All experiments were conducted on a Linux machine with 2.2 GHz Intel Xeon CPU and 128 GB RAM. A time limit of 1000 seconds and a 64GB memory limit were imposed on solving an instance. ... The default branching heuristics of Sharp SSAT is the variable state aware decaying sum (VSADS) (Sang, Beame, and Kautz 2005) that the score for each variable is calculated by score(VSADS) = p score(VSIDS) + q score(DLCS), where p and q are constants weighting the scores of VSIDS variable state independent decaying sum (VSIDS) (Mahajan, Fu, and Malik 2004) and dynamic largest combined sum (DLCS) (Sang, Beame, and Kautz 2005). |