Proof Logging for the Circuit Constraint
(2024) 21st International Conference on the Integration of Constraint Programming, Artificial Intelligence, and Operations Research, CPAIOR 2024 In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 14743 LNCS. p.38-55- Abstract
Proof logging in constraint programming is an approach to certifying a conclusion reached by a solver. To allow for this, different propagators must be augmented to produce justifications for any inferences they make, so that an independent proof checker can certify correctness. The Circuit constraint is used to enforce a Hamiltonian cycle on a set of vertices, e.g. for vehicle routing. Maintaining consistency for the Circuit constraint is hard, so various ad-hoc propagation techniques have been devised and implemented in solvers. We show that standard Circuit constraint inference rules can be efficiently justified within a pseudo-Boolean proof system, either by using a simple sequence of cutting planes steps or through a conditional... (More)
Proof logging in constraint programming is an approach to certifying a conclusion reached by a solver. To allow for this, different propagators must be augmented to produce justifications for any inferences they make, so that an independent proof checker can certify correctness. The Circuit constraint is used to enforce a Hamiltonian cycle on a set of vertices, e.g. for vehicle routing. Maintaining consistency for the Circuit constraint is hard, so various ad-hoc propagation techniques have been devised and implemented in solvers. We show that standard Circuit constraint inference rules can be efficiently justified within a pseudo-Boolean proof system, either by using a simple sequence of cutting planes steps or through a conditional counting argument.
(Less)
- author
- McIlree, Matthew J. ; McCreesh, Ciaran and Nordström, Jakob LU
- organization
- publishing date
- 2024
- type
- Chapter in Book/Report/Conference proceeding
- publication status
- published
- subject
- keywords
- Circuit, Constraint propagation, Proof logging
- host publication
- Integration of Constraint Programming, Artificial Intelligence, and Operations Research - 21st International Conference, CPAIOR 2024, Proceedings
- series title
- Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
- editor
- Dilkina, Bistra
- volume
- 14743 LNCS
- pages
- 18 pages
- publisher
- Springer Science and Business Media B.V.
- conference name
- 21st International Conference on the Integration of Constraint Programming, Artificial Intelligence, and Operations Research, CPAIOR 2024
- conference location
- Uppsala, Sweden
- conference dates
- 2024-05-28 - 2024-05-31
- external identifiers
-
- scopus:85195847767
- ISSN
- 0302-9743
- 1611-3349
- ISBN
- 9783031606014
- DOI
- 10.1007/978-3-031-60599-4_3
- language
- English
- LU publication?
- yes
- id
- 2096be00-a066-4362-a984-ce3dc778f6d4
- date added to LUP
- 2024-09-09 09:50:08
- date last changed
- 2025-07-15 14:10:13
@inproceedings{2096be00-a066-4362-a984-ce3dc778f6d4,
abstract = {{<p>Proof logging in constraint programming is an approach to certifying a conclusion reached by a solver. To allow for this, different propagators must be augmented to produce justifications for any inferences they make, so that an independent proof checker can certify correctness. The Circuit constraint is used to enforce a Hamiltonian cycle on a set of vertices, e.g. for vehicle routing. Maintaining consistency for the Circuit constraint is hard, so various ad-hoc propagation techniques have been devised and implemented in solvers. We show that standard Circuit constraint inference rules can be efficiently justified within a pseudo-Boolean proof system, either by using a simple sequence of cutting planes steps or through a conditional counting argument.</p>}},
author = {{McIlree, Matthew J. and McCreesh, Ciaran and Nordström, Jakob}},
booktitle = {{Integration of Constraint Programming, Artificial Intelligence, and Operations Research - 21st International Conference, CPAIOR 2024, Proceedings}},
editor = {{Dilkina, Bistra}},
isbn = {{9783031606014}},
issn = {{0302-9743}},
keywords = {{Circuit; Constraint propagation; Proof logging}},
language = {{eng}},
pages = {{38--55}},
publisher = {{Springer Science and Business Media B.V.}},
series = {{Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)}},
title = {{Proof Logging for the Circuit Constraint}},
url = {{http://dx.doi.org/10.1007/978-3-031-60599-4_3}},
doi = {{10.1007/978-3-031-60599-4_3}},
volume = {{14743 LNCS}},
year = {{2024}},
}