2. Verifying whether a logic circuit performs to specifications is an important part of the circuit design process. These benchmark SAT problems were generated during formal hardware verification on real circuits. If a circuit design was compiled to SAT, then the dwave quantum computer could solve that problem.
3. One way to factor numbers using adiabatic quantum computers is to recast them as optimization problems, where finding the global minimum of an optimization objective provides the factors requested. This presentation provides an overview of one such algorithm, which maps factoring into quadratic unconstrained binary optimization. Once a factoring problem is recast as a QUBO, it can be solved by calling the Orion web services QUBO solver.
4. Composition of music in the Common Practice Period (Baroque, Classical, Romantic) was governed by a large set of well-defined rules and recommendations on harmony and melody. This type of music is amenable to automatic generation because of its structure. Here is some work on defining how one would automate the generation of this type of music by recasting it as a constraint satisfaction problem. Some pop music can be created by identifying the appropriate formulaic rules.
6. Multiple sequence alignment problems (DNA, RNA, proteins) can be recast as quadratic binary optimization problems. Once the MSA problem has been recast in the QUBO form, it can be solved by calling the Orion web services QUBO solver. The reduction methods from MSA to QUBO can likely be significantly improved.