Hard Examples for Common Variable Decision Heuristics
Authors: Marc Vinyals1652-1659
AAAI 2020 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | In addition to proving a theoretical result, we run experiments on the formulas we craft. The experiments confirm our theoretical findings, that is the formulas are very hard for SAT solvers that employ the heuristics we discuss, but trivial if we specify a static variable order. We ran experiments on pitfall formulas using the Ca Di Ca L 1.0.3 (Biere 2017), Glucose 4.1 (Audemard and Simon 2009), and Maple COMSPS (Liang et al. 2016c) solvers, representing the VMTF, VSIDS, and CHB and LRB heuristics respectively. |
| Researcher Affiliation | Academia | Marc Vinyals Computer Science Department, Technion, Haifa 3200003, Israel marcviny@cs.technion.ac.il |
| Pseudocode | Yes | Algorithm 1: CDCL |
| Open Source Code | Yes | A formula generator is available as a CNFgen module (Lauria et al. 2017) at doi.org/10.5281/zenodo.3544727 |
| Open Datasets | Yes | A formula generator is available as a CNFgen module (Lauria et al. 2017) at doi.org/10.5281/zenodo.3544727, and the full data at doi.org/10.5281/zenodo.3544731. |
| Dataset Splits | No | The paper discusses running SAT solvers on crafted formulas and does not mention training, validation, or test splits of a dataset in the context of machine learning model training or evaluation. |
| Hardware Specification | No | Experiments were run on resources provided by the Swedish National Infrastructure for Computing (SNIC) at HPC2N. This specifies a computing cluster but does not provide details on specific CPU or GPU models, or memory configurations. |
| Software Dependencies | Yes | We ran experiments on pitfall formulas using the Ca Di Ca L 1.0.3 (Biere 2017), Glucose 4.1 (Audemard and Simon 2009), and Maple COMSPS (Liang et al. 2016c) solvers |
| Experiment Setup | Yes | We ran the solvers with their default parameters, except that we disabled preand inprocessing since these turn out to be counterproductive and experimentally lead to worse runtimes. We turned on VMTF and the unsat option in Ca Di Ca L, and we disabled the adaptive strategies of Glucose to obtain more consistent results. We chose the pure versions of Maple COMSPS to avoid interference from other heuristics. We set the block size of Y and Z variables to 30 and 5 respectively, which we experimentally found to be large enough to make the formulas hard, and use 4, 6, 8, and 10 blocks but focus on 6 and 8 since these yield formulas that are hard but not impossible. To account for different ways to initialize the variable order we shuffled the variables and clauses (but not the polarities) with 32 different seeds and report the aggregated result, assigning a time of 3600 s to unsolved instances. We do not do any shuffling when running with a fixed order. |