3 Search Results for "Wang, Ruiwei"

Document
Short Paper
DOI: 10.4230/LIPIcs.CP.2024.40
Encoding the Hamiltonian Cycle Problem into SAT Based on Vertex Elimination (Short Paper)

Authors: Neng-Fa Zhou

Published in: LIPIcs, Volume 307, 30th International Conference on Principles and Practice of Constraint Programming (CP 2024)

Abstract
This paper presents a SAT encoding, called vertex elimination encoding (VEE), for the Hamiltonian Cycle Problem (HCP). The encoding maps a Hamiltonian cycle in the reduced graph after vertex elimination to a Hamiltonian cycle in the original graph. While VEE is not competitive for large dense graphs due to its large encoding sizes, it can be utilized to reduce graphs when they are sparse. This paper compares VEE with the distance encoding, and shows that the hybridization of these two encodings is effective for the benchmarks. For the knight’s tour problem, in particular, the hybrid encoding solves some middle-sized instances that were beyond the reach for previous eager SAT encodings.
Cite as

Neng-Fa Zhou. Encoding the Hamiltonian Cycle Problem into SAT Based on Vertex Elimination (Short Paper). In 30th International Conference on Principles and Practice of Constraint Programming (CP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 307, pp. 40:1-40:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{zhou:LIPIcs.CP.2024.40,
  author =	{Zhou, Neng-Fa},
  title =	{{Encoding the Hamiltonian Cycle Problem into SAT Based on Vertex Elimination}},
  booktitle =	{30th International Conference on Principles and Practice of Constraint Programming (CP 2024)},
  pages =	{40:1--40:8},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-336-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{307},
  editor =	{Shaw, Paul},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2024.40},
  URN =		{urn:nbn:de:0030-drops-207258},
  doi =		{10.4230/LIPIcs.CP.2024.40},
  annote =	{Keywords: Graph constraints, the Hamiltonian cycle problem, SAT encoding, Vertex elimination, Graph synthesis}
}
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}
}
  • Refine by Type
  • 3 Document/PDF

  • Refine by Publication Year
  • 1 2024
  • 1 2023
  • 1 2022

  • Refine by Author
  • 2 Wang, Ruiwei
  • 2 Yap, Roland H. C.
  • 2 Zhou, Neng-Fa

  • Refine by Series/Journal
  • 3 LIPIcs

  • Refine by Classification
  • 2 Computing methodologies → Knowledge representation and reasoning
  • 2 Computing methodologies → Planning and scheduling
  • 2 Hardware → Theorem proving and SAT solving
  • 1 Computing methodologies → Artificial intelligence
  • 1 Software and its engineering → Constraint and logic languages

  • Refine by Keyword
  • 2 Graph constraints
  • 2 SAT encoding
  • 1 Acyclic constraint
  • 1 BCT
  • 1 CNF
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact