Bachelor's Thesis

Quantum Circuits Synthesis

Final Thesis 1.18 MB

Author of thesis: Jakub Havlík

Acad. year: 2025/2026

Supervisor: doc. Ing. Ondřej Lengál, Ph.D.

Reviewer: doc. Mgr. Lukáš Holík, Ph.D.

Abstract:

The field of quantum computing is growing steadily, with many hardware advancements occurring each year. However, many classes of quantum circuits are far from optimal, which renders the hardware’s power subpar. Furthermore, designing efficient quantum circuits and algorithms is counterintuitive and difficult. This makes efficient automatic quantum circuit synthesis essential. In this thesis, we tackle this task by expressing quantum circuits in firstorder logic and encoding the formulae in SMT and MILP. We also show that the state-ofthe-art class of interesting quantum repeat-until-success circuits can be further optimized, since they have a very specific form that necessitates special input specifications and reveal inconsistencies in existing RUS implementations. We compare our implementation to stateof-the-art tool Quokka# on a set of nearly 500 benchmarks and show that each approach is better than the other on some subset of benchmarks.

Keywords:

Quantum computing, Quantum circuit synthesis, SMT, MILP, Quantum algorithms, Quantum circuits, Quantum circuit optimization

Date of defence

16.06.2026

Result of the defence

Defended (thesis was successfully defended)

znamkaAznamka

Grading

A

Process of defence

Student nejprve prezentoval výsledky, kterých dosáhl v rámci své práce. Komise se poté seznámila s hodnocením vedoucího a posudkem oponenta práce. Student následně odpověděl na otázky oponenta a na další otázky přítomných. Komise se na základě posudku oponenta, hodnocení vedoucího, přednesené prezentace a odpovědí studenta na položené otázky rozhodla práci hodnotit stupněm A.

Topics for thesis defence

  1. It collaborations like this, it is hard to distinguish the contribution of the student from the input provided by the advisor. Could you name some ideas, contributions, that you are most proud of and that are "your own" the most?
  2. Comment on scalability of your tool in relation to practical usability, and perhaps perspectives for improvement.
  3. Is there a scalability limit?

Language of thesis

English

Faculty

Fakulta informačních technologií

Department

Department of Intelligent Systems

Study programme

Information Technology (BIT)

Composition of Committee

doc. Ing. Jan Kořenek, Ph.D. (předseda)
doc. Ing. Ondřej Lengál, Ph.D. (místopředseda)
Ing. Bohuslav Křena, Ph.D. (člen)
Ing. Šárka Květoňová, Ph.D. (člen)
Ing. David Bařina, Ph.D. (člen)

Supervisor’s report
doc. Ing. Ondřej Lengál, Ph.D.

Bakalářská práce Jakuba Havlíka přináší nové poznatky v oblasti syntézy kvantových obvodů. Student na práci pracoval svědomitě a velká její část jsou jeho originální myšlenky, které mají na to, dle mého mínění, být spolu s výsledky prezentovány na mezinárodní úrovni. Jako vedoucí hodnotím jeho práci známkou A.

Evaluation criteria Verbal classification
Informace k zadání

Zadání bylo značně náročné, jelikož se student musel seznámit se základy kvantového počítání včetně několika dost specifických technik, s technikami syntézy kvantových obvodů, SMT a MILP solvery. Zadání práce bylo dost výzkumné: dopředu nebylo jasné, jakým konkrétním směrem se bude ubírat. V průběhu práce byl však nalezen vhodný problém a potenciální přístupy k jeho řešení, které vedly k velmi dobrému výsledku, se kterým jsem zcela spokojen.
Práce s literaturou

Student dostal relevantní literaturu k dispozici, další vhodné zdroje si zvládl najít sám. Některá literatura byla dost netriviální a oceňuji schopnosti studenta, že byl schopen ji přečíst a pochopit.
Aktivita během řešení, konzultace, komunikace

Aktivita byla příkladná, student pravidelně konzultoval, na konzultace chodil připraven s konkrétnímy výstupy a dotazy.
Aktivita při dokončování

