On Probabilistic Generalization of Backdoors in Boolean Satisfiability
Authors: Alexander Semenov, Artem Pavlenko, Daniil Chivilikhin, Stepan Kochemazov10353-10361
AAAI 2022 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Results of computational experiments show that the use of (ε, δ)-SBSes found by the proposed algorithm allows speeding up solving of test problems related to equivalence checking and hard crafted and combinatorial benchmarks compared to state-of-the-art SAT solvers. |
| Researcher Affiliation | Academia | Alexander Semenov, Artem Pavlenko, Daniil Chivilikhin, Stepan Kochemazov, ITMO University, St. Petersburg, Russia |
| Pseudocode | No | The paper describes algorithms in prose but does not include structured pseudocode or clearly labeled algorithm blocks. |
| Open Source Code | Yes | The proposed approach was implemented in Python in the form of a multi-threaded application Evo Guess2, using Py SAT (Ignatiev, Morgado, and Marques-Silva 2018) for interfacing with SAT solvers. We used incremental SAT solvers that are available in Py SAT: namely, we mainly ran Glucose 3.0 (g3), Glucose 4.1 (g4), and Ca Di Ca L 1.0.3 (cd), though we also used Minisat 2.2 (m22) in one experiment. ... 2https://github.com/ctlab/EvoGuess/releases/tag/v2.0.0 |
| Open Datasets | Yes | The first set of benchmarks belongs to the general class of equivalence checking instances (Kuehlmann and Krohm 1997; Molitor and Mohnke 2007). ... We also considered some crafted tests: sgen (Spence 2015, 2017), Pigeonhole Principle formulas (PHP), Parity principle (par9), and pmg12 from SAT competition. |
| Dataset Splits | No | The paper refers to using 'test problems' and 'benchmarks' but does not specify any training, validation, or test dataset splits or cross-validation methodology for their experiments. |
| Hardware Specification | Yes | Preliminary experiments were done using one node of the HPC-cluster Academician V.M. Matrosov 3 (with two 18-core Intel Xeon E5-2695 CPUs). For main experiments, we used one node of a computing cluster in ITMO University equipped with an Intel Xeon Gold 6248R CPU @ 3.00 GHz. |
| Software Dependencies | Yes | Py SAT (Ignatiev, Morgado, and Marques-Silva 2018) for interfacing with SAT solvers. We used incremental SAT solvers that are available in Py SAT: namely, we mainly ran Glucose 3.0 (g3), Glucose 4.1 (g4), and Ca Di Ca L 1.0.3 (cd), though we also used Minisat 2.2 (m22) in one experiment. |
| Experiment Setup | Yes | In the reported experiments we started the search from the empty backdoor (strategy 2), and initially used random samples of size of N = 4000... We also doubled the value of N if for the current value we had ρB = 1... In the experiments, we used Q = 8, H = 2. ... In our experiments we used ω|X| {15, 20}... |