AllSATCC: Boosting AllSAT Solving with Efficient Component Analysis
Authors: Jiaxin Liang, Feifei Ma, Junping Zhou, Minghao Yin
IJCAI 2022 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | The experimental results show that our algorithm outperforms the state-of-the-art algorithms on most instances. |
| Researcher Affiliation | Academia | 1Northeast Normal University, China 2Institute of Software, Chinese Academy of Sciences, China |
| Pseudocode | Yes | Algorithm 1 shows the framework of All SATCC based on DPLL searching in a sole decision tree. |
| Open Source Code | Yes | The executable code and benchmarks are available at https://github.com/Lyre Rabbit/All SATCC. |
| Open Datasets | Yes | In our experiments, we empirically access the performance of All SATCC on real-world benchmark instances from SAT competitions from 2011 to 2017, SATLIB, and ISCAS85/89, which have recently been used for testing the solving efficiency of All SAT solvers in [Zhang et al., 2020a]. |
| Dataset Splits | No | The paper evaluates an algorithm on benchmark instances but does not describe training, validation, or test splits for a machine learning model or similar data partitioning for reproducibility. |
| Hardware Specification | Yes | All experiments are run on Intel Xeon CPU E5-2650 v4 @ 2.20GHz with 128GB RAM under Cent OS release 6.10. |
| Software Dependencies | Yes | All SATCC1, which is implemented in C++ with g++ compiler with version 4.8.1. |
| Experiment Setup | Yes | In the table, the first column records the name of each set as well as the number of instances in each set (in brackets). Four sets of these instances are graph coloring problems, denoted as Flatx-y, where x and y are the number of vertices and edges, respectively. For each set of instances, we report the number of variables (ave vars), the number of clauses (ave cls), the percentage of backbone variables (ave bb, ratio of the number of backbone variables to the number of variables), the number of full satisfying assignments (ave SAs), and the number of instances that each solver can solve within the cutoff time. |