A Cardinal Improvement to Pseudo-Boolean Solving
Authors: Jan Elffers, Jakob Nordstrm1495-1503
AAAI 2020 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | We have implemented our approach within the pseudo Boolean solver Rounding Sat (Elffers and Nordstr om 2018). We refer to the solver with cardinality detection as Rounding Sat-Card. We set wmax = 5 in all experiments. [...] We report results from two types of benchmarks: SAT and PB competitions from 2016 2018, and a number of crafted benchmarks. |
| Researcher Affiliation | Academia | Jan Elffers,1,2 Jakob Nordstr om2,3 1Lund University, 2University of Copenhagen, 3KTH Royal Institute of Technology jan.elffers@cs.lth.se, jn@di.ku.dk |
| Pseudocode | Yes | See Algorithm 1 for the pseudocode, where cut[p], if defined, contains a (recursively computed) cut of size less than wmax for the literal p in the implication graph. In Algorithm 1, the round To Clause method reduces the pseudo-Boolean reason constraint i aiℓi A for literal p to a clause i ℓi 1 (possibly after first having weakened the constraint by removing some literals, so that the rounded clause is still propagating). Next, the decision cut for p is constructed. [...] Algorithm 2: Conflict analysis with cardinality detection. |
| Open Source Code | No | The paper states, "We have implemented our cardinality detection algorithm inside the pseudo-Boolean solver Rounding Sat (Elffers and Nordstr om 2018)", but does not provide a specific link or explicit statement about the availability of their modified source code. |
| Open Datasets | Yes | We report results from two types of benchmarks: SAT and PB competitions from 2016 2018, and a number of crafted benchmarks. [...] synthesis of shortest straightline programs (Fuhs and Schneider-Kamp 2010) and the Grand Tourobs puzzle (Chowdhury, M uller, and You 2018). [...] standard PHP formulas (Biere et al. 2014). [...] The results are presented in Figure 7. Observe that RSCard scales reasonably well and much better than Rounding Sat without cardinality detection, for which these formulas are exponentially hard. We wish to highlight two technical challenges when solving this formula. Firstly, typically multiple cardinality constraints can be detected, but only one choice works. It turns out that extending with variables in the order of VSIDS scores selects the right constraint. Secondly, adding all ternary clause building blocks degrades performance (in terms of number of reasoning steps, not only running time), but adding a filtering step. [...] The even colouring formula (Markstr om 2006) is an unsatisfiable benchmark [...] Finally, let us discuss a set of benchmarks called division-friendly formulas (Gocht, Nordstr om, and Yehudayoff 2019), which are obfuscated versions of (otherwise extremely easy) subset cardinality formulas (Mikˇsa and Nordstr om 2014). |
| Dataset Splits | No | The paper discusses various benchmarks for evaluation but does not explicitly provide details about a dedicated validation dataset split for hyperparameter tuning or model selection. |
| Hardware Specification | No | Our computational experiments used resources provided by the Swedish National Infrastructure for Computing (SNIC) at the High Performance Computing Center North (HPC2N) at Ume a University. |
| Software Dependencies | No | The paper mentions various solvers used in the experiments such as "Ca Di Ca L (Ca Di Ca L 2019)", "Glucose (Audemard and Simon 2009)", and "Sat4j (Le Berre and Parrain 2010)", but it does not specify the exact version numbers of these software components or any other software dependencies, which are required for reproducibility. |
| Experiment Setup | Yes | We set wmax = 5 in all experiments. [...] For our experiments on SAT competition benchmarks we used a timeout of 5000 seconds. The results are as given in Figure 4. For the pseudo-Boolean competition 2016, using a timeout of 1800 seconds... |