6 Search Results for "Zhou, Neng-Fa"

Document
DOI: 10.4230/LIPIcs.SAT.2025.24
SAT-Based CEGAR Method for the Hamiltonian Cycle Problem Enhanced by Cut-Set Constraints

Authors: Ryoga Ohashi, Takehide Soh, Daniel Le Berre, Hidetomo Nabeshima, Mutsunori Banbara, Katsumi Inoue, and Naoyuki Tamura

Published in: LIPIcs, Volume 341, 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)

Abstract
In this paper, we propose an enhancement to the SAT-based counterexample-guided abstraction refinement (CEGAR) approach for solving the Hamiltonian Cycle Problem (HCP). Many SAT-based methods for HCP have been proposed, including a CEGAR-based method that repeatedly solves a relaxed version of HCP strengthened by counterexamples. However, when the counterexample space - represented by the full set of subcycle partitions - is large, it becomes difficult to find a solution. To address this, we introduce cut-set constraints in the refinement step, replacing traditional subcycle blocking constraints. Our evaluation shows that these cut-set constraints achieve equal or better reduction in the counterexample space, making it easier to find valid solutions. We further assessed performance using all 1001 instances from the FHCP challenge set and confirmed that the proposed method solved 937 instances within 1800 seconds, outperforming both the existing eager and CEGAR encodings (which solved at most 666 instances). This demonstrates the effectiveness of incorporating cut-set constraints into SAT-based CEGAR approaches.
Cite as

Ryoga Ohashi, Takehide Soh, Daniel Le Berre, Hidetomo Nabeshima, Mutsunori Banbara, Katsumi Inoue, and Naoyuki Tamura. SAT-Based CEGAR Method for the Hamiltonian Cycle Problem Enhanced by Cut-Set Constraints. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 24:1-24:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{ohashi_et_al:LIPIcs.SAT.2025.24,
  author =	{Ohashi, Ryoga and Soh, Takehide and Le Berre, Daniel and Nabeshima, Hidetomo and Banbara, Mutsunori and Inoue, Katsumi and Tamura, Naoyuki},
  title =	{{SAT-Based CEGAR Method for the Hamiltonian Cycle Problem Enhanced by Cut-Set Constraints}},
  booktitle =	{28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
  pages =	{24:1--24:10},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-381-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{341},
  editor =	{Berg, Jeremias and Nordstr\"{o}m, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.24},
  URN =		{urn:nbn:de:0030-drops-237585},
  doi =		{10.4230/LIPIcs.SAT.2025.24},
  annote =	{Keywords: Hamiltonian Cycle Problem, SAT Encoding, CEGAR}
}
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/OASIcs.ICLP.2017.11
Efficient Declarative Solutions in Picat for Optimal Multi-Agent Pathfinding

Authors: Neng-Fa Zhou and Roman Bartak

Published in: OASIcs, Volume 58, Technical Communications of the 33rd International Conference on Logic Programming (ICLP 2017)

Abstract
The multi-agent pathfinding (MAPF) problem has attracted considerable attention because of its relation to practical applications. The majority of solutions for MAPF are algorithmic. Recently, declarative solutions that reduce MAPF to encodings for off-the-shelf solvers have achieved remarkable success. We present a constraint-based declarative model for MAPF, together with its implementation in Picat, which uses SAT and MIP. We consider both the makespan and the sum-of-costs objectives, and propose a preprocessing technique for improving the performance of the model. Experimental results show that the implementation using SAT is highly competitive. We also analyze the high performance of the SAT solution by relating it to the SAT encoding algorithms that are used in the Picat compiler.
Cite as

Neng-Fa Zhou and Roman Bartak. Efficient Declarative Solutions in Picat for Optimal Multi-Agent Pathfinding. In Technical Communications of the 33rd International Conference on Logic Programming (ICLP 2017). Open Access Series in Informatics (OASIcs), Volume 58, pp. 11:1-11:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{zhou_et_al:OASIcs.ICLP.2017.11,
  author =	{Zhou, Neng-Fa and Bartak, Roman},
  title =	{{Efficient Declarative Solutions in Picat for Optimal Multi-Agent Pathfinding}},
  booktitle =	{Technical Communications of the 33rd International Conference on Logic Programming (ICLP 2017)},
  pages =	{11:1--11:2},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-058-3},
  ISSN =	{2190-6807},
  year =	{2018},
  volume =	{58},
  editor =	{Rocha, Ricardo and Son, Tran Cao and Mears, Christopher and Saeedloei, Neda},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.ICLP.2017.11},
  URN =		{urn:nbn:de:0030-drops-84595},
  doi =		{10.4230/OASIcs.ICLP.2017.11},
  annote =	{Keywords: Multi-agent Path Finding, SAT, MIP, Picat}
}
Document
Front Matter
DOI: 10.4230/OASIcs.SLATE.2013.i
Frontmatter

Authors: José Paulo Leal, Ricardo Rocha, and Alberto Simões

Published in: OASIcs, Volume 29, 2nd Symposium on Languages, Applications and Technologies (2013)

