On Irrelevant Literals in Pseudo-Boolean Constraint Learning
Authors: Daniel Le Berre, Pierre Marquis, Stefan Mengel, Romain Wallon
IJCAI 2020 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | This section provides experimental results showing to what extent irrelevant literals are present in the constraints inferred by PB solvers. We also give an attempt to evaluate their impact on the performance. |
| Researcher Affiliation | Academia | 1Universit e d Artois, Lens, France 2CRIL, CNRS UMR 8188, Lens, France 3Institut Universitaire de France |
| Pseudocode | No | The paper describes the detection algorithm in prose and mathematical terms within Section 4, but it does not provide a clearly labeled 'Pseudocode' or 'Algorithm' block with structured steps. |
| Open Source Code | No | The paper states 'we implemented the incomplete detection algorithm presented above in Sat4j', but it does not explicitly state that the authors' implementation code for this work is publicly available, nor does it provide a link to such a repository. |
| Open Datasets | Yes | To do so, we implemented the incomplete detection algorithm presented above in Sat4j [Le Berre and Parrain, 2010], and consider the whole set of decision benchmarks containing only small integers used in the PB evaluation since its very first edition [Manquinho and Roussel, 2006]. |
| Dataset Splits | No | The paper mentions using a 'set of decision benchmarks' but does not specify explicit training, validation, or test dataset splits, nor does it describe a cross-validation setup. |
| Hardware Specification | Yes | All experiments presented in this section have been run on a cluster equipped with quadcore bi-processors Intel XEON E5-5637 v4 (3.5 GHz) and 128 GB of memory, with a memory limit set to 64 GB. |
| Software Dependencies | Yes | To do so, we implemented the incomplete detection algorithm presented above in Sat4j [Le Berre and Parrain, 2010]. The citation [Le Berre and Parrain, 2010] refers to 'The SAT4J library, Release 2.2, System Description', indicating version 2.2 of Sat4j. |
| Experiment Setup | Yes | After some preliminary experiments, we chose 4547 as parameter p of our incomplete subset-sum algorithm, and 500 as bound on the number of literals in the constraints to consider. These values have been chosen in a way that nearly all constraints in our experiments are treated efficiently, while the number of literals wrongly detected as relevant remains reasonable. For these experiments, we let these solvers run for 5 minutes, and let them dump at most 100,000 constraints derived during their conflict analyses |