Search Results

Documents authored by Cherif, Sami

Artifact
Software
DOI: 10.4230/artifacts.26928
NLIPSat

Authors: Zhengling Yangli, Zhifei Zheng, Sami Cherif, Rui Sá Shibasaki, and Chu-Min Li

Abstract
Cite as

Zhengling Yangli, Zhifei Zheng, Sami Cherif, Rui Sá Shibasaki, Chu-Min Li. NLIPSat (Software, Source Code). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-26928,
   title = {{NLIPSat}}, 
   author = {Yangli, Zhengling and Zheng, Zhifei and Cherif, Sami and Shibasaki, Rui S\'{a} and Li, Chu-Min},
   note = {Software, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:1567209c46a147ae48868eca1e8a5b44f4fceed3;origin=https://github.com/ZhenglingYangli/NLIPSat-Toolkit;visit=swh:1:snp:ab40e9a04170812cbc1e7545f1e7cd0bfa88a38a;anchor=swh:1:rev:95f138d8b5721c72011108a89f865bc6c342e254}{\texttt{swh:1:dir:1567209c46a147ae48868eca1e8a5b44f4fceed3}} (visited on 2026-07-16)},
   url = {https://github.com/ZhenglingYangli/NLIPSat-Toolkit},
   doi = {10.4230/artifacts.26928},
}
Document
Tool Paper
DOI: 10.4230/LIPIcs.SAT.2026.43
NLIPSat: Satisfiability-Based Nonlinear Integer Programming Encoding Toolkit (Tool Paper)

Authors: Zhengling Yangli, Zhifei Zheng, Sami Cherif, Rui Sá Shibasaki, and Chu-Min Li

Published in: LIPIcs, Volume 377, 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)

Abstract
While Maximum Satisfiability (MaxSAT) has been successfully applied to a wide range of combinatorial optimization problems, the encoding of Nonlinear Integer Programming (NLIP) with polynomial functions into MaxSAT has so far only been studied at a theoretical level. In this paper, we introduce NLIPSat, the first tool capable of encoding bounded polynomial NLIP instances directly into Maximum Satisfiability. Building upon recent MaxSAT formulations for polynomial NLIP proposed in [Zhifei Zheng et al., 2025], NLIPSat enables the encoding of polynomial nonlinear objective functions as weighted soft clauses and also supports the encoding of hard non-linear polynomial constraints within a polynomial setting. Extensive experiments on different benchmarks show that NLIPSat outperforms the state-of-the-art SMT solver Z3 by a wide margin.
Cite as

Zhengling Yangli, Zhifei Zheng, Sami Cherif, Rui Sá Shibasaki, and Chu-Min Li. NLIPSat: Satisfiability-Based Nonlinear Integer Programming Encoding Toolkit (Tool Paper). In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 43:1-43:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{yangli_et_al:LIPIcs.SAT.2026.43,
  author =	{Yangli, Zhengling and Zheng, Zhifei and Cherif, Sami and Shibasaki, Rui S\'{a} and Li, Chu-Min},
  title =	{{NLIPSat: Satisfiability-Based Nonlinear Integer Programming Encoding Toolkit}},
  booktitle =	{29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
  pages =	{43:1--43:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-431-4},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{377},
  editor =	{Ignatiev, Alexey and Szeider, Stefan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.43},
  URN =		{urn:nbn:de:0030-drops-263492},
  doi =		{10.4230/LIPIcs.SAT.2026.43},
  annote =	{Keywords: Maximum Satisfiability, Nonlinear Integer Programming, Encodings, Tool}
}
Artifact
Software
DOI: 10.4230/artifacts.26907
SAT_for_TOKEN

Authors: Asma Khoualdia, Sami Cherif, Stéphane Devismes, and Léo Robert

Abstract
Cite as

Asma Khoualdia, Sami Cherif, Stéphane Devismes, Léo Robert. SAT_for_TOKEN (Software, Source Code and Benchmarks). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-26907,
   title = {{SAT\underlinefor\underlineTOKEN}}, 
   author = {Khoualdia, Asma and Cherif, Sami and Devismes, St\'{e}phane and Robert, L\'{e}o},
   note = {Software, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:0fe597aebfaba66c4b306d44a44a9e49dcf277d5;origin=https://github.com/asmakhoualdia98/async-token-circulation-sat;visit=swh:1:snp:ae3075e2950c87577ec2f3dabe7f025019446011;anchor=swh:1:rev:de00109298c91e2a931f90806309c549b1e4e247}{\texttt{swh:1:dir:0fe597aebfaba66c4b306d44a44a9e49dcf277d5}} (visited on 2026-07-13)},
   url = {https://github.com/asmakhoualdia98/async-token-circulation-sat},
   doi = {10.4230/artifacts.26907},
}
Artifact
Software
DOI: 10.4230/artifacts.25917
DA_kissat_MAB

Authors: Jinghu Liang, Sami Cherif, and Chu-Min Li

Abstract
Cite as

Jinghu Liang, Sami Cherif, Chu-Min Li. DA_kissat_MAB (Software, Source Code). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-25917,
   title = {{DA\underlinekissat\underlineMAB}}, 
   author = {Liang, Jinghu and Cherif, Sami and Li, Chu-Min},
   note = {Software, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:6a87ea34fdb8dfef213682f2d9dbfd0523d605e1;origin=https://github.com/JinghuLiang/Duration_Aware_kissat_MAB;visit=swh:1:snp:87ac8f74937a77042d5513b82a8be598e191d0bf;anchor=swh:1:rev:6cb1221a9de2d01602294c3c5cf4e12e269007fe}{\texttt{swh:1:dir:6a87ea34fdb8dfef213682f2d9dbfd0523d605e1}} (visited on 2026-07-13)},
   url = {https://github.com/JinghuLiang/Duration_Aware_kissat_MAB},
   doi = {10.4230/artifacts.25917},
}
Document
DOI: 10.4230/LIPIcs.CP.2026.5
Satisfiability for Large Weight Syndrome Decoding

Authors: Carl Berton, Sami Cherif, and Claire Delaplace

Published in: LIPIcs, Volume 379, 32nd International Conference on Principles and Practice of Constraint Programming (CP 2026)

Abstract
The Large Weight Syndrome Decoding problem LWSD is a fundamental problem in coding theory. It consists in determining whether a given linear code admits a high Hamming weight vector associated with a specific syndrome. LWSD is a variant of the classical syndrome decoding problem, which conversely seeks a low Hamming weight solution for a linear system defined over the binary field 𝔽₂. In this paper, we investigate a generalization of this problem to the case of a prime finite field 𝔽_Z, referred to as LWZSD. We propose several models using Boolean Satisfiability (SAT) formulas and compare the efficiency of our approaches using state-of-the-art solvers.
Cite as

Carl Berton, Sami Cherif, and Claire Delaplace. Satisfiability for Large Weight Syndrome Decoding. In 32nd International Conference on Principles and Practice of Constraint Programming (CP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 379, pp. 5:1-5:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{berton_et_al:LIPIcs.CP.2026.5,
  author =	{Berton, Carl and Cherif, Sami and Delaplace, Claire},
  title =	{{Satisfiability for Large Weight Syndrome Decoding}},
  booktitle =	{32nd International Conference on Principles and Practice of Constraint Programming (CP 2026)},
  pages =	{5:1--5:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-432-1},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{379},
  editor =	{Beldiceanu, Nicolas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2026.5},
  URN =		{urn:nbn:de:0030-drops-266385},
  doi =		{10.4230/LIPIcs.CP.2026.5},
  annote =	{Keywords: Large Weight Syndrome Decoding, Satisfiability, Cryptography}
}
Document
DOI: 10.4230/LIPIcs.CP.2026.32
On the Self-Stabilization of Dijkstra’s Asynchronous Token Circulation

Authors: Asma Khoualdia, Sami Cherif, Stéphane Devismes, and Léo Robert

Published in: LIPIcs, Volume 379, 32nd International Conference on Principles and Practice of Constraint Programming (CP 2026)

Abstract
Dijkstra’s token ring algorithm is a fundamental example of a self-stabilizing algorithm for solving mutual exclusion in an asynchronous distributed system arranged as a rooted directed ring. This paper studies the self-stabilization of this algorithm using an approach based on propositional satisfiability. We propose a logical modeling framework for the asynchronous executions of the algorithm that rigorously captures the state update rules, as well as the mechanisms for detecting convergence toward a legitimate configuration or, conversely, divergence through the existence of cycles between illegitimate configurations. Furthermore, we also optimize the efficiency and scalability of the analysis by introducing an offset-based symmetry-breaking technique applied to the initial configurations, thereby significantly reducing redundant explorations of equivalent execution scenarios. In addition, we extend the study to restricted daemon assumptions to assess open challenges.
Cite as

Asma Khoualdia, Sami Cherif, Stéphane Devismes, and Léo Robert. On the Self-Stabilization of Dijkstra’s Asynchronous Token Circulation. In 32nd International Conference on Principles and Practice of Constraint Programming (CP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 379, pp. 32:1-32:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{khoualdia_et_al:LIPIcs.CP.2026.32,
  author =	{Khoualdia, Asma and Cherif, Sami and Devismes, St\'{e}phane and Robert, L\'{e}o},
  title =	{{On the Self-Stabilization of Dijkstra’s Asynchronous Token Circulation}},
  booktitle =	{32nd International Conference on Principles and Practice of Constraint Programming (CP 2026)},
  pages =	{32:1--32:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-432-1},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{379},
  editor =	{Beldiceanu, Nicolas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2026.32},
  URN =		{urn:nbn:de:0030-drops-266645},
  doi =		{10.4230/LIPIcs.CP.2026.32},
  annote =	{Keywords: Self-stabilization, Token Circulation, Asynchronism, Satisfiability}
}
Document
DOI: 10.4230/LIPIcs.CP.2026.39
Not All Restarts Are Equal: MAB-Learning at the Right Time Scale for SAT

Authors: Jinghu Liang, Sami Cherif, and Chu-Min Li

Published in: LIPIcs, Volume 379, 32nd International Conference on Principles and Practice of Constraint Programming (CP 2026)

Abstract
Multi-Armed Bandit (MAB) mechanisms have proven effective for adaptive heuristic switching in modern CDCL SAT solvers, with Kissat_MAB and its variants demonstrating strong performance in recent SAT Competitions. However, while strategies like the Luby series generate restarts with high duration variability, standard bandit models treat each restart as a homogeneous unit. This mismatch can bias credit assignment and lead to suboptimal exploration–exploitation trade-offs between short and long restarts. In this paper, we study MAB-based heuristic selection under variable-duration restart policies and propose a duration-aware modification to both bandit feedback and selection mechanisms. Our approach normalizes and conditions rewards on the restarts and adapts exploration and exploitation accordingly, thereby better aligning bandit updates with the solver’s restart dynamics.
Cite as

Jinghu Liang, Sami Cherif, and Chu-Min Li. Not All Restarts Are Equal: MAB-Learning at the Right Time Scale for SAT. In 32nd International Conference on Principles and Practice of Constraint Programming (CP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 379, pp. 39:1-39:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{liang_et_al:LIPIcs.CP.2026.39,
  author =	{Liang, Jinghu and Cherif, Sami and Li, Chu-Min},
  title =	{{Not All Restarts Are Equal: MAB-Learning at the Right Time Scale for SAT}},
  booktitle =	{32nd International Conference on Principles and Practice of Constraint Programming (CP 2026)},
  pages =	{39:1--39:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-432-1},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{379},
  editor =	{Beldiceanu, Nicolas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2026.39},
  URN =		{urn:nbn:de:0030-drops-266718},
  doi =		{10.4230/LIPIcs.CP.2026.39},
  annote =	{Keywords: Satisfiablity, Branching, Restart, Multi-Armed Bandit}
}
Document
DOI: 10.4230/LIPIcs.CP.2026.60
Enhanced Lower Bound Computation in Branch-and-Bound for MaxSAT

Authors: Jialu Zhang, Chu-Min Li, Sami Cherif, and Shuolin Li

Published in: LIPIcs, Volume 379, 32nd International Conference on Principles and Practice of Constraint Programming (CP 2026)

Abstract
Maximum Satisfiability (MaxSAT) is an optimization extension of the Satisfiability (SAT) problem. In Branch-and-Bound (BnB) MaxSAT solving, the quality of the lower bound estimation is critical for effective search space pruning. State-of-the-art BnB solvers typically estimate this bound by identifying disjoint inconsistent subformulas (cores) via Unit Propagation (UP). However, a limitation of this standard approach is that UP fails to detect cores that exhibit complex dependencies with already identified cores. In this paper, we propose a further lookahead algorithm that leverages pre-detected cores to uncover additional disjoint inconsistencies, thereby tightening the lower bound. Experimental results demonstrate that the proposed algorithm significantly tightens the lower bound, enabling the state of the art BnB solver MaxCDCL to solve more instances.
Cite as

Jialu Zhang, Chu-Min Li, Sami Cherif, and Shuolin Li. Enhanced Lower Bound Computation in Branch-and-Bound for MaxSAT. In 32nd International Conference on Principles and Practice of Constraint Programming (CP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 379, pp. 60:1-60:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{zhang_et_al:LIPIcs.CP.2026.60,
  author =	{Zhang, Jialu and Li, Chu-Min and Cherif, Sami and Li, Shuolin},
  title =	{{Enhanced Lower Bound Computation in Branch-and-Bound for MaxSAT}},
  booktitle =	{32nd International Conference on Principles and Practice of Constraint Programming (CP 2026)},
  pages =	{60:1--60:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-432-1},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{379},
  editor =	{Beldiceanu, Nicolas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2026.60},
  URN =		{urn:nbn:de:0030-drops-266935},
  doi =		{10.4230/LIPIcs.CP.2026.60},
  annote =	{Keywords: Maximum Satisfiability, Branch and Bound, Lower Bound}
}
Artifact
Software
DOI: 10.4230/artifacts.23375
SAT_for_UNISON

Authors: Asma Khoualdia, Sami Cherif, Stéphane Devismes, and Léo Robert

Abstract
Cite as

Asma Khoualdia, Sami Cherif, Stéphane Devismes, Léo Robert. SAT_for_UNISON (Software, Source Code and Benchmarks). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-23375,
   title = {{SAT\underlinefor\underlineUNISON}}, 
   author = {Khoualdia, Asma and Cherif, Sami and Devismes, St\'{e}phane and Robert, L\'{e}o},
   note = {Software, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:4bc78d189155024f85110cb2dc9ae4aeb470d8bf;origin=https://github.com/asmakhoualdia98/SU_SAT_Exec;visit=swh:1:snp:af5a3ce14a7b5fdca4086ba55a5d21370fe4d3cb;anchor=swh:1:rev:6905da4a2f2dd404ea072c647393ba1f58ba0b4c}{\texttt{swh:1:dir:4bc78d189155024f85110cb2dc9ae4aeb470d8bf}} (visited on 2025-08-08)},
   url = {https://github.com/asmakhoualdia98/SU_SAT_Exec},
   doi = {10.4230/artifacts.23375},
}
Document
DOI: 10.4230/LIPIcs.CP.2025.19
Analyzing Self-Stabilization of Synchronous Unison via Propositional Satisfiability

Authors: Asma Khoualdia, Sami Cherif, Stéphane Devismes, and Léo Robert

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

Abstract
Synchronous unison is a classical clock synchronization problem in distributed computing, and especially in self-stabilization. This paper explores the self-stabilization of a synchronous unison algorithm proposed by Arora et al. using a propositional satisfiability-based approach. We give a logical formulation of the algorithm. This formulation includes the uniqueness of clock values at each node, the updates of clocks based on the minimum clock value in the neighborhood, and the detection of convergence or divergence. To optimize the models, additional constraints are introduced to reduce redundant cases of initial configurations to be analyzed. Our approach not only verifies the algorithm’s behaviour but also offers insights into enhancing its robustness and applicability to broader distributed systems.
Cite as

Asma Khoualdia, Sami Cherif, Stéphane Devismes, and Léo Robert. Analyzing Self-Stabilization of Synchronous Unison via Propositional Satisfiability. In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 19:1-19:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{khoualdia_et_al:LIPIcs.CP.2025.19,
  author =	{Khoualdia, Asma and Cherif, Sami and Devismes, St\'{e}phane and Robert, L\'{e}o},
  title =	{{Analyzing Self-Stabilization of Synchronous Unison via Propositional Satisfiability}},
  booktitle =	{31st International Conference on Principles and Practice of Constraint Programming (CP 2025)},
  pages =	{19:1--19:21},
  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.19},
  URN =		{urn:nbn:de:0030-drops-238806},
  doi =		{10.4230/LIPIcs.CP.2025.19},
  annote =	{Keywords: Self-stabilization, Synchronous Unison, Satisfiability}
}
Artifact
Software
DOI: 10.4230/artifacts.22455
ROADEF_SCHEDULING

Authors: Sami Cherif, Heythem Sattoutah, Chu-Min Li, Corinne Lucet, and Laure Brisoux-Devendeville

Abstract
Cite as

Sami Cherif, Heythem Sattoutah, Chu-Min Li, Corinne Lucet, Laure Brisoux-Devendeville. ROADEF_SCHEDULING (Software, Source Code,~Data,~Benchmark). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-22455,
   title = {{ROADEF\underlineSCHEDULING}}, 
   author = {Cherif, Sami and Sattoutah, Heythem and Li, Chu-Min and Lucet, Corinne and Brisoux-Devendeville, Laure},
   note = {Software, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:7083377094f69163d37d30b77d740c72c562139d;origin=https://github.com/satoutahhaithem/ROADEF_SCHEDULING;visit=swh:1:snp:c34fc60c52e7d5289f8e1c049ce6ba5e0adc48d2;anchor=swh:1:rev:92a1a45786ba37797dda7d78f7d02347f6f2a0a8}{\texttt{swh:1:dir:7083377094f69163d37d30b77d740c72c562139d}} (visited on 2024-11-28)},
   url = {https://github.com/satoutahhaithem/ROADEF_SCHEDULING},
   doi = {10.4230/artifacts.22455},
}
Document
Short Paper
DOI: 10.4230/LIPIcs.CP.2024.34
Minimizing Working-Group Conflicts in Conference Session Scheduling Through Maximum Satisfiability (Short Paper)

Authors: Sami Cherif, Heythem Sattoutah, Chu-Min Li, Corinne Lucet, and Laure Brisoux-Devendeville

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

Abstract
This paper explores the application of Maximum Satisfiability (Max-SAT) to the complex problem of conference session scheduling, with a particular focus on minimizing working-group conflicts within the context of the ROADEF conference, the largest French-speaking event aimed at bringing together researchers from various fields such as combinatorial optimization and operational research. A Max-SAT model is introduced then enhanced with new variables, and solved through state-of-the-art solvers. The results of applying our formulation to data from ROADEF demonstrate its ability to effectively compute session schedules, while enabling to reduce the number of conflicts and the maximum number of parallel sessions compared to the handmade solutions proposed by the organizing committees. These findings underscore the potential of Max-SAT as a valuable tool for optimizing conference scheduling processes, offering a systematic and efficient solution that ensures a smoother and more productive experience for attendees and organizers alike.
Cite as

Sami Cherif, Heythem Sattoutah, Chu-Min Li, Corinne Lucet, and Laure Brisoux-Devendeville. Minimizing Working-Group Conflicts in Conference Session Scheduling Through Maximum Satisfiability (Short Paper). In 30th International Conference on Principles and Practice of Constraint Programming (CP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 307, pp. 34:1-34:11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{cherif_et_al:LIPIcs.CP.2024.34,
  author =	{Cherif, Sami and Sattoutah, Heythem and Li, Chu-Min and Lucet, Corinne and Brisoux-Devendeville, Laure},
  title =	{{Minimizing Working-Group Conflicts in Conference Session Scheduling Through Maximum Satisfiability}},
  booktitle =	{30th International Conference on Principles and Practice of Constraint Programming (CP 2024)},
  pages =	{34:1--34:11},
  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.34},
  URN =		{urn:nbn:de:0030-drops-207190},
  doi =		{10.4230/LIPIcs.CP.2024.34},
  annote =	{Keywords: Maximum Satisfiability, Scheduling, Modeling}
}
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