License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CP.2022.40
URN: urn:nbn:de:0030-drops-166698
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/16669/
Go to the corresponding LIPIcs Volume Portal

Wang, Ruiwei ; Yap, Roland H. C.

CNF Encodings of Binary Constraint Trees

pdf-format:
LIPIcs-CP-2022-40.pdf (0.9 MB)

Abstract

Ordered Multi-valued Decision Diagrams (MDDs) have been shown to be useful to represent finite domain functions/relations. For example, various constraints can be modelled with MDD constraints. Recently, a new representation called Binary Constraint Tree (BCT), which is a (special) tree structure binary Constraint Satisfaction Problem, has been proposed to encode MDDs and shown to outperform existing MDD constraint propagators in Constraint Programming solvers. BCT is a compact representation, and it can be exponentially smaller than MDD for representing some constraints. Here, we also show that BCT is compact for representing non-deterministic finite state automaton (NFA) constraints. In this paper, we investigate how to encode BCT into CNF form, making it suitable for SAT solvers. We present and investigate five BCT CNF encodings. We compare the propagation strength of the BCT CNF encodings and experimentally evaluate the encodings on a range of existing benchmarks. We also compare with seven existing CNF encodings of MDD constraints. Experimental results show that the CNF encodings of BCT constraints can outperform those of MDD constraints on various benchmarks.

BibTeX - Entry

@InProceedings{wang_et_al:LIPIcs.CP.2022.40,
  author =	{Wang, Ruiwei and Yap, Roland H. C.},
  title =	{{CNF Encodings of Binary Constraint Trees}},
  booktitle =	{28th International Conference on Principles and Practice of Constraint Programming (CP 2022)},
  pages =	{40:1--40:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-240-2},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{235},
  editor =	{Solnon, Christine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2022/16669},
  URN =		{urn:nbn:de:0030-drops-166698},
  doi =		{10.4230/LIPIcs.CP.2022.40},
  annote =	{Keywords: BCT, CNF, MDD, NFA / MDD constraint, propagation strength}
}

Keywords: BCT, CNF, MDD, NFA / MDD constraint, propagation strength
Collection: 28th International Conference on Principles and Practice of Constraint Programming (CP 2022)
Issue Date: 2022
Date of publication: 23.07.2022

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI