The article deals with the topical issues of quantum phase logic application for solving practical problems of Boolean formulas satisfiability. The use of QPU allows to significantly increase the speed of solving SAT problems as one of the most important research areas that influence the development of such sections of artificial intelligence as brain modeling and cognitive science and their applied areas: formal logic, rules and analogies, problems of satisfiability of logical formulas, theorem proving. The article presents a general algorithm for modeling SAT tasks using QPU and a real-life example of solving the problem of a logical formula satisfiability, discusses topical issues of modeling a quantum system and interpreting the results.
formulae, conjunctive normal form
Science and technology have entered the era of new computing platforms built on the fundamental laws of the universe, which will lead to a revolutionary acceleration of solving practical applied problems from the point of view of the computational complexity theory. We are talking about quantum computing, which is part of the field of quantum information science (QIS). The prospects of quantum computers are primarily related to their ability to significantly expand the computing horizons of conventional computing tools, using their own "natural" parallelism of computation in the form of superposition and entanglement of qubits.
Obtaining a quantum superiority is considered for a certain range of tasks, which does not diminish the importance of quantum computers, given that some of these tasks are beyond the computational capabilities of any hypothetical computing device.
The use of quantum computing for solving applied problems is still in its formation and intensive
development. According to experts, the most promising areas for the use of quantum computers are
chemistry, the study of the properties of new materials, and financial services [
Among the existing quantum algorithms, we can distinguish the following [
quantum phase estimation; complex amplitude amplification; quantum Fourier transform (QFT); quantum search (QS); factorization of integers; finding the period of a function; eigenvalue estimation;
2023 Copyright for this paper by its authors. CEUR quantum machine learning; quantum over-sampling.
The listed algorithms and approaches are not exhaustive, but even this list gives an idea of the practical application of quantum computing, which is usually associated with big data processing, where processing time is critical.
One of the classes of problems that quantum search allows to solve includes problems that must obtain a yes/no answer, that is, derive the value of a traditional logical command and belong to NPcomplete problems.
Traditional tasks of this class are searching for a specific value in a database or solving satisfiability
problems of Boolean formulas (SAT problems). The search for methods to solve problems of this class
is very important in terms of their impact on the development of such areas of artificial intelligence as
whole brain emulation (WBE) and cognitive science (CGS). In turn, these areas of AI research and
development cover a wide range of tasks: formal logic (FL), rules and analogies (rules), Boolean
satisfiability problems (SAT), automated theorem proving (ATP), deep learning (DL) as a basis for
natural language processing (NLP) and computer vision (CV), etc. [
Due to the exceptional importance and relevance of these subject areas of knowledge for the development of integrated cognitive architectures, the article discusses the peculiarities of the practical implementation of quantum phase logic for solving actual problems of a logical formula satisfiability.
The object of the study is a quantum processor unit (QPU) as an environment for modeling logical algorithms within the framework of the study. The subject of the study is quantum phase logic as a tool for solving the problem of satisfiability of a logical formula (function). The aim of the study is to increase the speed of solving SAT problems by using quantum phase logic implemented in QPU.
Let us consider a general formulation of satisfiability problems of Boolean formulas in conjunctive
normal form (CNF). There is a set of Boolean variables that can take one of two values 0 or 1 (or
false \ true). A literal on is one of the variables or its negation ̃ [
= {0,1} ∈ , = [1 ÷ ] = 1 ∨ 2 ∨ ̃3 ∨ … ∨ , = [1 ÷ ] Logical assignment for is the assignment of values 0 or 1 to each literal in a condition.
The standard propositional 2,3 satisfiability (2,3-SAT) problem involves formulating a propositional logic formula that consists of a conjunction of literals disjunctions (conditions), where each condition consists of 2,3 literals that make the formula true. That is, the satisfiability problem is to find the values of literals that make the formula true (2):
Satisfiability problems are fundamental problems of combinatorial search, which are among the most difficult computational tasks. It is necessary to find independent solutions, fulfilling the truth constraints of a Boolean formula. Such problems belong to the class of NP-complete problems and can be solved in polynomial time. As a test example, consider the 3-SAT problem (3): ( ∨ ) ∧ ( ̃∨ ) ∧ ( ∨ ̃),
In accordance with the statement of the satisfiability problem, it is necessary to find, if they exist, such values of the literals , , that will make the logical formula (3) true.
The implementation of the logic described by formula (3), using logic gates that perform basic logic
operations according to the IEC 60617-12:1997 standard, is shown in Fig. 1. There are a number of
methods for solving the problems of the satisfiability of logical formulas based on classical deductive
methods of proving theorems [
С1 ∧ С2 ∧ … ∧ =
The algorithm considers the value of some literal to be true and calculates all the deterministic
consequences of this assumption, performing cyclic calculations until it finds a solution. In article [
GSAT (Greedy SAT) is local, as it makes decisions about the values of literals based on local information only. At the beginning of the algorithm, literals are assigned arbitrary values and the value of the variable is changed if it gives the largest increase in completed sentences.
Methods for solving SAT problems involve their parallelization using CDCL solvers
(conflictdriven clause learning) [
Common to the above methods of solving SAT problems is the search by enumerating the values of literals using implication graphs. It is clear that an increase in the number of literals will lead t o a quadratic increase in computational complexity, and at a certain number of them, calculations using classical computers will become almost impossible.
Let's look at the difference between the different types of logic used in computing systems [
Quantum computing, based on the principles of superposition and qubit entanglement, uses amplitude and phase logic. Quantum amplitude logic applies logic gates to the state of an input register to produce a superposition of results. Quantum phase logic inverts the phase of each qubit of the input register, which yields a 1 as a result of the measurement. In other words, the quantum circuit inverts the relative phases of all input values for which the logic operation is performed.
The construction of quantum algorithms for solving SAT problems is performed using basic digital
logic gates built from quantum CNOT gates and QPU operations realizing phase logic and involves a
number of consecutive steps [
1. Transformation of the formula from a satisfiability problem to a form consisting of a number of conditions and involving their simultaneous fulfillment, i.e., the conjunction operation (2). This approach reduces the number of service qubits, since the phase conjunction operation can be performed simultaneously for any number of qubits (i.e., literals) using a single CPHASE operation. 2. Represent each condition
using amplitude logic. As a rule, one service qubit is created for
each condition. As a practical example, consider the preparation of a gate that implements amplitude
OR logic (Fig. 2). Such a gate uses two working qubits and one service qubit to obtain the result of an
operation. Fig. 2 shows a code fragment of the gate implementation program, its detailed graphical
representation and as a subschema ("black box"), as well as the corresponding element of the digital
circuit of the Boolean formula (Fig. 1).
0
0
>=1
0
(Fig. 1): for the first digital circuit, the inputs [0], [
6. Perform a mirror subscheme of the complex amplitude amplification (AA) circuit to select the states of the input data that ensure making the logical formula to be truth. Due to the need to use the mirror subscheme several times
(4) to ensure the amplification of the amplitude of the required combination of literals in order to clearly detect them, it is also necessary to prepare the subscheme as a typical block (Fig. 3) and convert it into a general scheme for implementing the formula. = 4 √
2 (4) amplitude difference. (AA) iteration.
environment
The implementation of the mirror subscheme of the AA circuit (Fig. 3) involves the use of Adamar, NOT and CCPHASE gates. Phase inverting allows you to select a register value and highlight its phase against the background of others, and the mirror operation converts the phase difference into an
This combination of operations in quantum computing is called the complex amplitude amplification
The practical implementation of the logical formula (3) was carried out in the Python environment
using the Quiskit quantum computing module from IBM [
quantum input data register, represented by 3 working qubits (a, b, c) - upper register for
recording the values of three literals, three service qubits (s[0], s[
groups of quantum gates (gates) that perform operations of amplitude and phase quantum logic, cancellation of calculations of operations, mirror subscheme of the amplitude amplification (АА) three measurements, the results of which are written to the corresponding classical bits (m1,m2,m3) to save the results of calculations from working qubits. on the sign and is equal to 1/8 (fig.6).
Option 2. Modeling using the mirror subcircuit of the AA circuit.
The result of modeling formula (3) using 'statevector_simulator' in register phases is represented in the standard P.Dirac notation by the state vector of the quantum system (Fig.7). What is obvious, apart from the appearance of the relative phase π, is the increase in the amplitude of the system states encoding the logical assignment after a single application of amplitude amplification.
It should also be noted that the AA circuit inverted the phase of the qubits before amplifying the amplitude and set it to 0, leaving the relative phase unchanged. Since the AA circuit in this case amplified the amplitude, the simulation results using the 'qasm_simulator' already allow us to make conclusions about the states in which the logical assignment is encoded with a certain probability ((−0.53033)2 ≈ 0.282; 2825 ÷ 10000 ≈ 0.283) (Fig. 8). Using formula (4), we obtain the number of iterations of using the mirror subscheme of the AA circuit: = 4 √ 23 3 ≈ 1,28 Thus, for formula (3), one iteration of the mirror subscheme of the AA circuit is sufficient to obtain a result that will allow us to unambiguously identify the states of the quantum system in which the logical assignment for formula (3) is encoded.
As shown, simulations using the mirror subcircuit of the amplitude amplification circuit allow us to identify with high probability (Fig.8), after qubit measurements, the logic assignments encoded in the system states that make the logic formula true. It is also possible to identify the necessary encoded states without performing measurements by analyzing the relative phase, which is equal to π (Fig.5). The proposed simplified algorithm for constructing a logic function model with QPU using standardized sets of gates to implement amplitude and phase logic allows to implement a logic formula of any complexity. Since the quantum phase logic operation for the conjunctive normal form can be performed simultaneously for any number of qubits (i.e., literals) using a single CPHASE operation, the computation speed will significantly exceed existing algorithms. The search for the solution of SAT problems with a certain probability, for traditional algorithms is carried out in time ( ( )), because it is necessary to implement the procedure of searching for the values of literals times for literals. To speed up the traditional algorithms it is necessary to fulfill them with the help of quantum computing, replacing the probabilistic search procedure with the complex amplitude amplification algorithm, which will allow to solve the problem in (1.1(53 ( ))) time.