Divide and Conquer: Towards Faster Pseudo-Boolean Solving
Authors: Jan Elffers, Jakob Nordström
IJCAI 2018 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | In this section we report results from an experimental comparison of Rounding Sat to Sat4j and Open-WBO. Table 1: Results on benchmarks from past PB competitions (number of solved satisfiable instances + solved unsatisfiable instances). |
| Researcher Affiliation | Academia | Jan Elffers and Jakob Nordstr om KTH Royal Institute of Technology {elffers,jakobn}@kth.se |
| Pseudocode | Yes | Algorithm 1: CDCL main loop. Algorithm 2: propagate(ρ, D) Algorithm 3: analyze Conflict(Cconfl, ρ) Algorithm 4: Reduction by weakening and saturation. Algorithm 5: round To One(C, ℓ, ρ) Algorithm 6: Rounding Sat conflict analysis |
| Open Source Code | No | Some supplemental material (including experimental data) can be found at www.csc.kth.se/ jakobn/Rounding Sat. |
| Open Datasets | Yes | We evaluated the solvers on benchmarks submitted to the Pseudo-Boolean Competitions over the past two decades in the DEC-SMALLINT-LIN category (decision problems, small integers, linear constraints) since Rounding Sat is currently designed to solve decision problems and represents constraints using 32-bit integers. |
| Dataset Splits | No | The paper evaluates solvers on existing benchmarks from Pseudo-Boolean Competitions but does not specify any training, validation, or test dataset splits in the context of their experiments. |
| Hardware Specification | Yes | We ran our experiments on a cluster with a set-up of 6 AMD Opteron 6238 (2.6 GHz) cores and 16 GB of memory. |
| Software Dependencies | No | The paper states, 'We used the latest available versions of all solvers as of December 1, 2017.' but does not list specific version numbers for ancillary software components like programming languages or libraries used for running their own code. |
| Experiment Setup | Yes | We used 1800 seconds as the wall clock timeout, the same time limit as in the Pseudo-Boolean Competition 2016, and had a memory limit of 14 GB for all runs. |