Certified Dominance and Symmetry Breaking for Combinatorial Optimisation

Publikation: Bidrag til tidsskrift › Tidsskriftartikel › Forskning › fagfællebedømt

Standard

Certified Dominance and Symmetry Breaking for Combinatorial Optimisation. / Bogaerts, Bart; Gocht, Stephan; McCreesh, Ciaran; Nordström, Jakob.

I: Journal of Artificial Intelligence Research, Bind 77, 2023, s. 1539-1589.

Publikation: Bidrag til tidsskrift › Tidsskriftartikel › Forskning › fagfællebedømt

Harvard

Bogaerts, B, Gocht, S, McCreesh, C & Nordström, J 2023, 'Certified Dominance and Symmetry Breaking for Combinatorial Optimisation', Journal of Artificial Intelligence Research, bind 77, s. 1539-1589. https://doi.org/10.1613/jair.1.14296

APA

Bogaerts, B., Gocht, S., McCreesh, C., & Nordström, J. (2023). Certified Dominance and Symmetry Breaking for Combinatorial Optimisation. Journal of Artificial Intelligence Research, 77, 1539-1589. https://doi.org/10.1613/jair.1.14296

Vancouver

Bogaerts B, Gocht S, McCreesh C, Nordström J. Certified Dominance and Symmetry Breaking for Combinatorial Optimisation. Journal of Artificial Intelligence Research. 2023;77:1539-1589. https://doi.org/10.1613/jair.1.14296

Author

Bogaerts, Bart ; Gocht, Stephan ; McCreesh, Ciaran ; Nordström, Jakob. / Certified Dominance and Symmetry Breaking for Combinatorial Optimisation. I: Journal of Artificial Intelligence Research. 2023 ; Bind 77. s. 1539-1589.

Bibtex

@article{1a7cdb559b11432cb4e17864689ecc90,
title = "Certified Dominance and Symmetry Breaking for Combinatorial Optimisation",
abstract = "Symmetry and dominance breaking can be crucial for solving hard combinatorial search and optimisation problems, but the correctness of these techniques sometimes relies on subtle arguments. For this reason, it is desirable to produce efficient, machine-verifiable certificates that solutions have been computed correctly. Building on the cutting planes proof system, we develop a certification method for optimisation problems in which symmetry and dominance breaking is easily expressible. 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. In addition, we apply our method to maximum clique solving and constraint programming as a proof of concept that the approach applies to a wider range of combinatorial problems. ",
author = "Bart Bogaerts and Stephan Gocht and Ciaran McCreesh and Jakob Nordstr{\"o}m",
note = "Publisher Copyright: {\textcopyright}2023 The Authors.",
year = "2023",
doi = "10.1613/jair.1.14296",
language = "English",
volume = "77",
pages = "1539--1589",
journal = "Journal of Artificial Intelligence Research",
issn = "1076-9757",
publisher = "A A A I Press",

}

RIS

TY - JOUR

T1 - Certified Dominance and Symmetry Breaking for Combinatorial Optimisation

AU - Bogaerts, Bart

AU - Gocht, Stephan

AU - McCreesh, Ciaran

AU - Nordström, Jakob

N1 - Publisher Copyright: ©2023 The Authors.

PY - 2023

Y1 - 2023

N2 - Symmetry and dominance breaking can be crucial for solving hard combinatorial search and optimisation problems, but the correctness of these techniques sometimes relies on subtle arguments. For this reason, it is desirable to produce efficient, machine-verifiable certificates that solutions have been computed correctly. Building on the cutting planes proof system, we develop a certification method for optimisation problems in which symmetry and dominance breaking is easily expressible. 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. In addition, we apply our method to maximum clique solving and constraint programming as a proof of concept that the approach applies to a wider range of combinatorial problems.

AB - Symmetry and dominance breaking can be crucial for solving hard combinatorial search and optimisation problems, but the correctness of these techniques sometimes relies on subtle arguments. For this reason, it is desirable to produce efficient, machine-verifiable certificates that solutions have been computed correctly. Building on the cutting planes proof system, we develop a certification method for optimisation problems in which symmetry and dominance breaking is easily expressible. 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. In addition, we apply our method to maximum clique solving and constraint programming as a proof of concept that the approach applies to a wider range of combinatorial problems.

U2 - 10.1613/jair.1.14296

DO - 10.1613/jair.1.14296

M3 - Journal article

AN - SCOPUS:85171627621

VL - 77

SP - 1539

EP - 1589

JO - Journal of Artificial Intelligence Research

JF - Journal of Artificial Intelligence Research

SN - 1076-9757

ER -

ID: 391035770