Abstract
The success of the humankind relies on our ability to communicate and transform the world. For ages we developed tools and technologies that allowed us to thrive and prosper. As we expanded to every corner of the planet we created languages that enabled us to communicate and record knowledge, even if they also become barriers to communication in themselves. Technology and language have always been interconnected. Technologies to record language gave birth to history and the written language allowed us to preserve knowledge, including knowledge on technologies. Technology reshaped language as books, radio shows or motion pictures made us aware of how other people communicate. But technologies and language were not completely blend together until computers and networks become our favourite tool to communicate and transform the world. The goal of the Symposium on Languages, Applications and Technologies (SLATE) is to be a forum to discuss the different ways in which language and technology interplay in computer science, and they are many. The symposium is divided into three main tracks, each one focusing a specific aspect of languages, from natural languages to compilers. * The HHL (Human-Human Languages) track is dedicated to the discussion of research projects and ideas involving natural language processing and their industrial application. * The HCL (Human-Computer Languages) track is where researchers, developers and educators exchange ideas and information on the latest academic or industrial work on language design, processing, assessment and applications. * The CCL (Computer-Computer Languages) track main goal is to provide a broad space for discussion about the XML markup language, examples of usage and associated technologies. SLATE follows the footsteps of two former conferences: CoRTA, the Conference on Compilers, Related Technologies and Applications; and XATA, the conference on XML, Applications and Applied Technologies, both with more than a decade of history. This volume contains the proceedings of the 2nd edition of SLATE, held in the Department of Computer Science, Faculty of Sciences, University of Porto, Portugal, during June 20-21, 2013. This year, SLATE received a total of 26 paper submissions for the three tracks. Each submission was reviewed by at least three Program Committee members, which included 55 researchers (counting sub-reviewers). At the end, 19 papers were selected for publication and presentation at the symposium, resulting in a 27% rejection rate. The set of accepted papers present a variety of contributions and were divided into the following five sessions for presentation at the symposium: * Software Development Tools, includes four articles on programming languages compilation and analysis; * XML and Applications, includes four articles on the usage of XML in different areas, ranging from the annotation of documents to its use on the semantic web; * Languages on Learning Environments, includes three articles that focus the automation on exercises generation and evaluation; * Domain Specific Languages, includes four articles on languages for specific languages, from music, robots or graphical user interfaces; * Natural Language Processing, includes four articles related to processing and teaching natural languages. In addition to these sessions, the program also included two keynote presentations, one on the PICAT system, a scalable logic-based language, by Neng-Fa Zhou (Brooklyn College, New York), and another on software languages and their history, by Jean-Marie Favre (University of Grenoble, France). The organizers of SLATE 2013 are in debt to many people without whom this event would never been possible. We wish to thank to our sponsors for making this event possible and to the EasyChair conference management system for simplifying our task. Thanks must go also to the authors of all submitted papers for their contribution and interest in the symposium and to the participants for making the event a meeting point for a fruitful exchange of ideas and feedback on recent developments. Finally, we want to express our gratitude to the Program Committee members and sub-reviewers, as the symposium would not have been possible without their dedicated time and knowledge in evaluating and ranking so many submissions from so many different topics. To all, our deepest thanks!
Cite as

2nd Symposium on Languages, Applications and Technologies. Open Access Series in Informatics (OASIcs), Volume 29, pp. i-xiv, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{leal_et_al:OASIcs.SLATE.2013.i,
  author =	{Leal, Jos\'{e} Paulo and Rocha, Ricardo and Sim\~{o}es, Alberto},
  title =	{{Frontmatter}},
  booktitle =	{2nd Symposium on Languages, Applications and Technologies},
  pages =	{i--xiv},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-52-1},
  ISSN =	{2190-6807},
  year =	{2013},
  volume =	{29},
  editor =	{Leal, Jos\'{e} Paulo and Rocha, Ricardo and Sim\~{o}es, Alberto},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SLATE.2013.i},
  URN =		{urn:nbn:de:0030-drops-40473},
  doi =		{10.4230/OASIcs.SLATE.2013.i},
  annote =	{Keywords: natural language processing, interoperabilty languages, compilers, languages}
}
Document
Invited Talk
DOI: 10.4230/OASIcs.SLATE.2013.5
Picat: A Scalable Logic-based Language and System (Invited Talk)

Authors: Neng-Fa Zhou

Published in: OASIcs, Volume 29, 2nd Symposium on Languages, Applications and Technologies (2013)

Abstract
This talk will give the design principles of the Picat language (http://www.picat-lang.org), highlight the high-level and intuitive abstractions provided by Picat for easy programming, and contemplate why Picat is more robust and scalable than Prolog and could be more accessible than Prolog to ordinary programmers for scripting and modeling tasks.
Cite as

Neng-Fa Zhou. Picat: A Scalable Logic-based Language and System (Invited Talk). In 2nd Symposium on Languages, Applications and Technologies. Open Access Series in Informatics (OASIcs), Volume 29, pp. 5-6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{zhou:OASIcs.SLATE.2013.5,
  author =	{Zhou, Neng-Fa},
  title =	{{Picat: A Scalable Logic-based Language and System}},
  booktitle =	{2nd Symposium on Languages, Applications and Technologies},
  pages =	{5--6},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-52-1},
  ISSN =	{2190-6807},
  year =	{2013},
  volume =	{29},
  editor =	{Leal, Jos\'{e} Paulo and Rocha, Ricardo and Sim\~{o}es, Alberto},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SLATE.2013.5},
  URN =		{urn:nbn:de:0030-drops-40273},
  doi =		{10.4230/OASIcs.SLATE.2013.5},
  annote =	{Keywords: Functions, Relations, Loops, Constraints, Tabling}
}
  • Refine by Type
  • 6 Document/PDF
  • 1 Document/HTML

  • Refine by Publication Year
  • 1 2025
  • 1 2024
  • 1 2023
  • 1 2018
  • 2 2013

  • Refine by Author
  • 4 Zhou, Neng-Fa
  • 1 Banbara, Mutsunori
  • 1 Bartak, Roman
  • 1 Inoue, Katsumi
  • 1 Le Berre, Daniel
  • Show More...

  • Refine by Series/Journal
  • 3 LIPIcs
  • 3 OASIcs

  • 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 → Discrete space search

  • Refine by Keyword
  • 2 Graph constraints
  • 2 SAT encoding
  • 1 Acyclic constraint
  • 1 CEGAR
  • 1 Constraints
  • 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