On CNF encodings of decision diagrams

Ignasi Abío, Graeme Gange, Valentin Mayer-Eichberger, Peter J. Stuckey

Research output: Chapter in Book/Report/Conference proceedingConference PaperResearchpeer-review

4 Citations (Scopus)

Abstract

Decisions diagrams such as Binary Decision Diagrams (BDDs), Multi-valued Decision Diagrams (MDDs) and Negation Normal Forms (NNFs) provide succinct ways of representing Boolean and other finite functions. Hence they provide a powerful tool for modelling complex constraints in discrete satisfaction and optimization problems. Generic propagators for these global constraints exist, but they are complex and hard to implement. An alternative approach to making use of them for solving is to encode them to CNF, using SAT style solving technology to implement them efficiently. This may also have advantages since it is naturally incremental and exposes intermediate literals which may well be useful as search decisions for solving the problem. In this paper we explore different ways that we can map these constraints to CNF, and the different properties these mappings maintain. Surprisingly the most used encoding of BDDs does not maintain domain consistency in arbitrary BDDs. We also consider the strength of propagation with respect to the intermediate literals. We give experiments which compare the performance of the different encodings.

Original languageEnglish
Title of host publicationIntegration of AI and OR Techniques in Constraint Programming
Subtitle of host publication13th International Conference, CPAIOR 2016 Banff, AB, Canada, May 29 – June 1, 2016 Proceedings
EditorsClaude-Guy Quimper
Place of PublicationCham Switzerland
PublisherSpringer
Pages1-17
Number of pages17
ISBN (Electronic)9783319339542
ISBN (Print)9783319339535
DOIs
Publication statusPublished - 2016
Externally publishedYes
EventInternational Conference on Integration of Artificial Intelligence and Operations Research Techniques in Constraint Programming for Combinatorial Optimization Problems 2016 - Banff, Canada
Duration: 29 May 20161 Jun 2016
Conference number: 13th
https://symposia.cirrelt.ca/CPAIOR2016/en/home

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume9676
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

ConferenceInternational Conference on Integration of Artificial Intelligence and Operations Research Techniques in Constraint Programming for Combinatorial Optimization Problems 2016
Abbreviated titleCPAIOR 2016
CountryCanada
CityBanff
Period29/05/161/06/16
Internet address

Cite this

Abío, I., Gange, G., Mayer-Eichberger, V., & Stuckey, P. J. (2016). On CNF encodings of decision diagrams. In C-G. Quimper (Ed.), Integration of AI and OR Techniques in Constraint Programming: 13th International Conference, CPAIOR 2016 Banff, AB, Canada, May 29 – June 1, 2016 Proceedings (pp. 1-17). (Lecture Notes in Computer Science ; Vol. 9676). Springer. https://doi.org/10.1007/978-3-319-33954-2_1