Probabilistic Generalization of Backdoor Trees with Application to SAT
Authors: Alexander Semenov, Daniil Chivilikhin, Stepan Kochemazov, Ibragim Dzhiblavi
AAAI 2023 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | In the experimental part of the paper, we show that moving from the metaheuristic search for ρ-backdoors to that of ρ-backdoor trees allows drastically reducing the time required to construct the required decompositions without compromising their quality. |
| Researcher Affiliation | Academia | Alexander Semenov, Daniil Chivilikhin, Stepan Kochemazov, Ibragim Dzhiblavi ITMO University, St. Petersburg, Russia |
| Pseudocode | No | The paper describes algorithms and procedures in prose but does not include any explicitly labeled pseudocode or algorithm blocks. |
| Open Source Code | Yes | The search algorithm for ρ-backdoor trees was implemented in C++1. 1https://github.com/ctlab/itmo parsat |
| Open Datasets | No | The paper mentions using instances from a GitHub repository (Pavlenko 2022) but does not explicitly state that these datasets are publicly available or open, nor does it provide concrete access information in terms of citations with author/year or specific links to the datasets themselves, only to the repository for the instances. |
| Dataset Splits | No | The paper does not specify any training, validation, or test dataset splits. |
| Hardware Specification | Yes | All experiments were run on a computer with a 32-Core Intel(R) Xeon(R) 106 CPU @ 1.99 GHz and 128 GB of RAM. |
| Software Dependencies | No | The paper mentions using the Minisat solver (E en and S orensson 2004) and solvers Kissat (Biere 2022) and Ca Di Ca L (Biere 2021) but does not provide specific version numbers for these software dependencies. It only lists the commit hashes for Kissat and Ca Di Ca L in their references/footnotes, which are not explicitly presented as version numbers in the main text. |
| Experiment Setup | Yes | In the search algorithm, for all ρ-backdoor trees with |B| < 16, the value ρ was calculated exactly, and for larger backdoors the corresponding random sampling was used during fitness function evaluation. We used a sample of size 103 in these cases. The number is computed using Chernoff bounds in a way similar to (Semenov et al. 2022). |