Certified Dominance and Symmetry Breaking for Combinatorial Optimisation
(2023) In Journal of Artificial Intelligence Research 77. p.1539-1589- 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... (More)
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.
(Less)
- author
- Bogaerts, Bart ; Gocht, Stephan LU ; McCreesh, Ciaran and Nordström, Jakob LU
- organization
- publishing date
- 2023
- type
- Contribution to journal
- publication status
- published
- subject
- in
- Journal of Artificial Intelligence Research
- volume
- 77
- pages
- 51 pages
- publisher
- Morgan Kaufmann Publishers
- external identifiers
-
- scopus:85171627621
- ISSN
- 1076-9757
- DOI
- 10.1613/jair.1.14296
- language
- English
- LU publication?
- yes
- additional info
- Publisher Copyright: ©2023 The Authors.
- id
- 61c9b78d-c314-41c8-84d7-1842bb244938
- date added to LUP
- 2024-01-08 14:33:32
- date last changed
- 2024-02-09 10:36:37
@article{61c9b78d-c314-41c8-84d7-1842bb244938,
abstract = {{<p>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.</p>}},
author = {{Bogaerts, Bart and Gocht, Stephan and McCreesh, Ciaran and Nordström, Jakob}},
issn = {{1076-9757}},
language = {{eng}},
pages = {{1539--1589}},
publisher = {{Morgan Kaufmann Publishers}},
series = {{Journal of Artificial Intelligence Research}},
title = {{Certified Dominance and Symmetry Breaking for Combinatorial Optimisation}},
url = {{http://dx.doi.org/10.1613/jair.1.14296}},
doi = {{10.1613/jair.1.14296}},
volume = {{77}},
year = {{2023}},
}