Certified Dominance and Symmetry Breaking for Combinatorial Optimisation

Publikation: Bidrag til tidsskriftTidsskriftartikelForskningfagfællebedømt

Dokumenter

  • Fulltext

    Forlagets udgivne version, 598 KB, PDF-dokument

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.

OriginalsprogEngelsk
TidsskriftJournal of Artificial Intelligence Research
Vol/bind77
Sider (fra-til)1539-1589
Antal sider51
ISSN1076-9757
DOI
StatusUdgivet - 2023

Bibliografisk note

Funding Information:
Stephan Gocht and Jakob Nordström were supported by the Swedish Research Council grant 2016-00782, and Jakob Nordström also received funding from the Independent Research Fund Denmark grant 9040-00389B. Ciaran McCreesh was supported by a Royal Academy of Engineering research fellowship. Bart Bogaerts was supported by Fonds Weten-schappelijk Onderzoek – Vlaanderen (project G0B2221N), by the Flemish Government (AI Research Program), and by TAILOR, a project funded by EU Horizon 2020 research and innovation programme under GA No 952215.

Publisher Copyright:
©2023 The Authors.

ID: 391035770