kth.sePublications
System disruptions
We are currently experiencing disruptions on the search portals due to high traffic. We are working to resolve the issue, you may temporarily encounter an error message.
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Justifying All Differences Using Pseudo-Boolean Reasoning
Lund Univ, Lund, Sweden.;Univ Copenhagen, Copenhagen, Denmark..
Lund Univ, Lund, Sweden.;Univ Copenhagen, Copenhagen, Denmark..
Univ Glasgow, Glasgow, Lanark, Scotland..
KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS. Univ Copenhagen, Copenhagen, Denmark.;KTH Royal Inst Technol, Stockholm, Sweden..ORCID iD: 0000-0002-2700-4285
2020 (English)In: Thirty-Fourth Aaai Conference On Artificial Intelligence, The Thirty-Second Innovative Applications Of Artificial Intelligence Conference And The Tenth Aaai Symposium On Educational Advances In Artificial Intelligence, ASSOC ADVANCEMENT ARTIFICIAL INTELLIGENCE , 2020, p. 1486-1494Conference paper, Published paper (Refereed)
Abstract [en]

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.

Place, publisher, year, edition, pages
ASSOC ADVANCEMENT ARTIFICIAL INTELLIGENCE , 2020. p. 1486-1494
Series
AAAI Conference on Artificial Intelligence, ISSN 2159-5399 ; 34
National Category
Computer Sciences
Identifiers
URN: urn:nbn:se:kth:diva-299716ISI: 000667722801068Scopus ID: 2-s2.0-85091293070OAI: oai:DiVA.org:kth-299716DiVA, id: diva2:1585801
Conference
34th AAAI Conference on Artificial Intelligence / 32nd Innovative Applications of Artificial Intelligence Conference / 10th AAAI Symposium on Educational Advances in Artificial Intelligence, FEB 07-12, 2020, New York, NY
Note

QC 20210818

Available from: 2021-08-18 Created: 2021-08-18 Last updated: 2023-04-05Bibliographically approved

Open Access in DiVA

No full text in DiVA

Scopus

Authority records

Nordström, Jakob

Search in DiVA

By author/editor
Nordström, Jakob
By organisation
Theoretical Computer Science, TCS
Computer Sciences

Search outside of DiVA

GoogleGoogle Scholar

urn-nbn

Altmetric score

urn-nbn
Total: 36 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf