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 Coakley et alK. L. Coakley, T. Snelleman, H. Hoos, and O. E. Gundersen, "The embrace of open science: An analysis of a decade of AI research and 56 800 conference papers," Under Review, 2026..
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. |