DROPS

Artifact

Software

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}
}

Document

DOI: 10.4230/LIPIcs.FUN.2021.20

Card-Based ZKP Protocols for Takuzu and Juosan

Authors: Daiki Miyahara, Léo Robert, Pascal Lafourcade, So Takeshige, Takaaki Mizuki, Kazumasa Shinagawa, Atsuki Nagao, and Hideaki Sone

Published in: LIPIcs, Volume 157, 10th International Conference on Fun with Algorithms (FUN 2021) (2020)

Abstract

Takuzu and Juosan are logical Nikoli games in the spirit of Sudoku. In Takuzu, a grid must be filled with 0’s and 1’s under specific constraints. In Juosan, the grid must be filled with vertical and horizontal dashes with specific constraints. We give physical algorithms using cards to realize zero-knowledge proofs for those games. The goal is to allow a player to show that he/she has the solution without revealing it. Previous work on Takuzu showed a protocol with multiple instances needed. We propose two improvements: only one instance needed and a soundness proof. We also propose a similar proof for Juosan game.

Cite as

Daiki Miyahara, Léo Robert, Pascal Lafourcade, So Takeshige, Takaaki Mizuki, Kazumasa Shinagawa, Atsuki Nagao, and Hideaki Sone. Card-Based ZKP Protocols for Takuzu and Juosan. In 10th International Conference on Fun with Algorithms (FUN 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 157, pp. 20:1-20:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{miyahara_et_al:LIPIcs.FUN.2021.20,
  author =	{Miyahara, Daiki and Robert, L\'{e}o and Lafourcade, Pascal and Takeshige, So and Mizuki, Takaaki and Shinagawa, Kazumasa and Nagao, Atsuki and Sone, Hideaki},
  title =	{{Card-Based ZKP Protocols for Takuzu and Juosan}},
  booktitle =	{10th International Conference on Fun with Algorithms (FUN 2021)},
  pages =	{20:1--20:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-145-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{157},
  editor =	{Farach-Colton, Martin and Prencipe, Giuseppe and Uehara, Ryuhei},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FUN.2021.20},
  URN =		{urn:nbn:de:0030-drops-127817},
  doi =		{10.4230/LIPIcs.FUN.2021.20},
  annote =	{Keywords: Zero-knowledge proof, Card-based cryptography, Takuzu, Juosan}
}

Search Results

Documents authored by Robert, Léo

SAT_for_UNISON

Abstract

Cite as

Analyzing Self-Stabilization of Synchronous Unison via Propositional Satisfiability

Abstract

Cite as

Card-Based ZKP Protocols for Takuzu and Juosan

Abstract

Cite as

Thanks for your feedback!

Could not send message