On Division Versus Saturation in Pseudo-Boolean Solving
Authors: Stephan Gocht, Jakob Nordström, Amir Yehudayoff
IJCAI 2019 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | We also perform some experiments to see whether these phenomena can be observed in actual solvers. Our conclusion is that a careful combination of division and saturation seems to be crucial to harness more of the power of cutting planes. |
| Researcher Affiliation | Academia | 1KTH Royal Institute of Technology 2University of Copenhagen 3Technion Israel Institute of Technology |
| Pseudocode | No | The paper does not contain any clearly labeled pseudocode or algorithm blocks. |
| Open Source Code | No | The paper does not provide any explicit statements about releasing source code for their described methodology, nor does it provide a link to such code. |
| Open Datasets | Yes | To obtain benchmarks that are easy for division but hard for saturation, we use subset cardinality formulas as in Section 3, generated from 4-regular random bipartite graphs with an additional random edge added (see [Mikˇsa and Nordstr om, 2014] for more details). |
| Dataset Splits | No | The paper does not specify training, validation, or test dataset splits. |
| Hardware Specification | Yes | All experiments were performed on 4 AMD Opteron 6238 (Interlagos) 12-core 2.6 GHz processors with 128 GB RAM with a 5000-second time-out. |
| Software Dependencies | No | The paper mentions using "instrumented versions of Sat4j" and "Rounding Sat" but does not specify their version numbers or any other software dependencies with versions. |
| Experiment Setup | Yes | All experiments were performed on 4 AMD Opteron 6238 (Interlagos) 12-core 2.6 GHz processors with 128 GB RAM with a 5000-second time-out. The heuristics for PB solvers are not at all as well-tuned as those for CDCL solvers, and small changes in internal settings can have huge, and currently not so well understood, effects on performance. In order to measure the overall impact of division versus saturation rather than of some other, unrelated settings we have therefore run the solvers with several different parameter settings and measured for each PB instance the best result with division and saturation, thus obtaining virtual best solvers (VBS) for division and saturation, respectively. |