Certifying Bounds Propagation for Integer Multiplication Constraints
Authors: Matthew J. McIlree, Ciaran McCreesh
AAAI 2025 | Venue PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | To test this empirically, we ran the solver on some minimal CSP instances, with and without both kinds of proof logging and verified the produced proof files with the Veri PB tool. For further validation, we tested the solver on one thousand synthetic instances, each consisting of a single ternary multiplication constraint with domains that are randomly chosen (increasingly large) sub-intervals of [ 200 . . . 200]. We used hardware with dual AMD EPYC 7643 CPUs, 2TBytes RAM, running Ubuntu 22.04. The results of this are shown in Figure 1. Clearly BC proof logging is much faster than the auto-tabulation baseline here. |
| Researcher Affiliation | Academia | Matthew J. Mc Ilree, Ciaran Mc Creesh University of Glasgow, Scotland (UK) EMAIL, EMAIL |
| Pseudocode | No | The paper presents mathematical propositions and proofs but does not include any explicitly labeled pseudocode or algorithm blocks. |
| Open Source Code | Yes | Code https://doi.org/10.5281/zenodo.14500848 |
| Open Datasets | Yes | For further validation, we tested the solver on one thousand synthetic instances, each consisting of a single ternary multiplication constraint with domains that are randomly chosen (increasingly large) sub-intervals of [ 200 . . . 200]. ... Then for an additional example, we modelled the n-fractions problem from CSPLib2 for n = 2, which uses several multiplication constraints with domains of up to size 10,000. |
| Dataset Splits | No | The paper describes the generation of synthetic instances and models a problem from CSPLib2, but does not provide specific training/test/validation dataset splits typically found in machine learning experiments. |
| Hardware Specification | Yes | We used hardware with dual AMD EPYC 7643 CPUs, 2TBytes RAM, running Ubuntu 22.04. |
| Software Dependencies | No | The paper mentions "Ubuntu 22.04" (an operating system with a version) and tools like the "Glasgow Constraint Solver (GCS)" and "Veri PB tool" without specifying their version numbers. |
| Experiment Setup | Yes | For further validation, we tested the solver on one thousand synthetic instances, each consisting of a single ternary multiplication constraint with domains that are randomly chosen (increasingly large) sub-intervals of [ 200 . . . 200]. ... Then for an additional example, we modelled the n-fractions problem from CSPLib2 for n = 2, which uses several multiplication constraints with domains of up to size 10,000. |