The Boolean satisfiability problem (SAT) is widely applied in modern tasks of microelectronics design automation. An important application of such a task is the design of logic circuits with specified characteristics from a given set of logic gates. To solve an SAT problem, both standard solvers and modern optimization tools can be used, including a relatively new hardware tool for solving the quantum annealing problem. The solution of this problem can be performed on a quantum annealing system by constructing a socalled Boolean network according to special rules and selecting an appropriate objective function. The article discusses the practical application of quantum annealing to the construction of short logic circuits by solving an SAT problem based on the methods proposed in the literature, and also analyzes the practical aspects of applying such methods to the construction of quantum circuits.