Search Results

Documents authored by Habet, Djamal

Document
DOI: 10.4230/LIPIcs.CP.2023.16
A CP Approach for the Liner Shipping Network Design Problem

Authors: Yousra El Ghazi, Djamal Habet, and Cyril Terrioux

Published in: LIPIcs, Volume 280, 29th International Conference on Principles and Practice of Constraint Programming (CP 2023)

Abstract
The liner shipping network design problem consists, for a shipowner, in determining, on the one hand, which maritime lines (in the form of rotations serving a set of ports) to open, and, on the other hand, the assignment of ships (container ships) with the adapted sizes for the different lines to carry all the container flows. In this paper, we propose a modeling of this problem using constraint programming. Then, we present a preliminary study of its solving using a state-of-the-art solver, namely the OR-Tools CP-SAT solver.
Cite as

Yousra El Ghazi, Djamal Habet, and Cyril Terrioux. A CP Approach for the Liner Shipping Network Design Problem. In 29th International Conference on Principles and Practice of Constraint Programming (CP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 280, pp. 16:1-16:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{elghazi_et_al:LIPIcs.CP.2023.16,
  author =	{El Ghazi, Yousra and Habet, Djamal and Terrioux, Cyril},
  title =	{{A CP Approach for the Liner Shipping Network Design Problem}},
  booktitle =	{29th International Conference on Principles and Practice of Constraint Programming (CP 2023)},
  pages =	{16:1--16:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-300-3},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{280},
  editor =	{Yap, Roland H. C.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2023.16},
  URN =		{urn:nbn:de:0030-drops-190532},
  doi =		{10.4230/LIPIcs.CP.2023.16},
  annote =	{Keywords: Constraint optimization problem, modeling, solving, industrial application}
}
Document
DOI: 10.4230/LIPIcs.CP.2022.12
From Crossing-Free Resolution to Max-SAT Resolution

Authors: Mohamed Sami Cherif, Djamal Habet, and Matthieu Py

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

Abstract
Adapting a SAT resolution proof into a Max-SAT resolution proof without considerably increasing its size is an open problem. Read-once resolution, where each clause is used at most once in the proof, represents the only fragment of resolution for which an adaptation using exclusively Max-SAT resolution is known and trivial. Proofs containing non read-once clauses are difficult to adapt because the Max-SAT resolution rule replaces the premises by the conclusions. This paper contributes to this open problem by defining, for the first time since the introduction of Max-SAT resolution, a new fragment of resolution whose proofs can be adapted to Max-SAT resolution proofs without substantially increasing their size. In this fragment, called crossing-free resolution, non read-once clauses are used independently to infer new information thus enabling to bring along each non read-once clause while unfolding the proof until a substitute is required.
Cite as

Mohamed Sami Cherif, Djamal Habet, and Matthieu Py. From Crossing-Free Resolution to Max-SAT Resolution. In 28th International Conference on Principles and Practice of Constraint Programming (CP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 235, pp. 12:1-12:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{cherif_et_al:LIPIcs.CP.2022.12,
  author =	{Cherif, Mohamed Sami and Habet, Djamal and Py, Matthieu},
  title =	{{From Crossing-Free Resolution to Max-SAT Resolution}},
  booktitle =	{28th International Conference on Principles and Practice of Constraint Programming (CP 2022)},
  pages =	{12:1--12: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.12},
  URN =		{urn:nbn:de:0030-drops-166412},
  doi =		{10.4230/LIPIcs.CP.2022.12},
  annote =	{Keywords: Satisfiability, Proof, Max-SAT Resolution}
}
Document
DOI: 10.4230/LIPIcs.CP.2021.20
Combining VSIDS and CHB Using Restarts in SAT

Authors: Mohamed Sami Cherif, Djamal Habet, and Cyril Terrioux

Published in: LIPIcs, Volume 210, 27th International Conference on Principles and Practice of Constraint Programming (CP 2021)

Abstract
Conflict Driven Clause Learning (CDCL) solvers are known to be efficient on structured instances and manage to solve ones with a large number of variables and clauses. An important component in such solvers is the branching heuristic which picks the next variable to branch on. In this paper, we evaluate different strategies which combine two state-of-the-art heuristics, namely the Variable State Independent Decaying Sum (VSIDS) and the Conflict History-Based (CHB) branching heuristic. These strategies take advantage of the restart mechanism, which helps to deal with the heavy-tailed phenomena in SAT, to switch between these heuristics thus ensuring a better and more diverse exploration of the search space. Our experimental evaluation shows that combining VSIDS and CHB using restarts achieves competitive results and even significantly outperforms both heuristics for some chosen strategies.
Cite as

Mohamed Sami Cherif, Djamal Habet, and Cyril Terrioux. Combining VSIDS and CHB Using Restarts in SAT. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 20:1-20:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{cherif_et_al:LIPIcs.CP.2021.20,
  author =	{Cherif, Mohamed Sami and Habet, Djamal and Terrioux, Cyril},
  title =	{{Combining VSIDS and CHB Using Restarts in SAT}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{20:1--20:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.20},
  URN =		{urn:nbn:de:0030-drops-153110},
  doi =		{10.4230/LIPIcs.CP.2021.20},
  annote =	{Keywords: Satisfiability, Branching Heuristic, Restarts}
}
Document
DOI: 10.4230/LIPIcs.CP.2021.38
Combining Clause Learning and Branch and Bound for MaxSAT

Authors: Chu-Min Li, Zhenxing Xu, Jordi Coll, Felip Manyà, Djamal Habet, and Kun He

Published in: LIPIcs, Volume 210, 27th International Conference on Principles and Practice of Constraint Programming (CP 2021)

Abstract
Branch and Bound (BnB) is a powerful technique that has been successfully used to solve many combinatorial optimization problems. However, MaxSAT is a notorious exception because BnB MaxSAT solvers perform poorly on many instances encoding interesting real-world and academic optimization problems. This has formed a prevailing opinion in the community stating that BnB is not so useful for MaxSAT, except for random and some special crafted instances. In fact, there has been no advance allowing to significantly speed up BnB MaxSAT solvers in the past few years, as illustrated by the absence of BnB solvers in the annual MaxSAT Evaluation since 2017. Our work aims to change this situation and proposes a new BnB MaxSAT solver, called MaxCDCL, by combining clause learning and an efficient bounding procedure. The experimental results show that, contrary to the prevailing opinion, BnB can be competitive for MaxSAT. MaxCDCL is ranked among the top 5 solvers of the 15 solvers that participated in the 2020 MaxSAT Evaluation, solving a number of instances that other solvers cannot solve. Furthermore, MaxCDCL, when combined with the best existing solvers, solves the highest number of instances of the MaxSAT Evaluations.
Cite as

Chu-Min Li, Zhenxing Xu, Jordi Coll, Felip Manyà, Djamal Habet, and Kun He. Combining Clause Learning and Branch and Bound for MaxSAT. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 38:1-38:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{li_et_al:LIPIcs.CP.2021.38,
  author =	{Li, Chu-Min and Xu, Zhenxing and Coll, Jordi and Many\`{a}, Felip and Habet, Djamal and He, Kun},
  title =	{{Combining Clause Learning and Branch and Bound for MaxSAT}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{38:1--38:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.38},
  URN =		{urn:nbn:de:0030-drops-153291},
  doi =		{10.4230/LIPIcs.CP.2021.38},
  annote =	{Keywords: MaxSAT, Branch\&Bound, CDCL}
}
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-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact