Notice: The reproducibility variables underlying each score are classified using an automated LLM-based pipeline, validated against a manually labeled dataset. LLM-based classification introduces uncertainty and potential bias; scores should be interpreted as estimates. Full accuracy metrics and methodology are described in [1].
Certified Dominance and Symmetry Breaking for Combinatorial Optimisation
Authors: Bart Bogaerts, Stephan Gocht, Ciaran McCreesh, Jakob Nordström
JAIR 2023 | Venue PDF | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Our experimental evaluation demonstrates that we can efficiently verify fully general symmetry breaking in Boolean satisfiability (SAT) solving, thus providing, for the first time, a unified method to certify a range of advanced SAT techniques that also includes cardinality and parity (XOR) reasoning. |
| Researcher Affiliation | Academia | Bart Bogaerts EMAIL Vrije Universiteit Brussel, Brussels, Belgium Stephan Gocht EMAIL Lund University, Lund, Sweden University of Copenhagen, Copenhagen, Denmark Ciaran Mc Creesh Ciaran.Mc EMAIL University of Glasgow, Glasgow, UK Jakob Nordstr om EMAIL University of Copenhagen, Copenhagen, Denmark Lund University, Lund, Sweden |
| Pseudocode | Yes | Algorithm 1: Max clique algorithm without dominance. |
| Open Source Code | Yes | All code for our implementations and experiments, as well as data and scripts for all plots, can be found in the repository (Bogaerts, Gocht, Mc Creesh, & Nordstr om, 2022b). |
| Open Datasets | Yes | Among the benchmark instances from all the SAT competitions between the years 2016 and 2020, we selected all instances in which at least one symmetry was detected; there were 1089 such instances in total. |
| Dataset Splits | No | The paper mentions using "SAT competition benchmarks" and selecting instances based on certain criteria but does not provide specific training/test/validation dataset splits with percentages, sample counts, or explicit splitting methodology for reproducing data partitioning. |
| Hardware Specification | Yes | We performed our computational experiments on machines with dual Intel Xeon E5-2697A v4 processors with 512GBytes RAM and solid-state drives (SSD) running on the Ubuntu 20.04 operating system. We ran twenty instances in parallel on each machine, where we limited each instance to 16GBytes RAM. |
| Software Dependencies | Yes | To validate our approach, we implemented pseudo-Boolean proof logging in the Veri PB proof format for the symmetry breaking method in Break ID, and modified Kissat4 to output Veri PB-proofs (since the redundance rule is a generalization of the RAT rule, this required only purely syntactic changes). |
| Experiment Setup | Yes | We ran twenty instances in parallel on each machine, where we limited each instance to 16GBytes RAM. We used a timeout of 5,000 seconds for solving and 100,000 seconds for verification of the proofs produced during the solving process. |