DROPS

Document

DOI: 10.4230/LIPIcs.SAT.2023.30

A Comparison of SAT Encodings for Acyclicity of Directed Graphs

Authors: Neng-Fa Zhou, Ruiwei Wang, and Roland H. C. Yap

Published in: LIPIcs, Volume 271, 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)

Abstract

Many practical applications require synthesizing directed graphs that satisfy the acyclic constraint along with some side constraints. Several methods have been devised for encoding acyclicity of directed graphs into SAT, each of which is based on a cycle-detecting algorithm. The leaf-elimination encoding (LEE) repeatedly eliminates leaves from the graph, and judges the graph to be acyclic if the graph becomes empty at a certain time. The vertex-elimination encoding (VEE) exploits the property that the cyclicity of the resulting graph produced by the vertex-elimination operation entails the cyclicity of the original graph. While VEE is significantly smaller than the transitive-closure encoding for sparse graphs, it generates prohibitively large encodings for large dense graphs. This paper reports on a comparison study of four SAT encodings for acyclicity of directed graphs, namely, LEE using unary encoding for time variables (LEE-u), LEE using binary encoding for time variables (LEE-b), VEE, and a hybrid encoding which combines LEE-b and VEE. The results show that the hybrid encoding significantly outperforms the others.

Cite as

Neng-Fa Zhou, Ruiwei Wang, and Roland H. C. Yap. A Comparison of SAT Encodings for Acyclicity of Directed Graphs. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 30:1-30:9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{zhou_et_al:LIPIcs.SAT.2023.30,
  author =	{Zhou, Neng-Fa and Wang, Ruiwei and Yap, Roland H. C.},
  title =	{{A Comparison of SAT Encodings for Acyclicity of Directed Graphs}},
  booktitle =	{26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
  pages =	{30:1--30:9},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-286-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{271},
  editor =	{Mahajan, Meena and Slivovsky, Friedrich},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023.30},
  URN =		{urn:nbn:de:0030-drops-184927},
  doi =		{10.4230/LIPIcs.SAT.2023.30},
  annote =	{Keywords: Graph constraints, Acyclic constraint, SAT encoding, Graph Synthesis}
}

Document

DOI: 10.4230/LIPIcs.CP.2022.40

CNF Encodings of Binary Constraint Trees

Authors: Ruiwei Wang and Roland H. C. Yap

Published in: LIPIcs, Volume 235, 28th International Conference on Principles and Practice of Constraint Programming (CP 2022)

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.

Cite as

Ruiwei Wang and Roland H. C. Yap. CNF Encodings of Binary Constraint Trees. In 28th International Conference on Principles and Practice of Constraint Programming (CP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 235, pp. 40:1-40:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@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/entities/document/10.4230/LIPIcs.CP.2022.40},
  URN =		{urn:nbn:de:0030-drops-166698},
  doi =		{10.4230/LIPIcs.CP.2022.40},
  annote =	{Keywords: BCT, CNF, MDD, NFA / MDD constraint, propagation strength}
}

Search Results

Documents authored by Wang, Ruiwei

A Comparison of SAT Encodings for Acyclicity of Directed Graphs

Abstract

Cite as

CNF Encodings of Binary Constraint Trees

Abstract

Cite as

Thanks for your feedback!

Could not send message