Проверка выполнимости булевых формул с помощью квантового отжига

Мария Алексеевна Мальцева, Александр Сергеевич Румянцев, Mariya Maltseva, Alexander Rumyantsev

Аннотация


Проверка выполнимости булевых формул (SAT) широко применяется при решении современных задач автоматизации проектирования микроэлектроники. Важным приложением такой задачи является проектирование логических цепей с заданными характеристиками из заданного набора логических вентилей. Для решения SAT-задачи можно применять как стандартные решатели, так и современные оптимизационные инструменты, в том числе относительно новый инструмент аппаратного решения задачи квантового отжига. Решение данной задачи может выполняться на системе квантового отжига с помощью построения по особым правилам так называемой булевой сети и выбора соответствующей целевой функции. В статье рассматривается практическое применение квантового отжига к построению коротких логических цепей с помощью решения SAT-задачи на основе предложенных в литературе методов, а также проводится анализ практических аспектов применения таких методов к построению квантовых цепей.

Ключевые слова


задача выполнимости булевых формул; квантовый отжиг; логические цепи; квантовые цепи; бинарное представление

Полный текст:

PDF

Литература


Заикин О. С., Семенов А. А., Посыпкин М. А. Процедуры построения декомпозиционных множеств для распределенного решения SAT-задач в проекте добровольных вычислений SAT@HOME // Управление большими системами. 2013. Вып. 43. С. 138–156.

Заплетина М. А., Жуков Д. В., Гаврилов С. В. Методы анализа выполнимости булевых формул для современных задач систем автоматизации проектирования в микроэлектронике // Изв. вузов. Электроника. 2020. Т. 25, № 6. С. 525–538.

doi: 10.24151/1561-5405-2020-25-6-525-538

Berent L., Burgholzer L., Wille R. Towards a SAT encoding for quantum circuits: A journe from classical circuits to Clifford circuits and beyond // Schloss Dagstuhl - Leibniz-Zentrum

f¨ur Informatik. 2022. Vol. 236. P. 1–17.

doi: 10.4230/LIPICS.SAT.2022.18

Bian Z., Chudak F., Macready W., Aidan R., Sebastiani R., Varotti S. Solving SAT and MaxSAT with a quantum annealer: Foundations, encodings, and preliminary results // Inf. Comput. 2018. Vol. 275. Art. 104609.

doi: 10.1016/j.ic.2020.104609

Cook S. A. The complexity of theorem-proving procedures // STOC 71: Proceedings of the third annual ACM symposium on Theory of computing. Association for Computing Machinery, New York, USA. 1971. P. 151–158. doi: 10.1145/800157.805047

D-Wave upgrades quantum chip to 2,000 qubits, gets first customer for its $15 million machine // ZME Science [Электронный ресурс]. URL: https://www.zmescience.com/science/newsscience/ d-wave-quantum-chip/ (дата обращения:14.05.2023).

de Falco D., Apolloni B., Cesa-Bianchi N.

A numerical implementation of quantum annealing // Conference: Stochastic Processes, Physics and

Geometry. July 1988.

Formal logic [Электронный ресурс]. URL:

https://en.wikibooks.org/wiki/Formal_Logic (дата

обращения: 14.05.2023).

Goldberg E. I., Prasad M. R., Brayton R. K.

Using SAT for combinational equivalence

checking // Proceedings Design, Automation

and Test in Europe. Conference and Exhibition

, Munich, Germany. 2001. P. 114–121.

doi: 10.1109/DATE.2001.915010

Große D., Chen X., Dueck G., Drechsler R.

Exact sat-based toffoli network synthesis

// Proceedings of the 17th ACM Great Lakes Symposium on VLSI 2007, Stresa, Lago Maggiore, Italy. Association for Computing Machinery, New York, USA. 2007. P. 96–101.

doi: 10.1145/1228784.1228812

IBM Unveils 400 Qubit-Plus Quantum Processor

and Next-Generation IBM Quantum System Two // IBM Newsroom [Электронный ресурс]. URL: https://newsroom.ibm.com/2022-11-09-IBMUnveils-

-Qubit-Plus-Quantum-Processor-and-

Next-Generation-IBM-Quantum-System-Two (дата обращения: 14.05.2023).

McGeoch C. C. Adiabatic quantum computation

and quantum annealing: Theory and practice // Synthesis Lectures on Quantum Computing. 2014. Vol. 5, no. 2. P. 1–93. doi: 10.1007/978-3-031-02518-1

Meuli G., Soeken M., De Micheli G. SAT-based {CNOT, T} Quantum circuit synthesis // Lecture Notes in Computer Science / Eds. J. Kari, I. Ulidowski. Vol. 11106. Cham: Springer Int. Publ., 2018. P. 175–188. doi: 10.1007/978-3-319-99498-7_12

Nabeshima H., Inoue K. Reproducible efficient

parallel SAT solving // SAT 2020: Theory and Applications

of Satisfiability Testing. 2020. Vol. 12178. P. 123–138.

doi: 10.1007/978-3-030-51825-7_10




DOI: http://dx.doi.org/10.17076/mat1783

Ссылки

  • На текущий момент ссылки отсутствуют.


Лицензия Creative Commons
Это произведение доступно по лицензии Creative Commons «Attribution» («Атрибуция») 4.0 Всемирная.

© Труды КарНЦ РАН, 2014-2019