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 Symmetry and Dominance Breaking for Combinatorial Optimisation
Authors: Bart Bogaerts, Stephan Gocht, Ciaran McCreesh, Jakob Nordström3698-3707
AAAI 2022 | 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 XOR and cardinality reasoning. |
| Researcher Affiliation | Academia | Vrije Universiteit Brussel 2 Lund University, Lund, Sweden 3 University of Copenhagen, Copenhagen, Denmark 4 University of Glasgow, Glasgow, UK |
| Pseudocode | No | The paper describes formal rules and theoretical concepts, but does not include any explicitly labeled pseudocode or algorithm blocks. |
| Open Source Code | Yes | All code for our implementations and experiments, as well as data and scripts for all plots, can be found at https://doi.org/10.5281/zenodo.6373986. |
| Open Datasets | Yes | Out of all the benchmark instances from all the SAT competitions since 2016, 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 'benchmark instances from all the SAT competitions since 2016' but does not specify any training, validation, or test splits within these instances. |
| Hardware Specification | Yes | We performed our experiments on machines with dual Intel Xeon E5-2697A v4 processors with 512GBytes RAM and solid-state drive (SSD), running Ubuntu 20.04. |
| Software Dependencies | Yes | We implemented Veri PB proof logging for the symmetry breaking method in Break ID, and modified Kissat3 to output Veri PB-proofs |
| Experiment Setup | Yes | We ran twenty instances in parallel on each machine, limiting each instance to 16GBytes RAM, and with a timeout of 5,000s for solving and 100,000s for verification. |