Justifying All Differences Using Pseudo-Boolean Reasoning
Abstract
Constraint programming solvers support rich global constraints and propagators, which make them both powerful and hard to debug. In the Boolean satisfiability community, proof-logging is the standard solution for generating trustworthy outputs, and this has become key to the social acceptability of computer-generated proofs. However, reusing this technology for constraint programming requires either much weaker propagation, or an impractical blowup in proof length. This paper demonstrates that simple, clean, and efficient proof logging is still possible for the all-different constraint, through pseudo-Boolean reasoning. We explain how such proofs can be expressed and verified mechanistically, describe an implementation, and discuss the broader implications for proof logging in constraint programming.
Cite
Text
Elffers et al. "Justifying All Differences Using Pseudo-Boolean Reasoning." AAAI Conference on Artificial Intelligence, 2020. doi:10.1609/AAAI.V34I02.5507Markdown
[Elffers et al. "Justifying All Differences Using Pseudo-Boolean Reasoning." AAAI Conference on Artificial Intelligence, 2020.](https://mlanthology.org/aaai/2020/elffers2020aaai-justifying/) doi:10.1609/AAAI.V34I02.5507BibTeX
@inproceedings{elffers2020aaai-justifying,
title = {{Justifying All Differences Using Pseudo-Boolean Reasoning}},
author = {Elffers, Jan and Gocht, Stephan and McCreesh, Ciaran and Nordström, Jakob},
booktitle = {AAAI Conference on Artificial Intelligence},
year = {2020},
pages = {1486-1494},
doi = {10.1609/AAAI.V34I02.5507},
url = {https://mlanthology.org/aaai/2020/elffers2020aaai-justifying/}
}