Práce byla dokončena v dostatečném předstihu a její finální obsah vhodně konzultován.
Publikační činnost, ocenění

Tady je to komplikovanější; studentovi se podařilo zkraje práce identifikovat chybu v článku, který zavedl RUS obvody. Na základě tohoto nálezu započala výzkumná práce s kolegy z Taiwanu, která vyústila v prezentaci příspěvku "Jyun-Ao Lin, Yu-Fang Chen, Jakub Havlík, Ondřej Lengál, Fang-Yi Lo, Wei-Lun Tsai. Verifying Repeat-Until-Success Circuits with AutoQ" na mezinárodním workshopu PLanQC 2026 a také zaslaném článku "Jyun-Ao Lin, Yu-Fang Chen, Jakub Havlík, Ondrej Lengal, Fang-Yi Lo, Wei-Lun Tsai, You-Jie Wu. Verifying repeat-until-success protocols within automata" na konferenci OOPSLA 2026 (zda bude článek přijat by mělo být známo až 10. června). Samotné výsledky bakalářské práce byly přijaty k prezentaci na mezinárodním workshopu FMQC 2026 a je plán z nich udělat regulérní vědecký článek na solidní mezinárodní konferenci. Práce také byla prezentována na studentské přehlídce Excel@FIT 2026.
Points proposed by supervisor: 95

Grade proposed by supervisor: A

Reviewer’s report
doc. Mgr. Lukáš Holík, Ph.D.

Exceptional work in terms of the difficulty of the problematics as well as of results and of their presentation. 

Evaluation criteria Verbal classification Points
Náročnost zadání

Evaluation level: značně obtížné zadání

The assignment combines two very challenging areas of cutting edge research, analysis of quantum circuits and SMT/constraint solving.
The students maximalistic approach, on a level of a proper scientific work with the goal of pushing the actual state of the art, makes the assignment very challenging. 
Prezentační úroveň technické zprávy

I am evaluating the text in the context of the AI powered age
(10 years ago, this would be an amazing quality for a bachelor student).
The structure is very good, although I had trouble to distinguish genuinely new ideas, their importance, and what is  truly new from what is "normal" in the field (I am not a quantum expert).
The text is of a very good quality, although sometimes verbose, and with sometimes complex English of somewhat fuzzy meaning, though, this is much less prevalent than in many other works. Occasional mistakes in English (not a perfectly fitting word, a misplaced comma) can be found but are quite rare.


 


 90
Formální úprava technické zprávy

Quality of a good sientific publication. 

 100
Realizační výstup

Realisation is significantly beyond a standard bachelor thesis, with multiple real scientific contributions, notably:

- quantum circuit synthesis using SMT and MILP constraints,
- synthesis tool supporting several solvers, complex-number representations, and optimization modes,
- incremental synthesis to optimize gate count,
- the analysis of the specific matrix form of RUS circuits and stronger input specifications needed for RUS synthesis,
- identification of inconsistencies in existing RUS implementations,
- and an experimental comparison of the students tool with the state-of-the-art tool Quokka#, showing the competitiveness of the new tool

 100
Využitelnost výsledků

Could likely lead to a good sicentific paper, could be a basis of a real circuit synthesis and optimization tool.
Rozsah splnění požadavků zadání

Evaluation level: zadání splněno a práce obsahuje podstatná rozšíření

The assignment is succinct and offers a lot of freedom.
The students maximalistic approach, the number of results, and quality of the work may be seen as a significant extension. 
Rozsah technické zprávy

Evaluation level: je v obvyklém rozmezí
Práce s literaturou

Adequate and comprehensive usage of very challenging literature on quantum and SAT/SMT and Linar constraint solving. 

 100
Topics for thesis defence:
  1. It collaborations like this, it is hard to distinguish the contribution of the student from the input provided by the advisor. Could you name some ideas, contributions, that you are most proud of and that are "your own" the most?
  2. Comment on scalability of your tool in relation to practical usability, and perhaps perspectives for improvement.
Points proposed by reviewer: 95

Grade proposed by reviewer: A

Responsibility: Mgr. et Mgr. Hana Odstrčilová