Search Results

Documents authored by Shaik, Irfansha

Artifact
Software
DOI: 10.4230/artifacts.22468
Q-Synth

Authors: Irfansha Shaik and Jaco van de Pol

Abstract
Cite as

Irfansha Shaik, Jaco van de Pol. Q-Synth (Software). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-22468,
   title = {{Q-Synth}}, 
   author = {Shaik, Irfansha and van de Pol, Jaco},
   note = {Software, version 2.0., IFD (Innovation Fund Denmark), swhId: \href{https://archive.softwareheritage.org/swh:1:dir:be31c57364bd541c6b65afac80603e9004cf4008;origin=https://github.com/irfansha/Q-Synth;visit=swh:1:snp:f376849e93533f1d9039b7cd543ed56b6edcf01d;anchor=swh:1:rev:553d54c9942b73a0246328d42565caaaaac38117}{\texttt{swh:1:dir:be31c57364bd541c6b65afac80603e9004cf4008}} (visited on 2024-11-28)},
   url = {https://github.com/irfansha/Q-Synth},
   doi = {10.4230/artifacts.22468},
}
Artifact
Software
DOI: 10.4230/artifacts.22469
Q-Synth v2.0 release

Authors: Irfansha Shaik and Jaco van de Pol

Abstract
Cite as

Irfansha Shaik, Jaco van de Pol. Q-Synth v2.0 release (Software, Github Tag). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-22469,
   title = {{Q-Synth v2.0 release}}, 
   author = {Shaik, Irfansha and van de Pol, Jaco},
   note = {Software, version 2.0., IFD (Innovation Fund Denmark), swhId: \href{https://archive.softwareheritage.org/swh:1:dir:be31c57364bd541c6b65afac80603e9004cf4008;origin=https://github.com/irfansha/Q-Synth;visit=swh:1:snp:f376849e93533f1d9039b7cd543ed56b6edcf01d;anchor=swh:1:rev:553d54c9942b73a0246328d42565caaaaac38117}{\texttt{swh:1:dir:be31c57364bd541c6b65afac80603e9004cf4008}} (visited on 2024-11-28)},
   url = {https://github.com/irfansha/Q-Synth/releases/tag/Q-Synth-v2.0-SAT2024},
   doi = {10.4230/artifacts.22469},
}
Document
DOI: 10.4230/LIPIcs.SAT.2024.26
Optimal Layout Synthesis for Deep Quantum Circuits on NISQ Processors with 100+ Qubits

Authors: Irfansha Shaik and Jaco van de Pol

Published in: LIPIcs, Volume 305, 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)

Abstract
Layout synthesis is mapping a quantum circuit to a quantum processor. SWAP gate insertions are needed for scheduling 2-qubit gates only on connected physical qubits. With the ever-increasing number of qubits in NISQ processors, scalable layout synthesis is of utmost importance. With large optimality gaps observed in heuristic approaches, scalable exact methods are needed. While recent exact and near-optimal approaches scale to moderate circuits, large deep circuits are still out of scope. In this work, we propose a SAT encoding based on parallel plans that apply 1 SWAP and a group of CNOTs at each time step. Using domain-specific information, we maintain optimality in parallel plans while scaling to large and deep circuits. From our results, we show the scalability of our approach which significantly outperforms leading exact and near-optimal approaches (up to 100x). For the first time, we can optimally map several 8, 14, and 16 qubit circuits onto 54, 80, and 127 qubit platforms with up to 17 SWAPs. While adding optimal SWAPs, we also report near-optimal depth in our mapped circuits.
Cite as

Irfansha Shaik and Jaco van de Pol. Optimal Layout Synthesis for Deep Quantum Circuits on NISQ Processors with 100+ Qubits. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 26:1-26:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{shaik_et_al:LIPIcs.SAT.2024.26,
  author =	{Shaik, Irfansha and van de Pol, Jaco},
  title =	{{Optimal Layout Synthesis for Deep Quantum Circuits on NISQ Processors with 100+ Qubits}},
  booktitle =	{27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)},
  pages =	{26:1--26:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-334-8},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{305},
  editor =	{Chakraborty, Supratik and Jiang, Jie-Hong Roland},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.26},
  URN =		{urn:nbn:de:0030-drops-205487},
  doi =		{10.4230/LIPIcs.SAT.2024.26},
  annote =	{Keywords: Layout Synthesis, Transpiling, Qubit Mapping and Routing, Quantum Circuits, Propositional Satisfiability, Parallel Plans}
}
Document
DOI: 10.4230/LIPIcs.SAT.2023.24
Validation of QBF Encodings with Winning Strategies

Authors: Irfansha Shaik, Maximilian Heisinger, Martina Seidl, and Jaco van de Pol

Published in: LIPIcs, Volume 271, 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)

Abstract
When using a QBF solver for solving application problems encoded to quantified Boolean formulas (QBFs), mainly two things can potentially go wrong: (1) the solver could be buggy and return a wrong result or (2) the encoding could be incorrect. To ensure the correctness of solvers, sophisticated fuzzing and testing techniques have been presented. To ultimately trust a solving result, solvers have to provide a proof certificate that can be independently checked. Much less attention, however, has been paid to the question how to ensure the correctness of encodings. The validation of QBF encodings is particularly challenging because of the variable dependencies introduced by the quantifiers. In contrast to SAT, the solution of a true QBF is not simply a variable assignment, but a winning strategy. For each existential variable x, a winning strategy provides a function that defines how to set x based on the values of the universal variables that precede x in the quantifier prefix. Winning strategies for false formulas are defined dually. In this paper, we provide a tool for validating encodings using winning strategies and interactive game play with a QBF solver. As the representation of winning strategies can get huge, we also introduce validation based on partial winning strategies. Finally, we employ winning strategies for testing if two different encodings of one problem have the same solutions.
Cite as

Irfansha Shaik, Maximilian Heisinger, Martina Seidl, and Jaco van de Pol. Validation of QBF Encodings with Winning Strategies. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 24:1-24:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{shaik_et_al:LIPIcs.SAT.2023.24,
  author =	{Shaik, Irfansha and Heisinger, Maximilian and Seidl, Martina and van de Pol, Jaco},
  title =	{{Validation of QBF Encodings with Winning Strategies}},
  booktitle =	{26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
  pages =	{24:1--24:10},
  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.24},
  URN =		{urn:nbn:de:0030-drops-184863},
  doi =		{10.4230/LIPIcs.SAT.2023.24},
  annote =	{Keywords: QBF, Validation, Winning Strategy, Equivalence, Certificates}
}
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