Search Results

Documents authored by Zhong, Allen Z.

Artifact
Software
DOI: 10.4230/artifacts.24103
Huub: Lazy Clause Generation Solver

Authors: Jip J. Dekker, Alexey Ignatiev, Peter J. Stuckey, and Allen Z. Zhong

Abstract
Cite as

Jip J. Dekker, Alexey Ignatiev, Peter J. Stuckey, Allen Z. Zhong. Huub: Lazy Clause Generation Solver (Software, Source Code). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@misc{huub2025zenodo,
   title = {{Huub: Lazy Clause Generation Solver}}, 
   author = {Dekker, Jip J. and Ignatiev, Alexey and Stuckey, Peter J. and Zhong, Allen Z.},
   note = {Software, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:b28854946ae60e86a37051ea89465cce8b84b7ed}{\texttt{swh:1:dir:b28854946ae60e86a37051ea89465cce8b84b7ed}} (visited on 2025-08-08)},
   url = {https://github.com/huub-solver/huub},
   doi = {10.4230/artifacts.24103},
}
Document
DOI: 10.4230/LIPIcs.CP.2025.5
Transition Dominance in Domain-Independent Dynamic Programming

Authors: J. Christopher Beck, Ryo Kuroiwa, Jimmy H. M. Lee, Peter J. Stuckey, and Allen Z. Zhong

Published in: LIPIcs, Volume 340, 31st International Conference on Principles and Practice of Constraint Programming (CP 2025)

Abstract
Domain-independent dynamic programming (DIDP) is a model-based paradigm for dynamic programming (DP) that enables users to define DP models based on a state transition system. Heuristic search-based solvers have demonstrated strong performance in solving combinatorial optimization problems. In this paper, we formally define transition dominance in DIDP, where one transition consistently leads to better solutions than another, allowing the search process to safely ignore dominated transitions. To facilitate the efficient use of transition dominance, we introduce an interface for defining transition dominance and propose the use of state functions to cache values, thereby avoiding redundant computations when verifying transition dominance. Experimental results on DP models across multiple problem classes indicate that incorporating transition dominance and state functions yields a 5 to 10 times speed-up on average for different search algorithms within the DIDP framework compared to the baseline.
Cite as

J. Christopher Beck, Ryo Kuroiwa, Jimmy H. M. Lee, Peter J. Stuckey, and Allen Z. Zhong. Transition Dominance in Domain-Independent Dynamic Programming. In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 5:1-5:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{beck_et_al:LIPIcs.CP.2025.5,
  author =	{Beck, J. Christopher and Kuroiwa, Ryo and Lee, Jimmy H. M. and Stuckey, Peter J. and Zhong, Allen Z.},
  title =	{{Transition Dominance in Domain-Independent Dynamic Programming}},
  booktitle =	{31st International Conference on Principles and Practice of Constraint Programming (CP 2025)},
  pages =	{5:1--5:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-380-5},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{340},
  editor =	{de la Banda, Maria Garcia},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2025.5},
  URN =		{urn:nbn:de:0030-drops-238661},
  doi =		{10.4230/LIPIcs.CP.2025.5},
  annote =	{Keywords: Dominance, Dynamic Programming, Combinatorial Optimization}
}
Document
Short Paper
DOI: 10.4230/LIPIcs.CP.2025.42
Towards Modern and Modular SAT for LCG (Short Paper)

Authors: Jip J. Dekker, Alexey Ignatiev, Peter J. Stuckey, and Allen Z. Zhong

Published in: LIPIcs, Volume 340, 31st International Conference on Principles and Practice of Constraint Programming (CP 2025)

Abstract
Lazy Clause Generation (LCG) is an architecture for building Constraint Programming (CP) solvers using an underlying Boolean Satisfiability (SAT) engine. The CP propagation engine lazily creates clauses that define the integer variables and impose problem restrictions. The SAT engine uses the clausal model to reason and search, including, crucially, the generation of nogoods. However, while SAT solving has made significant advances recently, the underlying SAT technology in most LCG solvers has largely remained the same. Using a new interface to SAT engines, IPASIR-UP, we can construct an LCG solver which can swap out the underlying SAT engine with any that supports the interface. This new approach means we need to revisit many of the design and engineering decisions for LCG solvers, to take maximum advantage of a better underlying SAT engine while adhering to the restrictions of the interface. In this paper, we explore the possibilities and challenges of using IPASIR-UP for LCG, showing that it can be used to create a highly competitive solver.
Cite as

Jip J. Dekker, Alexey Ignatiev, Peter J. Stuckey, and Allen Z. Zhong. Towards Modern and Modular SAT for LCG (Short Paper). In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 42:1-42:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{dekker_et_al:LIPIcs.CP.2025.42,
  author =	{Dekker, Jip J. and Ignatiev, Alexey and Stuckey, Peter J. and Zhong, Allen Z.},
  title =	{{Towards Modern and Modular SAT for LCG}},
  booktitle =	{31st International Conference on Principles and Practice of Constraint Programming (CP 2025)},
  pages =	{42:1--42:12},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-380-5},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{340},
  editor =	{de la Banda, Maria Garcia},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2025.42},
  URN =		{urn:nbn:de:0030-drops-239038},
  doi =		{10.4230/LIPIcs.CP.2025.42},
  annote =	{Keywords: Lazy Clause Generation, Boolean Satisfiability, IPASIR-UP}
}
Document
DOI: 10.4230/LIPIcs.CP.2022.31
Exploiting Functional Constraints in Automatic Dominance Breaking for Constraint Optimization

Authors: Jimmy H. M. Lee and Allen Z. Zhong

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

Abstract
Dominance breaking is an effective technique to reduce the time for solving constraint optimization problems. Lee and Zhong propose an automatic dominance breaking framework for a class of constraint optimization problems based on specific forms of objectives and constraints. In this paper, we propose to enhance the framework for problems with nested function calls which can be flattened to functional constraints. In particular, we focus on aggregation functions and exploit such properties as monotonicity, commutativity and associativity to give an efficient procedure for generating effective dominance breaking nogoods. Experimentation also shows orders-of-magnitude runtime speedup using the generated dominance breaking nogoods and demonstrates the ability of our proposal to reveal dominance relations in the literature and discover new dominance relations on problems with ineffective or no known dominance breaking constraints.
Cite as

Jimmy H. M. Lee and Allen Z. Zhong. Exploiting Functional Constraints in Automatic Dominance Breaking for Constraint Optimization. In 28th International Conference on Principles and Practice of Constraint Programming (CP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 235, pp. 31:1-31:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{lee_et_al:LIPIcs.CP.2022.31,
  author =	{Lee, Jimmy H. M. and Zhong, Allen Z.},
  title =	{{Exploiting Functional Constraints in Automatic Dominance Breaking for Constraint Optimization}},
  booktitle =	{28th International Conference on Principles and Practice of Constraint Programming (CP 2022)},
  pages =	{31:1--31:17},
  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.31},
  URN =		{urn:nbn:de:0030-drops-166607},
  doi =		{10.4230/LIPIcs.CP.2022.31},
  annote =	{Keywords: Constraint Optimization Problems, Dominance Breaking}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

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